feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 (#27969)

If $v_1, ..., v_k$ is a a finite collection of non-trivial and pairwise inequivalent absolute values in a field, then for each $v_i$ there is a point $a$ for which $1 < v_i(a)$ while $v_j(a) < 1$ for all $j \neq i$. This generalises the corresponding result on pairs of absolute values PR'd in #27964 

This PR continues the work from #22142.

Original PR: #22142

Author: smmercuri

Mathlib/Analysis/AbsoluteValue/Equivalence.lean

@@ -151,6 +151,130 @@ theorem exists_one_lt_lt_one_of_not_isEquiv {v w : AbsoluteValue R S} (hv : v.Is
 
 end LinearOrderedSemifield
 
+section LinearOrderedField
+
+open Filter
+open scoped Topology
+
+variable {R S : Type*} [Field R] [Field S] [LinearOrder S] {v w : AbsoluteValue R S}
+  [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [OrderTopology S]
+  {ι : Type*} [Fintype ι] [DecidableEq ι] {v : ι → AbsoluteValue R S} {w : AbsoluteValue R S}
+  {a b : R} {i : ι}
+
+/--
+Suppose that
+- `v i` and `w` are absolute values on a field `R`.
+- `v i` is inequivalent to `v j` for all `j ≠ i` via the divergent point `a : R`.
+- `v i` is inequivalent to `w` via the divergent point `b : R`.
+- `w a = 1`.
+
+Then there is a common divergent point `k` causing both `v i` and `w` to be inequivalent to
+each `v j` for `j ≠ i`.
+-/
+private theorem exists_one_lt_lt_one_pi_of_eq_one (ha : 1 < v i a) (haj : ∀ j ≠ i, v j a < 1)
+    (haw : w a = 1) (hb : 1 < v i b) (hbw : w b < 1) :
+    ∃ k : R, 1 < v i k ∧ (∀ j ≠ i, v j k < 1) ∧ w k < 1 := by
+  let c : ℕ → R := fun n ↦ a ^ n * b
+  have hcᵢ : Tendsto (fun n ↦ (v i) (c n)) atTop atTop := by
+    simpa [c] using Tendsto.atTop_mul_const (by linarith) (tendsto_pow_atTop_atTop_of_one_lt ha)
+  have hcⱼ (j : ι) (hj : j ≠ i) : Tendsto (fun n ↦ (v j) (c n)) atTop (𝓝 0) := by
+    simpa [c] using (tendsto_pow_atTop_nhds_zero_of_lt_one ((v j).nonneg _) (haj j hj)).mul_const _
+  simp_rw [OrderTopology.topology_eq_generate_intervals,
+    TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_atTop_sets, Set.mem_preimage] at hcⱼ
+  choose r₁ hr₁ using tendsto_atTop_atTop.1 hcᵢ 2
+  choose rₙ hrₙ using fun j hj ↦ hcⱼ j hj (.Iio 1) (by simpa using ⟨1, .inr rfl⟩) (by simp)
+  let r := Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h
+  refine ⟨c r, lt_of_lt_of_le (by linarith) (hr₁ r ?_), fun j hj ↦ ?_, by simpa [c, haw]⟩
+  · exact Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl
+  · simpa using hrₙ j hj _ <| Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _
+
+/--
+Suppose that
+- `v i` and `w` are absolute values on a field `R`.
+- `v i` is inequivalent to `v j` for all `j ≠ i` via the divergent point `a : R`.
+- `v i` is inequivalent to `w` via the divergent point `b : R`.
+- `1 < w a`.
+
+Then there is a common divergent point `k : R` causing both `v i` and `w` to be inequivalent to
+each `v j` for `j ≠ i`.
+-/
+private theorem exists_one_lt_lt_one_pi_of_one_lt (ha : 1 < v i a) (haj : ∀ j ≠ i, v j a < 1)
+    (haw : 1 < w a) (hb : 1 < v i b) (hbw : w b < 1) :
+    ∃ k : R, 1 < v i k ∧ (∀ j ≠ i, v j k < 1) ∧ w k < 1 := by
+  let c : ℕ → R := fun n ↦ 1 / (1 + a⁻¹ ^ n) * b
+  have hcᵢ : Tendsto (fun n ↦ v i (c n)) atTop (𝓝 (v i b)) := by
+    have : v i a⁻¹ < 1 := map_inv₀ (v i) a ▸ inv_lt_one_of_one_lt₀ ha
+    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (v i b)
+  have hcⱼ (j : ι) (hj : j ≠ i) : atTop.Tendsto (fun n ↦ v j (c n)) (𝓝 0) := by
+    have : 1 < v j a⁻¹ := map_inv₀ (v j) _ ▸
+      (one_lt_inv₀ <| (v j).pos fun h ↦ by linarith [map_zero (v _) ▸ h ▸ ha]).2 (haj j hj)
+    simpa [c] using (tendsto_div_one_add_pow_nhds_zero this).mul_const _
+  have hcₙ : atTop.Tendsto (fun n ↦ w (c n)) (𝓝 (w b)) := by
+    have : w a⁻¹ < 1 := map_inv₀ w _ ▸ inv_lt_one_of_one_lt₀ haw
+    simpa [c] using (tendsto_div_one_add_pow_nhds_one this).mul_const (w b)
+  simp_rw [OrderTopology.topology_eq_generate_intervals,
+    TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_atTop_sets, Set.mem_preimage] at hcⱼ
+  choose r₁ hr₁ using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_const_lt hb hcᵢ
+  choose rₙ hrₙ using fun j hj ↦ hcⱼ j hj (.Iio 1) (by simpa using ⟨1, .inr rfl⟩) (by simp)
+  choose rN hrN using Filter.eventually_atTop.1 <| Filter.Tendsto.eventually_lt_const hbw hcₙ
+  let r := max (Finset.univ.sup fun j ↦ if h : j = i then r₁ else rₙ j h) rN
+  refine ⟨c r, hr₁ r ?_, fun j hj ↦ ?_, ?_⟩
+  · exact le_max_iff.2 <| .inl <|
+      Finset.le_sup_dite_pos (p := fun j ↦ j = i) (f := fun _ _ ↦ r₁) (Finset.mem_univ _) rfl
+  · exact hrₙ j hj _ <| le_max_iff.2 <| .inl <|
+      Finset.le_sup_dite_neg (fun j ↦ j = i) (Finset.mem_univ j) _
+  · exact hrN _ <| le_max_iff.2 (.inr le_rfl)
+
+open Fintype Subtype in
+/--
+If `v : ι → AbsoluteValue R S` is a finite collection of non-trivial and pairwise inequivalent
+absolute values, then for any `i` there is some `a : R` such that `1 < v i a` and
+`v j a < 1` for all `j ≠ i`.
+-/
+theorem exists_one_lt_lt_one_pi_of_not_isEquiv (h : ∀ i, (v i).IsNontrivial)
+    (hv : Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) :
+    ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1 := by
+  let P (ι : Type _) [Fintype ι] : Prop := [DecidableEq ι] →
+    ∀ v : ι → AbsoluteValue R S, (∀ i, (v i).IsNontrivial) →
+      (Pairwise fun i j ↦ ¬(v i).IsEquiv (v j)) → ∀ i, ∃ (a : R), 1 < v i a ∧ ∀ j ≠ i, v j a < 1
+  -- Use strong induction on the index.
+  revert hv h; refine induction_subsingleton_or_nontrivial (P := P) ι (fun ι _ _ _ v h hv i ↦ ?_)
+    (fun ι _ _ ih _ v h hv i ↦ ?_) v
+  · -- If `ι` is trivial this follows immediately from `(v i).IsNontrivial`.
+    let ⟨a, ha⟩ := (h i).exists_abv_gt_one
+    exact ⟨a, ha, fun j hij ↦ absurd (Subsingleton.elim i j) hij.symm⟩
+  · rcases eq_or_ne (card ι) 2 with (hc | hc)
+    · -- If `ι` has two elements this is `exists_one_lt_lt_one_of_not_isEquiv`.
+      let ⟨j, hj⟩ := (Nat.card_eq_two_iff' i).1 <| card_eq_nat_card ▸ hc
+      let ⟨a, ha⟩ := (v i).exists_one_lt_lt_one_of_not_isEquiv (h i) (h j) (hv hj.1.symm)
+      exact ⟨a, ha.1, fun _ h ↦ hj.2 _ h ▸ ha.2⟩
+    have hlt : 2 < card ι := Nat.lt_of_le_of_ne (one_lt_card_iff_nontrivial.2 ‹_›) hc.symm
+    -- Otherwise, choose another distinguished index `j ≠ i`.
+    let ⟨j, hj⟩ := exists_ne i
+    -- Apply induction first on the subcollection `v i` for `i ≠ j` to get `a : K`
+    let ⟨a, ha⟩ := ih {k : ι // k ≠ j} (card_subtype_lt fun a ↦ a rfl) (restrict _ v)
+      (fun i ↦ h _) (hv.comp_of_injective val_injective) ⟨i, hj.symm⟩
+    -- Then apply induction next to the subcollection `{v i, v j}` to get `b : K`.
+    let ⟨b, hb⟩ := ih {k : ι // k = i ∨ k = j} (by linarith [card_subtype_eq_or_eq_of_ne hj.symm])
+      (restrict _ v) (fun _ ↦ h _) (hv.comp_of_injective val_injective) ⟨i, .inl rfl⟩
+    rcases eq_or_ne (v j a) 1 with (ha₁ | ha₁)
+    · -- If `v j a = 1` then take a large enough value from the sequence `a ^ n * b`.
+      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_eq_one ha.1 ha.2 ha₁ hb.1 (hb.2 ⟨j, .inr rfl⟩
+        (by grind))
+      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
+      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)
+    rcases ha₁.lt_or_gt with (ha_lt | ha_gt)
+    · -- If `v j a < 1` then `a` works as the divergent point.
+      refine ⟨a, ha.1, fun k hk ↦ ?_⟩
+      rcases eq_or_ne k j with (rfl | h); try exact ha_lt; exact ha.2 ⟨k, h⟩ (by grind)
+    · -- If `1 < v j a` then take a large enough value from the sequence `b / (1 + a ^ (-n))`.
+      let ⟨c, hc⟩ := exists_one_lt_lt_one_pi_of_one_lt ha.1 ha.2 ha_gt hb.1 (hb.2 ⟨j, .inr rfl⟩
+        (by grind))
+      refine ⟨c, hc.1, fun k hk ↦ ?_⟩
+      rcases eq_or_ne k j with (rfl | h); try exact hc.2.2; exact hc.2.1 ⟨k, h⟩ (by grind)
+
+end LinearOrderedField
+
 section Real
 
 open Real

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -235,6 +235,30 @@ lemma tendsto_pow_atTop_nhds_zero_iff_norm_lt_one {R : Type*} [SeminormedRing R]
   | base => simp
   | succ n hn IH => simp [pow_succ, IH]
 
+variable {R S : Type*} [Field R] [Field S] [LinearOrder S] {v w : AbsoluteValue R S}
+  [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S]
+
+/-- `v (1 / (1 + a ^n))` tends to `1` for all `v : AbsoluteValue R S` for fields `R` and `S`,
+provided `v a < 1`. -/
+theorem AbsoluteValue.tendsto_div_one_add_pow_nhds_one {v : AbsoluteValue R S} {a : R}
+    (ha : v a < 1) : atTop.Tendsto (fun (n : ℕ) ↦ v (1 / (1 + a ^ n))) (𝓝 1) := by
+  simp_rw [map_div₀ v, v.map_one]
+  apply one_div_one (G := S) ▸ Tendsto.div tendsto_const_nhds _ one_ne_zero
+  have h_add := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_add 1
+  have h_sub := (tendsto_pow_atTop_nhds_zero_of_lt_one (v.nonneg _) ha).const_sub 1
+  exact tendsto_of_tendsto_of_tendsto_of_le_of_le (by simpa using h_sub) (by simpa using h_add)
+    (fun n ↦ le_trans (by simp) (v.le_add _ _))
+    (fun n ↦ le_trans (v.add_le _ _) (by simp))
+
+/-- `v (1 / (1 + a ^n))` tends to `0` whenever `v : AbsoluteValue R S` for fields `R` and `S`,
+provided `1 < v a`. -/
+theorem AbsoluteValue.tendsto_div_one_add_pow_nhds_zero {v : AbsoluteValue R S} {a : R}
+    (ha : 1 < v a) : Filter.Tendsto (fun (n : ℕ) ↦ v (1 / (1 + a ^ n))) Filter.atTop (𝓝 0) := by
+  simp_rw [div_eq_mul_inv, one_mul, map_inv₀, fun n ↦ add_comm 1 (a ^ n)]
+  refine (tendsto_atTop_mono (fun n ↦ v.le_add _ _) ?_).inv_tendsto_atTop
+  simpa using (tendsto_atTop_add_right_of_le _ _ (tendsto_pow_atTop_atTop_of_one_lt ha)
+    (fun _ ↦ le_rfl)).congr fun n ↦ (sub_eq_add_neg (v a ^ n) 1).symm
+
 /-! ### Geometric series -/
 
 /-- A normed ring has summable geometric series if, for all `ξ` of norm `< 1`, the geometric series

Mathlib/Data/Fintype/Sum.lean

@@ -137,6 +137,10 @@ theorem Fintype.card_subtype_or_disjoint (p q : α → Prop) (h : Disjoint p q)
     convert Fintype.card_congr (subtypeOrEquiv p q h)
     simp
 
+theorem Fintype.card_subtype_eq_or_eq_of_ne {α : Type*} [Fintype α] [DecidableEq α] {a b : α}
+    (h : a ≠ b) : Fintype.card { c : α // c = a ∨ c = b } = 2 :=
+  Fintype.card_subtype_or_disjoint _ _ fun _ ha hb _ hc ↦ ha _ hc ▸ hb _ hc ▸ h <| rfl
+
 attribute [local instance] Fintype.ofFinite in
 @[simp]
 theorem infinite_sum : Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β := by