refactor: generalized weak approximation (leanprover-community#41157)

refactor the existing proof of weak approximation to the generalized version applied to pairwise inequivalent  absolute value

Author: Oliiiiver

Mathlib/Analysis/AbsoluteValue/Equivalence.lean

@@ -389,4 +389,51 @@ theorem isEquiv_iff_isHomeomorph (v w : AbsoluteValue F ℝ) :
 
 end Real
 
+section WeakApproximation
+
+open Filter
+open scoped Topology
+
+variable {F : Type*} [Field F]
+
+/--
+If `v : ι → AbsoluteValue F ℝ` is a finite family of nontrivial, pairwise inequivalent
+real absolute values on a field `F`, then the diagonal embedding
+`algebraMap F ((i : ι) → WithAbs (v i))` has dense range.
+
+This is the abstract weak approximation theorem; see
+`NumberField.InfinitePlace.denseRange_algebraMap_pi` for the number-field special case.
+-/
+theorem denseRange_algebraMap_pi {ι : Type*} [Finite ι] {v : ι → AbsoluteValue F ℝ}
+    (h : ∀ i, (v i).IsNontrivial)
+    (hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) :
+    DenseRange <| algebraMap F ((i : ι) → WithAbs (v i)) := by
+  classical
+  have := Fintype.ofFinite ι
+  refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_
+  choose a hx using exists_one_lt_lt_one_pi_of_not_isEquiv h hv
+  let y := fun n : ℕ ↦ ∑ i, (1 / (1 + (a i)⁻¹ ^ n)) * WithAbs.equiv (v i) (z i)
+  have htend : atTop.Tendsto (fun n i ↦ (WithAbs.equiv (v i)).symm (y n)) (𝓝 z) := by
+    refine tendsto_pi_nhds.mpr fun u ↦ ?_
+    simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]
+    refine tendsto_finsetSum _ fun w _ ↦ ?_
+    by_cases hw : u = w
+    · rw [← hw, Pi.single_eq_same]
+      have hlt : (v u) (a u)⁻¹ < 1 := by
+        simpa [← inv_pow, inv_lt_one_iff₀] using Or.inr (hx u).1
+      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one hlt).mul_const (z u)
+    · rw [Pi.single_eq_of_ne (M := fun i ↦ WithAbs (v i)) hw (z w)]
+      have hgt : 1 < (v u) (a w)⁻¹ := by
+        rw [map_inv₀]
+        refine one_lt_inv_iff₀.mpr ⟨(v u).pos_iff.mpr fun ha ↦ ?_, (hx w).2 u hw⟩
+        linarith [map_zero (v w) ▸ ha ▸ (hx w).1]
+      have := (v u).tendsto_div_one_add_pow_nhds_zero hgt
+      simp_rw [← WithAbs.norm_toAbs_eq] at this
+      simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
+        ((WithAbs.equiv (v u)).symm _)
+  let ⟨N, hN⟩ := Metric.tendsto_atTop.1 htend r hr
+  exact ⟨y N, dist_comm z (algebraMap F _ (y N)) ▸ hN N le_rfl⟩
+
+end WeakApproximation
+
 end AbsoluteValue

Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

@@ -596,47 +596,15 @@ theorem isNontrivial : v.1.IsNontrivial := by
 
 variable {v} (K)
 
-open Filter in
 /--
 *Weak approximation for infinite places*
 The number field `K` is dense when embedded diagonally in the product
 `(v : InfinitePlace K) → WithAbs v.1`, in which `WithAbs v.1` represents `K` equipped with the
 topology coming from the infinite place `v`.
 -/
 theorem denseRange_algebraMap_pi [NumberField K] :
-    DenseRange <| algebraMap K ((v : InfinitePlace K) → WithAbs v.1) := by
-  classical
-  -- We have to show that given `(zᵥ)ᵥ` with `zᵥ : WithAbs v.1`, there is a `y : K` that is
-  -- arbitrarily close to each `zᵥ` in `v`'s topology.
-  refine Metric.denseRange_iff.mpr fun z r hr ↦ ?_
-  -- Given `v`, by previous results we can select a `aᵥ : K` for each infinite place `v`
-  -- such that `1 < v aᵥ` while `w aᵥ < 1` for all `w ≠ v`.
-  choose a hx using AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv isNontrivial
-    fun _ _ hwv ↦ (eq_iff_isEquiv (K := K)).not.mp hwv
-  -- Define the sequence `yₙ = ∑ v, 1 / (1 + aᵥ⁻ⁿ) * zᵥ` in `K`
-  let y := fun n ↦ ∑ v, (1 / (1 + (a v)⁻¹ ^ n)) * WithAbs.equiv v.1 (z v)
-  -- We will show that this sequence converges to `z` in the product topology.
-  have : atTop.Tendsto
-      (fun n (v : InfinitePlace K) ↦ (WithAbs.equiv v.1).symm (y n)) (𝓝 z) := by
-    -- At a fixed place `u`, the limit of `y` with respect to `u`'s topology is `zᵤ`.
-    refine tendsto_pi_nhds.mpr fun u ↦ ?_
-    simp_rw [← Fintype.sum_pi_single u z, y, map_sum, map_mul]
-    refine tendsto_finsetSum _ fun w _ ↦ ?_
-    by_cases hw : u = w
-    · -- Because `1 / (1 + aᵤ⁻ⁿ) → 1` in `WithAbs u.1`.
-      rw [← hw, Pi.single_eq_same]
-      have : u (a u)⁻¹ < 1 := by simpa [← inv_pow, inv_lt_one_iff₀] using .inr (hx u).1
-      simpa using (WithAbs.tendsto_one_div_one_add_pow_nhds_one this).mul_const (z u)
-    · -- And `1 / (1 + aᵤ⁻ⁿ) → 0` in `WithAbs w.1` when `w ≠ u`.
-      rw [Pi.single_eq_of_ne (M := fun v ↦ WithAbs v.1) hw (z w)]
-      have hu : 1 < u (a w)⁻¹ := by simpa [one_lt_inv_iff₀] using
-        ⟨u.pos_iff.2 fun ha ↦ by linarith [map_zero w ▸ ha ▸ (hx w).1], (hx w).2 u hw⟩
-      have := u.1.tendsto_div_one_add_pow_nhds_zero hu
-      simp_rw [← WithAbs.norm_toAbs_eq] at this
-      simpa using (tendsto_zero_iff_norm_tendsto_zero.2 this).mul_const
-        ((WithAbs.equiv u.1).symm (WithAbs.equiv w.1 (z w)))
-  -- So taking a sufficiently large index of the sequence `yₙ` gives the desired term.
-  let ⟨N, h⟩ := Metric.tendsto_atTop.1 this r hr
-  exact ⟨y N, dist_comm z (algebraMap K _ (y N)) ▸ h N le_rfl⟩
+    DenseRange <| algebraMap K ((v : InfinitePlace K) → WithAbs v.1) :=
+  AbsoluteValue.denseRange_algebraMap_pi (fun v ↦ v.isNontrivial)
+    fun _ _ h ↦ (eq_iff_isEquiv (K := K)).not.mp h
 
 end NumberField.InfinitePlace