Documentation

Mathlib.Algebra.Order.BigOperators.Group.Multiset

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 α} :
(∀ xs, 0 x)0 s.sum
theorem Multiset.one_le_prod_of_one_le {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
(∀ xs, 1 x)1 s.prod
theorem Multiset.single_le_sum {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} :
(∀ xs, 0 x)xs, x s.sum
theorem Multiset.single_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
(∀ xs, 1 x)xs, x s.prod
theorem Multiset.sum_le_card_nsmul {α : Type u_2} [OrderedAddCommMonoid α] (s : Multiset α) (n : α) (h : xs, x n) :
s.sum Multiset.card s n
theorem Multiset.prod_le_pow_card {α : Type u_2} [OrderedCommMonoid α] (s : Multiset α) (n : α) (h : xs, 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 α} :
(∀ xs, 0 x)s.sum = 0xs, x = 0
theorem Multiset.all_one_of_le_one_le_of_prod_eq_one {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} :
(∀ xs, 1 x)s.prod = 1xs, 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 : is, 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 : is, 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 : xs, f x x) :
(Multiset.map f s).sum s.sum
theorem Multiset.prod_map_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} (f : αα) (h : xs, f x x) :
(Multiset.map f s).prod s.prod
theorem Multiset.sum_le_sum_map {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} (f : αα) (h : xs, x f x) :
s.sum (Multiset.map f s).sum
theorem Multiset.prod_le_prod_map {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} (f : αα) (h : xs, x f x) :
s.prod (Multiset.map f s).prod
theorem Multiset.card_nsmul_le_sum {α : Type u_2} [OrderedAddCommMonoid α] {s : Multiset α} {a : α} (h : xs, a x) :
Multiset.card s a s.sum
theorem Multiset.pow_card_le_prod {α : Type u_2} [OrderedCommMonoid α] {s : Multiset α} {a : α} (h : xs, 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 ap bf (a + b) f a + f b) (hp_mul : ∀ (a b : α), p ap bp (a + b)) (s : Multiset α) (hps : as, 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 ap bf (a * b) f a * f b) (hp_mul : ∀ (a b : α), p ap bp (a * b)) (s : Multiset α) (hps : as, 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 ap bf (a + b) f a + f b) (hp_mul : ∀ (a b : α), p ap bp (a + b)) (s : Multiset α) (hs_nonempty : s ) (hs : as, 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 ap bf (a * b) f a * f b) (hp_mul : ∀ (a b : α), p ap bp (a * b)) (s : Multiset α) (hs_nonempty : s ) (hs : as, 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 : is, f i g i) (hlt : is, 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 : is, f i g i) (hlt : is, 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 : is, 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 : is, 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 xm, x = 0
theorem Multiset.prod_eq_one_iff {α : Type u_2} [CanonicallyOrderedCommMonoid α] {m : Multiset α} :
m.prod = 1 xm, 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 : xl, x 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