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.natCast_card_filter {ι : Type u_1} {α : Type u_2} [AddCommMonoidWithOne α] (p : ι → Prop) [DecidablePred p] (s : Finset ι) : ↑(Finset.filter p s).card = Finset.sum s fun (a : ι) => if p a then 1 else 0

@[simp]

theorem Finset.sum_boole {ι : Type u_1} {α : Type u_2} [AddCommMonoidWithOne α] (p : ι → Prop) [DecidablePred p] (s : Finset ι) : (Finset.sum s fun (x : ι) => if p x then 1 else 0) = ↑(Finset.filter p s).card

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_6} (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 Commute.sum_right {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute b (f i)) : Commute b (Finset.sum s fun (i : ι) => f i)

theorem Commute.sum_left {ι : Type u_1} {α : Type u_2} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute (f i) b) : Commute (Finset.sum s fun (i : ι) => f i) b

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_add_prod_eq {ι : Type u_1} {α : Type u_2} [CommSemiring α] {s : Finset ι} {i : ι} {f : ι → α} {g : ι → α} {h : ι → α} (hi : i ∈ s) (h1 : g i + h i = f i) (h2 : ∀ j ∈ s, j ≠ i → g j = f j) (h3 : ∀ j ∈ s, j ≠ i → h j = f j) : ((Finset.prod s fun (i : ι) => g i) + Finset.prod s fun (i : ι) => h i) = Finset.prod s fun (i : ι) => f i

If f = g = h everywhere but at i, where f i = g i + h i, then the product of f over s is the sum of the products of g and h.

theorem Finset.prod_sum {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_5} [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_5} [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_6} [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_6) [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

theorem Fintype.sum_pow {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommSemiring α] (f : ι → α) (n : ℕ) : (Finset.sum Finset.univ fun (a : ι) => f a) ^ n = Finset.sum Finset.univ fun (p : Fin n → ι) => Finset.prod Finset.univ fun (i : Fin n) => f (p i)

theorem Fintype.sum_mul_sum {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommSemiring α] (f : ι → α) (g : κ → α) : ((Finset.sum Finset.univ fun (i : ι) => f i) * Finset.sum Finset.univ fun (j : κ) => g j) = Finset.sum Finset.univ fun (i : ι) => Finset.sum Finset.univ fun (j : κ) => f i * g j

theorem Fintype.prod_add {ι : Type u_6} {α : Type u_8} [DecidableEq ι] [Fintype ι] [CommSemiring α] (f : ι → α) (g : ι → α) : (Finset.prod Finset.univ fun (a : ι) => f a + g a) = Finset.sum Finset.univ fun (t : Finset ι) => (Finset.prod t fun (a : ι) => f a) * Finset.prod tᶜ fun (a : ι) => g a

theorem Nat.sum_div {ι : Type u_6} {s : Finset ι} {f : ι → ℕ} {n : ℕ} (hf : ∀ i ∈ s, n ∣ f i) : (Finset.sum s fun (i : ι) => f i) / n = Finset.sum s fun (i : ι) => f i / n

@[simp]

theorem Nat.cast_list_sum {β : Type u_3} [AddMonoidWithOne β] (s : List ℕ) : ↑(List.sum s) = List.sum (List.map Nat.cast s)

@[simp]

theorem Nat.cast_list_prod {β : Type u_3} [Semiring β] (s : List ℕ) : ↑(List.prod s) = List.prod (List.map Nat.cast s)

@[simp]

theorem Nat.cast_multiset_sum {β : Type u_3} [AddCommMonoidWithOne β] (s : Multiset ℕ) : ↑(Multiset.sum s) = Multiset.sum (Multiset.map Nat.cast s)

@[simp]

theorem Nat.cast_multiset_prod {β : Type u_3} [CommSemiring β] (s : Multiset ℕ) : ↑(Multiset.prod s) = Multiset.prod (Multiset.map Nat.cast s)

@[simp]

theorem Nat.cast_sum {α : Type u_2} {β : Type u_3} [AddCommMonoidWithOne β] (s : Finset α) (f : α → ℕ) : ↑(Finset.sum s fun (x : α) => f x) = Finset.sum s fun (x : α) => ↑(f x)

@[simp]

theorem Nat.cast_prod {α : Type u_2} {β : Type u_3} [CommSemiring β] (f : α → ℕ) (s : Finset α) : ↑(Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => ↑(f i)

@[simp]

theorem Int.cast_list_sum {β : Type u_3} [AddGroupWithOne β] (s : List ℤ) : ↑(List.sum s) = List.sum (List.map Int.cast s)

@[simp]

theorem Int.cast_list_prod {β : Type u_3} [Ring β] (s : List ℤ) : ↑(List.prod s) = List.prod (List.map Int.cast s)

@[simp]

theorem Int.cast_multiset_sum {β : Type u_3} [AddCommGroupWithOne β] (s : Multiset ℤ) : ↑(Multiset.sum s) = Multiset.sum (Multiset.map Int.cast s)

@[simp]

theorem Int.cast_multiset_prod {R : Type u_6} [CommRing R] (s : Multiset ℤ) : ↑(Multiset.prod s) = Multiset.prod (Multiset.map Int.cast s)

@[simp]

theorem Int.cast_sum {α : Type u_2} {β : Type u_3} [AddCommGroupWithOne β] (s : Finset α) (f : α → ℤ) : ↑(Finset.sum s fun (x : α) => f x) = Finset.sum s fun (x : α) => ↑(f x)

@[simp]

theorem Int.cast_prod {α : Type u_2} {R : Type u_6} [CommRing R] (f : α → ℤ) (s : Finset α) : ↑(Finset.prod s fun (i : α) => f i) = Finset.prod s fun (i : α) => ↑(f i)