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_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α) : (Finset.sum s fun (i : ι) => f i) * a = Finset.sum s fun (i : ι) => f i * a

theorem Finset.mul_sum {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α) : (a * Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => a * f i

theorem Finset.sum_mul_sum {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] {κ : Type u_4} (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : ((Finset.sum s fun (i : ι) => f i) * Finset.sum t fun (j : κ) => g j) = Finset.sum s fun (i : ι) => Finset.sum t fun (j : κ) => f i * g j

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

theorem Finset.dvd_sum {ι : Type u_1} {α : Type u_2} {s : Finset ι} {a : α} {f : ι → α} [NonUnitalSemiring α] (h : ∀ i ∈ s, a ∣ f i) : a ∣ Finset.sum s fun (i : ι) => f i

theorem Finset.sum_mul_boole {ι : Type u_1} {α : Type u_2} [NonAssocSemiring α] [DecidableEq ι] (s : Finset ι) (f : ι → α) (i : ι) : (Finset.sum s fun (j : ι) => f j * if i = j then 1 else 0) = if i ∈ s then f i else 0

theorem Finset.sum_boole_mul {ι : Type u_1} {α : Type u_2} [NonAssocSemiring α] [DecidableEq ι] (s : Finset ι) (f : ι → α) (i : ι) : (Finset.sum s fun (j : ι) => (if i = j then 1 else 0) * f i) = if i ∈ s then f i else 0

theorem Finset.prod_sum {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [CommSemiring α] [DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (Finset.prod s fun (a : ι) => Finset.sum (t a) fun (b : κ a) => f a b) = Finset.sum (Finset.pi s t) fun (p : (a : ι) → a ∈ s → κ a) => Finset.prod (Finset.attach s) fun (x : { x : ι // x ∈ s }) => f (↑x) (p ↑x ⋯)

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_univ_sum {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [CommSemiring α] [DecidableEq ι] [Fintype ι] (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : (Finset.prod Finset.univ fun (i : ι) => Finset.sum (t i) fun (j : κ i) => f i j) = Finset.sum (Fintype.piFinset t) fun (x : (a : ι) → κ a) => Finset.prod Finset.univ fun (i : ι) => f i (x i)

The product over univ of a sum can be written as a sum over the product of sets, Fintype.piFinset. Finset.prod_sum is an alternative statement when the product is not over univ.

theorem Finset.sum_prod_piFinset {ι : Type u_1} {α : Type u_2} [CommSemiring α] [DecidableEq ι] {κ : Type u_4} [Fintype ι] (s : Finset κ) (g : ι → κ → α) : (Finset.sum (Fintype.piFinset fun (x : ι) => s) fun (f : ι → κ) => Finset.prod Finset.univ fun (i : ι) => g i (f i)) = Finset.prod Finset.univ fun (i : ι) => Finset.sum s fun (j : κ) => g i j

theorem Finset.sum_pow' {ι : Type u_1} {α : Type u_2} [CommSemiring α] (s : Finset ι) (f : ι → α) (n : ℕ) : (Finset.sum s fun (a : ι) => f a) ^ n = Finset.sum (Fintype.piFinset fun (_i : Fin n) => s) fun (p : Fin n → ι) => Finset.prod Finset.univ fun (i : Fin n) => f (p i)

theorem Finset.prod_add {ι : Type u_1} {α : Type u_2} [CommSemiring α] [DecidableEq ι] (f : ι → α) (g : ι → α) (s : Finset ι) : (Finset.prod s fun (i : ι) => f i + g i) = Finset.sum (Finset.powerset s) fun (t : Finset ι) => (Finset.prod t fun (i : ι) => f i) * Finset.prod (s \ t) fun (i : ι) => g i

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} {α : Type u_2} [LinearOrder ι] [CommSemiring α] (s : Finset ι) (f : ι → α) (g : ι → α) : (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.sum_pow_mul_eq_add_pow {ι : Type u_1} {α : Type u_2} [CommSemiring α] (a : α) (b : α) (s : Finset ι) : (Finset.sum (Finset.powerset s) fun (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 Fintype.sum_pow_mul_eq_add_pow {α : Type u_2} [CommSemiring α] (ι : Type u_4) [Fintype ι] (a : α) (b : α) : (Finset.sum Finset.univ fun (s : Finset ι) => a ^ s.card * b ^ (Fintype.card ι - s.card)) = (a + b) ^ Fintype.card ι

Summing a^s.card * b^(n-s.card) over all finite subsets s of a fintype of cardinality n gives (a + b)^n. The "good" proof involves expanding along all coordinates using the fact that x^n is multilinear, but multilinear maps are only available now over rings, so we give instead a proof reducing to the usual binomial theorem to have a result over semirings.

theorem Finset.prod_natCast {ι : Type u_1} {α : Type u_2} [CommSemiring α] (s : Finset ι) (f : ι → ℕ) : ↑(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ↑(f i)

theorem Finset.prod_sub_ordered {ι : Type u_1} {α : Type u_2} [CommRing α] [LinearOrder ι] (s : Finset ι) (f : ι → α) (g : ι → α) : (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} {α : Type u_2} [CommRing α] [LinearOrder ι] (s : Finset ι) (f : ι → α) : (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.prod_range_cast_nat_sub {α : Type u_2} [CommRing α] (n : ℕ) (k : ℕ) : (Finset.prod (Finset.range k) fun (i : ℕ) => ↑n - ↑i) = ↑(Finset.prod (Finset.range k) fun (i : ℕ) => n - i)

theorem Finset.sum_div {ι : Type u_1} {α : Type u_2} [DivisionSemiring α] (s : Finset ι) (f : ι → α) (a : α) : (Finset.sum s fun (i : ι) => f i) / a = Finset.sum s fun (i : ι) => f i / a