NRR.EMP.WeightShift — additive‑constant shift invariance of power weights

Adding a fixed constant c to all power weights leaves every power cell — and hence every restricted cell, the whole area vector, and the equal‑area property — unchanged. Intuitively, the power distance powerDist s w i x = ‖x - sᵢ‖² - wᵢ shifts by exactly -c at every site simultaneously, so all the comparisons powerDist i x ≤ powerDist j x defining the cells are preserved.

Definition

• EMP.addConstWeight w c = fun i => w i + c — the constant shift of a weight vector.

API

• PowerDiagram.powerDist_addConstWeight — the power distance shifts by -c.
• PowerDiagram.cell_addConstWeight — power cells are unchanged.
• PowerDiagram.bodyCellSet_addConstWeight — restricted power cells are unchanged.
• EMP.areaVec_addConstWeight — the equal‑area area vector is unchanged.
• EMP.IsEqualAreaWeight_addConstWeight — the equal‑area property is preserved.

No equal‑area existence, no normalization, and no variation of sites is used: the sites s are held fixed throughout and every result is a pure algebraic cancellation of the constant.

def NRR.EMP.addConstWeight {n : ℕ} (w : Fin n → ℝ) (c : ℝ) : Fin n → ℝ

Constant shift of a weight vector: add the fixed constant c to every weight.

Equations

• NRR.EMP.addConstWeight w c i = w i + c

@[simp]

theorem NRR.EMP.addConstWeight_apply {n : ℕ} (w : Fin n → ℝ) (c : ℝ) (i : Fin n) : addConstWeight w c i = w i + c

theorem NRR.PowerDiagram.powerDist_addConstWeight {n : ℕ} (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (c : ℝ) (i : Fin n) (x : Geometry.Plane) : powerDist s (EMP.addConstWeight w c) i x = powerDist s w i x - c

Power distance under a constant weight shift. Adding c to all weights decreases every power distance by exactly c.

theorem NRR.PowerDiagram.cell_addConstWeight {n : ℕ} (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (c : ℝ) (i : Fin n) : cell s (EMP.addConstWeight w c) i = cell s w i

Cell invariance under a constant weight shift. Since every power distance shifts by the same constant, all defining comparisons are preserved, so the power cell is unchanged.

theorem NRR.PowerDiagram.bodyCellSet_addConstWeight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (c : ℝ) (i : Fin n) : bodyCellSet K s (EMP.addConstWeight w c) i = bodyCellSet K s w i

Restricted‑cell invariance under a constant weight shift. Immediate from cell_addConstWeight, since the restricted cell is K ∩ cell.

theorem NRR.EMP.areaVec_addConstWeight {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (c : ℝ) : areaVec K s (addConstWeight w c) = areaVec K s w

Area‑vector invariance under a constant weight shift. Every restricted cell is unchanged, hence so is its area and the whole area vector.

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

Equal‑area invariance under a constant weight shift. Since the area vector is unchanged (areaVec_addConstWeight), the equal‑area property is preserved.