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 off i
over alli ∈ s
. Not to be mistaken with the cartesian productMultiset.product
.Multiset.sum
:s.sum f
is the sum off i
over alli ∈ s
.
Sum of a multiset given a commutative additive monoid structure on α
.
sum {a, b, c} = a + b + c
Equations
- Multiset.sum = Multiset.foldr (fun (x1 x2 : α) => x1 + x2) 0
Instances For
theorem
Multiset.sum.proof_1
{α : Type u_1}
[AddCommMonoid α]
:
LeftCommutative fun (x1 x2 : α) => x1 + x2
Product of a multiset given a commutative monoid structure on α
.
prod {a, b, c} = a * b * c
Equations
- Multiset.prod = Multiset.foldr (fun (x1 x2 : α) => x1 * x2) 1
Instances For
theorem
Multiset.sum_eq_foldr
{α : Type u_3}
[AddCommMonoid α]
(s : Multiset α)
:
s.sum = Multiset.foldr (fun (x1 x2 : α) => x1 + x2) 0 s
theorem
Multiset.prod_eq_foldr
{α : Type u_3}
[CommMonoid α]
(s : Multiset α)
:
s.prod = Multiset.foldr (fun (x1 x2 : α) => x1 * x2) 1 s
theorem
Multiset.sum_eq_foldl
{α : Type u_3}
[AddCommMonoid α]
(s : Multiset α)
:
s.sum = Multiset.foldl (fun (x1 x2 : α) => x1 + x2) 0 s
theorem
Multiset.prod_eq_foldl
{α : Type u_3}
[CommMonoid α]
(s : Multiset α)
:
s.prod = Multiset.foldl (fun (x1 x2 : α) => x1 * x2) 1 s
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Multiset.sum_erase
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
{a : α}
[DecidableEq α]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.prod_erase
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
{a : α}
[DecidableEq α]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.sum_map_erase
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
f a + (Multiset.map f (m.erase a)).sum = (Multiset.map f m).sum
@[simp]
theorem
Multiset.prod_map_erase
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
f a * (Multiset.map f (m.erase a)).prod = (Multiset.map f m).prod
@[simp]
@[simp]
theorem
Multiset.sum_filter_add_sum_filter_not
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
(p : α → Prop)
[DecidablePred p]
:
(Multiset.filter p s).sum + (Multiset.filter (fun (a : α) => ¬p a) s).sum = s.sum
theorem
Multiset.prod_filter_mul_prod_filter_not
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
(p : α → Prop)
[DecidablePred p]
:
(Multiset.filter p s).prod * (Multiset.filter (fun (a : α) => ¬p a) s).prod = s.prod
@[simp]
theorem
Multiset.sum_replicate
{α : Type u_3}
[AddCommMonoid α]
(n : ℕ)
(a : α)
:
(Multiset.replicate n a).sum = n • a
@[simp]
theorem
Multiset.prod_replicate
{α : Type u_3}
[CommMonoid α]
(n : ℕ)
(a : α)
:
(Multiset.replicate n a).prod = a ^ n
theorem
Multiset.sum_map_eq_nsmul_single
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
(i : ι)
(hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 0)
:
(Multiset.map f m).sum = Multiset.count i m • f i
theorem
Multiset.prod_map_eq_pow_single
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
(i : ι)
(hf : ∀ (i' : ι), i' ≠ i → i' ∈ m → f i' = 1)
:
(Multiset.map f m).prod = f i ^ Multiset.count i m
theorem
Multiset.sum_eq_nsmul_single
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0)
:
s.sum = Multiset.count a s • a
theorem
Multiset.prod_eq_pow_single
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1)
:
s.prod = a ^ Multiset.count a s
theorem
Multiset.sum_eq_zero
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
(h : ∀ x ∈ s, x = 0)
:
s.sum = 0
theorem
Multiset.prod_eq_one
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
(h : ∀ x ∈ s, x = 1)
:
s.prod = 1
theorem
Multiset.nsmul_count
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
:
Multiset.count a s • a = (Multiset.filter (Eq a) s).sum
theorem
Multiset.pow_count
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
:
a ^ Multiset.count a s = (Multiset.filter (Eq a) s).prod
theorem
Multiset.sum_hom_ne_zero
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
{s : Multiset α}
(hs : s ≠ 0)
{F : Type u_7}
[FunLike F α β]
[AddHomClass F α β]
(f : F)
:
(Multiset.map (⇑f) s).sum = f s.sum
theorem
Multiset.prod_hom_ne_zero
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
{s : Multiset α}
(hs : s ≠ 0)
{F : Type u_7}
[FunLike F α β]
[MulHomClass F α β]
(f : F)
:
(Multiset.map (⇑f) s).prod = f s.prod
theorem
Multiset.sum_hom
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset α)
{F : Type u_7}
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
:
(Multiset.map (⇑f) s).sum = f s.sum
theorem
Multiset.prod_hom
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset α)
{F : Type u_7}
[FunLike F α β]
[MonoidHomClass F α β]
(f : F)
:
(Multiset.map (⇑f) s).prod = f s.prod
theorem
Multiset.sum_hom'
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset ι)
{F : Type u_7}
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
(g : ι → α)
:
(Multiset.map (fun (i : ι) => f (g i)) s).sum = f (Multiset.map g s).sum
theorem
Multiset.prod_hom'
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset ι)
{F : Type u_7}
[FunLike F α β]
[MonoidHomClass F α β]
(f : F)
(g : ι → α)
:
(Multiset.map (fun (i : ι) => f (g i)) s).prod = f (Multiset.map g s).prod
theorem
Multiset.sum_hom₂_ne_zero
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_6}
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
{s : Multiset ι}
(hs : s ≠ 0)
(f : α → β → γ)
(hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d)
(f₁ : ι → α)
(f₂ : ι → β)
:
(Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
theorem
Multiset.prod_hom₂_ne_zero
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_6}
[CommMonoid α]
[CommMonoid β]
[CommMonoid γ]
{s : Multiset ι}
(hs : s ≠ 0)
(f : α → β → γ)
(hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d)
(f₁ : ι → α)
(f₂ : ι → β)
:
(Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
theorem
Multiset.sum_hom₂
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_6}
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
(s : Multiset ι)
(f : α → β → γ)
(hf : ∀ (a b : α) (c d : β), f (a + b) (c + d) = f a c + f b d)
(hf' : f 0 0 = 0)
(f₁ : ι → α)
(f₂ : ι → β)
:
(Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).sum = f (Multiset.map f₁ s).sum (Multiset.map f₂ s).sum
theorem
Multiset.prod_hom₂
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
{γ : Type u_6}
[CommMonoid α]
[CommMonoid β]
[CommMonoid γ]
(s : Multiset ι)
(f : α → β → γ)
(hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d)
(hf' : f 1 1 = 1)
(f₁ : ι → α)
(f₂ : ι → β)
:
(Multiset.map (fun (i : ι) => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
theorem
Multiset.sum_hom_rel
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset ι)
{r : α → β → Prop}
{f : ι → α}
{g : ι → β}
(h₁ : r 0 0)
(h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a + b) (g a + c))
:
r (Multiset.map f s).sum (Multiset.map g s).sum
theorem
Multiset.prod_hom_rel
{ι : Type u_2}
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset ι)
{r : α → β → Prop}
{f : ι → α}
{g : ι → β}
(h₁ : r 1 1)
(h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c))
:
r (Multiset.map f s).prod (Multiset.map g s).prod
theorem
Multiset.sum_map_zero
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
:
(Multiset.map (fun (x : ι) => 0) m).sum = 0
theorem
Multiset.prod_map_one
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
:
(Multiset.map (fun (x : ι) => 1) m).prod = 1
@[simp]
theorem
Multiset.sum_map_add
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{g : ι → α}
:
(Multiset.map (fun (i : ι) => f i + g i) m).sum = (Multiset.map f m).sum + (Multiset.map g m).sum
@[simp]
theorem
Multiset.prod_map_mul
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
{f : ι → α}
{g : ι → α}
:
(Multiset.map (fun (i : ι) => f i * g i) m).prod = (Multiset.map f m).prod * (Multiset.map g m).prod
theorem
Multiset.sum_map_nsmul
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{n : ℕ}
:
(Multiset.map (fun (i : ι) => n • f i) m).sum = n • (Multiset.map f m).sum
theorem
Multiset.prod_map_pow
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
{f : ι → α}
{n : ℕ}
:
(Multiset.map (fun (i : ι) => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
theorem
Multiset.sum_map_sum_map
{α : Type u_3}
{β' : Type u_5}
{γ : Type u_6}
[AddCommMonoid α]
(m : Multiset β')
(n : Multiset γ)
{f : β' → γ → α}
:
(Multiset.map (fun (a : β') => (Multiset.map (fun (b : γ) => f a b) n).sum) m).sum = (Multiset.map (fun (b : γ) => (Multiset.map (fun (a : β') => f a b) m).sum) n).sum
theorem
Multiset.prod_map_prod_map
{α : Type u_3}
{β' : Type u_5}
{γ : Type u_6}
[CommMonoid α]
(m : Multiset β')
(n : Multiset γ)
{f : β' → γ → α}
:
(Multiset.map (fun (a : β') => (Multiset.map (fun (b : γ) => f a b) n).prod) m).prod = (Multiset.map (fun (b : γ) => (Multiset.map (fun (a : β') => f a b) m).prod) n).prod
theorem
Multiset.sum_induction
{α : Type u_3}
[AddCommMonoid α]
(p : α → Prop)
(s : Multiset α)
(p_mul : ∀ (a b : α), p a → p b → p (a + b))
(p_one : p 0)
(p_s : ∀ a ∈ s, p a)
:
p s.sum
theorem
Multiset.prod_induction
{α : Type u_3}
[CommMonoid α]
(p : α → Prop)
(s : Multiset α)
(p_mul : ∀ (a b : α), p a → p b → p (a * b))
(p_one : p 1)
(p_s : ∀ a ∈ s, p a)
:
p s.prod
theorem
Multiset.sum_induction_nonempty
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
(p : α → Prop)
(p_mul : ∀ (a b : α), p a → p b → p (a + b))
(hs : s ≠ ∅)
(p_s : ∀ a ∈ s, p a)
:
p s.sum
theorem
Multiset.prod_induction_nonempty
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
(p : α → Prop)
(p_mul : ∀ (a b : α), p a → p b → p (a * b))
(hs : s ≠ ∅)
(p_s : ∀ a ∈ s, p a)
:
p s.prod
theorem
Multiset.prod_dvd_prod_of_le
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
{t : Multiset α}
(h : s ≤ t)
:
s.prod ∣ t.prod
theorem
map_multiset_sum
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
(s : Multiset α)
:
f s.sum = (Multiset.map (⇑f) s).sum
theorem
map_multiset_prod
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
[FunLike F α β]
[MonoidHomClass F α β]
(f : F)
(s : Multiset α)
:
f s.prod = (Multiset.map (⇑f) s).prod
theorem
map_multiset_ne_zero_sum
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
[FunLike F α β]
[AddHomClass F α β]
(f : F)
{s : Multiset α}
(hs : s ≠ 0)
:
f s.sum = (Multiset.map (⇑f) s).sum
theorem
map_multiset_ne_zero_prod
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
[FunLike F α β]
[MulHomClass F α β]
(f : F)
{s : Multiset α}
(hs : s ≠ 0)
:
f s.prod = (Multiset.map (⇑f) s).prod
theorem
AddMonoidHom.map_multiset_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(f : α →+ β)
(s : Multiset α)
:
f s.sum = (Multiset.map (⇑f) s).sum
theorem
MonoidHom.map_multiset_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(f : α →* β)
(s : Multiset α)
:
f s.prod = (Multiset.map (⇑f) s).prod
theorem
AddHom.map_multiset_ne_zero_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(f : AddHom α β)
(s : Multiset α)
(hs : s ≠ 0)
:
f s.sum = (Multiset.map (⇑f) s).sum
theorem
MulHom.map_multiset_ne_zero_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(f : α →ₙ* β)
(s : Multiset α)
(hs : s ≠ 0)
:
f s.prod = (Multiset.map (⇑f) s).prod
theorem
Multiset.fst_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset (α × β))
:
s.sum.1 = (Multiset.map Prod.fst s).sum
theorem
Multiset.fst_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset (α × β))
:
s.prod.1 = (Multiset.map Prod.fst s).prod
theorem
Multiset.snd_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset (α × β))
:
s.sum.2 = (Multiset.map Prod.snd s).sum
theorem
Multiset.snd_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset (α × β))
:
s.prod.2 = (Multiset.map Prod.snd s).prod
theorem
Multiset.prod_dvd_prod_of_dvd
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{S : Multiset α}
(g1 : α → β)
(g2 : α → β)
(h : ∀ a ∈ S, g1 a ∣ g2 a)
:
(Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod
Multiset.sum
, the sum of the elements of a multiset, promoted to a morphism of
AddCommMonoid
s.
Equations
- Multiset.sumAddMonoidHom = { toFun := Multiset.sum, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
Multiset.coe_sumAddMonoidHom
{α : Type u_3}
[AddCommMonoid α]
:
⇑Multiset.sumAddMonoidHom = Multiset.sum
theorem
Multiset.sum_map_neg'
{α : Type u_3}
[SubtractionCommMonoid α]
(m : Multiset α)
:
(Multiset.map Neg.neg m).sum = -m.sum
theorem
Multiset.prod_map_inv'
{α : Type u_3}
[DivisionCommMonoid α]
(m : Multiset α)
:
(Multiset.map Inv.inv m).prod = m.prod⁻¹
@[simp]
theorem
Multiset.sum_map_neg
{ι : Type u_2}
{α : Type u_3}
[SubtractionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
:
(Multiset.map (fun (i : ι) => -f i) m).sum = -(Multiset.map f m).sum
@[simp]
theorem
Multiset.prod_map_inv
{ι : Type u_2}
{α : Type u_3}
[DivisionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
:
(Multiset.map (fun (i : ι) => (f i)⁻¹) m).prod = (Multiset.map f m).prod⁻¹
@[simp]
theorem
Multiset.sum_map_sub
{ι : Type u_2}
{α : Type u_3}
[SubtractionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{g : ι → α}
:
(Multiset.map (fun (i : ι) => f i - g i) m).sum = (Multiset.map f m).sum - (Multiset.map g m).sum
@[simp]
theorem
Multiset.prod_map_div
{ι : Type u_2}
{α : Type u_3}
[DivisionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{g : ι → α}
:
(Multiset.map (fun (i : ι) => f i / g i) m).prod = (Multiset.map f m).prod / (Multiset.map g m).prod
theorem
Multiset.sum_map_zsmul
{ι : Type u_2}
{α : Type u_3}
[SubtractionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{n : ℤ}
:
(Multiset.map (fun (i : ι) => n • f i) m).sum = n • (Multiset.map f m).sum
theorem
Multiset.prod_map_zpow
{ι : Type u_2}
{α : Type u_3}
[DivisionCommMonoid α]
{m : Multiset ι}
{f : ι → α}
{n : ℤ}
:
(Multiset.map (fun (i : ι) => f i ^ n) m).prod = (Multiset.map f m).prod ^ n
@[simp]
theorem
Multiset.sum_map_singleton
{α : Type u_3}
(s : Multiset α)
:
(Multiset.map (fun (a : α) => {a}) s).sum = s