Documentation

LeanPool.NandakumarRamanaRao.NRR.EMP.EqualAreaWeightsUniqueness

NRR.EMP.EqualAreaWeightsUniqueness — uniqueness of equal-area power weights #

Equal-area power weights for fixed pairwise-distinct sites are unique up to a global additive constant. The proof is internal to the repository: for two solutions, take the indices on which w' - w is maximal. Cell rigidity identifies their restricted power cells in the two diagrams; the union of those cells is relatively clopen in the convex body, hence all of the body. Positive cell area and null pairwise overlap force every index to be maximal. Normalization then removes the common additive constant.

source
theorem NRR.EMP.powerDiagram_equalArea_weights_unique_core {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hs : Function.Injective s) {w w' : Fin n → ℝ} (hw : IsEqualAreaWeight K s w) (hw' : IsEqualAreaWeight K s w') :
∃ (c : ℝ), ∀ (i : Fin n), w' i = w i + c

Two equal-area weight vectors differ by a global additive constant. No positivity hypothesis on n is needed: the statement is vacuous when n = 0.

source
theorem NRR.EMP.equalArea_weights_unique {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hs : Function.Injective s) {w w' : Fin n → ℝ} (hw : IsEqualAreaWeight K s w) (hw' : IsEqualAreaWeight K s w') :
∃ (c : ℝ), ∀ (i : Fin n), w' i = w i + c

Uniqueness up to additive constants. For a planar convex body K and pairwise‑distinct sites s, any two equal‑area weight vectors differ by a global additive constant.

Derived directly from the isolated uniqueness core EMP.powerDiagram_equalArea_weights_unique_core.

The conclusion also holds for an empty site set, with additive constant c = 0.

source
theorem NRR.EMP.equalArea_weights_unique_normalized {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hn : 0 < n) (hs : Function.Injective s) {w w' : Fin n → ℝ} (hw : IsEqualAreaWeight K s w) (hw' : IsEqualAreaWeight K s w') (hnorm : WeightNormalized w) (hnorm' : WeightNormalized w') :
w = w'

Normalization uniqueness. For a planar convex body K and pairwise‑distinct sites s, two equal‑area weight vectors that are both normalized (∑ i, w i = 0) are equal.

proved from EMP.equalArea_weights_unique: writing w' i = w i + c and summing over all i, normalization gives 0 = 0 + (Fintype.card (Fin n)) • c, and over a nonempty index set this forces c = 0; over an empty index set the weight vectors are trivially equal.