mathlib documentation

algebra.​big_operators.​ring

algebra.​big_operators.​ring

Results about big operators with values in a (semi)ring

We prove results about big operators that involve some interaction between multiplicative and additive structures on the values being combined.

theorem finset.​sum_mul {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β} [semiring β] :
s.sum (λ (x : α), f x) * b = s.sum (λ (x : α), f x * b)

theorem finset.​mul_sum {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β} [semiring β] :
b * s.sum (λ (x : α), f x) = s.sum (λ (x : α), b * f x)

theorem finset.​sum_mul_boole {α : Type u} {β : Type v} [semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
s.sum (λ (x : α), f x * ite (a = x) 1 0) = ite (a s) (f a) 0

theorem finset.​sum_boole_mul {α : Type u} {β : Type v} [semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
s.sum (λ (x : α), ite (a = x) 1 0 * f x) = ite (a s) (f a) 0

theorem finset.​sum_div {α : Type u} {β : Type v} [division_ring β] {s : finset α} {f : α → β} {b : β} :
s.sum (λ (x : α), f x) / b = s.sum (λ (x : α), f x / b)

theorem finset.​prod_sum {α : Type u} {β : Type v} [comm_semiring β] {δ : α → Type u_1} [decidable_eq α] [Π (a : α), decidable_eq (δ a)] {s : finset α} {t : Π (a : α), finset (δ a)} {f : Π (a : α), δ a → β} :
s.prod (λ (a : α), (t a).sum (λ (b : δ a), f a b)) = (s.pi t).sum (λ (p : Π (a : α), a sδ a), s.attach.prod (λ (x : {x // x s}), f x.val (p x.val _)))

The product over a sum can be written as a sum over the product of sets, finset.pi. finset.prod_univ_sum is an alternative statement when the product is over univ.

theorem finset.​sum_mul_sum {β : Type v} [comm_semiring β] {ι₁ : Type u_1} {ι₂ : Type u_2} (s₁ : finset ι₁) (s₂ : finset ι₂) (f₁ : ι₁ → β) (f₂ : ι₂ → β) :
s₁.sum (λ (x₁ : ι₁), f₁ x₁) * s₂.sum (λ (x₂ : ι₂), f₂ x₂) = (s₁.product s₂).sum (λ (p : ι₁ × ι₂), f₁ p.fst * f₂ p.snd)

theorem finset.​prod_add {α : Type u} {β : Type v} [comm_semiring β] (f g : α → β) (s : finset α) :
s.prod (λ (a : α), f a + g a) = s.powerset.sum (λ (t : finset α), t.prod (λ (a : α), f a) * (s \ t).prod (λ (a : α), g a))

The product of f a + g a over all of s is the sum over the powerset of s of the product of f over a subset t times the product of g over the complement of t

theorem finset.​sum_pow_mul_eq_add_pow {α : Type u_1} {R : Type u_2} [comm_semiring R] (a b : R) (s : finset α) :
s.powerset.sum (λ (t : finset α), a ^ t.card * b ^ (s.card - t.card)) = (a + b) ^ s.card

Summing a^s.card * b^(n-s.card) over all finite subsets s of a finset gives (a + b)^s.card.

theorem finset.​prod_pow_eq_pow_sum {α : Type u} {β : Type v} [comm_semiring β] {x : β} {f : α → } {s : finset α} :
s.prod (λ (i : α), x ^ f i) = x ^ s.sum (λ (x : α), f x)

theorem finset.​dvd_sum {α : Type u} {β : Type v} [comm_semiring β] {b : β} {s : finset α} {f : α → β} :
(∀ (x : α), x sb f x)b s.sum (λ (x : α), f x)

theorem finset.​prod_nat_cast {α : Type u} {β : Type v} [comm_semiring β] (s : finset α) (f : α → ) :
(s.prod (λ (x : α), f x)) = s.prod (λ (x : α), (f x))

theorem finset.​sum_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] [add_comm_monoid β] {s : finset α} {x : α} (h : x s) (f : finset α → β) :
(has_insert.insert x s).powerset.sum (λ (a : finset α), f a) = s.powerset.sum (λ (a : finset α), f a) + s.powerset.sum (λ (t : finset α), f (has_insert.insert x t))

theorem finset.​prod_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x s) (f : finset α → β) :
(has_insert.insert x s).powerset.prod (λ (a : finset α), f a) = s.powerset.prod (λ (a : finset α), f a) * s.powerset.prod (λ (t : finset α), f (has_insert.insert x t))

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.