Big operators on a multiset in ordered groups

This file contains the results concerning the interaction of multiset big operators with ordered groups.

theorem Multiset.one_le_prod_of_one_le {α : Type u_2} [CommMonoid α] [Preorder α] {s : Multiset α} [MulLeftMono α] : (∀ (x : α), x ∈ s → 1 ≤ x) → 1 ≤ s.prod

theorem Multiset.sum_nonneg {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} [AddLeftMono α] : (∀ (x : α), x ∈ s → 0 ≤ x) → 0 ≤ s.sum

theorem Multiset.single_le_prod {α : Type u_2} [CommMonoid α] [Preorder α] {s : Multiset α} [IsOrderedMonoid α] : (∀ (x : α), x ∈ s → 1 ≤ x) → ∀ (x : α), x ∈ s → x ≤ s.prod

theorem Multiset.single_le_sum {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} [IsOrderedAddMonoid α] : (∀ (x : α), x ∈ s → 0 ≤ x) → ∀ (x : α), x ∈ s → x ≤ s.sum

theorem Multiset.prod_le_pow_card {α : Type u_2} [CommMonoid α] [Preorder α] [MulLeftMono α] (s : Multiset α) (n : α) (h : ∀ (x : α), x ∈ s → x ≤ n) : s.prod ≤ n ^ s.card

theorem Multiset.sum_le_card_nsmul {α : Type u_2} [AddCommMonoid α] [Preorder α] [AddLeftMono α] (s : Multiset α) (n : α) (h : ∀ (x : α), x ∈ s → x ≤ n) : s.sum ≤ s.card • n

theorem Multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_4} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] {s : Multiset α} : (∀ (x : α), x ∈ s → 1 ≤ x) → s.prod = 1 → ∀ (x : α), x ∈ s → x = 1

theorem Multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_4} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : (∀ (x : α), x ∈ s → 0 ≤ x) → s.sum = 0 → ∀ (x : α), x ∈ s → x = 0

theorem Multiset.prod_le_prod_of_rel_le {α : Type u_2} [CommMonoid α] [Preorder α] {s t : Multiset α} [MulLeftMono α] (h : Rel (fun (x1 x2 : α) => x1 ≤ x2) s t) : s.prod ≤ t.prod

theorem Multiset.sum_le_sum_of_rel_le {α : Type u_2} [AddCommMonoid α] [Preorder α] {s t : Multiset α} [AddLeftMono α] (h : Rel (fun (x1 x2 : α) => x1 ≤ x2) s t) : s.sum ≤ t.sum

theorem Multiset.prod_map_le_prod_map {ι : Type u_1} {α : Type u_2} [CommMonoid α] [Preorder α] [MulLeftMono α] {s : Multiset ι} (f g : ι → α) (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : (map f s).prod ≤ (map g s).prod

theorem Multiset.sum_map_le_sum_map {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Preorder α] [AddLeftMono α] {s : Multiset ι} (f g : ι → α) (h : ∀ (i : ι), i ∈ s → f i ≤ g i) : (map f s).sum ≤ (map g s).sum

theorem Multiset.prod_map_le_prod {α : Type u_2} [CommMonoid α] [Preorder α] {s : Multiset α} [MulLeftMono α] (f : α → α) (h : ∀ (x : α), x ∈ s → f x ≤ x) : (map f s).prod ≤ s.prod

theorem Multiset.sum_map_le_sum {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} [AddLeftMono α] (f : α → α) (h : ∀ (x : α), x ∈ s → f x ≤ x) : (map f s).sum ≤ s.sum

theorem Multiset.prod_le_prod_map {α : Type u_2} [CommMonoid α] [Preorder α] {s : Multiset α} [MulLeftMono α] (f : α → α) (h : ∀ (x : α), x ∈ s → x ≤ f x) : s.prod ≤ (map f s).prod

theorem Multiset.sum_le_sum_map {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} [AddLeftMono α] (f : α → α) (h : ∀ (x : α), x ∈ s → x ≤ f x) : s.sum ≤ (map f s).sum

theorem Multiset.pow_card_le_prod {α : Type u_2} [CommMonoid α] [Preorder α] {s : Multiset α} {a : α} [MulLeftMono α] (h : ∀ (x : α), x ∈ s → a ≤ x) : a ^ s.card ≤ s.prod

theorem Multiset.card_nsmul_le_sum {α : Type u_2} [AddCommMonoid α] [Preorder α] {s : Multiset α} {a : α} [AddLeftMono α] (h : ∀ (x : α), x ∈ s → a ≤ x) : s.card • a ≤ s.sum

theorem Multiset.le_prod_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (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)) (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a) : f s.prod ≤ (map f s).prod

theorem Multiset.le_sum_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_zero : f 0 ≤ 0) (hp_zero : p 0) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a) : f s.sum ≤ (map f s).sum

theorem Multiset.le_prod_of_submultiplicative {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (f : α → β) (h_one : f 1 ≤ 1) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (s : Multiset α) : f s.prod ≤ (map f s).prod

theorem Multiset.le_sum_of_subadditive {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_zero : f 0 ≤ 0) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : Multiset α) : f s.sum ≤ (map f s).sum

theorem Multiset.le_prod_nonempty_of_submultiplicative_on_pred {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (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 ≤ (map f s).prod

theorem Multiset.le_sum_nonempty_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (s : Multiset α) (hs_nonempty : s ≠ ∅) (hs : ∀ (a : α), a ∈ s → p a) : f s.sum ≤ (map f s).sum

theorem Multiset.le_prod_nonempty_of_submultiplicative {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (f : α → β) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (map f s).prod

theorem Multiset.le_sum_nonempty_of_subadditive {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.sum ≤ (map f s).sum

theorem Multiset.prod_lt_prod' {ι : Type u_1} {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedCancelMonoid α] [MulLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hle : ∀ (i : ι), i ∈ s → f i ≤ g i) (hlt : ∃ (i : ι), i ∈ s ∧ f i < g i) : (map f s).prod < (map g s).prod

theorem Multiset.sum_lt_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hle : ∀ (i : ι), i ∈ s → f i ≤ g i) (hlt : ∃ (i : ι), i ∈ s ∧ f i < g i) : (map f s).sum < (map g s).sum

theorem Multiset.prod_lt_prod_of_nonempty' {ι : Type u_1} {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedCancelMonoid α] [MulLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hs : s ≠ ∅) (hfg : ∀ (i : ι), i ∈ s → f i < g i) : (map f s).prod < (map g s).prod

theorem Multiset.sum_lt_sum_of_nonempty {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedCancelAddMonoid α] [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α} (hs : s ≠ ∅) (hfg : ∀ (i : ι), i ∈ s → f i < g i) : (map f s).sum < (map g s).sum

theorem Multiset.prod_eq_one_iff {α : Type u_2} [CommMonoid α] {m : Multiset α} [PartialOrder α] [CanonicallyOrderedMul α] [IsOrderedMonoid α] : m.prod = 1 ↔ ∀ (x : α), x ∈ m → x = 1

theorem Multiset.sum_eq_zero_iff {α : Type u_2} [AddCommMonoid α] {m : Multiset α} [PartialOrder α] [CanonicallyOrderedAdd α] [IsOrderedAddMonoid α] : m.sum = 0 ↔ ∀ (x : α), x ∈ m → x = 0

theorem Multiset.le_prod_of_mem {α : Type u_2} [CommMonoid α] {m : Multiset α} {a : α} (ha : a ∈ m) [Preorder α] [CanonicallyOrderedMul α] : a ≤ m.prod

theorem Multiset.le_sum_of_mem {α : Type u_2} [AddCommMonoid α] {m : Multiset α} {a : α} (ha : a ∈ m) [Preorder α] [CanonicallyOrderedAdd α] : a ≤ m.sum

theorem Multiset.max_le_of_forall_le {α : Type u_4} [LinearOrder α] [OrderBot α] (l : Multiset α) (n : α) (h : ∀ (x : α), x ∈ l → x ≤ n) : fold max ⊥ l ≤ n

theorem Multiset.max_prod_le {ι : Type u_1} {α : Type u_2} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} : max (map f s).prod (map g s).prod ≤ (map (fun (i : ι) => max (f i) (g i)) s).prod

theorem Multiset.max_sum_le {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset ι} {f g : ι → α} : max (map f s).sum (map g s).sum ≤ (map (fun (i : ι) => max (f i) (g i)) s).sum

theorem Multiset.prod_min_le {ι : Type u_1} {α : Type u_2} [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} : (map (fun (i : ι) => min (f i) (g i)) s).prod ≤ min (map f s).prod (map g s).prod

theorem Multiset.sum_min_le {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset ι} {f g : ι → α} : (map (fun (i : ι) => min (f i) (g i)) s).sum ≤ min (map f s).sum (map g s).sum

theorem Multiset.abs_sum_le_sum_abs {α : Type u_2} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : |s.sum| ≤ (map abs s).sum

theorem Multiset.apply_prod_le_sum_map {α : Type u_2} {β : Type u_3} [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] (m : Multiset α) (f : α → β) (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b) : f m.prod ≤ (map f m).sum

theorem Multiset.sum_map_le_apply_prod {α : Type u_2} {β : Type u_3} [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] (m : Multiset α) (f : α → β) (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) : (map f m).sum ≤ f m.prod