Big operators #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define products and sums indexed by finite sets (specifically, finset).
Notation #
We introduce the following notation, localized in big_operators.
To enable the notation, use open_locale big_operators.
Let s be a finset α, and f : α → β a function.
∏ x in s, f xis notation forfinset.prod s f(assumingβis acomm_monoid)∑ x in s, f xis notation forfinset.sum s f(assumingβis anadd_comm_monoid)∏ x, f xis notation forfinset.prod finset.univ f(assumingαis afintypeandβis acomm_monoid)∑ x, f xis notation forfinset.sum finset.univ f(assumingαis afintypeandβis anadd_comm_monoid)
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.
@[protected]
∑ x in s, f x is the sum of f x as x ranges over the elements
of the finite set s.
Equations
- s.sum f = (multiset.map f s.val).sum
@[protected]
∏ x in s, f x is the product of f x
as x ranges over the elements of the finite set s.
Equations
- s.prod f = (multiset.map f s.val).prod
@[simp]
theorem
finset.prod_mk
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : multiset α)
(hs : s.nodup)
(f : α → β) :
@[simp]
theorem
finset.sum_mk
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : multiset α)
(hs : s.nodup)
(f : α → β) :
@[simp]
@[simp]
There is no established mathematical convention
for the operator precedence of big operators like ∏ and ∑.
We will have to make a choice.
Online discussions, such as https://math.stackexchange.com/q/185538/30839
seem to suggest that ∏ and ∑ should have the same precedence,
and that this should be somewhere between * and +.
The latter have precedence levels 70 and 65 respectively,
and we therefore choose the level 67.
In practice, this means that parentheses should be placed as follows:
∑ k in K, (a k + b k) = ∑ k in K, a k + ∑ k in K, b k →
∏ k in K, a k * b k = (∏ k in K, a k) * (∏ k in K, b k)
(Example taken from page 490 of Knuth's Concrete Mathematics.)
theorem
finset.prod_eq_multiset_prod
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(f : α → β) :
s.prod (λ (x : α), f x) = (multiset.map f s.val).prod
theorem
finset.sum_eq_multiset_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(f : α → β) :
s.sum (λ (x : α), f x) = (multiset.map f s.val).sum
theorem
finset.prod_eq_fold
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(f : α → β) :
s.prod (λ (x : α), f x) = finset.fold has_mul.mul 1 f s
theorem
finset.sum_eq_fold
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(f : α → β) :
s.sum (λ (x : α), f x) = finset.fold has_add.add 0 f s
@[protected]
theorem
add_monoid_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β →+ γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
@[protected]
theorem
monoid_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β →* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
add_equiv.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β ≃+ γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
@[protected]
theorem
mul_equiv.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β ≃* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
ring_hom.map_list_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(l : list β) :
Deprecated: use _root_.map_list_sum instead.
@[protected]
theorem
ring_hom.unop_map_list_prod
{β : Type u}
{γ : Type w}
[semiring β]
[semiring γ]
(f : β →+* γᵐᵒᵖ)
(l : list β) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod
A morphism into the opposite ring acts on the product by acting on the reversed elements.
Deprecated: use _root_.unop_map_list_prod instead.
@[protected]
theorem
ring_hom.map_multiset_prod
{β : Type u}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(f : β →+* γ)
(s : multiset β) :
Deprecated: use _root_.map_multiset_prod instead.
@[protected]
theorem
ring_hom.map_multiset_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(s : multiset β) :
Deprecated: use _root_.map_multiset_sum instead.
@[protected]
theorem
ring_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
ring_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
theorem
add_monoid_hom.coe_finset_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_zero_class β]
[add_comm_monoid γ]
(f : α → β →+ γ)
(s : finset α) :
theorem
monoid_hom.coe_finset_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[mul_one_class β]
[comm_monoid γ]
(f : α → β →* γ)
(s : finset α) :
@[simp]
theorem
add_monoid_hom.finset_sum_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[add_zero_class β]
[add_comm_monoid γ]
(f : α → β →+ γ)
(s : finset α)
(b : β) :
@[simp]
theorem
monoid_hom.finset_prod_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[mul_one_class β]
[comm_monoid γ]
(f : α → β →* γ)
(s : finset α)
(b : β) :
@[simp]
@[simp]
theorem
finset.prod_of_empty
{β : Type u}
{α : Type v}
{f : α → β}
[comm_monoid β]
[is_empty α]
(s : finset α) :
theorem
finset.sum_of_empty
{β : Type u}
{α : Type v}
{f : α → β}
[add_comm_monoid β]
[is_empty α]
(s : finset α) :
@[simp]
theorem
finset.sum_cons
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
(h : a ∉ s) :
(finset.cons a s h).sum (λ (x : α), f x) = f a + s.sum (λ (x : α), f x)
@[simp]
theorem
finset.prod_cons
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
(h : a ∉ s) :
(finset.cons a s h).prod (λ (x : α), f x) = f a * s.prod (λ (x : α), f x)
@[simp]
theorem
finset.prod_insert
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
@[simp]
theorem
finset.sum_insert
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
@[simp]
theorem
finset.sum_insert_of_eq_zero_if_not_mem
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : a ∉ s → f a = 0) :
(has_insert.insert a s).sum (λ (x : α), f x) = s.sum (λ (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 : α → β}
[comm_monoid β]
[decidable_eq α]
(h : a ∉ s → f a = 1) :
(has_insert.insert a s).prod (λ (x : α), f x) = s.prod (λ (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 : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : f a = 0) :
(has_insert.insert a s).sum (λ (x : α), f x) = s.sum (λ (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 : α → β}
[comm_monoid β]
[decidable_eq α]
(h : f a = 1) :
(has_insert.insert a s).prod (λ (x : α), f x) = s.prod (λ (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]
@[simp]
theorem
finset.prod_pair
{β : Type u}
{α : Type v}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{a b : α}
(h : a ≠ b) :
theorem
finset.sum_pair
{β : Type u}
{α : Type v}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{a b : α}
(h : a ≠ b) :
@[simp]
@[simp]
@[simp]
theorem
finset.sum_map
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
(s : finset α)
(e : α ↪ γ)
(f : γ → β) :
(finset.map e s).sum (λ (x : γ), f x) = s.sum (λ (x : α), f (⇑e x))
@[simp]
theorem
finset.prod_map
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
(s : finset α)
(e : α ↪ γ)
(f : γ → β) :
(finset.map e s).prod (λ (x : γ), f x) = s.prod (λ (x : α), f (⇑e x))
theorem
finset.sum_disj_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
(h : disjoint s₁ s₂) :
theorem
finset.prod_disj_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
(h : disjoint s₁ s₂) :
theorem
finset.prod_disj_Union
{ι : Type u_1}
{β : Type u}
{α : Type v}
{f : α → β}
[comm_monoid β]
(s : finset ι)
(t : ι → finset α)
(h : ↑s.pairwise_disjoint t) :
(s.disj_Union t h).prod (λ (x : α), f x) = s.prod (λ (i : ι), (t i).prod (λ (x : α), f x))
theorem
finset.sum_disj_Union
{ι : Type u_1}
{β : Type u}
{α : Type v}
{f : α → β}
[add_comm_monoid β]
(s : finset ι)
(t : ι → finset α)
(h : ↑s.pairwise_disjoint t) :
(s.disj_Union t h).sum (λ (x : α), f x) = s.sum (λ (i : ι), (t i).sum (λ (x : α), f x))
theorem
finset.prod_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : disjoint s₁ s₂) :
theorem
finset.sum_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : disjoint s₁ s₂) :
theorem
finset.sum_filter_add_sum_filter_not
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(p : α → Prop)
[decidable_pred p]
[decidable_pred (λ (x : α), ¬p x)]
(f : α → β) :
(finset.filter p s).sum (λ (x : α), f x) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem
finset.prod_filter_mul_prod_filter_not
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(p : α → Prop)
[decidable_pred p]
[decidable_pred (λ (x : α), ¬p x)]
(f : α → β) :
(finset.filter p s).prod (λ (x : α), f x) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem
equiv.perm.sum_comp'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
theorem
equiv.perm.prod_comp'
{β : Type u}
{α : Type v}
[comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
theorem
is_compl.sum_add_sum
{β : Type u}
{α : Type v}
[fintype α]
[add_comm_monoid β]
{s t : finset α}
(h : is_compl s t)
(f : α → β) :
theorem
is_compl.prod_mul_prod
{β : Type u}
{α : Type v}
[fintype α]
[comm_monoid β]
{s t : finset α}
(h : is_compl s t)
(f : α → β) :
theorem
finset.sum_add_sum_compl
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
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}
[comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
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.prod_compl_mul_prod
{β : Type u}
{α : Type v}
[comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.sum_compl_add_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.prod_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂) :
theorem
finset.sum_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂) :
theorem
finset.prod_bUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α}
(hs : ↑s.pairwise_disjoint t) :
theorem
finset.sum_bUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α}
(hs : ↑s.pairwise_disjoint t) :
theorem
finset.sum_bij
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{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 : a ∈ s), b = i a ha)) :
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}
[comm_monoid β]
{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 : a ∈ s), b = i a ha)) :
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}
[add_comm_monoid β]
{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) _ = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) _ = a) :
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}
[comm_monoid β]
{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) _ = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) _ = a) :
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.prod_comp_finset
{ι : Type u_1}
{β : Type u}
[comm_monoid β]
{ι' : Type u_2}
[decidable_eq ι]
(e : ι ≃ ι')
(f : ι' → β)
{s' : finset ι'}
{s : finset ι}
(h : s = finset.image ⇑(e.symm) s') :
Reindexing a product over a finset along an equivalence.
See equiv.prod_comp for the version where s and s' are univ.
theorem
finset.equiv.sum_comp_finset
{ι : Type u_1}
{β : Type u}
[add_comm_monoid β]
{ι' : Type u_2}
[decidable_eq ι]
(e : ι ≃ ι')
(f : ι' → β)
{s' : finset ι'}
{s : finset ι}
(h : s = finset.image ⇑(e.symm) s') :
Reindexing a sum over a finset along an equivalence.
See equiv.sum_comp for the version where s and s' are univ.
theorem
finset.prod_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[decidable_eq γ]
{s : finset α}
{t : finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β) :
theorem
finset.sum_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[decidable_eq γ]
{s : finset α}
{t : finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β) :
theorem
finset.prod_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = (finset.filter (λ (c' : γ), g c' = g c) s).prod (λ (x : γ), h x)) :
(finset.image g s).prod (λ (x : α), f x) = s.prod (λ (x : γ), h x)
theorem
finset.sum_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = (finset.filter (λ (c' : γ), g c' = g c) s).sum (λ (x : γ), h x)) :
(finset.image g s).sum (λ (x : α), f x) = s.sum (λ (x : γ), h x)
theorem
finset.sum_comm'
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : γ → finset α}
{t' : finset α}
{s' : α → finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β} :
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}
[comm_monoid β]
{s : finset γ}
{t : γ → finset α}
{t' : finset α}
{s' : α → finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β} :
Generalization of finset.prod_comm to the case when the inner finsets depend on the outer
variable.
theorem
finset.prod_filter_of_ne
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
{p : α → Prop}
[decidable_pred p]
(hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x) :
(finset.filter p s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem
finset.sum_filter_of_ne
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
{p : α → Prop}
[decidable_pred p]
(hp : ∀ (x : α), x ∈ s → f x ≠ 0 → p x) :
(finset.filter p s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem
finset.prod_filter_ne_one
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
[Π (x : α), decidable (f x ≠ 1)] :
(finset.filter (λ (x : α), f x ≠ 1) s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem
finset.sum_filter_ne_zero
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
[Π (x : α), decidable (f x ≠ 0)] :
(finset.filter (λ (x : α), f x ≠ 0) s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem
finset.prod_filter
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(p : α → Prop)
[decidable_pred p]
(f : α → β) :
(finset.filter p s).prod (λ (a : α), f a) = s.prod (λ (a : α), ite (p a) (f a) 1)
theorem
finset.sum_filter
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(p : α → Prop)
[decidable_pred p]
(f : α → β) :
(finset.filter p s).sum (λ (a : α), f a) = s.sum (λ (a : α), ite (p a) (f a) 0)
@[simp]
theorem
finset.prod_subtype_eq_prod_filter
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
(finset.subtype p s).prod (λ (x : subtype p), f ↑x) = (finset.filter p s).prod (λ (x : α), f x)
A product over s.subtype p equals one over s.filter p.
@[simp]
theorem
finset.sum_subtype_eq_sum_filter
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
(finset.subtype p s).sum (λ (x : subtype p), f ↑x) = (finset.filter p s).sum (λ (x : α), f x)
A sum over s.subtype p equals one over s.filter p.
theorem
finset.prod_subtype_of_mem
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p]
(h : ∀ (x : α), x ∈ s → p 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_of_mem
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p]
(h : ∀ (x : α), x ∈ s → p x) :
If all elements of a finset satisfy the predicate p, a sum
over s.subtype p equals that sum over s.
theorem
finset.sum_subtype_map_embedding
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β}
(h : ∀ (x : {x // p x}), x ∈ s → g ↑x = f x) :
(finset.map (function.embedding.subtype (λ (x : α), p x)) s).sum (λ (x : α), g x) = s.sum (λ (x : {x // p 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}
[comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β}
(h : ∀ (x : {x // p x}), x ∈ s → g ↑x = f x) :
(finset.map (function.embedding.subtype (λ (x : α), p x)) s).prod (λ (x : α), g x) = s.prod (λ (x : {x // p 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 α)
[add_comm_monoid β]
(f : ↥s → β) :
theorem
finset.prod_coe_sort_eq_attach
{β : Type u}
{α : Type v}
(s : finset α)
[comm_monoid β]
(f : ↥s → β) :
theorem
finset.sum_coe_sort
{β : Type u}
{α : Type v}
(s : finset α)
(f : α → β)
[add_comm_monoid β] :
theorem
finset.prod_finset_coe
{β : Type u}
{α : Type v}
[comm_monoid β]
(f : α → β)
(s : finset α) :
theorem
finset.sum_finset_coe
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(f : α → β)
(s : finset α) :
theorem
finset.sum_congr_set
{α : Type u_1}
[add_comm_monoid α]
{β : Type u_2}
[fintype β]
(s : set β)
[decidable_pred (λ (_x : β), _x ∈ s)]
(f : β → α)
(g : ↥s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩)
(w' : ∀ (x : β), x ∉ s → f x = 0) :
finset.univ.sum f = finset.univ.sum 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_1}
[comm_monoid α]
{β : Type u_2}
[fintype β]
(s : set β)
[decidable_pred (λ (_x : β), _x ∈ s)]
(f : β → α)
(g : ↥s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩)
(w' : ∀ (x : β), x ∉ s → f x = 1) :
finset.univ.prod f = finset.univ.prod 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.prod_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
[decidable_pred (λ (x : α), ¬p x)]
(f : Π (x : α), p x → γ)
(g : Π (x : α), ¬p x → γ)
(h : γ → β) :
s.prod (λ (x : α), h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx))) = (finset.filter p s).attach.prod (λ (x : {x // x ∈ finset.filter p s}), h (f x.val _)) * (finset.filter (λ (x : α), ¬p x) s).attach.prod (λ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}), h (g x.val _))
theorem
finset.sum_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
[decidable_pred (λ (x : α), ¬p x)]
(f : Π (x : α), p x → γ)
(g : Π (x : α), ¬p x → γ)
(h : γ → β) :
s.sum (λ (x : α), h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx))) = (finset.filter p s).attach.sum (λ (x : {x // x ∈ finset.filter p s}), h (f x.val _)) + (finset.filter (λ (x : α), ¬p x) s).attach.sum (λ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}), h (g x.val _))
theorem
finset.prod_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(h : γ → β) :
s.prod (λ (x : α), h (ite (p x) (f x) (g x))) = (finset.filter p s).prod (λ (x : α), h (f x)) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), h (g x))
theorem
finset.sum_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(h : γ → β) :
s.sum (λ (x : α), h (ite (p x) (f x) (g x))) = (finset.filter p s).sum (λ (x : α), h (f x)) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), h (g x))
theorem
finset.sum_dite
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
s.sum (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (finset.filter p s).attach.sum (λ (x : {x // x ∈ finset.filter p s}), f x.val _) + (finset.filter (λ (x : α), ¬p x) s).attach.sum (λ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}), g x.val _)
theorem
finset.prod_dite
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
s.prod (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (finset.filter p s).attach.prod (λ (x : {x // x ∈ finset.filter p s}), f x.val _) * (finset.filter (λ (x : α), ¬p x) s).attach.prod (λ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}), g x.val _)
theorem
finset.prod_ite
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β) :
s.prod (λ (x : α), ite (p x) (f x) (g x)) = (finset.filter p s).prod (λ (x : α), f x) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), g x)
theorem
finset.sum_ite
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β) :
s.sum (λ (x : α), ite (p x) (f x) (g x)) = (finset.filter p s).sum (λ (x : α), f x) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), g x)
theorem
finset.sum_extend_by_zero
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.prod_extend_by_one
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β) :
@[simp]
theorem
finset.prod_ite_mem
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
@[simp]
theorem
finset.sum_ite_mem
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
@[simp]
theorem
finset.prod_ite_eq
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
@[simp]
theorem
finset.sum_ite_eq
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
@[simp]
theorem
finset.sum_ite_eq'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
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}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
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.
@[simp]
theorem
finset.prod_pi_mul_single'
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(a : α)
(x : β)
(s : finset α) :
s.prod (λ (a' : α), pi.mul_single a x a') = ite (a ∈ s) x 1
@[simp]
theorem
finset.sum_pi_single'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(a : α)
(x : β)
(s : finset α) :
@[simp]
theorem
finset.sum_pi_single
{α : Type v}
{β : α → Type u_1}
[decidable_eq α]
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(f : Π (a : α), β a)
(s : finset α) :
@[simp]
theorem
finset.prod_pi_mul_single
{α : Type v}
{β : α → Type u_1}
[decidable_eq α]
[Π (a : α), comm_monoid (β a)]
(a : α)
(f : Π (a : α), β a)
(s : finset α) :
s.prod (λ (a' : α), pi.mul_single a' (f a') a) = ite (a ∈ s) (f a) 1
theorem
finset.prod_bij_ne_one
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{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₁ : a ∈ s) (h₂ : f a ≠ 1), b = i a h₁ h₂))
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) :
theorem
finset.sum_bij_ne_zero
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{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₁ : a ∈ s) (h₂ : f a ≠ 0), b = i a h₁ h₂))
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) :
theorem
finset.sum_dite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.prod_dite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.nonempty_of_sum_ne_zero
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(h : s.sum (λ (x : α), f x) ≠ 0) :
s.nonempty
theorem
finset.nonempty_of_prod_ne_one
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(h : s.prod (λ (x : α), f x) ≠ 1) :
s.nonempty
theorem
finset.prod_range_succ_comm
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).prod (λ (x : ℕ), f x) = f n * (finset.range n).prod (λ (x : ℕ), f x)
theorem
finset.sum_range_succ_comm
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).sum (λ (x : ℕ), f x) = f n + (finset.range n).sum (λ (x : ℕ), f x)
theorem
finset.prod_range_succ
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).prod (λ (x : ℕ), f x) = (finset.range n).prod (λ (x : ℕ), f x) * f n
theorem
finset.sum_range_succ
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).sum (λ (x : ℕ), f x) = (finset.range n).sum (λ (x : ℕ), f x) + f n
theorem
finset.prod_range_succ'
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).prod (λ (k : ℕ), f k) = (finset.range n).prod (λ (k : ℕ), f (k + 1)) * f 0
theorem
finset.sum_range_succ'
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).sum (λ (k : ℕ), f k) = (finset.range n).sum (λ (k : ℕ), f (k + 1)) + f 0
theorem
finset.prod_range_add
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n m : ℕ) :
(finset.range (n + m)).prod (λ (x : ℕ), f x) = (finset.range n).prod (λ (x : ℕ), f x) * (finset.range m).prod (λ (x : ℕ), f (n + x))
theorem
finset.sum_range_add
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n m : ℕ) :
(finset.range (n + m)).sum (λ (x : ℕ), f x) = (finset.range n).sum (λ (x : ℕ), f x) + (finset.range m).sum (λ (x : ℕ), f (n + x))
theorem
finset.sum_range_add_sub_sum_range
{α : Type u_1}
[add_comm_group α]
(f : ℕ → α)
(n m : ℕ) :
(finset.range (n + m)).sum (λ (k : ℕ), f k) - (finset.range n).sum (λ (k : ℕ), f k) = (finset.range m).sum (λ (k : ℕ), f (n + k))
theorem
finset.prod_range_add_div_prod_range
{α : Type u_1}
[comm_group α]
(f : ℕ → α)
(n m : ℕ) :
(finset.range (n + m)).prod (λ (k : ℕ), f k) / (finset.range n).prod (λ (k : ℕ), f k) = (finset.range m).prod (λ (k : ℕ), f (n + k))
theorem
finset.sum_range_zero
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β) :
(finset.range 0).sum (λ (k : ℕ), f k) = 0
theorem
finset.prod_range_zero
{β : Type u}
[comm_monoid β]
(f : ℕ → β) :
(finset.range 0).prod (λ (k : ℕ), f k) = 1
theorem
finset.sum_range_one
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β) :
(finset.range 1).sum (λ (k : ℕ), f k) = f 0
theorem
finset.prod_range_one
{β : Type u}
[comm_monoid β]
(f : ℕ → β) :
(finset.range 1).prod (λ (k : ℕ), f k) = f 0
theorem
finset.sum_list_map_count
{α : Type v}
[decidable_eq α]
(l : list α)
{M : Type u_1}
[add_comm_monoid M]
(f : α → M) :
theorem
finset.prod_list_map_count
{α : Type v}
[decidable_eq α]
(l : list α)
{M : Type u_1}
[comm_monoid M]
(f : α → M) :
theorem
finset.prod_list_count_of_subset
{α : Type v}
[decidable_eq α]
[comm_monoid α]
(m : list α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.prod = s.prod (λ (i : α), i ^ list.count i m)
theorem
finset.sum_list_count_of_subset
{α : Type v}
[decidable_eq α]
[add_comm_monoid α]
(m : list α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.sum = s.sum (λ (i : α), list.count i m • i)
theorem
finset.sum_filter_count_eq_countp
{α : Type v}
[decidable_eq α]
(p : α → Prop)
[decidable_pred p]
(l : list α) :
(finset.filter p l.to_finset).sum (λ (x : α), list.count x l) = list.countp p l
theorem
finset.prod_multiset_map_count
{α : Type v}
[decidable_eq α]
(s : multiset α)
{M : Type u_1}
[comm_monoid M]
(f : α → M) :
(multiset.map f s).prod = s.to_finset.prod (λ (m : α), f m ^ multiset.count m s)
theorem
finset.sum_multiset_map_count
{α : Type v}
[decidable_eq α]
(s : multiset α)
{M : Type u_1}
[add_comm_monoid M]
(f : α → M) :
(multiset.map f s).sum = s.to_finset.sum (λ (m : α), multiset.count m s • f m)
theorem
finset.sum_multiset_count
{α : Type v}
[decidable_eq α]
[add_comm_monoid α]
(s : multiset α) :
theorem
finset.prod_multiset_count_of_subset
{α : Type v}
[decidable_eq α]
[comm_monoid α]
(m : multiset α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.prod = s.prod (λ (i : α), i ^ multiset.count i m)
theorem
finset.sum_multiset_count_of_subset
{α : Type v}
[decidable_eq α]
[add_comm_monoid α]
(m : multiset α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.sum = s.sum (λ (i : α), multiset.count i m • i)
theorem
finset.sum_mem_multiset
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(m : multiset α)
(f : {x // x ∈ m} → β)
(g : α → β)
(hfg : ∀ (x : {x // x ∈ m}), f x = g ↑x) :
theorem
finset.prod_mem_multiset
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(m : multiset α)
(f : {x // x ∈ m} → β)
(g : α → β)
(hfg : ∀ (x : {x // x ∈ m}), f x = g ↑x) :
theorem
finset.prod_induction
{α : Type v}
{s : finset α}
{M : Type u_1}
[comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
(p_one : p 1)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (s.prod (λ (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
{α : Type v}
{s : finset α}
{M : Type u_1}
[add_comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
(p_one : p 0)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (s.sum (λ (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.sum_induction_nonempty
{α : Type v}
{s : finset α}
{M : Type u_1}
[add_comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
(hs_nonempty : s.nonempty)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (s.sum (λ (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_1}
[comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
(hs_nonempty : s.nonempty)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (s.prod (λ (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.prod_range_induction
{β : Type u}
[comm_monoid β]
(f s : ℕ → β)
(h0 : s 0 = 1)
(h : ∀ (n : ℕ), s (n + 1) = s n * f n)
(n : ℕ) :
(finset.range n).prod (λ (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_induction
{β : Type u}
[add_comm_monoid β]
(f s : ℕ → β)
(h0 : s 0 = 0)
(h : ∀ (n : ℕ), s (n + 1) = s n + f n)
(n : ℕ) :
(finset.range n).sum (λ (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.
A telescoping sum along {0, ..., n - 1} of an additive commutative group valued
function reduces to the difference of the last and first terms.
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_tsub
{α : Type v}
[canonically_ordered_add_monoid α]
[has_sub α]
[has_ordered_sub α]
[contravariant_class α α has_add.add has_le.le]
{f : ℕ → α}
(h : monotone f)
(n : ℕ) :
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]
@[simp]
theorem
finset.nsmul_eq_sum_const
{β : Type u}
[add_comm_monoid β]
(b : β)
(n : ℕ) :
n • b = (finset.range n).sum (λ (k : ℕ), b)
theorem
finset.pow_eq_prod_const
{β : Type u}
[comm_monoid β]
(b : β)
(n : ℕ) :
b ^ n = (finset.range n).prod (λ (k : ℕ), b)
theorem
finset.prod_flip
{β : Type u}
[comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range (n + 1)).prod (λ (r : ℕ), f (n - r)) = (finset.range (n + 1)).prod (λ (k : ℕ), f k)
theorem
finset.sum_flip
{β : Type u}
[add_comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range (n + 1)).sum (λ (r : ℕ), f (n - r)) = (finset.range (n + 1)).sum (λ (k : ℕ), f k)
theorem
finset.prod_involution
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{f : α → β}
(g : Π (a : α), a ∈ s → α)
(h : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1)
(g_ne : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(g_inv : ∀ (a : α) (ha : a ∈ s), g (g a ha) _ = a) :
theorem
finset.sum_involution
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
(g : Π (a : α), a ∈ s → α)
(h : ∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0)
(g_ne : ∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(g_inv : ∀ (a : α) (ha : a ∈ s), g (g a ha) _ = a) :
theorem
finset.prod_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[comm_monoid β]
[decidable_eq γ]
(f : γ → β)
(g : α → γ) :
s.prod (λ (a : α), f (g a)) = (finset.image g s).prod (λ (b : γ), f b ^ (finset.filter (λ (a : α), g a = b) s).card)
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_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[add_comm_monoid β]
[decidable_eq γ]
(f : γ → β)
(g : α → γ) :
s.sum (λ (a : α), f (g a)) = (finset.image g s).sum (λ (b : γ), (finset.filter (λ (a : α), g a = b) s).card • 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_inter_mul_prod_diff
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
theorem
finset.sum_inter_add_sum_diff
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
theorem
finset.prod_eq_mul_prod_diff_singleton
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β) :