feat(NumberTheory/Height/Basic): add bounds for sums (leanprover-community#34330)

The main purpose of this PR (no. 3 in the series on heights) is to state and prove bounds for the height of `x + y` and for the height of a finite sum of field elements.

Author: MichaelStollBayreuth

Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean

@@ -44,6 +44,20 @@ theorem prod_map_le_pow_card {F L : Type*} [FunLike F L R] {f : F} {r : R} {t :
   induction t using Quotient.inductionOn
   simp_all [List.prod_map_le_pow_length₀]
 
+variable {α : Type*}
+
+lemma prod_map_nonneg {s : Multiset α} {f : α → R} (h : ∀ a ∈ s, 0 ≤ f a) :
+    0 ≤ (s.map f).prod := by
+  refine prod_nonneg fun r hr ↦ ?_
+  obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
+  exact h a ha
+
+lemma one_le_prod_map {s : Multiset α} {f : α → R} (h : ∀ a ∈ s, 1 ≤ f a) :
+    1 ≤ (s.map f).prod := by
+  refine one_le_prod fun r hr ↦ ?_
+  obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
+  exact h a ha
+
 omit [PosMulMono R]
 variable [PosMulStrictMono R] [NeZero (1 : R)]
 

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -56,6 +56,17 @@ lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) :
   convert ← prod_le_prod h0 h1
   exact Finset.prod_const_one
 
+lemma le_prod_max_one {M : Type*} [CommMonoidWithZero M] [LinearOrder M] [ZeroLEOneClass M]
+    [PosMulMono M] {i : ι} (hi : i ∈ s) (f : ι → M) :
+    f i ≤ ∏ i ∈ s, max (f i) 1 := by
+  classical
+  rcases lt_or_ge (f i) 0 with hf | hf
+  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
+  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
+    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
+    simp
+  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
+
 end PosMulMono
 
 section PosMulStrictMono
@@ -85,6 +96,7 @@ lemma prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f
   exact ⟨i, hi, hfg i hi⟩
 
 end PosMulStrictMono
+
 end CommMonoidWithZero
 
 section OrderedSemiring

Mathlib/NumberTheory/Height/Basic.lean

@@ -6,10 +6,13 @@ Authors: Michael Stoll
 module
 
 public import Mathlib.Analysis.SpecialFunctions.Log.Basic
+public import Mathlib.Tactic.Positivity.Core
 
+import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
 import Mathlib.Algebra.Order.Group.Indicator
+import Mathlib.Algebra.Order.Ring.IsNonarchimedean
 import Mathlib.Data.Fintype.Order
-public import Mathlib.RingTheory.Nilpotent.Defs
+import Mathlib.RingTheory.Nilpotent.Defs
 
 /-!
 # Basic theory of heights
@@ -125,11 +128,9 @@ lemma mulHeight₁_one : mulHeight₁ (1 : K) = 1 := by
   simp [mulHeight₁_eq]
 
 /-- The mutliplicative height of a field element is always at least `1`. -/
-lemma one_le_mulHeight₁ (x : K) : 1 ≤ mulHeight₁ x := by
-  refine one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod fun _ h ↦ ?_) ?_
-  · obtain ⟨v, -, rfl⟩ := Multiset.mem_map.mp h
-    exact le_max_right ..
-  · exact one_le_finprod fun _ ↦ le_max_right ..
+lemma one_le_mulHeight₁ (x : K) : 1 ≤ mulHeight₁ x :=
+  one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun _ _ ↦ le_max_right ..) <|
+    one_le_finprod fun _ ↦ le_max_right ..
 
 -- This is needed as a side condition in proofs about logarithmic heights
 lemma mulHeight₁_pos (x : K) : 0 < mulHeight₁ x :=
@@ -276,14 +277,14 @@ private lemma max_eq_iSup {α : Type*} [ConditionallyCompleteLattice α] (a b :
 variable [Finite ι]
 
 private lemma mulSupport_iSup_nonarchAbsVal_finite {x : ι → K} (hx : x ≠ 0) :
-    (Function.mulSupport fun v : nonarchAbsVal ↦ ⨆ i, v.val (x i)).Finite := by
+    (fun v : nonarchAbsVal ↦ ⨆ i, v.val (x i)).mulSupport.Finite := by
   have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| Function.ne_iff.mp hx
-  suffices (Function.mulSupport fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).Finite by
+  suffices (fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).mulSupport.Finite by
     convert this with v
-    have ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
+    obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
     have : Nonempty ι := .intro i
-    refine le_antisymm (ciSup_le fun j ↦ ?_) <|
-      ciSup_le fun ⟨j, hj⟩ ↦ le_ciSup_of_le (Finite.bddAbove_range _) j le_rfl
+    refine le_antisymm ?_ (ciSup_le fun ⟨j, hj⟩ ↦ le_ciSup_of_le (Finite.bddAbove_range _) j le_rfl)
+    refine ciSup_le fun j ↦ ?_
     rcases eq_or_ne (x j) 0 with h | h
     · rw [h, v.val.map_zero]
       exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩
@@ -292,11 +293,9 @@ private lemma mulSupport_iSup_nonarchAbsVal_finite {x : ι → K} (hx : x ≠ 0)
     Function.mulSupport_iSup _
 
 private lemma mulSupport_max_nonarchAbsVal_finite (x : K) :
-    (Function.mulSupport fun v : nonarchAbsVal ↦ v.val x ⊔ 1).Finite := by
-  convert mulSupport_iSup_nonarchAbsVal_finite (x := ![x, 1]) <| by simp with v
-  rw [max_eq_iSup]
-  congr 1
-  ext1 i
+    (fun v : nonarchAbsVal ↦ max (v.val x) 1).mulSupport.Finite := by
+  simp_rw [max_eq_iSup]
+  convert mulSupport_iSup_nonarchAbsVal_finite (x := ![x, 1]) <| by simp with v i
   fin_cases i <;> simp
 
 /-- The multiplicative height of a tuple does not change under scaling. -/
@@ -317,11 +316,9 @@ lemma one_le_mulHeight (x : ι → K) : 1 ≤ mulHeight x := by
   obtain ⟨i, hi⟩ : ∃ i, x i ≠ 0 := Function.ne_iff.mp hx
   have hx' : (x i)⁻¹ • x ≠ 0 := by simp [hi, hx]
   rw [← mulHeight_smul_eq_mulHeight _ <| inv_ne_zero hi, mulHeight_eq hx']
-  refine one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod fun vx h ↦ ?_) ?_
-  · simp only [Pi.smul_apply, smul_eq_mul, AbsoluteValue.map_mul, map_inv₀, Multiset.mem_map] at h
-    obtain ⟨v, -, rfl⟩ := h
-    refine le_ciSup_of_le (Finite.bddAbove_range _) i <| le_of_eq ?_
-    exact (inv_mul_cancel₀ <| v.ne_zero_iff.mpr hi).symm
+  refine one_le_mul_of_one_le_of_one_le (Multiset.one_le_prod_map fun v _ ↦ ?_) ?_
+  · refine le_ciSup_of_le (Finite.bddAbove_range _) i <| le_of_eq ?_
+    simpa using (inv_mul_cancel₀ <| v.ne_zero_iff.mpr hi).symm
   · refine one_le_finprod fun v ↦ le_ciSup_of_le (Finite.bddAbove_range _) i ?_
     simp [inv_mul_cancel₀ <| v.val.ne_zero_iff.mpr hi]
 
@@ -477,3 +474,127 @@ lemma logHeight₁_zpow (x : K) (n : ℤ) : logHeight₁ (x ^ n) = n.natAbs * lo
   simp only [logHeight₁_eq_log_mulHeight₁, mulHeight₁_zpow, log_pow]
 
 end Height
+
+/-!
+### Bounds for the height of sums of field elements
+
+We prove the general case (finite sums of arbitrary length) first and deduce the result
+for sums of two elements from it.
+-/
+
+namespace Finset
+
+variable {R S : Type*} [Semiring R] [CommSemiring S] [LinearOrder S] [IsOrderedRing S]
+
+/-- The "local" version of the height bound for arbitrary sums for general (possibly archimedean)
+absolute values. -/
+lemma max_abv_sum_one_le [CharZero S] (v : AbsoluteValue R S) {ι : Type*} {s : Finset ι}
+    (hs : s.Nonempty) (x : ι → R) :
+    max (v (∑ i ∈ s, x i)) 1 ≤ #s * ∏ i ∈ s, max (v (x i)) 1 := by
+  refine sup_le ?_ ?_
+  · rw [← nsmul_eq_mul, ← sum_const]
+    grw [v.sum_le s x]
+    gcongr with i hi
+    exact le_prod_max_one hi fun i ↦ v (x i)
+  · nth_rewrite 1 [← mul_one 1]
+    gcongr
+    · simp [hs]
+    · exact s.one_le_prod fun _ ↦ le_max_right ..
+
+/-- The "local" version of the height bound for arbitrary sums for nonarchimedean
+absolute values. -/
+lemma max_abv_sum_one_le_of_isNonarchimedean {v : AbsoluteValue R S} (hv : IsNonarchimedean v)
+    {ι : Type*} (s : Finset ι) (x : ι → R) :
+    max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 1 := by
+  rcases s.eq_empty_or_nonempty with rfl | hs
+  · simp
+  refine sup_le ?_ <| s.one_le_prod fun _ ↦ le_max_right ..
+  grw [hv.apply_sum_le_sup_of_isNonarchimedean hs]
+  exact sup'_le hs (fun i ↦ v (x i)) fun i hi ↦ le_prod_max_one hi fun i ↦ v (x i)
+
+end Finset
+
+namespace Height
+
+variable {K : Type*} [Field K] [AdmissibleAbsValues K]
+
+open AdmissibleAbsValues Real
+
+open Finset Multiset in
+/-- The multiplicative height of a nonempty finite sum of field elements is at most
+`n ^ (totalWeight K)` times the product of the individual multiplicative
+heights, where `n` is the number of terms. -/
+lemma mulHeight₁_sum_le {α : Type*} {s : Finset α} (hs : s.Nonempty) (x : α → K) :
+    mulHeight₁ (∑ a ∈ s, x a) ≤ #s ^ (totalWeight K) * ∏ a ∈ s, mulHeight₁ (x a) := by
+  simp only [mulHeight₁_eq, totalWeight]
+  rw [prod_mul_distrib, ← prod_replicate, ← map_const,
+    ← finprod_prod_comm _ _ fun i _ ↦ mulSupport_max_nonarchAbsVal_finite (x i),
+    ← prod_map_prod, ← mul_assoc, ← prod_map_mul]
+  simp only [Function.const_apply]
+  gcongr
+  · exact finprod_nonneg fun _ ↦ by positivity
+  · exact prod_map_nonneg fun _ h ↦ by positivity
+  · exact prod_map_le_prod_map₀ _ _ (fun _ _ ↦ by positivity) fun _ _ ↦ max_abv_sum_one_le _ hs x
+  · refine finprod_le_finprod (mulSupport_max_nonarchAbsVal_finite _) (fun _ ↦ by grind) ?_ ?_
+    · exact (s.finite_toSet.biUnion fun _ _ ↦ mulSupport_max_nonarchAbsVal_finite _).subset <|
+        s.mulSupport_prod fun i (v : nonarchAbsVal) ↦ max (v.val (x i)) 1
+    · exact fun v ↦ max_abv_sum_one_le_of_isNonarchimedean (isNonarchimedean _ v.prop) _ x
+
+open Finset in
+/-- The logarithmic height of a finite sum of field elements is at most
+`totalWeight K * log n` plus the sum of the individual logarithmic heights,
+where `n` is the number of terms.
+
+(Note that here we do not need to assume that `s` is nonempty, due to the convenient
+junk value `log 0 = 0`.) -/
+lemma logHeight₁_sum_le {α : Type*} (s : Finset α) (x : α → K) :
+    logHeight₁ (∑ a ∈ s, x a) ≤ (totalWeight K) * log #s + ∑ a ∈ s, logHeight₁ (x a) := by
+  rcases s.eq_empty_or_nonempty with rfl | hs
+  · simp
+  simp only [logHeight₁_eq_log_mulHeight₁]
+  have : ∀ a ∈ s, mulHeight₁ (x a) ≠ 0 := fun _ _ ↦ by positivity
+  have : (#s : ℝ) ^ totalWeight K ≠ 0 := by simp [hs.ne_empty]
+  pull (disch := first | assumption | positivity) log
+  exact (log_le_log <| by positivity) <| mulHeight₁_sum_le hs x
+
+/-- The multiplicative height of `-x` is the same as that of `x`. -/
+@[simp]
+lemma mulHeight₁_neg (x : K) : mulHeight₁ (-x) = mulHeight₁ x := by
+  simp [mulHeight₁_eq]
+
+/-- The logarithmic height of `-x` is the same as that of `x`. -/
+@[simp]
+lemma logHeight₁_neg (x : K) : logHeight₁ (-x) = logHeight₁ x := by
+  simp [logHeight₁_eq_log_mulHeight₁, mulHeight₁_neg]
+
+/-- The multiplicative height of `x + y` is at most `2 ^ totalWeight K`
+times the product of the multiplicative heights of `x` and `y`. -/
+lemma mulHeight₁_add_le (x y : K) :
+    mulHeight₁ (x + y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ y := by
+  rw [show x + y = Finset.univ.sum ![x, y] by simp, mul_assoc]
+  grw [mulHeight₁_sum_le Finset.univ_nonempty ![x, y]]
+  simp
+
+/-- The logarithmic height of `x + y` is at most `totalWeight K * log 2`
+plus the sum of the logarithmic heights of `x` and `y`. -/
+lemma logHeight₁_add_le (x y : K) :
+    logHeight₁ (x + y) ≤ totalWeight K * log 2 + logHeight₁ x + logHeight₁ y := by
+  simp only [logHeight₁_eq_log_mulHeight₁]
+  pull (disch := positivity) log
+  exact (log_le_log <| by positivity) <| mulHeight₁_add_le ..
+
+/-- The multiplicative height of `x - y` is at most `2 ^ totalWeight K`
+times the product of the multiplicative heights of `x` and `y`. -/
+lemma mulHeight₁_sub_le (x y : K) :
+    mulHeight₁ (x - y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ y := by
+  rw [sub_eq_add_neg, ← mulHeight₁_neg y]
+  exact mulHeight₁_add_le x (-y)
+
+/-- The logarithmic height of `x - y` is at most `totalWeight K * log 2`
+plus the sum of the logarithmic heights of `x` and `y`. -/
+lemma logHeight₁_sub_le (x y : K) :
+    logHeight₁ (x - y) ≤ totalWeight K * log 2 + logHeight₁ x + logHeight₁ y := by
+  rw [sub_eq_add_neg, ← logHeight₁_neg y]
+  exact logHeight₁_add_le x (-y)
+
+end Height