feat: add List.le_prod_of_submultiplicative and friends (#31016)

Author: Ruben-VandeVelde

Mathlib/Algebra/BigOperators/Group/List/Defs.lean

@@ -83,6 +83,19 @@ theorem prod_map_one {l : List ι} :
   | nil => rfl
   | cons hd tl ih => rw [map_cons, prod_one_cons, ih]
 
+@[to_additive]
+lemma prod_induction_nonempty
+    (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (hl : l ≠ []) (base : ∀ x ∈ l, p x) :
+    p l.prod := by
+  induction l with
+  | nil => simp at hl
+  | cons a l ih =>
+    by_cases hl_empty : l = []
+    · simp [*]
+    rw [List.prod_cons]
+    simp only [mem_cons, forall_eq_or_imp] at base
+    exact hom _ _ (base.1) (ih hl_empty base.2)
+
 end MulOneClass
 
 section Monoid

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

@@ -71,7 +71,7 @@ such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e.,
 that `∀ i ∈ s, p (g i)`. Then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
 @[to_additive le_sum_of_subadditive_on_pred]
 theorem le_prod_of_submultiplicative_on_pred [IsOrderedMonoid N] (f : M → N) (p : M → Prop)
-    (h_one : f 1 = 1) (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y)
+    (h_one : f 1 ≤ 1) (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y)
     (hp_mul : ∀ x y, p x → p y → p (x * y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) :
     f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) := by
   rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)
@@ -87,7 +87,7 @@ add_decl_doc le_sum_of_subadditive_on_pred
 /-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y`, `f 1 = 1`, and `g i`,
 `i ∈ s`, is a finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`. -/
 @[to_additive le_sum_of_subadditive]
-theorem le_prod_of_submultiplicative [IsOrderedMonoid N] (f : M → N) (h_one : f 1 = 1)
+theorem le_prod_of_submultiplicative [IsOrderedMonoid N] (f : M → N) (h_one : f 1 ≤ 1)
     (h_mul : ∀ x y, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
     f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i) :=
   le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) (by simp)
@@ -248,7 +248,7 @@ lemma prod_min_le [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι 
 
 theorem abs_sum_le_sum_abs {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
     (f : ι → G) (s : Finset ι) :
-    |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i| := le_sum_of_subadditive _ abs_zero abs_add_le s f
+    |∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i| := le_sum_of_subadditive _ abs_zero.le abs_add_le s f
 
 theorem abs_sum_of_nonneg {G : Type*} [AddCommGroup G] [LinearOrder G] [AddLeftMono G]
     {f : ι → G} {s : Finset ι}

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -163,6 +163,50 @@ theorem le_prod_of_mem {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod :
 
 end Monoid
 
+section
+variable {α β : Type*} [Monoid α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β]
+
+@[to_additive le_sum_of_subadditive_on_pred]
+lemma le_prod_of_submultiplicative_on_pred (f : α → β)
+    (p : α → Prop) (h_one : f 1 ≤ 1) (hp_one : p 1)
+    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
+    (l : List α) (hpl : ∀ a, a ∈ l → p a) : f l.prod ≤ (l.map f).prod := by
+  induction l with
+  | nil => simp [h_one]
+  | cons a s ih =>
+    have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
+    have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
+    grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]
+
+@[to_additive le_sum_of_subadditive]
+lemma le_prod_of_submultiplicative (f : α → β) (h_one : f 1 ≤ 1)
+    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (l : List α) : f l.prod ≤ (l.map f).prod :=
+  le_prod_of_submultiplicative_on_pred f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y)
+    (by simp) l (by simp)
+
+@[to_additive le_sum_nonempty_of_subadditive_on_pred]
+lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
+    (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
+    (l : List α) (hl_nonempty : l ≠ []) (hl : ∀ a, a ∈ l → p a) : f l.prod ≤ (l.map f).prod := by
+  induction l with
+  | nil => simp at hl_nonempty
+  | cons a l ih =>
+    rw [prod_cons, map_cons, prod_cons]
+    by_cases hl_empty : l = []
+    · simp [hl_empty]
+    have hla_restrict : ∀ x, x ∈ l → p x := fun x hx => hl x (mem_cons_of_mem _ hx)
+    have hp_sup : p l.prod := prod_induction_nonempty p hp_mul hl_empty hla_restrict
+    have hp_a : p a := hl a mem_cons_self
+    grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]
+
+@[to_additive le_sum_nonempty_of_subadditive]
+lemma le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)
+    (l : List α) (hs_nonempty : l ≠ ∅) : f l.prod ≤ (l.map f).prod :=
+  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) l
+    hs_nonempty (by simp)
+
+end
+
 -- TODO: develop theory of tropical rings
 lemma sum_le_foldr_max [AddZeroClass M] [Zero N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0)
     (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : List M) : f l.sum ≤ (l.map f).foldr max 0 := by

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

@@ -80,45 +80,32 @@ variable [CommMonoid α] [CommMonoid β] [PartialOrder β] [IsOrderedMonoid β]
 
 @[to_additive le_sum_of_subadditive_on_pred]
 lemma le_prod_of_submultiplicative_on_pred (f : α → β)
-    (p : α → Prop) (h_one : f 1 = 1) (hp_one : p 1)
+    (p : α → Prop) (h_one : f 1 ≤ 1) (hp_one : p 1)
     (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
     (s : Multiset α) (hps : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod := by
-  revert s
-  refine Multiset.induction ?_ ?_
-  · simp [le_of_eq h_one]
-  intro a s hs hpsa
-  have hps : ∀ x, x ∈ s → p x := fun x hx => hpsa x (mem_cons_of_mem hx)
-  have hp_prod : p s.prod := prod_induction p s hp_mul hp_one hps
-  grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod,
-    hs hps]
+  induction s using Quotient.inductionOn with
+  | h l => simp [l.le_prod_of_submultiplicative_on_pred f p h_one hp_one h_mul hp_mul (by simpa)]
 
 @[to_additive le_sum_of_subadditive]
-lemma le_prod_of_submultiplicative (f : α → β) (h_one : f 1 = 1)
-    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) : f s.prod ≤ (s.map f).prod :=
-  le_prod_of_submultiplicative_on_pred f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y)
-    (by simp) s (by simp)
+lemma le_prod_of_submultiplicative (f : α → β) (h_one : f 1 ≤ 1)
+    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) : f s.prod ≤ (s.map f).prod := by
+  induction s using Quotient.inductionOn with
+  | h l => simp [l.le_prod_of_submultiplicative f h_one h_mul]
 
 @[to_additive le_sum_nonempty_of_subadditive_on_pred]
 lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
     (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b) (hp_mul : ∀ a b, p a → p b → p (a * b))
     (s : Multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod := by
-  revert s
-  refine Multiset.induction ?_ ?_
-  · simp
-  rintro a s hs - hsa_prop
-  rw [prod_cons, map_cons, prod_cons]
-  by_cases hs_empty : s = ∅
-  · simp [hs_empty]
-  have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
-  have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
-  have hp_a : p a := hsa_prop a (mem_cons_self a s)
-  grw [h_mul a _ hp_a hp_sup, ← hs hs_empty hsa_restrict]
+  induction s using Quotient.inductionOn with
+  | h l =>
+    simp [l.le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul
+      (by simpa using hs_nonempty) (by simpa)]
 
 @[to_additive le_sum_nonempty_of_subadditive]
 lemma le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)
-    (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod :=
-  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) s
-    hs_nonempty (by simp)
+    (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod := by
+  induction s using Quotient.inductionOn with
+  | h l => simp [l.le_prod_nonempty_of_submultiplicative f h_mul (by simpa using hs_nonempty)]
 
 end
 
@@ -176,6 +163,6 @@ lemma prod_min_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
 
 lemma abs_sum_le_sum_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} :
     |s.sum| ≤ (s.map abs).sum :=
-  le_sum_of_subadditive _ abs_zero abs_add_le s
+  le_sum_of_subadditive _ abs_zero.le abs_add_le s
 
 end Multiset

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

@@ -232,7 +232,7 @@ section AbsoluteValue
 lemma AbsoluteValue.sum_le [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S]
     (abv : AbsoluteValue R S)
     (s : Finset ι) (f : ι → R) : abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i) :=
-  Finset.le_sum_of_subadditive abv (map_zero _) abv.add_le _ _
+  Finset.le_sum_of_subadditive abv (map_zero _).le abv.add_le _ _
 
 lemma IsAbsoluteValue.abv_sum [Semiring R] [Semiring S] [PartialOrder S] [IsOrderedRing S]
     (abv : R → S) [IsAbsoluteValue abv]

Mathlib/Algebra/Order/Interval/Basic.lean

@@ -647,7 +647,7 @@ theorem length_sub_le : (s - t).length ≤ s.length + t.length := by
 
 theorem length_sum_le (f : ι → Interval α) (s : Finset ι) :
     (∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length :=
-  Finset.le_sum_of_subadditive _ length_zero length_add_le _ _
+  Finset.le_sum_of_subadditive _ length_zero.le length_add_le _ _
 
 end Interval
 

Mathlib/Analysis/Convex/Gauge.lean

@@ -190,7 +190,7 @@ theorem gauge_add_le (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (x y : E) :
 
 theorem gauge_sum_le {ι : Type*} (hs : Convex ℝ s) (absorbs : Absorbent ℝ s) (t : Finset ι)
     (f : ι → E) : gauge s (∑ i ∈ t, f i) ≤ ∑ i ∈ t, gauge s (f i) :=
-  Finset.le_sum_of_subadditive _ gauge_zero (gauge_add_le hs absorbs) _ _
+  Finset.le_sum_of_subadditive _ gauge_zero.le (gauge_add_le hs absorbs) _ _
 
 theorem self_subset_gauge_le_one : s ⊆ { x | gauge s x ≤ 1 } := fun _ => gauge_le_one_of_mem
 

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1152,25 +1152,25 @@ theorem dist_inv (x y : E) : dist x⁻¹ y = dist x y⁻¹ := by
 
 theorem norm_multiset_sum_le {E} [SeminormedAddCommGroup E] (m : Multiset E) :
     ‖m.sum‖ ≤ (m.map fun x => ‖x‖).sum :=
-  m.le_sum_of_subadditive norm norm_zero norm_add_le
+  m.le_sum_of_subadditive norm norm_zero.le norm_add_le
 
 @[to_additive existing]
 theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum := by
   rw [← Multiplicative.ofAdd_le, ofAdd_multiset_prod, Multiset.map_map]
   refine Multiset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _
-  · simp only [comp_apply, norm_one', ofAdd_zero]
+  · simp
   · exact norm_mul_le' x y
 
 variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] in
 @[bound]
 theorem enorm_sum_le (s : Finset ι) (f : ι → ε) :
     ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
-  s.le_sum_of_subadditive enorm enorm_zero enorm_add_le f
+  s.le_sum_of_subadditive enorm enorm_zero.le enorm_add_le f
 
 @[bound]
 theorem norm_sum_le {E} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) :
     ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ :=
-  s.le_sum_of_subadditive norm norm_zero norm_add_le f
+  s.le_sum_of_subadditive norm norm_zero.le norm_add_le f
 
 @[to_additive existing]
 theorem enorm_prod_le (s : Finset ι) (f : ι → ε) : ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ := by
@@ -1183,7 +1183,7 @@ theorem enorm_prod_le (s : Finset ι) (f : ι → ε) : ‖∏ i ∈ s, f i‖
 theorem norm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ := by
   rw [← Multiplicative.ofAdd_le, ofAdd_sum]
   refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ norm) ?_ (fun x y => ?_) _ _
-  · simp only [comp_apply, norm_one', ofAdd_zero]
+  · simp
   · exact norm_mul_le' x y
 
 @[to_additive]

Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

@@ -136,14 +136,15 @@ theorem eLpNorm'_sum_le [ContinuousAdd ε'] {ι} {f : ι → α → ε'} {s : Fi
     (hfs : ∀ i, i ∈ s → AEStronglyMeasurable (f i) μ) (hq1 : 1 ≤ q) :
     eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm' (f i) q μ :=
   Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm' f q μ)
-    (fun f => AEStronglyMeasurable f μ) (eLpNorm'_zero (zero_lt_one.trans_le hq1))
+    (fun f => AEStronglyMeasurable f μ) (eLpNorm'_zero (zero_lt_one.trans_le hq1)).le
     (fun _f _g hf hg => eLpNorm'_add_le hf hg hq1) (fun _f _g hf hg => hf.add hg) _ hfs
 
 theorem eLpNorm_sum_le [ContinuousAdd ε'] {ι} {f : ι → α → ε'} {s : Finset ι}
     (hfs : ∀ i, i ∈ s → AEStronglyMeasurable (f i) μ) (hp1 : 1 ≤ p) :
     eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm (f i) p μ :=
   Finset.le_sum_of_subadditive_on_pred (fun f : α → ε' => eLpNorm f p μ)
-    (fun f => AEStronglyMeasurable f μ) eLpNorm_zero (fun _f _g hf hg => eLpNorm_add_le hf hg hp1)
+    (fun f => AEStronglyMeasurable f μ) eLpNorm_zero.le
+    (fun _f _g hf hg => eLpNorm_add_le hf hg hp1)
     (fun _f _g hf hg => hf.add hg) _ hfs
 
 theorem MemLp.add [ContinuousAdd ε] (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f + g) p μ :=