Mean/deviation decomposition

noncomputable def NRR.coordinateMean (n : ℕ) : (Fin n → ℝ) →ₗ[ℝ] ℝ

The linear functional taking the mean of a coordinate vector, with value zero in dimension zero.

Equations

• NRR.coordinateMean n = { toFun := fun (v : Fin n → ℝ) => (∑ i : Fin n, v i) / ↑n, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NRR.coordinateMean_apply (n : ℕ) (v : Fin n → ℝ) : (coordinateMean n) v = (∑ i : Fin n, v i) / ↑n

noncomputable def NRR.coordinateDeviation {n : ℕ} (hn : 0 < n) : (Fin n → ℝ) →ₗ[ℝ] ZeroSum n

Subtract the coordinate mean to obtain a vector in the zero-sum representation.

Equations

• NRR.coordinateDeviation hn = { toFun := fun (v : Fin n → ℝ) => ⟨fun (i : Fin n) => v i - (NRR.coordinateMean n) v, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NRR.coordinateDeviation_apply {n : ℕ} (hn : 0 < n) (v : Fin n → ℝ) (i : Fin n) : ↑((coordinateDeviation hn) v) i = v i - (coordinateMean n) v

def NRR.reconstructCoordinates (n : ℕ) : ZeroSum n × ℝ →ₗ[ℝ] Fin n → ℝ

Reconstruct coordinates from a zero-sum vector and a constant.

Equations

• NRR.reconstructCoordinates n = { toFun := fun (z : NRR.ZeroSum n × ℝ) (i : Fin n) => ↑z.1 i + z.2, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem NRR.reconstructCoordinates_apply {n : ℕ} (u : ZeroSum n) (c : ℝ) (i : Fin n) : (reconstructCoordinates n) (u, c) i = ↑u i + c

theorem NRR.coordinateMean_reconstruct {n : ℕ} (hn : 0 < n) (u : ZeroSum n) (c : ℝ) : (coordinateMean n) ((reconstructCoordinates n) (u, c)) = c

@[simp]

theorem NRR.coordinateDeviation_reconstruct {n : ℕ} (hn : 0 < n) (u : ZeroSum n) (c : ℝ) : (coordinateDeviation hn) ((reconstructCoordinates n) (u, c)) = u

noncomputable def NRR.coordinateDecomposition {n : ℕ} (hn : 0 < n) : (Fin n → ℝ) ≃ₗ[ℝ] ZeroSum n × ℝ

Decompose a coordinate vector into its zero-sum deviation and scalar mean.

Equations

• One or more equations did not get rendered due to their size.

theorem NRR.coordinate_eq_zero_iff {n : ℕ} (hn : 0 < n) (v : Fin n → ℝ) : v = 0 ↔ (coordinateDeviation hn) v = 0 ∧ (coordinateMean n) v = 0

A coordinate vector vanishes iff both its deviation and mean vanish.

theorem NRR.coordinateMean_relabel (n : ℕ) (σ : Equiv.Perm (Fin n)) (v : Fin n → ℝ) : ((coordinateMean n) fun (i : Fin n) => v ((Equiv.symm σ) i)) = (coordinateMean n) v

Permutations preserve the coordinate mean.

theorem NRR.coordinateDeviation_relabel {n : ℕ} (hn : 0 < n) (σ : Equiv.Perm (Fin n)) (v : Fin n → ℝ) : ((coordinateDeviation hn) fun (i : Fin n) => v ((Equiv.symm σ) i)) = ZeroSum.relabel σ ((coordinateDeviation hn) v)

Mean subtraction commutes with relabelling.