feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq (leanprover-community#35408)

This adds
* two missing `logHeight` lemmas (their `mulHeight` versions are already there)
* `{mul|log}Height_comp_le`: the height of `x ∘ f` is bounded by the height of `x`
* `{mul|log}Height_fun_mul_eq`: the height of the "multiplication table" `fun (i, j) ↦ x i * y j` is the {product|sum} of the heights of `x` and of `y`
* `{mul|log}Height_fun_prod_eq`: the analogous result for products with arbitrarily many factors
* plus some API lemmas needed for these.

Author: MichaelStollBayreuth

Mathlib/Analysis/Normed/Ring/Basic.lean

@@ -11,6 +11,8 @@ public import Mathlib.Analysis.Normed.Group.Real
 public import Mathlib.Analysis.Normed.Group.Subgroup
 public import Mathlib.Analysis.Normed.Group.Submodule
 
+import Mathlib.Data.Fintype.Order
+
 /-!
 # Normed rings
 
@@ -923,3 +925,61 @@ noncomputable def toNormedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) :
     exact hxy.symm
 
 end AbsoluteValue
+
+namespace Real
+
+/-
+Note: We cannot easily generalize this to targets other than `ℝ`, because we need
+the fact that `⨆ i, f i = 0` when the indexing type is empty (`Real.iSup_of_isEmpty`).
+-/
+
+section mul
+
+variable {R ι ι' : Type*} [Semiring R] [Finite ι] [Finite ι']
+
+lemma iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg {F : Type*} [FunLike F R ℝ]
+    [NonnegHomClass F R ℝ] [MulHomClass F R ℝ] (v : F) (x : ι → R) (y : ι' → R) :
+    ⨆ a : ι × ι', v (x a.1 * y a.2) = (⨆ i, v (x i)) * ⨆ j, v (y j) := by
+  rcases isEmpty_or_nonempty ι
+  · simp
+  rcases isEmpty_or_nonempty ι'
+  · simp
+  simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
+    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]
+
+end mul
+
+/-
+Note: We cannot easily generalize this to targets other than `ℝ`, because we need
+the fact that `⨆ i, f i = 0` when the indexing type is empty (`Real.iSup_of_isEmpty`).
+-/
+
+section prod
+
+universe u v
+
+variable {α R : Type*} [Fintype α] {ι : α → Type u} [∀ a, Finite (ι a)]
+
+lemma iSup_prod_eq_prod_iSup_of_nonneg {f : (a : α) → ι a → ℝ} (hf₀ : ∀ a i, 0 ≤ f a i) :
+    ⨆ (i : (a : α) → ι a), ∏ a, f a (i a) = ∏ a, ⨆ i, f a i := by
+  rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h
+  · rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]
+    obtain ⟨a, ha⟩ := isEmpty_pi.mp h
+    exact ⟨a, by simp⟩
+  refine le_antisymm ?_ ?_
+  · exact ciSup_le fun i ↦ Finset.prod_le_prod (by simp [hf₀])
+      fun a ha ↦ Finite.le_ciSup_of_le _ le_rfl
+  · rw [Classical.nonempty_pi] at h
+    have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
+    choose i hi using H
+    simp only [← hi]
+    exact Finite.le_ciSup_of_le i le_rfl
+
+lemma iSup_prod_eq_prod_iSup_of_nonnegHomClass {F : Type*} [FunLike F R ℝ]
+    [NonnegHomClass F R ℝ] (v : F) {x : (a : α) → ι a → R} :
+    ⨆ (i : (a : α) → ι a), ∏ a, v (x a (i a)) = ∏ a, ⨆ i, v (x a i) :=
+  Real.iSup_prod_eq_prod_iSup_of_nonneg (f := fun a i ↦ v (x a i)) (fun _ _ ↦ apply_nonneg v _)
+
+end prod
+
+end Real

Mathlib/Data/Fintype/Order.lean

@@ -11,6 +11,7 @@ public import Mathlib.Data.Set.Finite.Basic
 public import Mathlib.Data.Set.Finite.Range
 public import Mathlib.Order.Atoms
 
+import Mathlib.Data.Finite.Prod
 import Mathlib.Order.ConditionallyCompleteLattice.Finset
 
 /-!
@@ -242,7 +243,7 @@ namespace Finite
 
 section CCL
 
-variable {α ι : Type*} [Finite ι] [ConditionallyCompleteLattice α]
+variable {α ι ι' : Type*} [Finite ι] [Finite ι'] [ConditionallyCompleteLattice α]
 
 lemma le_ciSup_of_le {a : α} {f : ι → α} (c : ι) (h : a ≤ f c) : a ≤ iSup f :=
   _root_.le_ciSup_of_le (bddAbove_range f) c h
@@ -272,6 +273,14 @@ lemma ciInf_inf [Nonempty ι] {f : ι → α} {a : α} :
     (⨅ i, f i) ⊓ a = ⨅ i, f i ⊓ a :=
   ciSup_sup (α := αᵒᵈ) ..
 
+lemma ciSup_prod (f : ι × ι' → α) :
+    ⨆ a, f a = ⨆ i, ⨆ i', f (i, i') :=
+  _root_.ciSup_prod (bddAbove_range f)
+
+lemma ciInf_prod (f : ι × ι' → α) :
+    ⨅ a, f a = ⨅ i, ⨅ i', f (i, i') :=
+  ciSup_prod (α := αᵒᵈ) f
+
 end CCL
 
 section CCLO

Mathlib/Data/Real/Archimedean.lean

@@ -299,6 +299,11 @@ lemma sSup_nonneg (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sSup s := by
 it suffices to show that all values of `f` are nonnegative to show that `0 ≤ ⨆ i, f i`. -/
 lemma iSup_nonneg (hf : ∀ i, 0 ≤ f i) : 0 ≤ ⨆ i, f i := sSup_nonneg <| Set.forall_mem_range.2 hf
 
+lemma iSup_nonneg_of_nonnegHomClass {ι F α : Type*} [FunLike F α ℝ] [NonnegHomClass F α ℝ] (f : F)
+    (g : ι → α) :
+    0 ≤ ⨆ i, f (g i) :=
+  iSup_nonneg (fun i ↦ apply_nonneg f (g i))
+
 /-- As `sInf s = 0` when `s` is a set of reals that's either empty or unbounded below,
 it suffices to show that all elements of `s` are nonpositive to show that `sInf s ≤ 0`. -/
 lemma sInf_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0 := by

Mathlib/NumberTheory/Height/Basic.lean

@@ -225,7 +225,7 @@ namespace Height
 
 open AdmissibleAbsValues Real Function
 
-variable {K : Type*} [Field K] [AdmissibleAbsValues K] {ι : Type*}
+variable {K : Type*} [Field K] [AdmissibleAbsValues K] {ι ι' : Type*}
 
 /-- The multiplicative height of a tuple of elements of `K`.
 For the zero tuple we take the junk value `1`. -/
@@ -252,7 +252,7 @@ lemma mulHeight_one : mulHeight (1 : ι → K) = 1 := by
     simp [mulHeight_eq hx]
 
 /-- The multiplicative height does not change under re-indexing. -/
-lemma mulHeight_comp_equiv {ι' : Type*} (e : ι ≃ ι') (x : ι' → K) :
+lemma mulHeight_comp_equiv (e : ι ≃ ι') (x : ι' → K) :
     mulHeight (x ∘ e) = mulHeight x := by
   have H (v : AbsoluteValue K ℝ) : ⨆ i, v (x (e i)) = ⨆ i, v (x i) := e.iSup_congr (congrFun rfl)
   rcases eq_or_ne x 0 with rfl | hx
@@ -273,13 +273,20 @@ def logHeight (x : ι → K) : ℝ := log (mulHeight x)
 lemma logHeight_eq_log_mulHeight (x : ι → K) : logHeight x = log (mulHeight x) := rfl
 
 @[to_fun (attr := simp)]
-lemma logHeight_zero {ι : Type*} : logHeight (0 : ι → K) = 0 := by
+lemma logHeight_zero : logHeight (0 : ι → K) = 0 := by
   simp [logHeight_eq_log_mulHeight]
 
 @[to_fun (attr := simp)]
-lemma logHeight_one {ι : Type*} : logHeight (1 : ι → K) = 0 := by
+lemma logHeight_one : logHeight (1 : ι → K) = 0 := by
   simp [logHeight_eq_log_mulHeight]
 
+lemma logHeight_comp_equiv (e : ι ≃ ι') (x : ι' → K) :
+    logHeight (x ∘ ⇑e) = logHeight x := by
+  simp only [logHeight_eq_log_mulHeight, mulHeight_comp_equiv]
+
+lemma logHeight_swap (x y : K) : logHeight ![x, y] = logHeight ![y, x] := by
+  simp only [logHeight_eq_log_mulHeight, mulHeight_swap]
+
 variable {α : Type*}
 
 /-- The multiplicative height of a finitely supported function. -/
@@ -300,7 +307,7 @@ private lemma max_eq_iSup {α : Type*} [ConditionallyCompleteLattice α] (a b :
     max a b = iSup ![a, b] :=
   eq_of_forall_ge_iff <| by simp [ciSup_le_iff, Fin.forall_fin_two]
 
-variable [Finite ι]
+variable [Finite ι] [Finite ι']
 
 @[fun_prop]
 private lemma mulSupport_iSup_nonarchAbsVal_finite {x : ι → K} (hx : x ≠ 0) :
@@ -358,6 +365,31 @@ lemma mulHeight_ne_zero (x : ι → K) : mulHeight x ≠ 0 :=
 lemma logHeight_nonneg (x : ι → K) : 0 ≤ logHeight x :=
   log_nonneg <| one_le_mulHeight x
 
+open Function in
+lemma mulHeight_comp_le (f : ι → ι') (x : ι' → K) :
+    mulHeight (x ∘ f) ≤ mulHeight x := by
+  rcases eq_or_ne (x ∘ f) 0 with h₀ | h₀
+  · simpa [h₀] using one_le_mulHeight _
+  rcases eq_or_ne x 0 with rfl | hx
+  · simp
+  have : Nonempty ι := .intro (ne_iff.mp h₀).choose
+  rw [mulHeight_eq h₀, mulHeight_eq hx]
+  have H (v : AbsoluteValue K ℝ) : ⨆ i, v ((x ∘ f) i) ≤ ⨆ i, v (x i) :=
+    ciSup_le fun i ↦ Finite.le_ciSup_of_le (f i) le_rfl
+  gcongr
+  · exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _
+  · exact Multiset.prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _
+  · exact Multiset.prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _)
+      fun v _ ↦ H v
+  · exact finprod_le_finprod (mulSupport_iSup_nonarchAbsVal_finite h₀)
+      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _) (mulSupport_iSup_nonarchAbsVal_finite hx)
+      fun v ↦ H v.val
+
+open Real in
+lemma logHeight_comp_le (f : ι → ι') (x : ι' → K) :
+    logHeight (x ∘ f) ≤ logHeight x := by
+  simpa [logHeight_eq_log_mulHeight] using log_le_log (mulHeight_pos _) <| mulHeight_comp_le ..
+
 end Height
 
 /-!
@@ -503,6 +535,93 @@ lemma logHeight₁_zpow (x : K) (n : ℤ) : logHeight₁ (x ^ n) = n.natAbs * lo
 
 end Height
 
+/-!
+### Heights and "Segre embedding"
+
+We show that the multiplicative height of `fun (i, j) ↦ x i * y j` is the product of the
+multiplicative heights of `x` and `y` (and the analogous statement for logarithmic heights).
+
+We also show the corresponding statements for product with arbitrarily many factors.
+-/
+
+namespace Height
+
+open Height.AdmissibleAbsValues Function
+
+variable {K : Type*} [Field K] [AdmissibleAbsValues K]
+
+section many
+
+universe u v
+
+variable {α : Type u} [Fintype α] {ι : α → Type v} [∀ a, Finite (ι a)]
+
+open Finset in
+/-- Consider a finite family `x : (a : α) → ι a → K` of tuples. Then the multiplicative height
+of the "multiplication table" `fun (I : (a : α) → ι a ↦ ∏ a, x a (I a))` is the product
+of the multiplicative heights of all the `x a`. -/
+lemma mulHeight_fun_prod_eq {x : (a : α) → ι a → K} (hx : ∀ a, x a ≠ 0) :
+    mulHeight (fun I : (a : α) → ι a ↦ ∏ a, x a (I a)) = ∏ a, mulHeight (x a) := by
+  rw [mulHeight_eq ?h₁]
+  case h₁ =>
+    simp_rw [ne_iff, Pi.zero_def] at hx ⊢
+    choose f hf using hx
+    exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩
+  simp_rw [map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass]
+  rw [Multiset.prod_map_prod,
+    finprod_prod_comm _ _ fun b _ ↦ mulSupport_iSup_nonarchAbsVal_finite (hx b), ← prod_mul_distrib]
+  exact prod_congr rfl fun a _ ↦ by rw [mulHeight_eq (hx a)]
+
+open Real in
+/-- Consider a finite family `x : (a : α) → ι a → K` of tuples. Then the logarithmic height
+of the "multiplication table" `fun (I : (a : α) → ι a ↦ ∏ a, x a (I a))` is the sum
+of the logarithmic heights of all the `x a`. -/
+lemma logHeight_fun_prod_eq {x : (a : α) → ι a → K} (hx : ∀ a, x a ≠ 0) :
+    logHeight (fun I : (a : α) → ι a ↦ ∏ a, x a (I a)) = ∑ a, logHeight (x a) := by
+  simp only [logHeight_eq_log_mulHeight]
+  rw [← log_prod fun a _ ↦ mulHeight_ne_zero _]
+  exact congrArg log <| mulHeight_fun_prod_eq hx
+
+end many
+
+section two
+
+/-
+Note: One could try to deduce the binary case from the general case above,
+but this leads into dependent type shenanigans (because `ι` and `ι'` can live in different
+universes) that would likely obfuscate the proofs more than simplify them.
+-/
+
+variable {ι ι' : Type*} [Finite ι] [Finite ι']
+
+/-- The multiplicative height of the "multiplication table" `fun (i, j) ↦ x i * y j`
+is the product of the multiplicative heights of `x` and `y`. -/
+lemma mulHeight_fun_mul_eq {x : ι → K} (hx : x ≠ 0) {y : ι' → K} (hy : y ≠ 0) :
+    mulHeight (fun a : ι × ι' ↦ x a.1 * y a.2) = mulHeight x * mulHeight y := by
+  have hxy : (fun a : ι × ι' ↦ x a.1 * y a.2) ≠ 0 := by
+    obtain ⟨i, hi⟩ := ne_iff.mp hx
+    obtain ⟨j, hj⟩ := ne_iff.mp hy
+    exact ne_iff.mpr ⟨⟨i, j⟩, mul_ne_zero hi hj⟩
+  rw [mulHeight_eq hx, mulHeight_eq hy, mulHeight_eq hxy, mul_mul_mul_comm, ← Multiset.prod_map_mul,
+    ← finprod_mul_distrib
+        (mulSupport_iSup_nonarchAbsVal_finite hx) (mulSupport_iSup_nonarchAbsVal_finite hy)]
+  congr <;> ext1 v
+  · exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v x y
+  · exact Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg v.val x y
+
+open Real in
+/-- The logarithmic height of the "multiplication table" `fun (i, j) ↦ x i * y j`
+is the sum of the logarithmic heights of `x` and `y`. -/
+lemma logHeight_fun_mul_eq {x : ι → K} (hx : x ≠ 0) {y : ι' → K} (hy : y ≠ 0) :
+    logHeight (fun a : ι × ι' ↦ x a.1 * y a.2) = logHeight x + logHeight y := by
+  simp only [logHeight_eq_log_mulHeight]
+  pull (disch := positivity) log
+  rw [mulHeight_fun_mul_eq hx hy]
+
+end two
+
+end Height
+
 /-!
 ### Bounds for the height of sums of field elements
 

Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

@@ -182,6 +182,31 @@ lemma ciInf_le_ciSup [Nonempty ι] {f : ι → α} (hf : BddBelow (range f)) (hf
     ⨅ i, f i ≤ ⨆ i, f i :=
   (ciInf_le hf (Classical.arbitrary _)).trans <| le_ciSup hf' (Classical.arbitrary _)
 
+lemma ciSup_prod {f : β × γ → α} (hf : BddAbove (Set.range f)) :
+    ⨆ p, f p = ⨆ b, ⨆ c, f (b, c) := by
+  rcases isEmpty_or_nonempty β
+  · simp [iSup_of_empty']
+  rcases isEmpty_or_nonempty γ
+  · simp [iSup_of_empty']
+  have h₁ : BddAbove (Set.range fun b ↦ ⨆ c, f (b, c)) := by
+    rw [bddAbove_def] at hf ⊢
+    obtain ⟨B, hB⟩ := hf
+    refine ⟨B, fun y hy ↦ ?_⟩
+    obtain ⟨z, rfl⟩ := Set.mem_range.mp hy
+    exact ciSup_le fun c ↦ by grind
+  have h₂ b : BddAbove (Set.range fun c ↦ f (b, c)) := by
+    rw [bddAbove_def] at hf ⊢
+    obtain ⟨B, hB⟩ := hf
+    exact ⟨B, by grind⟩
+  refine eq_of_forall_ge_iff fun c ↦ ?_
+  rw [ciSup_le_iff (bddAbove_iff_subset_Iic.mpr hf), ciSup_le_iff h₁]
+  conv_rhs => enter [b]; rw [ciSup_le_iff (h₂ b)]
+  simp [Prod.forall]
+
+lemma ciInf_prod {f : β × γ → α} (hf : BddBelow (Set.range f)) :
+    ⨅ p, f p = ⨅ b, ⨅ c, f (b, c) :=
+  ciSup_prod (α := αᵒᵈ) hf
+
 /-- Introduction rule to prove that `b` is the supremum of `f`: it suffices to check that `b`
 is larger than `f i` for all `i`, and that this is not the case of any `w<b`.
 See `iSup_eq_of_forall_le_of_forall_lt_exists_gt` for a version in complete lattices. -/