Big operators
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)
∑ x in s, f is the sum of f x as x ranges over the elements
of the finite set s.
∏ 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
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.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
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
add_monoid_hom.map_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β →+ γ)
(f : α → β)
(s : finset α) :
theorem
monoid_hom.map_prod
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β →* γ)
(f : α → β)
(s : finset α) :
theorem
add_equiv.map_sum
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β ≃+ γ)
(f : α → β)
(s : finset α) :
theorem
mul_equiv.map_prod
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β ≃* γ)
(f : α → β)
(s : finset α) :
theorem
ring_hom.map_multiset_prod
{β : Type v}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(f : β →+* γ)
(s : multiset β) :
theorem
ring_hom.map_prod
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
@[simp]
@[simp]
@[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.prod_insert_of_eq_one_if_not_mem
{α : Type u}
{β : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
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_of_eq_zero_if_not_mem
{α : Type u}
{β : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
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.sum_insert_zero
{α : Type u}
{β : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
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 α] :
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.sum_pair
{α : Type u}
{β : Type v}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{a b : α} :
theorem
finset.prod_pair
{α : Type u}
{β : Type v}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{a b : α} :
@[simp]
@[simp]
@[simp]
theorem
finset.sum_image
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α} :
@[simp]
theorem
finset.prod_image
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α} :
@[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.prod_congr
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[comm_monoid β] :
theorem
finset.sum_congr
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[add_comm_monoid β] :
theorem
finset.sum_union_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_union_inter
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
theorem
finset.sum_union
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_union
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
theorem
finset.sum_sdiff
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_sdiff
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
@[simp]
theorem
finset.prod_sum_elim
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[decidable_eq (α ⊕ γ)]
(s : finset α)
(t : finset γ)
(f : α → β)
(g : γ → β) :
@[simp]
theorem
finset.sum_sum_elim
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[decidable_eq (α ⊕ γ)]
(s : finset α)
(t : finset γ)
(f : α → β)
(g : γ → β) :
theorem
finset.prod_bind
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α} :
theorem
finset.sum_bind
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α} :
theorem
finset.prod_image'
{α : Type u}
{β : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α}
(h : γ → β) :
(∀ (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 : γ → β) :
(∀ (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.prod_mul_distrib
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[comm_monoid β] :
theorem
finset.sum_add_distrib
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[add_comm_monoid β] :
theorem
finset.sum_comm
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
theorem
finset.prod_comm
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
theorem
finset.sum_hom
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(s : finset α)
{f : α → β}
(g : β → γ)
[is_add_monoid_hom g] :
theorem
finset.prod_hom
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(s : finset α)
{f : α → β}
(g : β → γ)
[is_monoid_hom g] :
theorem
finset.prod_hom_rel
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : finset α} :
theorem
finset.sum_hom_rel
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : finset α} :
theorem
finset.prod_filter_of_ne
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
{p : α → Prop}
[decidable_pred p] :
theorem
finset.sum_filter_of_ne
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
{p : α → Prop}
[decidable_pred p] :
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_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.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)
theorem
finset.sum_attach
{α : Type u}
{β : Type v}
{s : finset α}
[add_comm_monoid β]
{f : α → β} :
@[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.sum_subtype_of_mem
{α : Type u}
{β : Type v}
{s : finset α}
[add_comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
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 α}
[comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
If all elements of a finset satisfy the predicate p, a product
over s.subtype p equals that product over s.
theorem
finset.prod_subtype_map_embedding
{α : Type u}
{β : Type v}
[comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β} :
(∀ (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_subtype_map_embedding
{α : Type u}
{β : Type v}
[add_comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β} :
(∀ (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.sum_eq_zero
{α : Type u}
{β : Type v}
[add_comm_monoid β]
{f : α → β}
{s : finset α} :
theorem
finset.prod_apply_dite
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(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}
(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.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.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_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.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.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_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.sum_ite_eq
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
@[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.prod_ite_eq'
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
When a product is taken over a conditional whose condition is an equality test on the index
and whose alternative is 1, then the product's value is either the term at that index or 1.
The difference with prod_ite_eq is that the arguments to eq are swapped.
theorem
finset.sum_bij
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset α}
{t : finset γ}
{f : α → β}
{g : γ → β}
(i : Π (a : α), a ∈ s → γ) :
theorem
finset.prod_bij
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{t : finset γ}
{f : α → β}
{g : γ → β}
(i : Π (a : α), a ∈ s → γ) :
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.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) :
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.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) :
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 → γ) :
(∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t) → (∀ (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₂) → (∀ (b : γ), b ∈ t → g b ≠ 0 → (∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), b = i a h₁ h₂)) → (∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) → s.sum (λ (x : α), f x) = t.sum (λ (x : γ), g x)
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 → γ) :
(∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t) → (∀ (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₂) → (∀ (b : γ), b ∈ t → g b ≠ 1 → (∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), b = i a h₁ h₂)) → (∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) → s.prod (λ (x : α), f x) = t.prod (λ (x : γ), g x)
theorem
finset.nonempty_of_prod_ne_one
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β] :
theorem
finset.nonempty_of_sum_ne_zero
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β] :
theorem
finset.exists_ne_zero_of_sum_ne_zero
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β] :
theorem
finset.exists_ne_one_of_prod_ne_one
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β] :
theorem
finset.sum_subset_zero_on_sdiff
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[add_comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_subset_one_on_sdiff
{α : Type u}
{β : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[comm_monoid β]
[decidable_eq α] :
theorem
finset.sum_range_succ
{β : Type u_1}
[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 v}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).prod (λ (x : ℕ), f x) = f n * (finset.range n).prod (λ (x : ℕ), f x)
theorem
finset.prod_range_succ'
{β : Type v}
[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_zero
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β) :
(finset.range 0).sum (λ (k : ℕ), f k) = 0
theorem
finset.prod_range_zero
{β : Type v}
[comm_monoid β]
(f : ℕ → β) :
(finset.range 0).prod (λ (k : ℕ), f k) = 1
theorem
finset.prod_range_one
{β : Type v}
[comm_monoid β]
(f : ℕ → β) :
(finset.range 1).prod (λ (k : ℕ), f k) = f 0
theorem
finset.sum_range_one
{δ : Type u_1}
[add_comm_monoid δ]
(f : ℕ → δ) :
(finset.range 1).sum (λ (k : ℕ), f k) = f 0
theorem
finset.prod_multiset_count
{α : Type u}
[decidable_eq α]
[comm_monoid α]
(s : multiset α) :
theorem
finset.prod_induction
{α : Type u}
{s : finset α}
{M : Type u_1}
[comm_monoid M]
(f : α → M)
(p : M → Prop) :
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 u}
{s : finset α}
{M : Type u_1}
[add_comm_monoid M]
(f : α → M)
(p : M → Prop) :
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
theorem
finset.prod_range_induction
{M : Type u_1}
[comm_monoid M]
(f s : ℕ → M)
(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
{M : Type u_1}
[add_comm_monoid M]
(f s : ℕ → M)
(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.
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.prod_pow
{α : Type u}
{β : Type v}
[comm_monoid β]
(s : finset α)
(n : ℕ)
(f : α → β) :
theorem
finset.prod_flip
{β : Type v}
[comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range (n + 1)).prod (λ (r : ℕ), f (n - r)) = (finset.range (n + 1)).prod (λ (k : ℕ), f k)
theorem
finset.prod_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[comm_monoid β]
[decidable_eq γ]
{s : finset α}
(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
theorem
finset.prod_piecewise
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f g : α → β) :
theorem
finset.sum_piecewise
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f g : α → β) :
theorem
finset.prod_cancels_of_partition_cancels
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r] :
If we can partition a product into subsets that cancel out, then the whole product cancels.
theorem
finset.sum_cancels_of_partition_cancels
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r] :
theorem
finset.prod_update_of_not_mem
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β) :
s.prod (λ (x : α), function.update f i b x) = s.prod (λ (x : α), f x)
theorem
finset.sum_update_of_not_mem
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β) :
s.sum (λ (x : α), function.update f i b x) = s.sum (λ (x : α), f x)
theorem
finset.prod_update_of_mem
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β) :
theorem
finset.eq_of_card_le_one_of_prod_eq
{α : Type u}
{β : Type v}
[comm_monoid β]
{s : finset α}
(hc : s.card ≤ 1)
{f : α → β}
{b : β}
(h : s.prod (λ (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.prod_erase
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
{f : α → β}
{a : α} :
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_erase
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
{f : α → β}
{a : α} :
If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a finset.
theorem
finset.eq_zero_of_sum_eq_zero
{α : Type u}
{β : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
{a : α}
(hp : s.sum (λ (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}
[comm_monoid β]
{s : finset α}
{f : α → β}
{a : α}
(hp : s.prod (λ (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.prod_pow_boole
{α : Type u}
{β : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
(a : α) :
theorem
finset.sum_update_of_mem
{α : Type u}
{β : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β) :
theorem
finset.sum_nsmul
{α : Type u}
{β : Type v}
[add_comm_monoid β]
(s : finset α)
(n : ℕ)
(f : α → β) :
@[simp]
@[simp]
theorem
finset.sum_boole
{α : Type u}
{β : Type v}
{s : finset α}
{p : α → Prop}
[semiring β]
{hp : decidable_pred p} :
theorem
finset.sum_comp
{α : Type u}
{β : Type v}
{γ : Type w}
[add_comm_monoid β]
[decidable_eq γ]
{s : finset α}
(f : γ → β)
(g : α → γ) :
s.sum (λ (a : α), f (g a)) = (finset.image g s).sum (λ (b : γ), (finset.filter (λ (a : α), g a = b) s).card •ℕ f b)
theorem
finset.sum_range_succ'
{β : Type v}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
(finset.range (n + 1)).sum (λ (i : ℕ), f i) = (finset.range n).sum (λ (i : ℕ), f (i + 1)) + f 0
theorem
finset.sum_flip
{β : Type v}
[add_comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
(finset.range (n + 1)).sum (λ (i : ℕ), f (n - i)) = (finset.range (n + 1)).sum (λ (i : ℕ), f i)
@[simp]
theorem
finset.sum_neg_distrib
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[add_comm_group β] :
@[simp]
theorem
finset.prod_inv_distrib
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_group β] :
theorem
finset.card_bind_le
{α : Type u}
{β : Type v}
[decidable_eq β]
{s : finset α}
{t : α → finset β} :
theorem
finset.card_eq_sum_card_image
{α : Type u}
{β : Type v}
[decidable_eq β]
(f : α → β)
(s : finset α) :
s.card = (finset.image f s).sum (λ (a : β), (finset.filter (λ (x : α), f x = a) s).card)
theorem
finset.gsmul_sum
{α : Type u}
{β : Type v}
[add_comm_group β]
{f : α → β}
{s : finset α}
(z : ℤ) :
@[simp]
theorem
finset.sum_sub_distrib
{α : Type u}
{β : Type v}
{s : finset α}
{f g : α → β}
[add_comm_group β] :
theorem
finset.prod_eq_zero
{α : Type u}
{β : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid_with_zero β] :
theorem
finset.prod_eq_zero_iff
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid_with_zero β]
[nontrivial β]
[no_zero_divisors β] :
theorem
finset.prod_ne_zero_iff
{α : Type u}
{β : Type v}
{s : finset α}
{f : α → β}
[comm_monoid_with_zero β]
[nontrivial β]
[no_zero_divisors β] :
@[simp]
theorem
multiset.to_finset_sum_count_eq
{α : Type u}
[decidable_eq α]
(s : multiset α) :
s.to_finset.sum (λ (a : α), multiset.count a s) = s.card