NRR.EMP.WeightSpace — finite‑dimensional algebra of normalized weights

This module packages the pure, finite‑dimensional linear algebra of weight vectors w : Fin n → ℝ, independent of any optimal‑transport / power‑diagram machinery. It provides the vocabulary used to pin down the additive‑constant freedom in equal‑area weights:

Definitions

• EMP.weightSum w = ∑ i, w i — the total of a weight vector.
• EMP.WeightNormalized w — the affine normalization EMP.weightSum w = 0 (equivalently ∑ i, w i = 0).
• EMP.weightMean w = EMP.weightSum w / n — the arithmetic mean of a weight vector.
• EMP.normalizeWeight w = fun i => w i - EMP.weightMean w — subtract the mean, producing a zero‑sum weight vector.

Main results

• EMP.weightSum_zero, EMP.weightSum_add_const — basic finite‑sum algebra.
• EMP.WeightNormalized_normalizeWeight — mean subtraction produces a normalized weight (for 0 < n).
• EMP.normalizeWeight_eq_sub_mean — the definitional unfolding of normalizeWeight.
• EMP.normalizeWeight_eq_self_of_normalized — normalization is idempotent on already normalized weights.

This file must not depend on optimal transport; it imports only Mathlib.

noncomputable def NRR.EMP.weightSum {n : ℕ} (w : Fin n → ℝ) : ℝ

Weight sum. The total ∑ i, w i of a weight vector.

Equations

• NRR.EMP.weightSum w = ∑ i : Fin n, w i

def NRR.EMP.WeightNormalized {n : ℕ} (w : Fin n → ℝ) : Prop

Normalized weights. The affine normalization ∑ i, w i = 0, used to remove the additive‑constant freedom in the weights.

Equations

• NRR.EMP.WeightNormalized w = (NRR.EMP.weightSum w = 0)

noncomputable def NRR.EMP.weightMean {n : ℕ} (w : Fin n → ℝ) : ℝ

Weight mean. The arithmetic mean (∑ i, w i) / n of a weight vector.

Equations

• NRR.EMP.weightMean w = NRR.EMP.weightSum w / ↑n

noncomputable def NRR.EMP.normalizeWeight {n : ℕ} (w : Fin n → ℝ) : Fin n → ℝ

Mean‑subtraction normalization. Subtract the mean from every weight, producing a zero‑sum weight vector.

Equations

• NRR.EMP.normalizeWeight w i = w i - NRR.EMP.weightMean w

@[simp]

theorem NRR.EMP.normalizeWeight_apply {n : ℕ} (w : Fin n → ℝ) (i : Fin n) : normalizeWeight w i = w i - weightMean w

theorem NRR.EMP.WeightNormalized_iff {n : ℕ} (w : Fin n → ℝ) : WeightNormalized w ↔ ∑ i : Fin n, w i = 0

EMP.WeightNormalized w unfolds to ∑ i, w i = 0.

@[simp]

theorem NRR.EMP.weightSum_zero {n : ℕ} : (weightSum fun (x : Fin n) => 0) = 0

The all‑zero weight has zero total.

theorem NRR.EMP.weightSum_add_const {n : ℕ} (w : Fin n → ℝ) (c : ℝ) : (weightSum fun (i : Fin n) => w i + c) = weightSum w + ↑n * c

Adding a constant c to every weight increases the total by n * c.

theorem NRR.EMP.WeightNormalized_normalizeWeight {n : ℕ} (w : Fin n → ℝ) (hn : 0 < n) : WeightNormalized (normalizeWeight w)

Mean subtraction normalizes. For 0 < n, the mean‑subtracted weight vector has zero sum.

theorem NRR.EMP.normalizeWeight_eq_sub_mean {n : ℕ} (w : Fin n → ℝ) : normalizeWeight w = fun (i : Fin n) => w i - weightMean w

Definitional unfolding of normalizeWeight.

theorem NRR.EMP.normalizeWeight_eq_self_of_normalized {n : ℕ} (w : Fin n → ℝ) (hw : WeightNormalized w) : normalizeWeight w = w

Normalizing an already normalized weight leaves it unchanged.

theorem NRR.EMP.natCast_card_fin {n : ℕ} : ↑Finset.univ.card = ↑n

Nat.cast of the Fin n cardinality equals (n : ℝ).