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
.
@[simp]
theorem
Multiset.prod_erase
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
{a : α}
[DecidableEq α]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.sum_erase
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
{a : α}
[DecidableEq α]
(h : a ∈ s)
:
@[simp]
theorem
Multiset.prod_map_erase
{ι : Type u_2}
{α : Type u_3}
[CommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
@[simp]
theorem
Multiset.sum_map_erase
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
{m : Multiset ι}
{f : ι → α}
[DecidableEq ι]
{a : ι}
(h : a ∈ m)
:
@[simp]
@[simp]
theorem
Multiset.prod_filter_mul_prod_filter_not
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
(p : α → Prop)
[DecidablePred p]
:
theorem
Multiset.sum_filter_add_sum_filter_not
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
(p : α → Prop)
[DecidablePred p]
:
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)
:
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)
:
theorem
Multiset.prod_eq_pow_single
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 1)
:
theorem
Multiset.sum_eq_nsmul_single
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
[DecidableEq α]
(a : α)
(h : ∀ (a' : α), a' ≠ a → a' ∈ s → a' = 0)
:
theorem
Multiset.prod_eq_one
{α : Type u_3}
[CommMonoid α]
{s : Multiset α}
(h : ∀ x ∈ s, x = 1)
:
s.prod = 1
theorem
Multiset.sum_eq_zero
{α : Type u_3}
[AddCommMonoid α]
{s : Multiset α}
(h : ∀ x ∈ s, x = 0)
:
s.sum = 0
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)
:
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)
:
theorem
Multiset.prod_hom
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset α)
{F : Type u_7}
[FunLike F α β]
[MonoidHomClass F α β]
(f : F)
:
theorem
Multiset.sum_hom
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset α)
{F : Type u_7}
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
:
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 : ι → α)
:
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 : ι → α)
:
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₂ : ι → β)
:
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₂ : ι → β)
:
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₂ : ι → β)
:
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₂ : ι → β)
:
theorem
Multiset.prod_dvd_prod_of_le
{α : Type u_3}
[CommMonoid α]
{s t : Multiset α}
(h : s ≤ t)
:
s.prod ∣ t.prod
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_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_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
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
MonoidHom.map_multiset_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(f : α →* β)
(s : Multiset α)
:
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
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
AddHom.map_multiset_ne_zero_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(f : α →ₙ+ β)
(s : Multiset α)
(hs : s ≠ 0)
:
f s.sum = (Multiset.map (⇑f) s).sum
theorem
Multiset.fst_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset (α × β))
:
theorem
Multiset.fst_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset (α × β))
:
theorem
Multiset.snd_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid α]
[CommMonoid β]
(s : Multiset (α × β))
:
theorem
Multiset.snd_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid α]
[AddCommMonoid β]
(s : Multiset (α × β))
:
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.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.sum_map_tsub
{ι : Type u_2}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[ExistsAddOfLE α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[Sub α]
[OrderedSub α]
(l : Multiset ι)
{f g : ι → α}
(hfg : ∀ x ∈ l, g x ≤ f x)
: