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.

source

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

source

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

source

@[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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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

source

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)

source

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

source

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

source

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

source

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).

source

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)

source

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.

source

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.

source

theorem Finset.prod_natCast {ι : Type u_1} {R : Type u_4} [CommSemiring R] (s : Finset ι) (f : ι → ℕ) :

↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

source

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.

source

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).

source

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.

source

theorem Finset.prod_range_natCast_sub {R : Type u_4} [CommRing R] (n k : ℕ) :

∏ i ∈ range k, (↑n - ↑i) = ↑(∏ i ∈ range k, (n - i))

source

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)

source

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) :