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.prod_pow_eq_pow_sum {α : Type u} {β : Type v} [CommMonoid β] {x : β} {f : α → ℕ} {s : Finset α} : (Finset.prod s fun i => x ^ f i) = x ^ Finset.sum s fun x => f x

theorem Finset.sum_mul {α : Type u} {β : Type v} {s : Finset α} {b : β} {f : α → β} [NonUnitalNonAssocSemiring β] : (Finset.sum s fun x => f x) * b = Finset.sum s fun x => f x * b

theorem Finset.mul_sum {α : Type u} {β : Type v} {s : Finset α} {b : β} {f : α → β} [NonUnitalNonAssocSemiring β] : (b * Finset.sum s fun x => f x) = Finset.sum s fun x => b * f x

theorem Finset.sum_mul_sum {β : Type v} [NonUnitalNonAssocSemiring β] {ι₁ : Type u_1} {ι₂ : Type u_2} (s₁ : Finset ι₁) (s₂ : Finset ι₂) (f₁ : ι₁ → β) (f₂ : ι₂ → β) : ((Finset.sum s₁ fun x₁ => f₁ x₁) * Finset.sum s₂ fun x₂ => f₂ x₂) = Finset.sum (s₁ ×ˢ s₂) fun p => f₁ p.fst * f₂ p.snd

theorem Finset.dvd_sum {α : Type u} {β : Type v} [NonUnitalSemiring β] {b : β} {s : Finset α} {f : α → β} (h : ∀ (x : α), x ∈ s → b ∣ f x) : b ∣ Finset.sum s fun x => f x

theorem Finset.sum_mul_boole {α : Type u} {β : Type v} [NonAssocSemiring β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (Finset.sum s fun x => f x * if a = x then 1 else 0) = if a ∈ s then f a else 0

theorem Finset.sum_boole_mul {α : Type u} {β : Type v} [NonAssocSemiring β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (Finset.sum s fun x => (if a = x then 1 else 0) * f x) = if a ∈ s then f a else 0

theorem Finset.sum_div {α : Type u} {β : Type v} [DivisionSemiring β] {s : Finset α} {f : α → β} {b : β} : (Finset.sum s fun x => f x) / b = Finset.sum s fun x => f x / b

theorem Finset.prod_sum {α : Type u} {β : Type v} [CommSemiring β] {δ : α → Type u_1} [DecidableEq α] [(a : α) → DecidableEq (δ a)] {s : Finset α} {t : (a : α) → Finset (δ a)} {f : (a : α) → δ a → β} : (Finset.prod s fun a => Finset.sum (t a) fun b => f a b) = Finset.sum (Finset.pi s t) fun p => Finset.prod (Finset.attach s) fun x => f (↑x) (p ↑x (_ : ↑x ∈ s))

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} [CommSemiring β] [DecidableEq α] (f : α → β) (g : α → β) (s : Finset α) : (Finset.prod s fun a => f a + g a) = Finset.sum (Finset.powerset s) fun t => (Finset.prod t fun a => f a) * Finset.prod (s \ t) fun 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.prod_add_ordered {ι : Type u_1} {R : Type u_2} [CommSemiring R] [LinearOrder ι] (s : Finset ι) (f : ι → R) (g : ι → R) : (Finset.prod s fun i => f i + g i) = (Finset.prod s fun i => f i) + Finset.sum s fun i => (g i * Finset.prod (Finset.filter (fun x => x < i) s) fun j => f j + g j) * Finset.prod (Finset.filter (fun j => i < j) s) fun j => 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} [CommRing R] [LinearOrder ι] (s : Finset ι) (f : ι → R) (g : ι → R) : (Finset.prod s fun i => f i - g i) = (Finset.prod s fun i => f i) - Finset.sum s fun i => (g i * Finset.prod (Finset.filter (fun x => x < i) s) fun j => f j - g j) * Finset.prod (Finset.filter (fun j => i < j) s) fun j => 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} [CommRing R] [LinearOrder ι] (s : Finset ι) (f : ι → R) : (Finset.prod s fun i => 1 - f i) = 1 - Finset.sum s fun i => f i * Finset.prod (Finset.filter (fun x => x < i) s) fun 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.

theorem Finset.sum_pow_mul_eq_add_pow {α : Type u_1} {R : Type u_2} [CommSemiring R] (a : R) (b : R) (s : Finset α) : (Finset.sum (Finset.powerset s) fun t => a ^ Finset.card t * b ^ (Finset.card s - Finset.card t)) = (a + b) ^ Finset.card s

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

theorem Finset.prod_natCast {α : Type u} {β : Type v} [CommSemiring β] (s : Finset α) (f : α → ℕ) : ↑(Finset.prod s fun x => f x) = Finset.prod s fun x => ↑(f x)

theorem Finset.prod_range_cast_nat_sub {R : Type u_1} [CommRing R] (n : ℕ) (k : ℕ) : (Finset.prod (Finset.range k) fun i => ↑n - ↑i) = ↑(Finset.prod (Finset.range k) fun i => n - i)

theorem Finset.sum_powerset_insert {α : Type u} {β : Type v} [DecidableEq α] [AddCommMonoid β] {s : Finset α} {x : α} (h : ¬x ∈ s) (f : Finset α → β) : (Finset.sum (Finset.powerset (insert x s)) fun a => f a) = (Finset.sum (Finset.powerset s) fun a => f a) + Finset.sum (Finset.powerset s) fun t => f (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.

theorem Finset.prod_powerset_insert {α : Type u} {β : Type v} [DecidableEq α] [CommMonoid β] {s : Finset α} {x : α} (h : ¬x ∈ s) (f : Finset α → β) : (Finset.prod (Finset.powerset (insert x s)) fun a => f a) = (Finset.prod (Finset.powerset s) fun a => f a) * Finset.prod (Finset.powerset s) fun t => 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} [AddCommMonoid β] (s : Finset α) (f : Finset α → β) : (Finset.sum (Finset.powerset s) fun t => f t) = Finset.sum (Finset.range (Finset.card s + 1)) fun j => Finset.sum (Finset.powersetLen j s) fun t => 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

theorem Finset.prod_powerset {α : Type u} {β : Type v} [CommMonoid β] (s : Finset α) (f : Finset α → β) : (Finset.prod (Finset.powerset s) fun t => f t) = Finset.prod (Finset.range (Finset.card s + 1)) fun j => Finset.prod (Finset.powersetLen j s) fun t => 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.

theorem Finset.sum_range_succ_mul_sum_range_succ {β : Type v} [NonUnitalNonAssocSemiring β] (n : ℕ) (k : ℕ) (f : ℕ → β) (g : ℕ → β) : ((Finset.sum (Finset.range (n + 1)) fun i => f i) * Finset.sum (Finset.range (k + 1)) fun i => g i) = (((Finset.sum (Finset.range n) fun i => f i) * Finset.sum (Finset.range k) fun i => g i) + f n * Finset.sum (Finset.range k) fun i => g i) + (Finset.sum (Finset.range n) fun i => f i) * g k + f n * g k