algebra.big_operators.ring

source

theorem finset.prod_pow_eq_pow_sum {α : Type u} {β : Type v} [comm_monoid β] {x : β} {f : α → ℕ} {s : finset α} :

s.prod (λ (i : α), x ^ f i) = x ^ s.sum (λ (x : α), f x)

source

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

s.sum (λ (x : α), f x) * b = s.sum (λ (x : α), f x * b)

source

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

b * s.sum (λ (x : α), f x) = s.sum (λ (x : α), b * f x)

source

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

s₁.sum (λ (x₁ : ι₁), f₁ x₁) * s₂.sum (λ (x₂ : ι₂), f₂ x₂) = (s₁ ×ˢ s₂).sum (λ (p : ι₁ × ι₂), f₁ p.fst * f₂ p.snd)

source

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

s.sum (λ (x : α), f x * ite (a = x) 1 0) = ite (a ∈ s) (f a) 0

source

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

s.sum (λ (x : α), ite (a = x) 1 0 * f x) = ite (a ∈ s) (f a) 0

source

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

s.sum (λ (x : α), f x) / b = s.sum (λ (x : α), f x / b)

source

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.

source

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

source

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

s.prod (λ (i : ι), f i + g i) = s.prod (λ (i : ι), f i) + s.sum (λ (i : ι), g i * (finset.filter (λ (_x : ι), _x < i) s).prod (λ (j : ι), f j + g j) * (finset.filter (λ (j : ι), i < j) s).prod (λ (j : ι), f j))

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

source

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

s.prod (λ (i : ι), f i - g i) = s.prod (λ (i : ι), f i) - s.sum (λ (i : ι), g i * (finset.filter (λ (_x : ι), _x < i) s).prod (λ (j : ι), f j - g j) * (finset.filter (λ (j : ι), i < j) s).prod (λ (j : ι), f j))

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

source

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

s.prod (λ (i : ι), 1 - f i) = 1 - s.sum (λ (i : ι), f i * (finset.filter (λ (_x : ι), _x < i) s).prod (λ (j : ι), 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.

source

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.

source

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

b ∣ s.sum (λ (x : α), f x)

source

@[norm_cast]

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

↑(s.prod (λ (x : α), f x)) = s.prod (λ (x : α), ↑(f x))

source

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

(finset.range k).prod (λ (i : ℕ), ↑n - ↑i) = ↑((finset.range k).prod (λ (i : ℕ), n - i))

source

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))

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

source

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.

source

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

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

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

source

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

s.powerset.prod (λ (t : finset α), f t) = (finset.range (s.card + 1)).prod (λ (j : ℕ), (finset.powerset_len j s).prod (λ (t : finset α), 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.

source

theorem finset.sum_range_succ_mul_sum_range_succ {β : Type v} [non_unital_non_assoc_semiring β] (n k : ℕ) (f g : ℕ → β) :

(finset.range (n + 1)).sum (λ (i : ℕ), f i) * (finset.range (k + 1)).sum (λ (i : ℕ), g i) = (finset.range n).sum (λ (i : ℕ), f i) * (finset.range k).sum (λ (i : ℕ), g i) + f n * (finset.range k).sum (λ (i : ℕ), g i) + (finset.range n).sum (λ (i : ℕ), f i) * g k + f n * g k

mathlib3 documentation

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