Documentation

Mathlib.Algebra.BigOperators.Ring

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 p s).card = as, 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 ι) :
(∑ xs, if p x then 1 else 0) = (Finset.filter p s).card
theorem Finset.sum_mul {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ια) (a : α) :
(∑ is, f i) * a = is, f i * a
theorem Finset.mul_sum {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ια) (a : α) :
a * is, f i = is, a * f i
theorem Finset.sum_mul_sum {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] {κ : Type u_7} (s : Finset ι) (t : Finset κ) (f : ια) (g : κα) :
(∑ is, f i) * jt, g j = is, jt, 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 : is, Commute b (f i)) :
Commute b (∑ is, f i)
theorem Commute.sum_left {ι : Type u_1} {α : Type u_3} [NonUnitalNonAssocSemiring α] (s : Finset ι) (f : ια) (b : α) (h : is, Commute (f i) b) :
Commute (∑ is, f i) b
theorem Finset.sum_range_succ_mul_sum_range_succ {α : Type u_3} [NonUnitalNonAssocSemiring α] (m : ) (n : ) (f : α) (g : α) :
(∑ iFinset.range (m + 1), f i) * iFinset.range (n + 1), g i = (∑ iFinset.range m, f i) * iFinset.range n, g i + f m * iFinset.range n, g i + (∑ iFinset.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 : is, a f i) :
a is, f i
theorem Finset.sum_mul_boole {ι : Type u_1} {α : Type u_3} [NonAssocSemiring α] [DecidableEq ι] (s : Finset ι) (f : ια) (i : ι) :
(∑ js, 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 : ι) :
js, (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 : js, j ig j = f j) (h3 : js, j ih j = f j) :
is, g i + is, h i = is, 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α) :
as, bt a, f a b = ps.pi t, xs.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 : ι, jt i, f i j = xFintype.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 : ικα) :
fFintype.piFinset fun (x : ι) => s, i : ι, g i (f i) = i : ι, js, g i j
theorem Finset.sum_pow' {ι' : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι') (f : ι'α) (n : ) :
(∑ as, f a) ^ n = pFintype.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 ι) :
is, (f i + g i) = ts.powerset, (∏ it, f i) * is \ 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 : ια) :
is, (f i + g i) = is, f i + is, (g i * jFinset.filter (fun (x : ι) => x < i) s, (f j + g j)) * jFinset.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 ι) :
ts.powerset, 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_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.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_3} [CommSemiring α] (s : Finset ι) (f : ι) :
(∏ is, f i) = is, (f i)
theorem Finset.prod_sub_ordered {ι : Type u_1} {α : Type u_3} [CommRing α] [LinearOrder ι] (s : Finset ι) (f : ια) (g : ια) :
is, (f i - g i) = is, f i - is, (g i * jFinset.filter (fun (x : ι) => x < i) s, (f j - g j)) * jFinset.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 : ια) :
is, (1 - f i) = 1 - is, f i * jFinset.filter (fun (x : ι) => x < 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 : ) :
iFinset.range k, (n - i) = (∏ iFinset.range k, (n - i))
@[deprecated Finset.prod_range_natCast_sub]
theorem Finset.prod_range_cast_nat_sub {α : Type u_3} [CommRing α] (n : ) (k : ) :
iFinset.range k, (n - i) = (∏ iFinset.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 : α) :
(∑ is, f i) / a = is, 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 ι, (∏ at, f a) * at, g a
theorem Nat.sum_div {ι : Type u_7} {s : Finset ι} {f : ι} {n : } (hf : is, n f i) :
(∑ is, f i) / n = is, 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 : α) :
(∑ xs, f x) = xs, (f x)
@[simp]
theorem Nat.cast_prod {α : Type u_3} {β : Type u_4} [CommSemiring β] (f : α) (s : Finset α) :
(∏ is, f i) = is, (f i)
theorem Int.sum_div {ι : Type u_7} {s : Finset ι} {f : ι} {n : } (hf : is, n f i) :
(∑ is, f i) / n = is, 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 : α) :
(∑ xs, f x) = xs, (f x)
@[simp]
theorem Int.cast_prod {α : Type u_3} {R : Type u_8} [CommRing R] (f : α) (s : Finset α) :
(∏ is, f i) = is, (f i)