Big operators #
In this file we define products and sums indexed by finite sets (specifically, Finset).
Notation #
We introduce the following notation, localized in BigOperators.
To enable the notation, use open BigOperators.
Let s be a Finset α, and f : α → β a function.
∏ x in s, f xis notation forFinset.prod s f(assumingβis aCommMonoid)∑ x in s, f xis notation forFinset.sum s f(assumingβis anAddCommMonoid)∏ x, f xis notation forFinset.prod Finset.univ f(assumingαis aFintypeandβis aCommMonoid)∑ x, f xis notation forFinset.sum Finset.univ f(assumingαis aFintypeandβis anAddCommMonoid)
Implementation Notes #
The first arguments in all definitions and lemmas is the codomain of the function of the big
operator. This is necessary for the heuristic in @[to_additive].
See the documentation of to_additive.attr for more information.
∑ x in s, f x is the sum of f x as x ranges over the elements
of the finite set s.
Instances For
∏ x in s, f x is the product of f x
as x ranges over the elements of the finite set s.
Instances For
@[simp]
theorem
Finset.sum_mk
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Multiset α)
(hs : Multiset.Nodup s)
(f : α → β)
:
Finset.sum { val := s, nodup := hs } f = Multiset.sum (Multiset.map f s)
@[simp]
theorem
Finset.prod_mk
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Multiset α)
(hs : Multiset.Nodup s)
(f : α → β)
:
Finset.prod { val := s, nodup := hs } f = Multiset.prod (Multiset.map f s)
@[simp]
theorem
Finset.sum_val
{α : Type v}
[AddCommMonoid α]
(s : Finset α)
:
Multiset.sum s.val = Finset.sum s id
@[simp]
theorem
Finset.prod_val
{α : Type v}
[CommMonoid α]
(s : Finset α)
:
Multiset.prod s.val = Finset.prod s id
∑ x, f x is notation for Finset.sum Finset.univ f. It is the sum of f x,
where x ranges over the finite domain of f.
Instances For
∏ x, f x is notation for Finset.prod Finset.univ f. It is the product of f x,
where x ranges over the finite domain of f.
Instances For
∑ x in s, f x is notation for Finset.sum s f. It is the sum of f x,
where x ranges over the finite set s.
Instances For
∏ x in s, f x is notation for Finset.prod s f. It is the product of f x,
where x ranges over the finite set s.
Instances For
Delaborator for Finset.prod. The pp.piBinderTypes option controls whether
to show the domain type when the product is over Finset.univ.
Instances For
Delaborator for Finset.prod. The pp.piBinderTypes option controls whether
to show the domain type when the sum is over Finset.univ.
Instances For
theorem
Finset.sum_eq_multiset_sum
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
(Finset.sum s fun x => f x) = Multiset.sum (Multiset.map f s.val)
theorem
Finset.prod_eq_multiset_prod
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
(Finset.prod s fun x => f x) = Multiset.prod (Multiset.map f s.val)
theorem
Finset.sum_eq_fold
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
(Finset.sum s fun x => f x) = Finset.fold (fun x x_1 => x + x_1) 0 f s
theorem
Finset.prod_eq_fold
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
(Finset.prod s fun x => f x) = Finset.fold (fun x x_1 => x * x_1) 1 f s
@[simp]
theorem
Finset.sum_multiset_singleton
{α : Type v}
(s : Finset α)
:
(Finset.sum s fun x => {x}) = s.val
theorem
map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
[AddCommMonoid γ]
{G : Type u_2}
[AddMonoidHomClass G β γ]
(g : G)
(f : α → β)
(s : Finset α)
:
↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)
theorem
map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
[CommMonoid γ]
{G : Type u_2}
[MonoidHomClass G β γ]
(g : G)
(f : α → β)
(s : Finset α)
:
↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)
@[deprecated]
theorem
AddMonoidHom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
[AddCommMonoid γ]
(g : β →+ γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)
Deprecated: use _root_.map_sum instead.
@[deprecated]
theorem
MonoidHom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
[CommMonoid γ]
(g : β →* γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)
Deprecated: use _root_.map_prod instead.
@[deprecated]
theorem
AddEquiv.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
[AddCommMonoid γ]
(g : β ≃+ γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)
Deprecated: use _root_.map_sum instead.
@[deprecated]
theorem
MulEquiv.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
[CommMonoid γ]
(g : β ≃* γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)
Deprecated: use _root_.map_prod instead.
@[deprecated map_list_sum]
theorem
RingHom.map_list_sum
{β : Type u}
{γ : Type w}
[NonAssocSemiring β]
[NonAssocSemiring γ]
(f : β →+* γ)
(l : List β)
:
@[deprecated unop_map_list_prod]
theorem
RingHom.unop_map_list_prod
{β : Type u}
{γ : Type w}
[Semiring β]
[Semiring γ]
(f : β →+* γᵐᵒᵖ)
(l : List β)
:
MulOpposite.unop (↑f (List.prod l)) = List.prod (List.reverse (List.map (MulOpposite.unop ∘ ↑f) l))
A morphism into the opposite ring acts on the product by acting on the reversed elements.
@[deprecated map_multiset_prod]
theorem
RingHom.map_multiset_prod
{β : Type u}
{γ : Type w}
[CommSemiring β]
[CommSemiring γ]
(f : β →+* γ)
(s : Multiset β)
:
↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)
@[deprecated map_multiset_sum]
theorem
RingHom.map_multiset_sum
{β : Type u}
{γ : Type w}
[NonAssocSemiring β]
[NonAssocSemiring γ]
(f : β →+* γ)
(s : Multiset β)
:
↑f (Multiset.sum s) = Multiset.sum (Multiset.map (↑f) s)
@[deprecated map_prod]
theorem
RingHom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[CommSemiring β]
[CommSemiring γ]
(g : β →+* γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)
@[deprecated map_sum]
theorem
RingHom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[NonAssocSemiring β]
[NonAssocSemiring γ]
(g : β →+* γ)
(f : α → β)
(s : Finset α)
:
↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)
theorem
AddMonoidHom.coe_finset_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[AddZeroClass β]
[AddCommMonoid γ]
(f : α → β →+ γ)
(s : Finset α)
:
↑(Finset.sum s fun x => f x) = Finset.sum s fun x => ↑(f x)
theorem
MonoidHom.coe_finset_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
:
↑(Finset.prod s fun x => f x) = Finset.prod s fun x => ↑(f x)
@[simp]
theorem
AddMonoidHom.finset_sum_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[AddZeroClass β]
[AddCommMonoid γ]
(f : α → β →+ γ)
(s : Finset α)
(b : β)
:
↑(Finset.sum s fun x => f x) b = Finset.sum s fun x => ↑(f x) b
@[simp]
theorem
MonoidHom.finset_prod_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
(b : β)
:
↑(Finset.prod s fun x => f x) b = Finset.prod s fun x => ↑(f x) b
@[simp]
theorem
Finset.sum_empty
{β : Type u}
{α : Type v}
{f : α → β}
[AddCommMonoid β]
:
(Finset.sum ∅ fun x => f x) = 0
@[simp]
theorem
Finset.prod_empty
{β : Type u}
{α : Type v}
{f : α → β}
[CommMonoid β]
:
(Finset.prod ∅ fun x => f x) = 1
theorem
Finset.sum_of_empty
{β : Type u}
{α : Type v}
{f : α → β}
[AddCommMonoid β]
[IsEmpty α]
(s : Finset α)
:
(Finset.sum s fun i => f i) = 0
theorem
Finset.prod_of_empty
{β : Type u}
{α : Type v}
{f : α → β}
[CommMonoid β]
[IsEmpty α]
(s : Finset α)
:
(Finset.prod s fun i => f i) = 1
@[simp]
theorem
Finset.sum_cons
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
(h : ¬a ∈ s)
:
(Finset.sum (Finset.cons a s h) fun x => f x) = f a + Finset.sum s fun x => f x
@[simp]
theorem
Finset.prod_cons
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
(h : ¬a ∈ s)
:
(Finset.prod (Finset.cons a s h) fun x => f x) = f a * Finset.prod s fun x => f x
@[simp]
theorem
Finset.sum_insert
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
:
¬a ∈ s → (Finset.sum (insert a s) fun x => f x) = f a + Finset.sum s fun x => f x
@[simp]
theorem
Finset.prod_insert
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
:
¬a ∈ s → (Finset.prod (insert a s) fun x => f x) = f a * Finset.prod s fun x => f x
@[simp]
theorem
Finset.sum_insert_of_eq_zero_if_not_mem
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : ¬a ∈ s → f a = 0)
:
(Finset.sum (insert a s) fun x => f x) = Finset.sum s fun x => f x
The sum of f over insert a s is the same as
the sum over s, as long as a is in s or f a = 0.
@[simp]
theorem
Finset.prod_insert_of_eq_one_if_not_mem
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : ¬a ∈ s → f a = 1)
:
(Finset.prod (insert a s) fun x => f x) = Finset.prod s fun x => f x
The product of f over insert a s is the same as
the product over s, as long as a is in s or f a = 1.
@[simp]
theorem
Finset.sum_insert_zero
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : f a = 0)
:
(Finset.sum (insert a s) fun x => f x) = Finset.sum s fun x => f x
The sum of f over insert a s is the same as
the sum over s, as long as f a = 0.
@[simp]
theorem
Finset.prod_insert_one
{β : Type u}
{α : Type v}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : f a = 1)
:
(Finset.prod (insert a s) fun x => f x) = Finset.prod s fun x => f x
The product of f over insert a s is the same as
the product over s, as long as f a = 1.
@[simp]
theorem
Finset.sum_singleton
{β : Type u}
{α : Type v}
{a : α}
{f : α → β}
[AddCommMonoid β]
:
(Finset.sum {a} fun x => f x) = f a
@[simp]
theorem
Finset.prod_singleton
{β : Type u}
{α : Type v}
{a : α}
{f : α → β}
[CommMonoid β]
:
(Finset.prod {a} fun x => f x) = f a
theorem
Finset.sum_pair
{β : Type u}
{α : Type v}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{a : α}
{b : α}
(h : a ≠ b)
:
(Finset.sum {a, b} fun x => f x) = f a + f b
theorem
Finset.prod_pair
{β : Type u}
{α : Type v}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{a : α}
{b : α}
(h : a ≠ b)
:
(Finset.prod {a, b} fun x => f x) = f a * f b
@[simp]
theorem
Finset.sum_const_zero
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
:
(Finset.sum s fun _x => 0) = 0
@[simp]
theorem
Finset.prod_const_one
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
:
(Finset.prod s fun _x => 1) = 1
@[simp]
theorem
Finset.sum_image
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
(∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y) →
(Finset.sum (Finset.image g s) fun x => f x) = Finset.sum s fun x => f (g x)
@[simp]
theorem
Finset.prod_image
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
(∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y) →
(Finset.prod (Finset.image g s) fun x => f x) = Finset.prod s fun x => f (g x)
@[simp]
theorem
Finset.sum_map
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(s : Finset α)
(e : α ↪ γ)
(f : γ → β)
:
(Finset.sum (Finset.map e s) fun x => f x) = Finset.sum s fun x => f (↑e x)
@[simp]
theorem
Finset.prod_map
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(s : Finset α)
(e : α ↪ γ)
(f : γ → β)
:
(Finset.prod (Finset.map e s) fun x => f x) = Finset.prod s fun x => f (↑e x)
theorem
Finset.sum_congr
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
[AddCommMonoid β]
(h : s₁ = s₂)
:
(∀ (x : α), x ∈ s₂ → f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g
theorem
Finset.prod_congr
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
[CommMonoid β]
(h : s₁ = s₂)
:
(∀ (x : α), x ∈ s₂ → f x = g x) → Finset.prod s₁ f = Finset.prod s₂ g
theorem
Finset.sum_disjUnion
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : Disjoint s₁ s₂)
:
(Finset.sum (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem
Finset.prod_disjUnion
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[CommMonoid β]
(h : Disjoint s₁ s₂)
:
(Finset.prod (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem
Finset.sum_disjiUnion
{ι : Type u_1}
{β : Type u}
{α : Type v}
{f : α → β}
[AddCommMonoid β]
(s : Finset ι)
(t : ι → Finset α)
(h : Set.PairwiseDisjoint (↑s) t)
:
(Finset.sum (Finset.disjiUnion s t h) fun x => f x) = Finset.sum s fun i => Finset.sum (t i) fun x => f x
theorem
Finset.prod_disjiUnion
{ι : Type u_1}
{β : Type u}
{α : Type v}
{f : α → β}
[CommMonoid β]
(s : Finset ι)
(t : ι → Finset α)
(h : Set.PairwiseDisjoint (↑s) t)
:
(Finset.prod (Finset.disjiUnion s t h) fun x => f x) = Finset.prod s fun i => Finset.prod (t i) fun x => f x
theorem
Finset.sum_union_inter
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
:
((Finset.sum (s₁ ∪ s₂) fun x => f x) + Finset.sum (s₁ ∩ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem
Finset.prod_union_inter
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
:
((Finset.prod (s₁ ∪ s₂) fun x => f x) * Finset.prod (s₁ ∩ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem
Finset.sum_union
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : Disjoint s₁ s₂)
:
(Finset.sum (s₁ ∪ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem
Finset.prod_union
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : Disjoint s₁ s₂)
:
(Finset.prod (s₁ ∪ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem
Finset.sum_filter_add_sum_filter_not
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
((Finset.sum (Finset.filter p s) fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.sum s fun x => f x
theorem
Finset.prod_filter_mul_prod_filter_not
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
((Finset.prod (Finset.filter p s) fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.prod s fun x => f x
@[simp]
theorem
Finset.sum_to_list
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
List.sum (List.map f (Finset.toList s)) = Finset.sum s f
@[simp]
theorem
Finset.prod_to_list
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
List.prod (List.map f (Finset.toList s)) = Finset.prod s f
theorem
Equiv.Perm.sum_comp
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → β)
(hs : {a | ↑σ a ≠ a} ⊆ ↑s)
:
(Finset.sum s fun x => f (↑σ x)) = Finset.sum s fun x => f x
theorem
Equiv.Perm.prod_comp
{β : Type u}
{α : Type v}
[CommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → β)
(hs : {a | ↑σ a ≠ a} ⊆ ↑s)
:
(Finset.prod s fun x => f (↑σ x)) = Finset.prod s fun x => f x
theorem
Equiv.Perm.sum_comp'
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → α → β)
(hs : {a | ↑σ a ≠ a} ⊆ ↑s)
:
(Finset.sum s fun x => f (↑σ x) x) = Finset.sum s fun x => f x (↑σ.symm x)
theorem
Equiv.Perm.prod_comp'
{β : Type u}
{α : Type v}
[CommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → α → β)
(hs : {a | ↑σ a ≠ a} ⊆ ↑s)
:
(Finset.prod s fun x => f (↑σ x) x) = Finset.prod s fun x => f x (↑σ.symm x)
theorem
IsCompl.sum_add_sum
{β : Type u}
{α : Type v}
[Fintype α]
[AddCommMonoid β]
{s : Finset α}
{t : Finset α}
(h : IsCompl s t)
(f : α → β)
:
((Finset.sum s fun i => f i) + Finset.sum t fun i => f i) = Finset.sum Finset.univ fun i => f i
theorem
IsCompl.prod_mul_prod
{β : Type u}
{α : Type v}
[Fintype α]
[CommMonoid β]
{s : Finset α}
{t : Finset α}
(h : IsCompl s t)
(f : α → β)
:
((Finset.prod s fun i => f i) * Finset.prod t fun i => f i) = Finset.prod Finset.univ fun i => f i
theorem
Finset.sum_add_sum_compl
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
((Finset.sum s fun i => f i) + Finset.sum sᶜ fun i => f i) = Finset.sum Finset.univ fun i => f i
Adding the sums of a function over s and over sᶜ gives the whole sum.
For a version expressed with subtypes, see Fintype.sum_subtype_add_sum_subtype.
theorem
Finset.prod_mul_prod_compl
{β : Type u}
{α : Type v}
[CommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
((Finset.prod s fun i => f i) * Finset.prod sᶜ fun i => f i) = Finset.prod Finset.univ fun i => f i
Multiplying the products of a function over s and over sᶜ gives the whole product.
For a version expressed with subtypes, see Fintype.prod_subtype_mul_prod_subtype.
theorem
Finset.sum_compl_add_sum
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
((Finset.sum sᶜ fun i => f i) + Finset.sum s fun i => f i) = Finset.sum Finset.univ fun i => f i
theorem
Finset.prod_compl_mul_prod
{β : Type u}
{α : Type v}
[CommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
((Finset.prod sᶜ fun i => f i) * Finset.prod s fun i => f i) = Finset.prod Finset.univ fun i => f i
theorem
Finset.sum_sdiff
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
:
((Finset.sum (s₂ \ s₁) fun x => f x) + Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x
theorem
Finset.prod_sdiff
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
:
((Finset.prod (s₂ \ s₁) fun x => f x) * Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x
@[simp]
theorem
Finset.sum_disj_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α ⊕ γ → β)
:
(Finset.sum (Finset.disjSum s t) fun x => f x) = (Finset.sum s fun x => f (Sum.inl x)) + Finset.sum t fun x => f (Sum.inr x)
@[simp]
theorem
Finset.prod_disj_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α ⊕ γ → β)
:
(Finset.prod (Finset.disjSum s t) fun x => f x) = (Finset.prod s fun x => f (Sum.inl x)) * Finset.prod t fun x => f (Sum.inr x)
theorem
Finset.sum_sum_elim
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α → β)
(g : γ → β)
:
(Finset.sum (Finset.disjSum s t) fun x => Sum.elim f g x) = (Finset.sum s fun x => f x) + Finset.sum t fun x => g x
theorem
Finset.prod_sum_elim
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α → β)
(g : γ → β)
:
(Finset.prod (Finset.disjSum s t) fun x => Sum.elim f g x) = (Finset.prod s fun x => f x) * Finset.prod t fun x => g x
theorem
Finset.sum_biUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : Set.PairwiseDisjoint (↑s) t)
:
(Finset.sum (Finset.biUnion s t) fun x => f x) = Finset.sum s fun x => Finset.sum (t x) fun i => f i
theorem
Finset.prod_biUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : Set.PairwiseDisjoint (↑s) t)
:
(Finset.prod (Finset.biUnion s t) fun x => f x) = Finset.prod s fun x => Finset.prod (t x) fun i => f i
theorem
Finset.sum_sigma
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{σ : α → Type u_2}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : Sigma σ → β)
:
(Finset.sum (Finset.sigma s t) fun x => f x) = Finset.sum s fun a => Finset.sum (t a) fun s => f { fst := a, snd := s }
Sum over a sigma type equals the sum of fiberwise sums. For rewriting
in the reverse direction, use Finset.sum_sigma'
theorem
Finset.prod_sigma
{β : Type u}
{α : Type v}
[CommMonoid β]
{σ : α → Type u_2}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : Sigma σ → β)
:
(Finset.prod (Finset.sigma s t) fun x => f x) = Finset.prod s fun a => Finset.prod (t a) fun s => f { fst := a, snd := s }
Product over a sigma type equals the product of fiberwise products. For rewriting
in the reverse direction, use Finset.prod_sigma'.
theorem
Finset.sum_sigma'
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{σ : α → Type u_2}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : (a : α) → σ a → β)
:
(Finset.sum s fun a => Finset.sum (t a) fun s => f a s) = Finset.sum (Finset.sigma s t) fun x => f x.fst x.snd
theorem
Finset.prod_sigma'
{β : Type u}
{α : Type v}
[CommMonoid β]
{σ : α → Type u_2}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : (a : α) → σ a → β)
:
(Finset.prod s fun a => Finset.prod (t a) fun s => f a s) = Finset.prod (Finset.sigma s t) fun x => f x.fst x.snd
theorem
Finset.sum_bij
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → γ)
(hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t)
(h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha))
(i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha)
:
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x
Reorder a sum.
The difference with sum_bij' is that the bijection is specified as a surjective injection,
rather than by an inverse function.
theorem
Finset.prod_bij
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → γ)
(hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t)
(h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha))
(i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha)
:
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x
Reorder a product.
The difference with prod_bij' is that the bijection is specified as a surjective injection,
rather than by an inverse function.
theorem
Finset.sum_bij'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → γ)
(hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t)
(h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha))
(j : (a : γ) → a ∈ t → α)
(hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s)
(left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (hi a ha) = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (hj a ha) = a)
:
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x
Reorder a sum.
The difference with sum_bij is that the bijection is specified with an inverse, rather than
as a surjective injection.
theorem
Finset.prod_bij'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → γ)
(hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t)
(h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha))
(j : (a : γ) → a ∈ t → α)
(hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s)
(left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (hi a ha) = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (hj a ha) = a)
:
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x
Reorder a product.
The difference with prod_bij is that the bijection is specified with an inverse, rather than
as a surjective injection.
theorem
Finset.Equiv.sum_comp_finset
{ι : Type u_1}
{β : Type u}
[AddCommMonoid β]
{ι' : Type u_2}
[DecidableEq ι]
(e : ι ≃ ι')
(f : ι' → β)
{s' : Finset ι'}
{s : Finset ι}
(h : s = Finset.image (↑e.symm) s')
:
(Finset.sum s' fun i' => f i') = Finset.sum s fun i => f (↑e i)
Reindexing a sum over a finset along an equivalence.
See Equiv.sum_comp for the version where s and s' are univ.
theorem
Finset.Equiv.prod_comp_finset
{ι : Type u_1}
{β : Type u}
[CommMonoid β]
{ι' : Type u_2}
[DecidableEq ι]
(e : ι ≃ ι')
(f : ι' → β)
{s' : Finset ι'}
{s : Finset ι}
(h : s = Finset.image (↑e.symm) s')
:
(Finset.prod s' fun i' => f i') = Finset.prod s fun i => f (↑e i)
Reindexing a product over a finset along an equivalence.
See Equiv.prod_comp for the version where s and s' are univ.
theorem
Finset.sum_finset_product
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(r : Finset (γ × α))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst)
{f : γ × α → β}
:
(Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (c, a)
theorem
Finset.prod_finset_product
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(r : Finset (γ × α))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst)
{f : γ × α → β}
:
(Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (c, a)
theorem
Finset.sum_finset_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(r : Finset (γ × α))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst)
{f : γ → α → β}
:
(Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f c a
theorem
Finset.prod_finset_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(r : Finset (γ × α))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst)
{f : γ → α → β}
:
(Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f c a
theorem
Finset.sum_finset_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(r : Finset (α × γ))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd)
{f : α × γ → β}
:
(Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (a, c)
theorem
Finset.prod_finset_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(r : Finset (α × γ))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd)
{f : α × γ → β}
:
(Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (a, c)
theorem
Finset.sum_finset_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
(r : Finset (α × γ))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd)
{f : α → γ → β}
:
(Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f a c
theorem
Finset.prod_finset_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
(r : Finset (α × γ))
(s : Finset γ)
(t : γ → Finset α)
(h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd)
{f : α → γ → β}
:
(Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f a c
theorem
Finset.sum_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
[DecidableEq γ]
{s : Finset α}
{t : Finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β)
:
(Finset.sum t fun y => Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.sum s fun x => f x
theorem
Finset.prod_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
[DecidableEq γ]
{s : Finset α}
{t : Finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β)
:
(Finset.prod t fun y => Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.prod s fun x => f x
theorem
Finset.sum_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = Finset.sum (Finset.filter (fun c' => g c' = g c) s) fun x => h x)
:
(Finset.sum (Finset.image g s) fun x => f x) = Finset.sum s fun x => h x
theorem
Finset.prod_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = Finset.prod (Finset.filter (fun c' => g c' = g c) s) fun x => h x)
:
(Finset.prod (Finset.image g s) fun x => f x) = Finset.prod s fun x => h x
theorem
Finset.sum_add_distrib
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
{g : α → β}
[AddCommMonoid β]
:
(Finset.sum s fun x => f x + g x) = (Finset.sum s fun x => f x) + Finset.sum s fun x => g x
theorem
Finset.prod_mul_distrib
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
{g : α → β}
[CommMonoid β]
:
(Finset.prod s fun x => f x * g x) = (Finset.prod s fun x => f x) * Finset.prod s fun x => g x
theorem
Finset.sum_product
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ × α → β}
:
(Finset.sum (s ×ˢ t) fun x => f x) = Finset.sum s fun x => Finset.sum t fun y => f (x, y)
theorem
Finset.prod_product
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ × α → β}
:
(Finset.prod (s ×ˢ t) fun x => f x) = Finset.prod s fun x => Finset.prod t fun y => f (x, y)
theorem
Finset.sum_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.sum (s ×ˢ t) fun x => f x.fst x.snd) = Finset.sum s fun x => Finset.sum t fun y => f x y
An uncurried version of Finset.sum_product
theorem
Finset.prod_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.prod (s ×ˢ t) fun x => f x.fst x.snd) = Finset.prod s fun x => Finset.prod t fun y => f x y
An uncurried version of Finset.prod_product.
theorem
Finset.sum_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ × α → β}
:
(Finset.sum (s ×ˢ t) fun x => f x) = Finset.sum t fun y => Finset.sum s fun x => f (x, y)
theorem
Finset.prod_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ × α → β}
:
(Finset.prod (s ×ˢ t) fun x => f x) = Finset.prod t fun y => Finset.prod s fun x => f (x, y)
theorem
Finset.sum_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.sum (s ×ˢ t) fun x => f x.fst x.snd) = Finset.sum t fun y => Finset.sum s fun x => f x y
An uncurried version of Finset.prod_product_right
theorem
Finset.prod_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.prod (s ×ˢ t) fun x => f x.fst x.snd) = Finset.prod t fun y => Finset.prod s fun x => f x y
An uncurried version of Finset.prod_product_right.
theorem
Finset.sum_comm'
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : γ → Finset α}
{t' : Finset α}
{s' : α → Finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β}
:
(Finset.sum s fun x => Finset.sum (t x) fun y => f x y) = Finset.sum t' fun y => Finset.sum (s' y) fun x => f x y
Generalization of Finset.sum_comm to the case when the inner Finsets depend on
the outer variable.
theorem
Finset.prod_comm'
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : γ → Finset α}
{t' : Finset α}
{s' : α → Finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β}
:
(Finset.prod s fun x => Finset.prod (t x) fun y => f x y) = Finset.prod t' fun y => Finset.prod (s' y) fun x => f x y
Generalization of Finset.prod_comm to the case when the inner Finsets depend on the outer
variable.
theorem
Finset.sum_comm
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.sum s fun x => Finset.sum t fun y => f x y) = Finset.sum t fun y => Finset.sum s fun x => f x y
theorem
Finset.prod_comm
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
(Finset.prod s fun x => Finset.prod t fun y => f x y) = Finset.prod t fun y => Finset.prod s fun x => f x y
theorem
Finset.sum_hom_rel
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
[AddCommMonoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : Finset α}
(h₁ : r 0 0)
(h₂ : (a : α) → (b : β) → (c : γ) → r b c → r (f a + b) (g a + c))
:
r (Finset.sum s fun x => f x) (Finset.sum s fun x => g x)
theorem
Finset.prod_hom_rel
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
[CommMonoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : Finset α}
(h₁ : r 1 1)
(h₂ : (a : α) → (b : β) → (c : γ) → r b c → r (f a * b) (g a * c))
:
r (Finset.prod s fun x => f x) (Finset.prod s fun x => g x)
theorem
Finset.sum_eq_zero
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{f : α → β}
{s : Finset α}
(h : ∀ (x : α), x ∈ s → f x = 0)
:
(Finset.sum s fun x => f x) = 0
theorem
Finset.prod_eq_one
{β : Type u}
{α : Type v}
[CommMonoid β]
{f : α → β}
{s : Finset α}
(h : ∀ (x : α), x ∈ s → f x = 1)
:
(Finset.prod s fun x => f x) = 1
theorem
Finset.sum_subset_zero_on_sdiff
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
(hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 0)
(hfg : ∀ (x : α), x ∈ s₁ → f x = g x)
:
(Finset.sum s₁ fun i => f i) = Finset.sum s₂ fun i => g i
theorem
Finset.prod_subset_one_on_sdiff
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
{g : α → β}
[CommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
(hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1)
(hfg : ∀ (x : α), x ∈ s₁ → f x = g x)
:
(Finset.prod s₁ fun i => f i) = Finset.prod s₂ fun i => g i
theorem
Finset.sum_subset
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ (x : α), x ∈ s₂ → ¬x ∈ s₁ → f x = 0)
:
(Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x
theorem
Finset.prod_subset
{β : Type u}
{α : Type v}
{s₁ : Finset α}
{s₂ : Finset α}
{f : α → β}
[CommMonoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ (x : α), x ∈ s₂ → ¬x ∈ s₁ → f x = 1)
:
(Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x
theorem
Finset.sum_filter_of_ne
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{p : α → Prop}
[DecidablePred p]
(hp : (x : α) → x ∈ s → f x ≠ 0 → p x)
:
(Finset.sum (Finset.filter p s) fun x => f x) = Finset.sum s fun x => f x
theorem
Finset.prod_filter_of_ne
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{p : α → Prop}
[DecidablePred p]
(hp : (x : α) → x ∈ s → f x ≠ 1 → p x)
:
(Finset.prod (Finset.filter p s) fun x => f x) = Finset.prod s fun x => f x
theorem
Finset.sum_filter_ne_zero
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
[(x : α) → Decidable (f x ≠ 0)]
:
(Finset.sum (Finset.filter (fun x => f x ≠ 0) s) fun x => f x) = Finset.sum s fun x => f x
theorem
Finset.prod_filter_ne_one
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
[(x : α) → Decidable (f x ≠ 1)]
:
(Finset.prod (Finset.filter (fun x => f x ≠ 1) s) fun x => f x) = Finset.prod s fun x => f x
theorem
Finset.sum_filter
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
(Finset.sum (Finset.filter p s) fun a => f a) = Finset.sum s fun a => if p a then f a else 0
theorem
Finset.prod_filter
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
(Finset.prod (Finset.filter p s) fun a => f a) = Finset.prod s fun a => if p a then f a else 1
theorem
Finset.sum_eq_single_of_mem
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0)
:
(Finset.sum s fun x => f x) = f a
theorem
Finset.prod_eq_single_of_mem
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1)
:
(Finset.prod s fun x => f x) = f a
theorem
Finset.sum_eq_single
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0)
(h₁ : ¬a ∈ s → f a = 0)
:
(Finset.sum s fun x => f x) = f a
theorem
Finset.prod_eq_single
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1)
(h₁ : ¬a ∈ s → f a = 1)
:
(Finset.prod s fun x => f x) = f a
theorem
Finset.sum_attach
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{f : α → β}
:
(Finset.sum (Finset.attach s) fun x => f ↑x) = Finset.sum s fun x => f x
theorem
Finset.prod_attach
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{f : α → β}
:
(Finset.prod (Finset.attach s) fun x => f ↑x) = Finset.prod s fun x => f x
@[simp]
theorem
Finset.sum_subtype_eq_sum_filter
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
:
(Finset.sum (Finset.subtype p s) fun x => f ↑x) = Finset.sum (Finset.filter p s) fun x => f x
A sum over s.subtype p equals one over s.filter p.
@[simp]
theorem
Finset.prod_subtype_eq_prod_filter
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
:
(Finset.prod (Finset.subtype p s) fun x => f ↑x) = Finset.prod (Finset.filter p s) fun x => f x
A product over s.subtype p equals one over s.filter p.
theorem
Finset.sum_subtype_of_mem
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
(h : (x : α) → x ∈ s → p x)
:
(Finset.sum (Finset.subtype p s) fun x => f ↑x) = Finset.sum s fun x => f x
If all elements of a Finset satisfy the predicate p, a sum
over s.subtype p equals that sum over s.
theorem
Finset.prod_subtype_of_mem
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
(h : (x : α) → x ∈ s → p x)
:
(Finset.prod (Finset.subtype p s) fun x => f ↑x) = Finset.prod s fun x => f x
If all elements of a Finset satisfy the predicate p, a product
over s.subtype p equals that product over s.
theorem
Finset.sum_subtype_map_embedding
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{p : α → Prop}
{s : Finset { x // p x }}
{f : { x // p x } → β}
{g : α → β}
(h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x)
:
(Finset.sum (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.sum s fun x => f x
A sum of a function over a Finset in a subtype equals a
sum in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.prod_subtype_map_embedding
{β : Type u}
{α : Type v}
[CommMonoid β]
{p : α → Prop}
{s : Finset { x // p x }}
{f : { x // p x } → β}
{g : α → β}
(h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x)
:
(Finset.prod (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.prod s fun x => f x
A product of a function over a Finset in a subtype equals a
product in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.sum_coe_sort_eq_attach
{β : Type u}
{α : Type v}
(s : Finset α)
[AddCommMonoid β]
(f : { x // x ∈ s } → β)
:
(Finset.sum Finset.univ fun i => f i) = Finset.sum (Finset.attach s) fun i => f i
theorem
Finset.prod_coe_sort_eq_attach
{β : Type u}
{α : Type v}
(s : Finset α)
[CommMonoid β]
(f : { x // x ∈ s } → β)
:
(Finset.prod Finset.univ fun i => f i) = Finset.prod (Finset.attach s) fun i => f i
theorem
Finset.sum_coe_sort
{β : Type u}
{α : Type v}
(s : Finset α)
(f : α → β)
[AddCommMonoid β]
:
(Finset.sum Finset.univ fun i => f ↑i) = Finset.sum s fun i => f i
theorem
Finset.prod_coe_sort
{β : Type u}
{α : Type v}
(s : Finset α)
(f : α → β)
[CommMonoid β]
:
(Finset.prod Finset.univ fun i => f ↑i) = Finset.prod s fun i => f i
theorem
Finset.sum_finset_coe
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(f : α → β)
(s : Finset α)
:
(Finset.sum Finset.univ fun i => f ↑i) = Finset.sum s fun i => f i
theorem
Finset.prod_finset_coe
{β : Type u}
{α : Type v}
[CommMonoid β]
(f : α → β)
(s : Finset α)
:
(Finset.prod Finset.univ fun i => f ↑i) = Finset.prod s fun i => f i
theorem
Finset.sum_subtype
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{p : α → Prop}
{F : Fintype (Subtype p)}
(s : Finset α)
(h : ∀ (x : α), x ∈ s ↔ p x)
(f : α → β)
:
(Finset.sum s fun a => f a) = Finset.sum Finset.univ fun a => f ↑a
theorem
Finset.prod_subtype
{β : Type u}
{α : Type v}
[CommMonoid β]
{p : α → Prop}
{F : Fintype (Subtype p)}
(s : Finset α)
(h : ∀ (x : α), x ∈ s ↔ p x)
(f : α → β)
:
(Finset.prod s fun a => f a) = Finset.prod Finset.univ fun a => f ↑a
theorem
Finset.sum_set_coe
{β : Type u}
{α : Type v}
{f : α → β}
[AddCommMonoid β]
(s : Set α)
[Fintype ↑s]
:
(Finset.sum Finset.univ fun i => f ↑i) = Finset.sum (Set.toFinset s) fun i => f i
theorem
Finset.prod_set_coe
{β : Type u}
{α : Type v}
{f : α → β}
[CommMonoid β]
(s : Set α)
[Fintype ↑s]
:
(Finset.prod Finset.univ fun i => f ↑i) = Finset.prod (Set.toFinset s) fun i => f i
abbrev
Finset.sum_congr_set.match_1
{β : Type u_1}
[Fintype β]
(s : Set β)
[DecidablePred fun x => x ∈ s]
(motive : (x : { x // x ∈ s }) → x ∈ Finset.univ → Prop)
:
Instances For
theorem
Finset.sum_congr_set
{α : Type u_2}
[AddCommMonoid α]
{β : Type u_3}
[Fintype β]
(s : Set β)
[DecidablePred fun x => x ∈ s]
(f : β → α)
(g : ↑s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h })
(w' : ∀ (x : β), ¬x ∈ s → f x = 0)
:
Finset.sum Finset.univ f = Finset.sum Finset.univ g
The sum of a function g defined only on a set s is equal to
the sum of a function f defined everywhere,
as long as f and g agree on s, and f = 0 off s.
theorem
Finset.prod_congr_set
{α : Type u_2}
[CommMonoid α]
{β : Type u_3}
[Fintype β]
(s : Set β)
[DecidablePred fun x => x ∈ s]
(f : β → α)
(g : ↑s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h })
(w' : ∀ (x : β), ¬x ∈ s → f x = 1)
:
Finset.prod Finset.univ f = Finset.prod Finset.univ g
The product of a function g defined only on a set s is equal to
the product of a function f defined everywhere,
as long as f and g agree on s, and f = 1 off s.
theorem
Finset.sum_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
[DecidablePred fun x => ¬p x]
(f : (x : α) → p x → γ)
(g : (x : α) → ¬p x → γ)
(h : γ → β)
:
(Finset.sum s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.sum (Finset.attach (Finset.filter p s)) fun x => h (f ↑x (_ : ↑x ∈ s ∧ p ↑x).right)) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g ↑x (_ : ¬p ↑x))
theorem
Finset.prod_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
[DecidablePred fun x => ¬p x]
(f : (x : α) → p x → γ)
(g : (x : α) → ¬p x → γ)
(h : γ → β)
:
(Finset.prod s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.prod (Finset.attach (Finset.filter p s)) fun x => h (f ↑x (_ : ↑x ∈ s ∧ p ↑x).right)) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g ↑x (_ : ¬p ↑x))
theorem
Finset.sum_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{_hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(h : γ → β)
:
(Finset.sum s fun x => h (if p x then f x else g x)) = (Finset.sum (Finset.filter p s) fun x => h (f x)) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => h (g x)
theorem
Finset.prod_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{_hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(h : γ → β)
:
(Finset.prod s fun x => h (if p x then f x else g x)) = (Finset.prod (Finset.filter p s) fun x => h (f x)) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => h (g x)
theorem
Finset.sum_dite
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = (Finset.sum (Finset.attach (Finset.filter p s)) fun x => f ↑x (_ : ↑x ∈ s ∧ p ↑x).right) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g ↑x (_ : ¬p ↑x)
theorem
Finset.prod_dite
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = (Finset.prod (Finset.attach (Finset.filter p s)) fun x => f ↑x (_ : ↑x ∈ s ∧ p ↑x).right) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g ↑x (_ : ¬p ↑x)
theorem
Finset.sum_ite
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
:
(Finset.sum s fun x => if p x then f x else g x) = (Finset.sum (Finset.filter p s) fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => g x
theorem
Finset.prod_ite
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
:
(Finset.prod s fun x => if p x then f x else g x) = (Finset.prod (Finset.filter p s) fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => g x
theorem
Finset.sum_ite_of_false
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
(h : ∀ (x : α), x ∈ s → ¬p x)
:
(Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => g x
theorem
Finset.prod_ite_of_false
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
(h : ∀ (x : α), x ∈ s → ¬p x)
:
(Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => g x
theorem
Finset.sum_ite_of_true
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
(h : (x : α) → x ∈ s → p x)
:
(Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => f x
theorem
Finset.prod_ite_of_true
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → β)
(g : α → β)
(h : (x : α) → x ∈ s → p x)
:
(Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => f x
theorem
Finset.sum_apply_ite_of_false
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → ¬p x)
:
(Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (g x)
theorem
Finset.prod_apply_ite_of_false
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → ¬p x)
:
(Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (g x)
theorem
Finset.sum_apply_ite_of_true
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(k : γ → β)
(h : (x : α) → x ∈ s → p x)
:
(Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (f x)
theorem
Finset.prod_apply_ite_of_true
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f : α → γ)
(g : α → γ)
(k : γ → β)
(h : (x : α) → x ∈ s → p x)
:
(Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (f x)
theorem
Finset.sum_extend_by_zero
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
(Finset.sum s fun i => if i ∈ s then f i else 0) = Finset.sum s fun i => f i
theorem
Finset.prod_extend_by_one
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
(Finset.prod s fun i => if i ∈ s then f i else 1) = Finset.prod s fun i => f i
@[simp]
theorem
Finset.sum_ite_mem
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
(Finset.sum s fun i => if i ∈ t then f i else 0) = Finset.sum (s ∩ t) fun i => f i
@[simp]
theorem
Finset.prod_ite_mem
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
(Finset.prod s fun i => if i ∈ t then f i else 1) = Finset.prod (s ∩ t) fun i => f i
@[simp]
theorem
Finset.sum_dite_eq
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → a = x → β)
:
(Finset.sum s fun x => if h : a = x then b x h else 0) = if a ∈ s then b a (_ : a = a) else 0
@[simp]
theorem
Finset.prod_dite_eq
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → a = x → β)
:
(Finset.prod s fun x => if h : a = x then b x h else 1) = if a ∈ s then b a (_ : a = a) else 1
@[simp]
theorem
Finset.sum_dite_eq'
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → x = a → β)
:
(Finset.sum s fun x => if h : x = a then b x h else 0) = if a ∈ s then b a (_ : a = a) else 0
@[simp]
theorem
Finset.prod_dite_eq'
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → x = a → β)
:
(Finset.prod s fun x => if h : x = a then b x h else 1) = if a ∈ s then b a (_ : a = a) else 1
@[simp]
theorem
Finset.sum_ite_eq
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
(Finset.sum s fun x => if a = x then b x else 0) = if a ∈ s then b a else 0
@[simp]
theorem
Finset.prod_ite_eq
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
(Finset.prod s fun x => if a = x then b x else 1) = if a ∈ s then b a else 1
@[simp]
theorem
Finset.sum_ite_eq'
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
(Finset.sum s fun x => if x = a then b x else 0) = if a ∈ s then b a else 0
A sum taken over a conditional whose condition is an equality
test on the index and whose alternative is 0 has value either the term at that index or 0.
The difference with Finset.sum_ite_eq is that the arguments to eq are swapped.
@[simp]
theorem
Finset.prod_ite_eq'
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
(Finset.prod s fun x => if x = a then b x else 1) = if a ∈ s then b a else 1
A product taken over a conditional whose condition is an equality test on the index and whose
alternative is 1 has value either the term at that index or 1.
The difference with Finset.prod_ite_eq is that the arguments to Eq are swapped.
theorem
Finset.sum_ite_index
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
(Finset.sum (if p then s else t) fun x => f x) = if p then Finset.sum s fun x => f x else Finset.sum t fun x => f x
theorem
Finset.prod_ite_index
{β : Type u}
{α : Type v}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
(Finset.prod (if p then s else t) fun x => f x) = if p then Finset.prod s fun x => f x else Finset.prod t fun x => f x
@[simp]
theorem
Finset.sum_ite_irrel
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : α → β)
(g : α → β)
:
(Finset.sum s fun x => if p then f x else g x) = if p then Finset.sum s fun x => f x else Finset.sum s fun x => g x
@[simp]
theorem
Finset.prod_ite_irrel
{β : Type u}
{α : Type v}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : α → β)
(g : α → β)
:
(Finset.prod s fun x => if p then f x else g x) = if p then Finset.prod s fun x => f x else Finset.prod s fun x => g x
@[simp]
theorem
Finset.sum_dite_irrel
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : p → α → β)
(g : ¬p → α → β)
:
(Finset.sum s fun x => if h : p then f h x else g h x) = if h : p then Finset.sum s fun x => f h x else Finset.sum s fun x => g h x
@[simp]
theorem
Finset.prod_dite_irrel
{β : Type u}
{α : Type v}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : p → α → β)
(g : ¬p → α → β)
:
(Finset.prod s fun x => if h : p then f h x else g h x) = if h : p then Finset.prod s fun x => f h x else Finset.prod s fun x => g h x
@[simp]
theorem
Finset.sum_pi_single'
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(a : α)
(x : β)
(s : Finset α)
:
(Finset.sum s fun a' => Pi.single a x a') = if a ∈ s then x else 0
@[simp]
theorem
Finset.prod_pi_mulSingle'
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(a : α)
(x : β)
(s : Finset α)
:
(Finset.prod s fun a' => Pi.mulSingle a x a') = if a ∈ s then x else 1
@[simp]
theorem
Finset.sum_pi_single
{α : Type v}
{β : α → Type u_2}
[DecidableEq α]
[(a : α) → AddCommMonoid (β a)]
(a : α)
(f : (a : α) → β a)
(s : Finset α)
:
(Finset.sum s fun a' => Pi.single a' (f a') a) = if a ∈ s then f a else 0
@[simp]
theorem
Finset.prod_pi_mulSingle
{α : Type v}
{β : α → Type u_2}
[DecidableEq α]
[(a : α) → CommMonoid (β a)]
(a : α)
(f : (a : α) → β a)
(s : Finset α)
:
(Finset.prod s fun a' => Pi.mulSingle a' (f a') a) = if a ∈ s then f a else 1
theorem
Finset.sum_bij_ne_zero
{β : Type u}
{α : Type v}
{γ : Type w}
[AddCommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → f a ≠ 0 → γ)
(hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t)
(i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
(i_surj : ∀ (b : γ), b ∈ t → g b ≠ 0 → ∃ a h₁ h₂, b = i a h₁ h₂)
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂))
:
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x
theorem
Finset.prod_bij_ne_one
{β : Type u}
{α : Type v}
{γ : Type w}
[CommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → f a ≠ 1 → γ)
(hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t)
(i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
(i_surj : ∀ (b : γ), b ∈ t → g b ≠ 1 → ∃ a h₁ h₂, b = i a h₁ h₂)
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂))
:
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x
theorem
Finset.sum_dite_of_false
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(h : ∀ (x : α), x ∈ s → ¬p x)
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => g (↑x) (h ↑x (_ : ↑x ∈ s))
theorem
Finset.prod_dite_of_false
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(h : ∀ (x : α), x ∈ s → ¬p x)
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => g (↑x) (h ↑x (_ : ↑x ∈ s))
theorem
Finset.sum_dite_of_true
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(h : (x : α) → x ∈ s → p x)
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => f (↑x) (h ↑x (_ : ↑x ∈ s))
theorem
Finset.prod_dite_of_true
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(h : (x : α) → x ∈ s → p x)
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => f (↑x) (h ↑x (_ : ↑x ∈ s))
theorem
Finset.nonempty_of_sum_ne_zero
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : (Finset.sum s fun x => f x) ≠ 0)
:
theorem
Finset.nonempty_of_prod_ne_one
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(h : (Finset.prod s fun x => f x) ≠ 1)
:
theorem
Finset.exists_ne_zero_of_sum_ne_zero
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : (Finset.sum s fun x => f x) ≠ 0)
:
theorem
Finset.exists_ne_one_of_prod_ne_one
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(h : (Finset.prod s fun x => f x) ≠ 1)
:
theorem
Finset.sum_range_succ_comm
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.sum (Finset.range (n + 1)) fun x => f x) = f n + Finset.sum (Finset.range n) fun x => f x
theorem
Finset.prod_range_succ_comm
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.prod (Finset.range (n + 1)) fun x => f x) = f n * Finset.prod (Finset.range n) fun x => f x
theorem
Finset.sum_range_succ
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.sum (Finset.range (n + 1)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + f n
theorem
Finset.prod_range_succ
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.prod (Finset.range (n + 1)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * f n
theorem
Finset.sum_range_succ'
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.sum (Finset.range (n + 1)) fun k => f k) = (Finset.sum (Finset.range n) fun k => f (k + 1)) + f 0
theorem
Finset.prod_range_succ'
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
(Finset.prod (Finset.range (n + 1)) fun k => f k) = (Finset.prod (Finset.range n) fun k => f (k + 1)) * f 0
theorem
Finset.eventually_constant_sum
{β : Type u}
[AddCommMonoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ (n : ℕ), n ≥ N → u n = 0)
{n : ℕ}
(hn : N ≤ n)
:
(Finset.sum (Finset.range n) fun k => u k) = Finset.sum (Finset.range N) fun k => u k
theorem
Finset.eventually_constant_prod
{β : Type u}
[CommMonoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ (n : ℕ), n ≥ N → u n = 1)
{n : ℕ}
(hn : N ≤ n)
:
(Finset.prod (Finset.range n) fun k => u k) = Finset.prod (Finset.range N) fun k => u k
theorem
Finset.sum_range_add
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
(m : ℕ)
:
(Finset.sum (Finset.range (n + m)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + Finset.sum (Finset.range m) fun x => f (n + x)
theorem
Finset.prod_range_add
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
(m : ℕ)
:
(Finset.prod (Finset.range (n + m)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * Finset.prod (Finset.range m) fun x => f (n + x)
theorem
Finset.sum_range_add_sub_sum_range
{α : Type u_2}
[AddCommGroup α]
(f : ℕ → α)
(n : ℕ)
(m : ℕ)
:
((Finset.sum (Finset.range (n + m)) fun k => f k) - Finset.sum (Finset.range n) fun k => f k) = Finset.sum (Finset.range m) fun k => f (n + k)
theorem
Finset.prod_range_add_div_prod_range
{α : Type u_2}
[CommGroup α]
(f : ℕ → α)
(n : ℕ)
(m : ℕ)
:
((Finset.prod (Finset.range (n + m)) fun k => f k) / Finset.prod (Finset.range n) fun k => f k) = Finset.prod (Finset.range m) fun k => f (n + k)
theorem
Finset.sum_range_zero
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
:
(Finset.sum (Finset.range 0) fun k => f k) = 0
theorem
Finset.prod_range_zero
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
:
(Finset.prod (Finset.range 0) fun k => f k) = 1
theorem
Finset.sum_range_one
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
:
(Finset.sum (Finset.range 1) fun k => f k) = f 0
theorem
Finset.prod_range_one
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
:
(Finset.prod (Finset.range 1) fun k => f k) = f 0
theorem
Finset.sum_list_map_count
{α : Type v}
[DecidableEq α]
(l : List α)
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
:
List.sum (List.map f l) = Finset.sum (List.toFinset l) fun m => List.count m l • f m
theorem
Finset.prod_list_map_count
{α : Type v}
[DecidableEq α]
(l : List α)
{M : Type u_2}
[CommMonoid M]
(f : α → M)
:
List.prod (List.map f l) = Finset.prod (List.toFinset l) fun m => f m ^ List.count m l
theorem
Finset.sum_list_count
{α : Type v}
[DecidableEq α]
[AddCommMonoid α]
(s : List α)
:
List.sum s = Finset.sum (List.toFinset s) fun m => List.count m s • m
theorem
Finset.prod_list_count
{α : Type v}
[DecidableEq α]
[CommMonoid α]
(s : List α)
:
List.prod s = Finset.prod (List.toFinset s) fun m => m ^ List.count m s
theorem
Finset.sum_list_count_of_subset
{α : Type v}
[DecidableEq α]
[AddCommMonoid α]
(m : List α)
(s : Finset α)
(hs : List.toFinset m ⊆ s)
:
List.sum m = Finset.sum s fun i => List.count i m • i
theorem
Finset.prod_list_count_of_subset
{α : Type v}
[DecidableEq α]
[CommMonoid α]
(m : List α)
(s : Finset α)
(hs : List.toFinset m ⊆ s)
:
List.prod m = Finset.prod s fun i => i ^ List.count i m
theorem
Finset.sum_filter_count_eq_countP
{α : Type v}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(l : List α)
:
(Finset.sum (Finset.filter p (List.toFinset l)) fun x => List.count x l) = List.countP (fun b => decide (p b)) l
theorem
Finset.sum_multiset_map_count
{α : Type v}
[DecidableEq α]
(s : Multiset α)
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
:
Multiset.sum (Multiset.map f s) = Finset.sum (Multiset.toFinset s) fun m => Multiset.count m s • f m
theorem
Finset.prod_multiset_map_count
{α : Type v}
[DecidableEq α]
(s : Multiset α)
{M : Type u_2}
[CommMonoid M]
(f : α → M)
:
Multiset.prod (Multiset.map f s) = Finset.prod (Multiset.toFinset s) fun m => f m ^ Multiset.count m s
theorem
Finset.sum_multiset_count
{α : Type v}
[DecidableEq α]
[AddCommMonoid α]
(s : Multiset α)
:
Multiset.sum s = Finset.sum (Multiset.toFinset s) fun m => Multiset.count m s • m
theorem
Finset.prod_multiset_count
{α : Type v}
[DecidableEq α]
[CommMonoid α]
(s : Multiset α)
:
Multiset.prod s = Finset.prod (Multiset.toFinset s) fun m => m ^ Multiset.count m s
theorem
Finset.sum_multiset_count_of_subset
{α : Type v}
[DecidableEq α]
[AddCommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : Multiset.toFinset m ⊆ s)
:
Multiset.sum m = Finset.sum s fun i => Multiset.count i m • i
theorem
Finset.prod_multiset_count_of_subset
{α : Type v}
[DecidableEq α]
[CommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : Multiset.toFinset m ⊆ s)
:
Multiset.prod m = Finset.prod s fun i => i ^ Multiset.count i m
theorem
Finset.sum_mem_multiset
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(m : Multiset α)
(f : { x // x ∈ m } → β)
(g : α → β)
(hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x)
:
(Finset.sum Finset.univ fun x => f x) = Finset.sum (Multiset.toFinset m) fun x => g x
theorem
Finset.prod_mem_multiset
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(m : Multiset α)
(f : { x // x ∈ m } → β)
(g : α → β)
(hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x)
:
(Finset.prod Finset.univ fun x => f x) = Finset.prod (Multiset.toFinset m) fun x => g x
theorem
Finset.sum_induction
{α : Type v}
{s : Finset α}
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : (a b : M) → p a → p b → p (a + b))
(unit : p 0)
(base : (x : α) → x ∈ s → p (f x))
:
p (Finset.sum s fun x => f x)
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
theorem
Finset.prod_induction
{α : Type v}
{s : Finset α}
{M : Type u_2}
[CommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : (a b : M) → p a → p b → p (a * b))
(unit : p 1)
(base : (x : α) → x ∈ s → p (f x))
:
p (Finset.prod s fun x => f x)
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
theorem
Finset.sum_induction_nonempty
{α : Type v}
{s : Finset α}
{M : Type u_2}
[AddCommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : (a b : M) → p a → p b → p (a + b))
(nonempty : Finset.Nonempty s)
(base : (x : α) → x ∈ s → p (f x))
:
p (Finset.sum s fun x => f x)
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
theorem
Finset.prod_induction_nonempty
{α : Type v}
{s : Finset α}
{M : Type u_2}
[CommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : (a b : M) → p a → p b → p (a * b))
(nonempty : Finset.Nonempty s)
(base : (x : α) → x ∈ s → p (f x))
:
p (Finset.prod s fun x => f x)
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
theorem
Finset.sum_range_induction
{β : Type u}
[AddCommMonoid β]
(f : ℕ → β)
(s : ℕ → β)
(base : s 0 = 0)
(step : ∀ (n : ℕ), s (n + 1) = s n + f n)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun k => f k) = s n
For any sum along {0, ..., n - 1} of a commutative-monoid-valued function, we can
verify that it's equal to a different function just by checking differences of adjacent terms.
This is a discrete analogue of the fundamental theorem of calculus.
theorem
Finset.prod_range_induction
{β : Type u}
[CommMonoid β]
(f : ℕ → β)
(s : ℕ → β)
(base : s 0 = 1)
(step : ∀ (n : ℕ), s (n + 1) = s n * f n)
(n : ℕ)
:
(Finset.prod (Finset.range n) fun k => f k) = s n
For any product along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify
that it's equal to a different function just by checking ratios of adjacent terms.
This is a multiplicative discrete analogue of the fundamental theorem of calculus.
theorem
Finset.sum_range_sub
{M : Type u_2}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun i => f (i + 1) - f i) = f n - f 0
A telescoping sum along {0, ..., n - 1} of an additive commutative group valued
function reduces to the difference of the last and first terms.
theorem
Finset.prod_range_div
{M : Type u_2}
[CommGroup M]
(f : ℕ → M)
(n : ℕ)
:
(Finset.prod (Finset.range n) fun i => f (i + 1) / f i) = f n / f 0
A telescoping product along {0, ..., n - 1} of a commutative group valued function reduces to
the ratio of the last and first factors.
theorem
Finset.sum_range_sub'
{M : Type u_2}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun i => f i - f (i + 1)) = f 0 - f n
theorem
Finset.prod_range_div'
{M : Type u_2}
[CommGroup M]
(f : ℕ → M)
(n : ℕ)
:
(Finset.prod (Finset.range n) fun i => f i / f (i + 1)) = f 0 / f n
theorem
Finset.eq_sum_range_sub
{M : Type u_2}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
f n = f 0 + Finset.sum (Finset.range n) fun i => f (i + 1) - f i
theorem
Finset.eq_prod_range_div
{M : Type u_2}
[CommGroup M]
(f : ℕ → M)
(n : ℕ)
:
f n = f 0 * Finset.prod (Finset.range n) fun i => f (i + 1) / f i
theorem
Finset.eq_sum_range_sub'
{M : Type u_2}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
f n = Finset.sum (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i - f (i - 1)
theorem
Finset.eq_prod_range_div'
{M : Type u_2}
[CommGroup M]
(f : ℕ → M)
(n : ℕ)
:
f n = Finset.prod (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i / f (i - 1)
theorem
Finset.sum_range_tsub
{α : Type v}
[CanonicallyOrderedAddMonoid α]
[Sub α]
[OrderedSub α]
[ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
{f : ℕ → α}
(h : Monotone f)
(n : ℕ)
:
(Finset.sum (Finset.range n) fun i => f (i + 1) - f i) = f n - f 0
A telescoping sum along {0, ..., n-1} of an ℕ-valued function
reduces to the difference of the last and first terms
when the function we are summing is monotone.
@[simp]
theorem
Finset.sum_const
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
(b : β)
:
(Finset.sum s fun _x => b) = Finset.card s • b
@[simp]
theorem
Finset.prod_const
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
(b : β)
:
(Finset.prod s fun _x => b) = b ^ Finset.card s
theorem
Finset.sum_eq_card_nsmul
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{b : β}
(hf : ∀ (a : α), a ∈ s → f a = b)
:
(Finset.sum s fun a => f a) = Finset.card s • b
theorem
Finset.prod_eq_pow_card
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{b : β}
(hf : ∀ (a : α), a ∈ s → f a = b)
:
(Finset.prod s fun a => f a) = b ^ Finset.card s
theorem
Finset.nsmul_eq_sum_const
{β : Type u}
[AddCommMonoid β]
(b : β)
(n : ℕ)
:
n • b = Finset.sum (Finset.range n) fun _k => b
theorem
Finset.pow_eq_prod_const
{β : Type u}
[CommMonoid β]
(b : β)
(n : ℕ)
:
b ^ n = Finset.prod (Finset.range n) fun _k => b
theorem
Finset.sum_nsmul
{β : Type u}
{α : Type v}
[AddCommMonoid β]
(s : Finset α)
(n : ℕ)
(f : α → β)
:
(Finset.sum s fun x => n • f x) = n • Finset.sum s fun x => f x
theorem
Finset.prod_pow
{β : Type u}
{α : Type v}
[CommMonoid β]
(s : Finset α)
(n : ℕ)
(f : α → β)
:
(Finset.prod s fun x => f x ^ n) = (Finset.prod s fun x => f x) ^ n
theorem
Finset.sum_flip
{β : Type u}
[AddCommMonoid β]
{n : ℕ}
(f : ℕ → β)
:
(Finset.sum (Finset.range (n + 1)) fun r => f (n - r)) = Finset.sum (Finset.range (n + 1)) fun k => f k
theorem
Finset.prod_flip
{β : Type u}
[CommMonoid β]
{n : ℕ}
(f : ℕ → β)
:
(Finset.prod (Finset.range (n + 1)) fun r => f (n - r)) = Finset.prod (Finset.range (n + 1)) fun k => f k
theorem
Finset.sum_involution
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
(g : (a : α) → a ∈ s → α)
:
abbrev
Finset.sum_involution.match_1
{α : Type u_1}
(s : Finset α)
(motive : Finset.Nonempty s → Prop)
:
(x : Finset.Nonempty s) → ((x : α) → (hx : x ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive x
Instances For
theorem
Finset.prod_involution
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{f : α → β}
(g : (a : α) → a ∈ s → α)
:
theorem
Finset.sum_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[AddCommMonoid β]
[DecidableEq γ]
(f : γ → β)
(g : α → γ)
:
(Finset.sum s fun a => f (g a)) = Finset.sum (Finset.image g s) fun b => Finset.card (Finset.filter (fun a => g a = b) s) • f b
The sum of the composition of functions f and g, is the sum over b ∈ s.image g
of f b times of the cardinality of the fibre of b. See also Finset.sum_image.
theorem
Finset.prod_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : Finset α}
[CommMonoid β]
[DecidableEq γ]
(f : γ → β)
(g : α → γ)
:
(Finset.prod s fun a => f (g a)) = Finset.prod (Finset.image g s) fun b => f b ^ Finset.card (Finset.filter (fun a => g a = b) s)
The product of the composition of functions f and g, is the product over b ∈ s.image g of
f b to the power of the cardinality of the fibre of b. See also Finset.prod_image.
theorem
Finset.sum_piecewise
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
(g : α → β)
:
(Finset.sum s fun x => Finset.piecewise t f g x) = (Finset.sum (s ∩ t) fun x => f x) + Finset.sum (s \ t) fun x => g x
theorem
Finset.prod_piecewise
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
(g : α → β)
:
(Finset.prod s fun x => Finset.piecewise t f g x) = (Finset.prod (s ∩ t) fun x => f x) * Finset.prod (s \ t) fun x => g x
theorem
Finset.sum_inter_add_sum_diff
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
((Finset.sum (s ∩ t) fun x => f x) + Finset.sum (s \ t) fun x => f x) = Finset.sum s fun x => f x
theorem
Finset.prod_inter_mul_prod_diff
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(t : Finset α)
(f : α → β)
:
((Finset.prod (s ∩ t) fun x => f x) * Finset.prod (s \ t) fun x => f x) = Finset.prod s fun x => f x
theorem
Finset.sum_eq_add_sum_diff_singleton
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
(Finset.sum s fun x => f x) = f i + Finset.sum (s \ {i}) fun x => f x
theorem
Finset.prod_eq_mul_prod_diff_singleton
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
(Finset.prod s fun x => f x) = f i * Finset.prod (s \ {i}) fun x => f x
theorem
Finset.sum_eq_sum_diff_singleton_add
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
(Finset.sum s fun x => f x) = (Finset.sum (s \ {i}) fun x => f x) + f i
theorem
Finset.prod_eq_prod_diff_singleton_mul
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
(Finset.prod s fun x => f x) = (Finset.prod (s \ {i}) fun x => f x) * f i
theorem
Fintype.sum_eq_add_sum_compl
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
(Finset.sum Finset.univ fun i => f i) = f a + Finset.sum {a}ᶜ fun i => f i
theorem
Fintype.prod_eq_mul_prod_compl
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
(Finset.prod Finset.univ fun i => f i) = f a * Finset.prod {a}ᶜ fun i => f i
theorem
Fintype.sum_eq_sum_compl_add
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
(Finset.sum Finset.univ fun i => f i) = (Finset.sum {a}ᶜ fun i => f i) + f a
theorem
Fintype.prod_eq_prod_compl_mul
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
(Finset.prod Finset.univ fun i => f i) = (Finset.prod {a}ᶜ fun i => f i) * f a
theorem
Finset.dvd_prod_of_mem
{β : Type u}
{α : Type v}
[CommMonoid β]
(f : α → β)
{a : α}
{s : Finset α}
(ha : a ∈ s)
:
f a ∣ Finset.prod s fun i => f i
theorem
Finset.sum_partition
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(R : Setoid α)
[DecidableRel Setoid.r]
:
(Finset.sum s fun x => f x) = Finset.sum (Finset.image Quotient.mk'' s) fun xbar =>
Finset.sum (Finset.filter (fun x => Quotient.mk R x = xbar) s) fun y => f y
A sum can be partitioned into a sum of sums, each equivalent under a setoid.
theorem
Finset.prod_partition
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(R : Setoid α)
[DecidableRel Setoid.r]
:
(Finset.prod s fun x => f x) = Finset.prod (Finset.image Quotient.mk'' s) fun xbar =>
Finset.prod (Finset.filter (fun x => Quotient.mk R x = xbar) s) fun y => f y
A product can be partitioned into a product of products, each equivalent under a setoid.
theorem
Finset.sum_cancels_of_partition_cancels
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(R : Setoid α)
[DecidableRel Setoid.r]
(h : ∀ (x : α), x ∈ s → (Finset.sum (Finset.filter (fun y => y ≈ x) s) fun a => f a) = 0)
:
(Finset.sum s fun x => f x) = 0
If we can partition a sum into subsets that cancel out, then the whole sum cancels.
theorem
Finset.prod_cancels_of_partition_cancels
{β : Type u}
{α : Type v}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(R : Setoid α)
[DecidableRel Setoid.r]
(h : ∀ (x : α), x ∈ s → (Finset.prod (Finset.filter (fun y => y ≈ x) s) fun a => f a) = 1)
:
(Finset.prod s fun x => f x) = 1
If we can partition a product into subsets that cancel out, then the whole product cancels.
theorem
Finset.sum_update_of_not_mem
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : ¬i ∈ s)
(f : α → β)
(b : β)
:
(Finset.sum s fun x => Function.update f i b x) = Finset.sum s fun x => f x
theorem
Finset.prod_update_of_not_mem
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : ¬i ∈ s)
(f : α → β)
(b : β)
:
(Finset.prod s fun x => Function.update f i b x) = Finset.prod s fun x => f x
theorem
Finset.sum_update_of_mem
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
(Finset.sum s fun x => Function.update f i b x) = b + Finset.sum (s \ {i}) fun x => f x
theorem
Finset.prod_update_of_mem
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
(Finset.prod s fun x => Function.update f i b x) = b * Finset.prod (s \ {i}) fun x => f x
theorem
Finset.eq_of_card_le_one_of_sum_eq
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
(hc : Finset.card s ≤ 1)
{f : α → β}
{b : β}
(h : (Finset.sum s fun x => f x) = b)
(x : α)
:
If a sum of a Finset of size at most 1 has a given
value, so do the terms in that sum.
theorem
Finset.eq_of_card_le_one_of_prod_eq
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
(hc : Finset.card s ≤ 1)
{f : α → β}
{b : β}
(h : (Finset.prod s fun x => f x) = b)
(x : α)
:
If a product of a Finset of size at most 1 has a given value, so
do the terms in that product.
theorem
Finset.add_sum_erase
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
(f a + Finset.sum (Finset.erase s a) fun x => f x) = Finset.sum s fun x => f x
Taking a sum over s : Finset α is the same as adding the value on a single element
f a to the sum over s.erase a.
See Multiset.sum_map_erase for the Multiset version.
theorem
Finset.mul_prod_erase
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
(f a * Finset.prod (Finset.erase s a) fun x => f x) = Finset.prod s fun x => f x
Taking a product over s : Finset α is the same as multiplying the value on a single element
f a by the product of s.erase a.
See Multiset.prod_map_erase for the Multiset version.
theorem
Finset.sum_erase_add
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
(Finset.sum (Finset.erase s a) fun x => f x) + f a = Finset.sum s fun x => f x
A variant of Finset.add_sum_erase with the addition swapped.
theorem
Finset.prod_erase_mul
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
(Finset.prod (Finset.erase s a) fun x => f x) * f a = Finset.prod s fun x => f x
A variant of Finset.mul_prod_erase with the multiplication swapped.
theorem
Finset.sum_erase
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
{f : α → β}
{a : α}
(h : f a = 0)
:
(Finset.sum (Finset.erase s a) fun x => f x) = Finset.sum s fun x => f x
If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.prod_erase
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
{f : α → β}
{a : α}
(h : f a = 1)
:
(Finset.prod (Finset.erase s a) fun x => f x) = Finset.prod s fun x => f x
If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.sum_ite_zero
{β : Type u}
{α : Type v}
{s : Finset α}
[AddCommMonoid β]
{f : α → Prop}
[DecidablePred f]
(hf : Set.PairwiseDisjoint (↑s) f)
(a : β)
:
(Finset.sum s fun i => if f i then a else 0) = if ∃ i, i ∈ s ∧ f i then a else 0
See also Finset.sum_boole.
theorem
Finset.prod_ite_one
{β : Type u}
{α : Type v}
{s : Finset α}
[CommMonoid β]
{f : α → Prop}
[DecidablePred f]
(hf : Set.PairwiseDisjoint (↑s) f)
(a : β)
:
(Finset.prod s fun i => if f i then a else 1) = if ∃ i, i ∈ s ∧ f i then a else 1
See also Finset.prod_boole.
theorem
Finset.sum_erase_lt_of_pos
{α : Type v}
{γ : Type u_2}
[DecidableEq α]
[OrderedAddCommMonoid γ]
[CovariantClass γ γ (fun x x_1 => x + x_1) fun x x_1 => x < x_1]
{s : Finset α}
{d : α}
(hd : d ∈ s)
{f : α → γ}
(hdf : 0 < f d)
:
(Finset.sum (Finset.erase s d) fun m => f m) < Finset.sum s fun m => f m
theorem
Finset.prod_erase_lt_of_one_lt
{α : Type v}
{γ : Type u_2}
[DecidableEq α]
[OrderedCommMonoid γ]
[CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1]
{s : Finset α}
{d : α}
(hd : d ∈ s)
{f : α → γ}
(hdf : 1 < f d)
:
(Finset.prod (Finset.erase s d) fun m => f m) < Finset.prod s fun m => f m
theorem
Finset.eq_zero_of_sum_eq_zero
{β : Type u}
{α : Type v}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
{a : α}
(hp : (Finset.sum s fun x => f x) = 0)
(h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 0)
(x : α)
:
If a sum is 0 and the function is 0 except possibly at one
point, it is 0 everywhere on the Finset.
theorem
Finset.eq_one_of_prod_eq_one
{β : Type u}
{α : Type v}
[CommMonoid β]
{s : Finset α}
{f : α → β}
{a : α}
(hp : (Finset.prod s fun x => f x) = 1)
(h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1)
(x : α)
:
If a product is 1 and the function is 1 except possibly at one
point, it is 1 everywhere on the Finset.
theorem
Finset.sum_boole_nsmul
{β : Type u}
{α : Type v}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
(a : α)
:
(Finset.sum s fun x => (if a = x then 1 else 0) • f x) = if a ∈ s then f a else 0
theorem
Finset.prod_pow_boole
{β : Type u}
{α : Type v}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
(a : α)
:
(Finset.prod s fun x => f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1
theorem
Finset.prod_dvd_prod_of_dvd
{β : Type u}
{α : Type v}
[CommMonoid β]
{S : Finset α}
(g1 : α → β)
(g2 : α → β)
(h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a)
:
Finset.prod S g1 ∣ Finset.prod S g2
theorem
Finset.prod_dvd_prod_of_subset
{ι : Type u_2}
{M : Type u_3}
[CommMonoid M]
(s : Finset ι)
(t : Finset ι)
(f : ι → M)
(h : s ⊆ t)
:
(Finset.prod s fun i => f i) ∣ Finset.prod t fun i => f i
theorem
Finset.prod_add_prod_eq
{β : Type u}
{α : Type v}
[CommSemiring β]
{s : Finset α}
{i : α}
{f : α → β}
{g : α → β}
{h : α → β}
(hi : i ∈ s)
(h1 : g i + h i = f i)
(h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j)
(h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j)
:
((Finset.prod s fun i => g i) + Finset.prod s fun i => h i) = Finset.prod s fun i => f i
If f = g = h everywhere but at i, where f i = g i + h i, then the product of f over s
is the sum of the products of g and h.
theorem
Finset.card_eq_sum_ones
{α : Type v}
(s : Finset α)
:
Finset.card s = Finset.sum s fun x => 1
theorem
Finset.sum_const_nat
{α : Type v}
{s : Finset α}
{m : ℕ}
{f : α → ℕ}
(h₁ : ∀ (x : α), x ∈ s → f x = m)
:
(Finset.sum s fun x => f x) = Finset.card s * m
@[simp]
theorem
Finset.sum_boole
{β : Type u}
{α : Type v}
{s : Finset α}
{p : α → Prop}
[NonAssocSemiring β]
{hp :