mathlib documentation

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 : α → β} [non_unital_non_assoc_semiring β] :

(∑ (x : α) in s, f x) * b = ∑ (x : α) in s, (f x) * b

theorem finset.mul_sum {α : Type u} {β : Type v} {s : finset α} {b : β} {f : α → β} [non_unital_non_assoc_semiring β] :

b * ∑ (x : α) in s, f x = ∑ (x : α) in s, b * f x

theorem finset.sum_mul_sum {β : Type v} [non_unital_non_assoc_semiring β] {ι₁ : Type u_1} {ι₂ : Type u_2} (s₁ : finset ι₁) (s₂ : finset ι₂) (f₁ : ι₁ → β) (f₂ : ι₂ → β) :

(∑ (x₁ : ι₁) in s₁, f₁ x₁) * ∑ (x₂ : ι₂) in s₂, f₂ x₂ = ∑ (p : ι₁ × ι₂) in s₁.product s₂, (f₁ p.fst) * f₂ p.snd

theorem finset.sum_mul_boole {α : Type u} {β : Type v} [non_assoc_semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :

∑ (x : α) in s, (f x) * ite (a = x) 1 0 = ite (a ∈ s) (f a) 0

theorem finset.sum_boole_mul {α : Type u} {β : Type v} [non_assoc_semiring β] [decidable_eq α] (s : finset α) (f : α → β) (a : α) :

∑ (x : α) in s, (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 : β} :

(∑ (x : α) in s, f x) / b = ∑ (x : α) in s, 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 → β} :

∏ (a : α) in s, ∑ (b : δ a) in t a, f a b = ∑ (p : Π (a : α), a ∈ s → δ a) in s.pi t, ∏ (x : {x // x ∈ s}) in s.attach, 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.prod_add {α : Type u} {β : Type v} [comm_semiring β] (f g : α → β) (s : finset α) :

∏ (a : α) in s, (f a + g a) = ∑ (t : finset α) in s.powerset, (∏ (a : α) in t, f a) * ∏ (a : α) in s \ t, 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.prod_add_ordered {ι : Type u_1} {R : Type u_2} [comm_semiring R] [linear_order ι] (s : finset ι) (f g : ι → R) :

∏ (i : ι) in s, (f i + g i) = ∏ (i : ι) in s, f i + ∑ (i : ι) in s, ((g i) * ∏ (j : ι) in finset.filter (λ (_x : ι), _x < i) s, (f j + g j)) * ∏ (j : ι) in finset.filter (λ (j : ι), i < j) s, f j

∏ i, (f i + g i) = (∏ i, f i) + ∑ i, g i * (∏ j < i, f j + g j) * (∏ j > i, f j).

theorem finset.prod_sub_ordered {ι : Type u_1} {R : Type u_2} [comm_ring R] [linear_order ι] (s : finset ι) (f g : ι → R) :

∏ (i : ι) in s, (f i - g i) = ∏ (i : ι) in s, f i - ∑ (i : ι) in s, ((g i) * ∏ (j : ι) in finset.filter (λ (_x : ι), _x < i) s, (f j - g j)) * ∏ (j : ι) in finset.filter (λ (j : ι), i < j) s, f j

∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j).

theorem finset.prod_one_sub_ordered {ι : Type u_1} {R : Type u_2} [comm_ring R] [linear_order ι] (s : finset ι) (f : ι → R) :

∏ (i : ι) in s, (1 - f i) = 1 - ∑ (i : ι) in s, (f i) * ∏ (j : ι) in finset.filter (λ (_x : ι), _x < i) s, (1 - f j)

∏ i, (1 - f i) = 1 - ∑ i, f i * (∏ j < i, 1 - f j). This formula is useful in construction of a partition of unity from a collection of “bump” functions.

theorem finset.sum_pow_mul_eq_add_pow {α : Type u_1} {R : Type u_2} [comm_semiring R] (a b : R) (s : finset α) :

∑ (t : finset α) in s.powerset, (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 α} :

∏ (i : α) in s, x ^ f i = x ^ ∑ (x : α) in s, f x

theorem finset.dvd_sum {α : Type u} {β : Type v} [comm_semiring β] {b : β} {s : finset α} {f : α → β} (h : ∀ (x : α), x ∈ s → b ∣ f x) :

b ∣ ∑ (x : α) in s, f x

@[norm_cast]

theorem finset.prod_nat_cast {α : Type u} {β : Type v} [comm_semiring β] (s : finset α) (f : α → ℕ) :

↑∏ (x : α) in s, f x = ∏ (x : α) in s, ↑(f x)

theorem finset.prod_range_cast_nat_sub {R : Type u_1} [comm_ring R] (n k : ℕ) :

∏ (i : ℕ) in finset.range k, (↑n - ↑i) = ↑∏ (i : ℕ) in finset.range k, (n - i)

theorem finset.sum_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] [add_comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) :

∑ (a : finset α) in (insert x s).powerset, f a = ∑ (a : finset α) in s.powerset, f a + ∑ (t : finset α) in s.powerset, f (insert x t)

theorem finset.prod_powerset_insert {α : Type u} {β : Type v} [decidable_eq α] [comm_monoid β] {s : finset α} {x : α} (h : x ∉ s) (f : finset α → β) :

∏ (a : finset α) in (insert x s).powerset, f a = (∏ (a : finset α) in s.powerset, f a) * ∏ (t : finset α) in s.powerset, f (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.

theorem finset.sum_powerset {α : Type u} {β : Type v} [add_comm_monoid β] (s : finset α) (f : finset α → β) :

∑ (t : finset α) in s.powerset, f t = ∑ (j : ℕ) in finset.range (s.card + 1), ∑ (t : finset α) in finset.powerset_len j s, f t

theorem finset.prod_powerset {α : Type u} {β : Type v} [comm_monoid β] (s : finset α) (f : finset α → β) :

∏ (t : finset α) in s.powerset, f t = ∏ (j : ℕ) in finset.range (s.card + 1), ∏ (t : finset α) in finset.powerset_len j s, f t

A product over powerset s is equal to the double product over sets of subsets of s with card s = k, for k = 1, ... , card s.