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.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 : is, 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