Identities for finite sums in commutative rings

Scaling weighted sums of natural numbers

In a commutative semiring, multiplying a weighted sum ∑ᵢ sᵢ cᵢ of natural numbers cᵢ by a natural number d gives the weighted sum ∑ᵢ sᵢ (cᵢ d) of the products, computed in ℕ. This turns inequalities for counts cᵢ weighted by a dimension d, such as the strong Morse inequalities with coefficients in a d-dimensional space, into inequalities for the sequence cᵢ d of natural numbers.

Replacing the factors of a triple product by constants

TauCeti.sum_sum_sum_mul_sub_eq writes the difference between a triple sum ∑ x, ∑ y, ∑ z, a x y * b x z * c y z and the sum of the constant product of the three constants over all triples, (#s₀ * #s₁ * #s₂) * (p * q * r), as a sum of three one-factor discrepancies.

theorem TauCeti.natCast_mul_sum_mul_natCast {ι : Type u_1} {R : Type u_2} [CommSemiring R] (d : ℕ) (s : ι → R) (c : ι → ℕ) (t : Finset ι) : ↑d * ∑ i ∈ t, s i * ↑(c i) = ∑ i ∈ t, s i * ↑(c i * d)

Scaling a weighted sum of natural numbers cᵢ by a natural number d gives the same weighted sum of the products cᵢ d: d ∑ᵢ sᵢ cᵢ = ∑ᵢ sᵢ (cᵢ d). This turns the strong inequalities for counts cᵢ weighted by the dimension d of a coefficient space into strong inequalities for the sequence cᵢ d.

theorem TauCeti.sum_sum_sum_mul_sub_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : Type u_4} [CommRing R] (a : α → β → R) (b : α → γ → R) (c : β → γ → R) (p q r : R) (s₀ : Finset α) (s₁ : Finset β) (s₂ : Finset γ) : ∑ x ∈ s₀, ∑ y ∈ s₁, ∑ z ∈ s₂, a x y * b x z * c y z - ↑s₀.card * ↑s₁.card * ↑s₂.card * (p * q * r) = ∑ z ∈ s₂, ∑ x ∈ s₀, ∑ y ∈ s₁, b x z * c y z * (a x y - p) + p * ∑ y ∈ s₁, ∑ x ∈ s₀, ∑ z ∈ s₂, c y z * (b x z - q) + p * q * (↑s₀.card * ∑ y ∈ s₁, ∑ z ∈ s₂, (c y z - r))

Replacing the three factors of a triple product by constants one at a time: the difference of ∑ a b c and the triple sum (#s₀ * #s₁ * #s₂) * (p * q * r) of the constant product is a sum of three one-factor discrepancies.