NRR.EMP.NormalizedWeights — normalized equal‑area power weights and existence

This module defines the normalized equal‑area weight subtype together with the mean‑subtraction normalization operation, and proves that normalized equal‑area weights exist.

Definitions

• EMP.NormalizedEqualAreaWeight K s — the subtype of weight vectors that are simultaneously equal‑area (EMP.IsEqualAreaWeight) and normalized (EMP.WeightNormalized, i.e. ∑ i, w i = 0).
• EMP.weightMean w = (∑ i, w i) / 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.

API

• EMP.WeightNormalized_normalizeWeight — mean subtraction produces a normalized weight (needs 0 < n).
• EMP.IsEqualAreaWeight_normalizeWeight — mean subtraction preserves the equal‑area property, using the constant‑shift invariance EMP.areaVec_addConstWeight: subtracting the mean is the constant shift by -(weightMean w).
• EMP.exists_normalized_equalArea_weight — normalized equal‑area weights exist, combining the existence theorem EMP.exists_equalArea_weights with the two facts above.

def NRR.EMP.NormalizedEqualAreaWeight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) : Type

Normalized equal‑area weight. A weight vector that is both equal‑area for the sites s in K and normalized (∑ i, w i = 0).

Equations

• NRR.EMP.NormalizedEqualAreaWeight K s = { w : Fin n → ℝ // NRR.EMP.IsEqualAreaWeight K s w ∧ NRR.EMP.WeightNormalized w }

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

normalizeWeight w is the constant shift of w by -(weightMean w).

theorem NRR.EMP.IsEqualAreaWeight_normalizeWeight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hw : IsEqualAreaWeight K s w) : IsEqualAreaWeight K s (normalizeWeight w)

Mean subtraction preserves the equal‑area property. Subtracting the mean is a constant shift, and the area vector is invariant under constant shifts (EMP.areaVec_addConstWeight, the project). Constant-shift invariance gives the result for every number of sites.

theorem NRR.EMP.exists_normalized_equalArea_weight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) : Nonempty (NormalizedEqualAreaWeight K s)

Existence of normalized equal‑area weights. For a planar convex body K, n > 0 pairwise‑distinct sites s, there exists a weight vector that is both equal‑area and normalized. Combines existence (EMP.exists_equalArea_weights, the project) with mean subtraction (constant‑shift invariance, the project).