The mean of a finite family of vectors

The mean m = (card ι)⁻¹ • ∑ i, z i of a finite family z : ι → E in a vector space over a field R is its center of mass with equal weights, Finset.univ.centerMass (fun _ ↦ 1) z. Through total inversion, the mean of the empty family is 0. For a nonempty family this is the affine Finset.centroid, which has no canonical value on the empty family. Mathlib's average Finset.expect needs a ℚ≥0-module structure, which a vector space over a general field, such as an inner product space over ℝ or ℂ, does not carry as an instance.

Over a field of characteristic zero, this file records the identities of descriptive statistics used for sample means and scatter operators: the sum of a family is its size times its mean, the deviations zᵢ - m sum to zero, subtracting a constant c from a nonempty family subtracts it from the mean, and appending a point y to a family of n points moves the mean by (n + 1)⁻¹ (y - m), including for n = 0.

Main declarations

• TauCeti.finiteMean: the mean of a finite family.
• TauCeti.finiteMean_of_isEmpty: the mean of the empty family is 0.
• TauCeti.sum_eq_card_smul_finiteMean: ∑ i, z i = card ι • m.
• TauCeti.sum_sub_finiteMean: ∑ i, (z i - m) = 0.
• TauCeti.finiteMean_sub_const: the mean of the deviations zᵢ - c is m - c.
• TauCeti.finiteMean_snoc: the mean after appending a point.

noncomputable def TauCeti.finiteMean (R : Type u_1) {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] (z : ι → E) : E

The mean (card ι)⁻¹ • ∑ i, z i of a finite family z of vectors: its center of mass with equal weights. The mean of the empty family is 0.

theorem TauCeti.finiteMean_def {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] (z : ι → E) : finiteMean R z = Finset.univ.centerMass (fun (x : ι) => 1) z

theorem TauCeti.finiteMean_eq_inv_smul_sum {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] (z : ι → E) : finiteMean R z = (↑(Fintype.card ι))⁻¹ • ∑ i : ι, z i

@[simp]

theorem TauCeti.finiteMean_of_isEmpty {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] [IsEmpty ι] (z : ι → E) : finiteMean R z = 0

The mean of the empty family is 0.

theorem TauCeti.sum_eq_card_smul_finiteMean {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] [CharZero R] (z : ι → E) : ∑ i : ι, z i = ↑(Fintype.card ι) • finiteMean R z

The sum of a finite family is its size times its mean.

theorem TauCeti.sum_sub_finiteMean {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] [CharZero R] (z : ι → E) : ∑ i : ι, (z i - finiteMean R z) = 0

The deviations of a finite family from its mean sum to zero.

theorem TauCeti.finiteMean_sub_const {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Field R] [AddCommGroup E] [Module R E] [Fintype ι] [CharZero R] [Nonempty ι] (z : ι → E) (c : E) : (finiteMean R fun (i : ι) => z i - c) = finiteMean R z - c

Subtracting a constant from every member of a nonempty family subtracts it from the mean.

theorem TauCeti.finiteMean_snoc {R : Type u_1} {E : Type u_2} [Field R] [AddCommGroup E] [Module R E] [CharZero R] {n : ℕ} (z : Fin n → E) (y : E) : finiteMean R (Fin.snoc z y) = finiteMean R z + (↑n + 1)⁻¹ • (y - finiteMean R z)

Appending a point. Appending y to a family z of n points with mean m moves the mean by (n + 1)⁻¹ • (y - m). For n = 0 this says that the mean of the single point y is y.