Algebra of finite averages

Over a ring in which the number of terms is invertible, the average ⅟#s • ∑ i ∈ s, f i of a family is the usual normalised sum. Averaging a constant family returns the constant. This is the step that closes averaging arguments (Reynolds operators, Bochner averages, Maschke-type projections) once the averaged terms have been shown to coincide.

The squared deviation from an average also expands into the double sum of centered products. This identity is useful for second-moment calculations without any independence assumptions.

Main results

• Finset.invOf_card_smul_sum_const: ⅟#s • ∑ _i ∈ s, v = v.
• Fintype.invOf_card_smul_sum_const: the same over all of a finite type.
• TauCeti.average_sub_sq_eq_sum_sum: the squared deviation as a double sum.

theorem Finset.invOf_card_smul_sum_const {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Finset ι) [Invertible ↑s.card] (v : M) : ⅟↑s.card • ∑ _i ∈ s, v = v

Averaging a constant over a finset returns it.

theorem Fintype.invOf_card_smul_sum_const {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [Invertible ↑(card ι)] (v : M) : ⅟↑(card ι) • ∑ _i : ι, v = v

Averaging a constant over a finite type returns it.

theorem TauCeti.average_sub_sq_eq_sum_sum {ι : Type u_4} {R : Type u_5} [Field R] [CharZero R] {s : Finset ι} (hs : s.Nonempty) (a : ι → R) (b : R) : ((↑s.card)⁻¹ * ∑ i ∈ s, a i - b) ^ 2 = (↑s.card)⁻¹ ^ 2 * ∑ i ∈ s, ∑ j ∈ s, (a i - b) * (a j - b)

The squared deviation of an average, as a double sum. For a nonempty finite index set s, the square of (#s)⁻¹ * ∑ i ∈ s, a i - b is (#s)⁻¹ ^ 2 times the double sum of (a i - b) * (a j - b) over s × s.