feat(Algebra/Order/BigOperators): prove lemmas for List.prod and `M…

…ultiset.prod` on `CommMonoidWithZero` (#16573)

Also relax typeclass assumptions on `prod_nonneg`.



Co-authored-by: Daniel Weber <[email protected]>

Mathlib.lean

@@ -540,6 +540,8 @@ import Mathlib.Algebra.Order.Archimedean.Hom
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.List
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
+import Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
+import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Ring.List
 import Mathlib.Algebra.Order.BigOperators.Ring.Multiset

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

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2021 Stuart Presnell. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stuart Presnell, Daniel Weber
+-/
+import Mathlib.Algebra.BigOperators.Group.List
+import Mathlib.Algebra.Order.GroupWithZero.Unbundled
+
+/-!
+# Big operators on a list in ordered groups with zeros
+
+This file contains the results concerning the interaction of list big operators with ordered
+groups with zeros.
+-/
+
+namespace List
+variable {R : Type*} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
+
+lemma prod_nonneg {s : List R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod := by
+  induction s with
+  | nil => simp
+  | cons head tail hind =>
+    simp only [prod_cons]
+    simp only [mem_cons, forall_eq_or_imp] at h
+    exact mul_nonneg h.1 (hind h.2)
+
+
+lemma one_le_prod {s : List R} (h : ∀ a ∈ s, 1 ≤ a) : 1 ≤ s.prod := by
+  induction s with
+  | nil => simp
+  | cons head tail hind =>
+    simp only [prod_cons]
+    simp only [mem_cons, forall_eq_or_imp] at h
+    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)
+
+theorem prod_map_le_prod_map₀ {ι : Type*} {s : List ι} (f : ι → R) (g : ι → R)
+    (h0 : ∀ i ∈ s, 0 ≤ f i) (h : ∀ i ∈ s, f i ≤ g i) :
+    (map f s).prod ≤ (map g s).prod := by
+  induction s with
+  | nil => simp
+  | cons a s hind =>
+    simp only [map_cons, prod_cons]
+    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
+    apply mul_le_mul
+    · apply h
+      simp
+    · apply hind
+      · intro i hi
+        apply h0
+        simp [hi]
+      · intro i hi
+        apply h
+        simp [hi]
+    apply prod_nonneg
+    · simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+      intro a ha
+      apply h0
+      simp [ha]
+    apply (h0 _ _).trans (h _ _) <;> simp
+
+omit [PosMulMono R]
+variable [PosMulStrictMono R] [NeZero (1 : R)]
+
+lemma prod_pos {s : List R} (h : ∀ a ∈ s, 0 < a) : 0 < s.prod := by
+  induction s with
+  | nil => simp
+  | cons a s hind =>
+    simp only [prod_cons]
+    simp only [mem_cons, forall_eq_or_imp] at h
+    exact mul_pos h.1 (hind h.2)
+
+theorem prod_map_lt_prod_map {ι : Type*} {s : List ι} (hs : s ≠ [])
+    (f : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 < f i) (h : ∀ i ∈ s, f i < g i) :
+    (map f s).prod < (map g s).prod := by
+  match s with
+  | [] => contradiction
+  | a :: s =>
+    simp only [map_cons, prod_cons]
+    have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
+    apply mul_lt_mul
+    · apply h
+      simp
+    · apply prod_map_le_prod_map₀
+      · intro i hi
+        apply le_of_lt
+        apply h0
+        simp [hi]
+      · intro i hi
+        apply le_of_lt
+        apply h
+        simp [hi]
+    apply prod_pos
+    · simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+      intro a ha
+      apply h0
+      simp [ha]
+    apply le_of_lt ((h0 _ _).trans (h _ _)) <;> simp
+
+end List

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

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Ruben Van de Velde. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ruben Van de Velde, Daniel Weber
+-/
+import Mathlib.Algebra.Order.BigOperators.GroupWithZero.List
+import Mathlib.Algebra.BigOperators.Group.Multiset
+
+/-!
+# Big operators on a multiset in ordered groups with zeros
+
+This file contains the results concerning the interaction of multiset big operators with ordered
+groups with zeros.
+-/
+
+namespace Multiset
+variable {R : Type*} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
+
+lemma prod_nonneg {s : Multiset R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod := by
+  cases s using Quotient.ind
+  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
+  apply List.prod_nonneg h
+
+lemma one_le_prod {s : Multiset R} (h : ∀ a ∈ s, 1 ≤ a) : 1 ≤ s.prod := by
+  cases s using Quotient.ind
+  simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
+  apply List.one_le_prod h
+
+theorem prod_map_le_prod_map₀ {ι : Type*} {s : Multiset ι} (f : ι → R) (g : ι → R)
+    (h0 : ∀ i ∈ s, 0 ≤ f i) (h : ∀ i ∈ s, f i ≤ g i) :
+    (map f s).prod ≤ (map g s).prod := by
+  cases s using Quotient.ind
+  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
+  apply List.prod_map_le_prod_map₀ f g h0 h
+
+omit [PosMulMono R]
+variable [PosMulStrictMono R] [NeZero (1 : R)]
+
+lemma prod_pos {s : Multiset R} (h : ∀ a ∈ s, 0 < a) : 0 < s.prod := by
+  cases s using Quotient.ind
+  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
+  apply List.prod_pos h
+
+theorem prod_map_lt_prod_map {ι : Type*} {s : Multiset ι} (hs : s ≠ 0)
+    (f : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 < f i) (h : ∀ i ∈ s, f i < g i) :
+    (map f s).prod < (map g s).prod := by
+  cases s using Quotient.ind
+  simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *
+  apply List.prod_map_lt_prod_map hs f g h0 h
+
+end Multiset

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

@@ -14,23 +14,10 @@ This file contains the results concerning the interaction of list big operators
 
 variable {R : Type*}
 
-namespace List
-
-/-- The product of a list of positive natural numbers is positive,
-and likewise for any nontrivial ordered semiring. -/
-lemma prod_pos [StrictOrderedSemiring R] (l : List R) (h : ∀ a ∈ l, (0 : R) < a) :
-    0 < l.prod := by
-  induction' l with a l ih
-  · simp
-  · rw [prod_cons]
-    exact mul_pos (h _ <| mem_cons_self _ _) (ih fun a ha => h a <| mem_cons_of_mem _ ha)
-
 /-- A variant of `List.prod_pos` for `CanonicallyOrderedCommSemiring`. -/
-@[simp] lemma _root_.CanonicallyOrderedCommSemiring.list_prod_pos
+@[simp] lemma CanonicallyOrderedCommSemiring.list_prod_pos
     {α : Type*} [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
     ∀ {l : List α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
   | [] => by simp
-  | (x :: xs) => by simp_rw [prod_cons, forall_mem_cons, CanonicallyOrderedCommSemiring.mul_pos,
-    list_prod_pos]
-
-end List
+  | (x :: xs) => by simp_rw [List.prod_cons, List.forall_mem_cons,
+      CanonicallyOrderedCommSemiring.mul_pos, list_prod_pos]

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

@@ -13,26 +13,10 @@ This file contains the results concerning the interaction of multiset big operat
 rings.
 -/
 
-namespace Multiset
-variable {R : Type*}
-
-section OrderedCommSemiring
-variable [OrderedCommSemiring R] {s : Multiset R}
-
-lemma prod_nonneg (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod := by
-  revert h
-  refine s.induction_on ?_ fun a s hs ih ↦ ?_
-  · simp
-  · rw [prod_cons]
-    exact mul_nonneg (ih _ <| mem_cons_self _ _) (hs fun a ha ↦ ih _ <| mem_cons_of_mem ha)
-
-end OrderedCommSemiring
-
 @[simp]
-lemma _root_.CanonicallyOrderedCommSemiring.multiset_prod_pos [CanonicallyOrderedCommSemiring R]
-    [Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x := by
+lemma CanonicallyOrderedCommSemiring.multiset_prod_pos {R : Type*}
+    [CanonicallyOrderedCommSemiring R] [Nontrivial R] {m : Multiset R} :
+    0 < m.prod ↔ ∀ x ∈ m, 0 < x := by
   rcases m with ⟨l⟩
   rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
   exact CanonicallyOrderedCommSemiring.list_prod_pos
-
-end Multiset