feat: {List,Multiset,Finset}.prod_le_sum (#31012)

Author: Ruben-VandeVelde

Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -430,22 +430,17 @@ theorem totalDegree_monomial_le (s : σ →₀ ℕ) (c : R) :
 theorem totalDegree_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
     (X s ^ n : MvPolynomial σ R).totalDegree = n := by simp [X_pow_eq_monomial, one_ne_zero]
 
-theorem totalDegree_list_prod :
-    ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
-  | [] => by rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]
-  | p::ps => by
-    grw [List.prod_cons, List.map, List.sum_cons, totalDegree_mul, totalDegree_list_prod]
+theorem totalDegree_list_prod (l : List (MvPolynomial σ R)) :
+    l.prod.totalDegree ≤ (l.map MvPolynomial.totalDegree).sum :=
+  l.apply_prod_le_sum_map _ totalDegree_one.le totalDegree_mul
 
 theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
-    s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum := by
-  refine Quotient.inductionOn s fun l => ?_
-  rw [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe, Multiset.sum_coe]
-  exact totalDegree_list_prod l
+    s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum :=
+  s.apply_prod_le_sum_map _ totalDegree_one.le totalDegree_mul
 
 theorem totalDegree_finset_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
-    (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree := by
-  refine le_trans (totalDegree_multiset_prod _) ?_
-  simp only [Multiset.map_map, comp_apply, Finset.sum_map_val, le_refl]
+    (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree :=
+  s.apply_prod_le_sum_apply _ totalDegree_one.le totalDegree_mul
 
 theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
     (s.sum f).totalDegree ≤ Finset.sup s fun i => (f i).totalDegree := by

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

@@ -236,6 +236,22 @@ lemma prod_image_le_of_one_le [MulLeftMono N]
 
 end OrderedCommMonoid
 
+section ProdSum
+
+variable [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β]
+  (s : Finset ι) {f : ι → α} (g : α → β)
+
+theorem apply_prod_le_sum_apply (h_one : g 1 ≤ 0) (h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b) :
+    g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x) := by
+  refine (Multiset.apply_prod_le_sum_map _ _ h_one h_mul).trans_eq ?_
+  rw [Multiset.map_map, Function.comp_def, Finset.sum_map_val]
+
+theorem sum_apply_le_apply_prod (h_one : 0 ≤ g 1) (h_mul : ∀ (a b : α), g a + g b ≤ g (a * b)) :
+    ∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x) :=
+  s.apply_prod_le_sum_apply (β := βᵒᵈ) g h_one h_mul
+
+end ProdSum
+
 @[to_additive]
 lemma max_prod_le [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
     max (s.prod f) (s.prod g) ≤ s.prod (fun i ↦ max (f i) (g i)) :=

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

@@ -252,4 +252,21 @@ lemma all_one_of_le_one_le_of_prod_eq_one [CommMonoid M] [PartialOrder M] [IsOrd
     · exact (length l)
     · rfl⟩
 
+section ProdSum
+
+variable {α β : Type*} [Monoid α] [AddMonoid β] [Preorder β] [AddLeftMono β]
+  (l : List α) (f : α → β)
+
+theorem apply_prod_le_sum_map (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b) :
+    f l.prod ≤ (l.map f).sum := by
+  induction l with
+  | nil => simp [h_one]
+  | cons hd tl IH => simpa using (h_mul _ _).trans (add_le_add_left IH _)
+
+theorem sum_map_le_apply_prod (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) :
+    (l.map f).sum ≤ f l.prod :=
+  apply_prod_le_sum_map (β := βᵒᵈ) l f h_one h_mul
+
+end ProdSum
+
 end List

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

@@ -165,4 +165,19 @@ lemma abs_sum_le_sum_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid
     |s.sum| ≤ (s.map abs).sum :=
   le_sum_of_subadditive _ abs_zero.le abs_add_le s
 
+section ProdSum
+
+variable [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] (m : Multiset α) (f : α → β)
+
+lemma apply_prod_le_sum_map (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b) :
+    f m.prod ≤ (m.map f).sum := by
+  induction m using Quotient.inductionOn with
+  | h l => simp [l.apply_prod_le_sum_map _ h_one h_mul]
+
+lemma sum_map_le_apply_prod (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) :
+    (m.map f).sum ≤ f m.prod :=
+  m.apply_prod_le_sum_map (β := βᵒᵈ) f h_one h_mul
+
+end ProdSum
+
 end Multiset

Mathlib/Algebra/Polynomial/BigOperators.lean

@@ -83,15 +83,11 @@ theorem degree_list_sum_le (l : List S[X]) : degree l.sum ≤ (l.map natDegree).
     use p
     simp [hp]
 
-theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum := by
-  induction l with
-  | nil => simp
-  | cons p l ih => dsimp; grw [natDegree_mul_le, ih]
+theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum :=
+  l.apply_prod_le_sum_map _ natDegree_one.le fun _ _ => natDegree_mul_le
 
-theorem degree_list_prod_le (l : List S[X]) : degree l.prod ≤ (l.map degree).sum := by
-  induction l with
-  | nil => simp
-  | cons p l ih => dsimp; grw [degree_mul_le, ih]
+theorem degree_list_prod_le (l : List S[X]) : degree l.prod ≤ (l.map degree).sum :=
+  l.apply_prod_le_sum_map _ degree_one_le degree_mul_le
 
 theorem coeff_list_prod_of_natDegree_le (l : List S[X]) (n : ℕ) (hl : ∀ p ∈ l, natDegree p ≤ n) :
     coeff (List.prod l) (l.length * n) = (l.map fun p => coeff p n).prod := by

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -1155,11 +1155,8 @@ theorem norm_multiset_sum_le {E} [SeminormedAddCommGroup E] (m : Multiset E) :
   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
-  · exact norm_mul_le' x y
+theorem norm_multiset_prod_le (m : Multiset E) : ‖m.prod‖ ≤ (m.map fun x => ‖x‖).sum :=
+  m.apply_prod_le_sum_map _ norm_one'.le norm_mul_le'
 
 variable {ε : Type*} [TopologicalSpace ε] [ESeminormedAddCommMonoid ε] in
 @[bound]
@@ -1173,18 +1170,12 @@ theorem norm_sum_le {E} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E
   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
-  rw [← Multiplicative.ofAdd_le, ofAdd_sum]
-  refine Finset.le_prod_of_submultiplicative (Multiplicative.ofAdd ∘ enorm) ?_ (fun x y => ?_) _ _
-  · simp
-  · exact enorm_mul_le' x y
+theorem enorm_prod_le (s : Finset ι) (f : ι → ε) : ‖∏ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
+  s.apply_prod_le_sum_apply _ enorm_one'.le enorm_mul_le'
 
 @[to_additive existing]
-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
-  · exact norm_mul_le' x y
+theorem norm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖ :=
+  s.apply_prod_le_sum_apply _ norm_one'.le norm_mul_le'
 
 @[to_additive]
 theorem enorm_prod_le_of_le (s : Finset ι) {f : ι → ε} {n : ι → ℝ≥0∞} (h : ∀ b ∈ s, ‖f b‖ₑ ≤ n b) :