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.sum_nonneg {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} : (∀ x ∈ s, 0 ≤ x) → 0 ≤ s.sum

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

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

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

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

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

theorem Multiset.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} : (∀ x ∈ s, 0 ≤ x) → s.sum = 0 → ∀ x ∈ s, x = 0

theorem Multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} : (∀ x ∈ s, 1 ≤ x) → s.prod = 1 → ∀ x ∈ s, x = 1

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

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

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

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

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

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

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

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

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

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

theorem Multiset.le_sum_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : α → β) (p : α → Prop) (h_one : f 0 = 0) (hp_one : p 0) (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 ∈ s, p a) : f s.sum ≤ (Multiset.map f s).sum

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

theorem Multiset.le_sum_of_subadditive {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (f : α → β) (h_one : f 0 = 0) (h_mul : ∀ (a b : α), f (a + b) ≤ f a + f b) (s : Multiset α) : f s.sum ≤ (Multiset.map f s).sum

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

theorem Multiset.le_sum_nonempty_of_subadditive_on_pred {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [OrderedAddCommMonoid β] (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 ∈ s, p a) : f s.sum ≤ (Multiset.map f s).sum

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

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

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

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

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

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

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

theorem Multiset.sum_eq_zero_iff {α : Type u_2} [CanonicallyOrderedAddCommMonoid α] {m : Multiset α} : m.sum = 0 ↔ ∀ x ∈ m, x = 0

theorem Multiset.prod_eq_one_iff {α : Type u_2} [CanonicallyOrderedCommMonoid α] {m : Multiset α} : m.prod = 1 ↔ ∀ x ∈ m, x = 1

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

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

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

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

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

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

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

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