Sums and products over multisets

In this file we define products and sums indexed by multisets. This is later used to define products and sums indexed by finite sets.

Main declarations

• Multiset.prod: s.prod f is the product of f i over all i ∈ s. Not to be mistaken with the cartesian product Multiset.product.
• Multiset.sum: s.sum f is the sum of f i over all i ∈ s.

def Multiset.prod {M : Type u_3} [CommMonoid M] : Multiset M → M

Product of a multiset given a commutative monoid structure on M. prod {a, b, c} = a * b * c

Equations

• Multiset.prod = Multiset.foldr (fun (x1 x2 : M) => x1 * x2) 1

def Multiset.sum {M : Type u_3} [AddCommMonoid M] : Multiset M → M

Sum of a multiset given a commutative additive monoid structure on M. sum {a, b, c} = a + b + c

Equations

• Multiset.sum = Multiset.foldr (fun (x1 x2 : M) => x1 + x2) 0

theorem Multiset.prod_eq_foldr {M : Type u_3} [CommMonoid M] (s : Multiset M) : s.prod = foldr (fun (x1 x2 : M) => x1 * x2) 1 s

theorem Multiset.sum_eq_foldr {M : Type u_3} [AddCommMonoid M] (s : Multiset M) : s.sum = foldr (fun (x1 x2 : M) => x1 + x2) 0 s

theorem Multiset.prod_eq_foldl {M : Type u_3} [CommMonoid M] (s : Multiset M) : s.prod = foldl (fun (x1 x2 : M) => x1 * x2) 1 s

theorem Multiset.sum_eq_foldl {M : Type u_3} [AddCommMonoid M] (s : Multiset M) : s.sum = foldl (fun (x1 x2 : M) => x1 + x2) 0 s

@[simp]

theorem Multiset.prod_coe {M : Type u_3} [CommMonoid M] (l : List M) : (↑l).prod = l.prod

@[simp]

theorem Multiset.sum_coe {M : Type u_3} [AddCommMonoid M] (l : List M) : (↑l).sum = l.sum

@[simp]

theorem Multiset.prod_toList {M : Type u_3} [CommMonoid M] (s : Multiset M) : s.toList.prod = s.prod

@[simp]

theorem Multiset.sum_toList {M : Type u_3} [AddCommMonoid M] (s : Multiset M) : s.toList.sum = s.sum

@[simp]

theorem Multiset.prod_zero {M : Type u_3} [CommMonoid M] : prod 0 = 1

@[simp]

theorem Multiset.sum_zero {M : Type u_3} [AddCommMonoid M] : sum 0 = 0

@[simp]

theorem Multiset.prod_cons {M : Type u_3} [CommMonoid M] (a : M) (s : Multiset M) : (a ::ₘ s).prod = a * s.prod

@[simp]

theorem Multiset.sum_cons {M : Type u_3} [AddCommMonoid M] (a : M) (s : Multiset M) : (a ::ₘ s).sum = a + s.sum

@[simp]

theorem Multiset.prod_singleton {M : Type u_3} [CommMonoid M] (a : M) : {a}.prod = a

@[simp]

theorem Multiset.sum_singleton {M : Type u_3} [AddCommMonoid M] (a : M) : {a}.sum = a

theorem Multiset.prod_pair {M : Type u_3} [CommMonoid M] (a b : M) : {a, b}.prod = a * b

theorem Multiset.sum_pair {M : Type u_3} [AddCommMonoid M] (a b : M) : {a, b}.sum = a + b

@[simp]

theorem Multiset.prod_replicate {M : Type u_3} [CommMonoid M] (n : ℕ) (a : M) : (replicate n a).prod = a ^ n

@[simp]

theorem Multiset.sum_replicate {M : Type u_3} [AddCommMonoid M] (n : ℕ) (a : M) : (replicate n a).sum = n • a

theorem Multiset.pow_count {M : Type u_3} [CommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) : a ^ count a s = (filter (Eq a) s).prod

theorem Multiset.nsmul_count {M : Type u_3} [AddCommMonoid M] {s : Multiset M} [DecidableEq M] (a : M) : count a s • a = (filter (Eq a) s).sum

theorem Multiset.prod_hom_rel {ι : Type u_2} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] (s : Multiset ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)) : r (map f s).prod (map g s).prod

theorem Multiset.sum_hom_rel {ι : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (s : Multiset ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 0 0) (h₂ : ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a + b) (g a + c)) : r (map f s).sum (map g s).sum

theorem Multiset.prod_map_one {ι : Type u_2} {M : Type u_3} [CommMonoid M] {m : Multiset ι} : (map (fun (x : ι) => 1) m).prod = 1

theorem Multiset.sum_map_zero {ι : Type u_2} {M : Type u_3} [AddCommMonoid M] {m : Multiset ι} : (map (fun (x : ι) => 0) m).sum = 0

theorem Multiset.prod_induction {M : Type u_3} [CommMonoid M] (p : M → Prop) (s : Multiset M) (p_mul : ∀ (a b : M), p a → p b → p (a * b)) (p_one : p 1) (p_s : ∀ a ∈ s, p a) : p s.prod

theorem Multiset.sum_induction {M : Type u_3} [AddCommMonoid M] (p : M → Prop) (s : Multiset M) (p_mul : ∀ (a b : M), p a → p b → p (a + b)) (p_one : p 0) (p_s : ∀ a ∈ s, p a) : p s.sum

theorem Multiset.prod_induction_nonempty {M : Type u_3} [CommMonoid M] {s : Multiset M} (p : M → Prop) (p_mul : ∀ (a b : M), p a → p b → p (a * b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p s.prod

theorem Multiset.sum_induction_nonempty {M : Type u_3} [AddCommMonoid M] {s : Multiset M} (p : M → Prop) (p_mul : ∀ (a b : M), p a → p b → p (a + b)) (hs : s ≠ ∅) (p_s : ∀ a ∈ s, p a) : p s.sum