NRR.EMP.AreaVectorTarget — area vector into the fixed total‑mass hyperplane

This module packages the equal‑area area vector EMP.areaVec K s w relative to the fixed total mass K.area, phrasing the equal‑area problem as finding zeroes of a continuous finite‑dimensional deviation map.

Definitions

• EMP.equalAreaTarget K n : Fin n → ℝ — the constant target vector fun _ => K.area / n, whose components sum to K.area (for n > 0).
• EMP.areaDeviation K s w : Fin n → ℝ — the deviation EMP.areaVec K s w - equalAreaTarget, which lies in the zero‑sum hyperplane for distinct sites.

API

• sum_equalAreaTarget — the target components sum to K.area.
• sum_areaDeviation_eq_zero — the deviation is zero‑sum (distinct sites, at least one site).
• continuous_areaDeviation_weights — with distinct fixed sites, w ↦ areaDeviation K s w is continuous in the weights.

Necessary nondegeneracy hypotheses

• sum_equalAreaTarget needs hn : 0 < n (an empty sum is 0, not K.area).
• sum_areaDeviation_eq_zero needs hn : 0 < n and hs : Function.Injective s — the total‑mass identity sum_EMP_areaVec_eq_area uses the almost‑disjoint covering of K by the restricted cells, which requires distinct sites (and at least one site).
• continuous_areaDeviation_weights needs hs : Function.Injective s: it reduces to the continuity of EMP.areaVec (a constant target is continuous), which is genuinely false when two sites coincide (see NRR.PowerDiagram.CellAreaVector). The signature in the design omitted hs; it is added here because the statement is false without it.

No existence of equal‑area weights and no topological‑degree/obstruction argument is used or proved here.

noncomputable def NRR.EMP.equalAreaTarget (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : Fin n → ℝ

Target equal‑area vector. The constant vector whose every component is the average area K.area / n.

Equations

• NRR.EMP.equalAreaTarget K n x✝ = K.area / ↑n

noncomputable def NRR.EMP.areaDeviation {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) : Fin n → ℝ

Zero‑sum deviation map. The difference between the area vector and the equal‑area target; for distinct sites its components sum to zero.

Equations

• NRR.EMP.areaDeviation K s w i = NRR.EMP.areaVec K s w i - NRR.EMP.equalAreaTarget K n i

@[simp]

theorem NRR.EMP.equalAreaTarget_apply (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) (i : Fin n) : equalAreaTarget K n i = K.area / ↑n

@[simp]

theorem NRR.EMP.areaDeviation_apply {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : areaDeviation K s w i = areaVec K s w i - equalAreaTarget K n i

theorem NRR.EMP.sum_equalAreaTarget {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (hn : 0 < n) : ∑ i : Fin n, equalAreaTarget K n i = K.area

Total mass of the target vector. The equal‑area target components sum to K.area.

theorem NRR.EMP.sum_areaDeviation_eq_zero {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (hn : 0 < n) (hs : Function.Injective s) : ∑ i : Fin n, areaDeviation K s w i = 0

Zero‑sum deviation. With distinct sites and at least one site, the deviation vector has zero total mass.

theorem NRR.EMP.continuous_areaDeviation_weights {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (hs : Function.Injective s) : Continuous fun (w : Fin n → ℝ) => areaDeviation K s w

Fixed‑site weight‑continuity of the deviation map. With sites s fixed and pairwise distinct (hs), the map w ↦ EMP.areaDeviation K s w is continuous in the weights.