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_neg {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] [HasDistribNeg M] (f : ι → M) : ∏ x ∈ s, -f x = (-1) ^ s.card * ∏ x ∈ s, f x

theorem Finset.natCast_card_filter {ι : Type u_1} {R : Type u_4} [AddCommMonoidWithOne R] (p : ι → Prop) [DecidablePred p] (s : Finset ι) : ↑{x ∈ s | p x}.card = ∑ a ∈ s, if p a then 1 else 0

@[simp]

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

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

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

theorem Finset.sum_mul_sum {ι : Type u_1} {κ : Type u_2} {R : Type u_4} [NonUnitalNonAssocSemiring R] (s : Finset ι) (t : Finset κ) (f : ι → R) (g : κ → R) : (∑ 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_2} {R : Type u_4} [NonUnitalNonAssocSemiring R] [Fintype ι] [Fintype κ] (f : ι → R) (g : κ → R) : (∑ i : ι, f i) * ∑ j : κ, g j = ∑ i : ι, ∑ j : κ, f i * g j

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

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

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

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

theorem Finset.sum_mul_boole {ι : Type u_1} {R : Type u_4} [NonAssocSemiring R] [DecidableEq ι] (s : Finset ι) (f : ι → R) (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} {R : Type u_4} [NonAssocSemiring R] [DecidableEq ι] (s : Finset ι) (f : ι → R) (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} {R : Type u_4} [CommSemiring R] {s : Finset ι} {i : ι} {f g h : ι → R} (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} {R : Type u_4} [CommSemiring R] [DecidableEq ι] {κ : ι → Type u_5} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R) : ∏ 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} {R : Type u_4} [CommSemiring R] [DecidableEq ι] {κ : ι → Type u_5} [Fintype ι] (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R) : ∏ 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_2} {R : Type u_4} [CommSemiring R] [DecidableEq ι] [Fintype ι] (s : Finset κ) (g : ι → κ → R) : ∑ f ∈ Fintype.piFinset fun (x : ι) => s, ∏ i : ι, g i (f i) = ∏ i : ι, ∑ j ∈ s, g i j

theorem Finset.sum_pow' {κ : Type u_2} {R : Type u_4} [CommSemiring R] (s : Finset κ) (f : κ → R) (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} {R : Type u_4} [CommSemiring R] [DecidableEq ι] (f g : ι → R) (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_one_add {ι : Type u_1} {R : Type u_4} [CommSemiring R] {f : ι → R} (s : Finset ι) : ∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

theorem Finset.prod_add_one {ι : Type u_1} {R : Type u_4} [CommSemiring R] {f : ι → R} (s : Finset ι) : ∏ i ∈ s, (f i + 1) = ∑ t ∈ s.powerset, ∏ i ∈ t, f i

theorem Finset.prod_add_ordered {ι : Type u_1} {R : Type u_4} [CommSemiring R] [LinearOrder ι] (s : Finset ι) (f g : ι → R) : ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, f i + ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j + g j)) * ∏ j ∈ s with i < 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_add_ordered {ι : Type u_1} {R : Type u_4} [CommSemiring R] [LinearOrder ι] (s : Finset ι) (f : ι → R) : ∏ i ∈ s, (1 + f i) = 1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j)

theorem Finset.sum_pow_mul_eq_add_pow {ι : Type u_1} {R : Type u_4} [CommSemiring R] (a b : R) (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 {R : Type u_4} [CommSemiring R] (ι : Type u_5) [Fintype ι] (a b : R) : ∑ s : Finset ι, a ^ s.card * b ^ (card ι - s.card) = (a + b) ^ 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} {R : Type u_4} [CommSemiring R] (s : Finset ι) (f : ι → ℕ) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

theorem Finset.prod_sub {ι : Type u_1} {R : Type u_4} [CommRing R] [DecidableEq ι] (f g : ι → R) (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} {R : Type u_4} [CommRing R] [LinearOrder ι] (s : Finset ι) (f g : ι → R) : ∏ i ∈ s, (f i - g i) = ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < 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_4} [CommRing R] [LinearOrder ι] (s : Finset ι) (f : ι → R) : ∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (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 {R : Type u_4} [CommRing R] (n k : ℕ) : ∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

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

theorem Fintype.prod_sum {ι : Type u_5} {R : Type u_7} [Fintype ι] [CommSemiring R] [DecidableEq ι] {κ : ι → Type u_8} [(i : ι) → Fintype (κ i)] (f : (i : ι) → κ i → R) : ∏ 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_5} {R : Type u_7} [Fintype ι] [CommSemiring R] [DecidableEq ι] (f g : ι → R) : ∏ a : ι, (f a + g a) = ∑ t : Finset ι, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a

theorem Nat.sum_div {ι : Type u_5} {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 {R : Type u_4} [AddMonoidWithOne R] (s : List ℕ) : ↑s.sum = (List.map Nat.cast s).sum

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Int.sum_div {ι : Type u_5} {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 {R : Type u_4} [AddGroupWithOne R] (s : List ℤ) : ↑s.sum = (List.map Int.cast s).sum

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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