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_3} [AddCommMonoidWithOne α] (p : ι → Prop) [DecidablePred p] (s : Finset ι) : ↑(Finset.filter (fun (x : ι) => p x) s).card = ∑ a ∈ s, if p a then 1 else 0

@[simp]

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

theorem Finset.sum_mul {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α) : (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a

theorem Finset.mul_sum {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (a : α) : a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i

theorem Finset.sum_mul_sum {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] {κ : Type u_7} (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) : (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

theorem Fintype.sum_mul_sum {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] {κ : Type u_7} [Fintype ι] [Fintype κ] (f : ι → α) (g : κ → α) : (∑ i : ι, f i) * ∑ j : κ, g j = ∑ i : ι, ∑ j : κ, f i * g j

theorem Commute.sum_right {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute b (f i)) : Commute b (∑ i ∈ s, f i)

theorem Commute.sum_left {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ι → α) (b : α) (h : ∀ i ∈ s, Commute (f i) b) : Commute (∑ i ∈ s, f i) b

theorem Finset.sum_range_succ_mul_sum_range_succ {α : Type u_3} [NonUnitalNonAssocSemiring α] (m : ℕ) (n : ℕ) (f : ℕ → α) (g : ℕ → α) : (∑ i ∈ Finset.range (m + 1), f i) * ∑ i ∈ Finset.range (n + 1), g i = (∑ i ∈ Finset.range m, f i) * ∑ i ∈ Finset.range n, g i + f m * ∑ i ∈ Finset.range n, g i + (∑ i ∈ Finset.range m, f i) * g n + f m * g n

theorem Finset.dvd_sum {ι : Type u_1} {α : Type u_3} {s : Finset ι} {a : α} {f : ι → α} [NonUnitalSemiring α] (h : ∀ i ∈ s, a ∣ f i) : a ∣ ∑ i ∈ s, f i

theorem Finset.sum_mul_boole {ι : Type u_1} {α : Type u_3} [NonAssocSemiring α] [DecidableEq ι] (s : Finset ι) (f : ι → α) (i : ι) : (∑ j ∈ s, 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_3} [NonAssocSemiring α] [DecidableEq ι] (s : Finset ι) (f : ι → α) (i : ι) : ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0

theorem Finset.prod_add_prod_eq {ι : Type u_1} {α : Type u_3} [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) : ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, 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_3} {κ : ι → Type u_6} [CommSemiring α] [DecidableEq ι] (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, 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_3} {κ : ι → Type u_6} [CommSemiring α] [DecidableEq ι] [Fintype ι] (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → α) : ∏ i : ι, ∑ j ∈ t i, f i j = ∑ x ∈ Fintype.piFinset t, ∏ 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_3} [CommSemiring α] [DecidableEq ι] {κ : Type u_7} [Fintype ι] (s : Finset κ) (g : ι → κ → α) : ∑ f ∈ Fintype.piFinset fun (x : ι) => s, ∏ i : ι, g i (f i) = ∏ i : ι, ∑ j ∈ s, g i j

theorem Finset.sum_pow' {ι' : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι') (f : ι' → α) (n : ℕ) : (∑ a ∈ s, f a) ^ n = ∑ p ∈ Fintype.piFinset fun (_i : Fin n) => s, ∏ i : Fin n, f (p i)

theorem Finset.prod_add {ι : Type u_1} {α : Type u_3} [CommSemiring α] [DecidableEq ι] (f : ι → α) (g : ι → α) (s : Finset ι) : ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, 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_3} [CommSemiring α] [LinearOrder ι] (s : Finset ι) (f : ι → α) (g : ι → α) : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ Finset.filter (fun (j : ι) => j < i) s, (f j + g j)) * ∏ j ∈ Finset.filter (fun (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.sum_pow_mul_eq_add_pow {ι : Type u_1} {α : Type u_3} [CommSemiring α] (a : α) (b : α) (s : Finset ι) : ∑ t ∈ s.powerset, a ^ t.card * b ^ (s.card - t.card) = (a + b) ^ s.card

Summing a ^ #t * b ^ (n - #t) over all finite subsets t of a finset s gives (a + b) ^ #s.

theorem Fintype.sum_pow_mul_eq_add_pow {α : Type u_3} [CommSemiring α] (ι : Type u_7) [Fintype ι] (a : α) (b : α) : ∑ s : Finset ι, a ^ s.card * b ^ (Fintype.card ι - s.card) = (a + b) ^ Fintype.card ι

Summing a^#s * b^(n-#s) 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_3} [CommSemiring α] (s : Finset ι) (f : ι → ℕ) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

theorem Finset.prod_sub {ι : Type u_1} {α : Type u_3} [CommRing α] [DecidableEq ι] (f : ι → α) (g : ι → α) (s : Finset ι) : ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, ((-1) ^ t.card * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

The product of f i - g i over all of s is the sum over the powerset of s of the product of g over a subset t times the product of f over the complement of t times (-1) ^ #t.

theorem Finset.prod_sub_ordered {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder ι] (s : Finset ι) (f : ι → α) (g : ι → α) : ∏ i ∈ s, (f i - g i) = ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ Finset.filter (fun (j : ι) => j < i) s, (f j - g j)) * ∏ j ∈ Finset.filter (fun (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} {α : Type u_3} [CommRing α] [LinearOrder ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ Finset.filter (fun (j : ι) => j < 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.prod_range_natCast_sub {α : Type u_3} [CommRing α] (n : ℕ) (k : ℕ) : ∏ i ∈ Finset.range k, (↑n - ↑i) = ↑(∏ i ∈ Finset.range k, (n - i))

@[deprecated Finset.prod_range_natCast_sub]

theorem Finset.prod_range_cast_nat_sub {α : Type u_3} [CommRing α] (n : ℕ) (k : ℕ) : ∏ i ∈ Finset.range k, (↑n - ↑i) = ↑(∏ i ∈ Finset.range k, (n - i))

Alias of Finset.prod_range_natCast_sub.

theorem Finset.sum_div {ι : Type u_1} {α : Type u_3} [DivisionSemiring α] (s : Finset ι) (f : ι → α) (a : α) : (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

theorem Fintype.sum_pow {ι : Type u_7} {α : Type u_9} [Fintype ι] [CommSemiring α] (f : ι → α) (n : ℕ) : (∑ a : ι, f a) ^ n = ∑ p : Fin n → ι, ∏ i : Fin n, f (p i)

theorem Fintype.prod_sum {ι : Type u_7} {α : Type u_9} [Fintype ι] [CommSemiring α] [DecidableEq ι] {κ : ι → Type u_10} [(i : ι) → Fintype (κ i)] (f : (i : ι) → κ i → α) : ∏ i : ι, ∑ j : κ i, f i j = ∑ x : (i : ι) → κ i, ∏ i : ι, f i (x i)

A product of sums can be written as a sum of products.

theorem Fintype.prod_add {ι : Type u_7} {α : Type u_9} [Fintype ι] [CommSemiring α] [DecidableEq ι] (f : ι → α) (g : ι → α) : ∏ a : ι, (f a + g a) = ∑ t : Finset ι, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.cast_sum {α : Type u_3} {β : Type u_4} [AddCommMonoidWithOne β] (s : Finset α) (f : α → ℕ) : ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)

@[simp]

theorem Nat.cast_prod {α : Type u_3} {β : Type u_4} [CommSemiring β] (f : α → ℕ) (s : Finset α) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

theorem Int.sum_div {ι : Type u_7} {s : Finset ι} {f : ι → ℤ} {n : ℤ} (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Int.cast_sum {α : Type u_3} {β : Type u_4} [AddCommGroupWithOne β] (s : Finset α) (f : α → ℤ) : ↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)

@[simp]

theorem Int.cast_prod {α : Type u_3} {R : Type u_8} [CommRing R] (f : α → ℤ) (s : Finset α) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)