NRR.PowerDiagram.CellAreaContinuityWeights

Weight‑continuity of restricted power‑cell areas with fixed sites.

Fixing the sites s : Fin n → Plane and letting the weights w : Fin n → ℝ vary, the restricted power cell of site i is a finite intersection of fixed‑normal halfspaces whose offsets move linearly (hence continuously) with the weights:

• normal of the j‑th halfspace is sepNormal s i j = 2 • (s j - s i) — independent of w;
• offset of the j‑th halfspace is sepOffset s w i j = ‖s j‖² - ‖s i‖² - w j + w i.

Specializing the moving‑halfspace area‑continuity result of NRR/Geometry/HalfspaceFiniteIntersectionAreaContinuity.lean then yields continuity of w ↦ bodyCellArea K s w i.

The distinct‑sites hypothesis is necessary

The main theorem carries hs : ∀ j, j ≠ i → s j ≠ s i. This nondegeneracy hypothesis is mathematically required: if s j = s i for some j ≠ i then sepNormal s i j = 0 and the j‑th halfspace degenerates to {x | 0 ≤ sepOffset s w i j} = {x | w i ≥ w j}, i.e. the whole plane when w i ≥ w j and the empty set when w i < w j. The restricted area then jumps discontinuously (from a positive value to 0) as w i crosses w j. So without distinct sites the statement is genuinely false; the hypothesis is how the degenerate case is handled rather than omitted.

Note the diagonal term j = i always has sepNormal s i i = 0 and sepOffset s w i i = 0, so its halfspace is the constant whole plane {x | 0 ≤ 0}; it contributes nothing and is harmless, which is why the diagonal is exempted (only the off‑diagonal normals must be nonzero).

theorem NRR.PowerDiagram.bodyCellSet_eq_finiteHalfspaceIntersection {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : bodyCellSet K s w i = K.finiteHalfspaceIntersection (fun (j : Fin n) => sepNormal s i j) fun (j : Fin n) => sepOffset s w i j

Restricted power cell as a fixed‑normal finite halfspace intersection. With sites s fixed, bodyCellSet K s w i is exactly the finite intersection of K with the fixed‑normal halfspaces sepNormal s i j at the (weight‑dependent) offsets sepOffset s w i j.

theorem NRR.PowerDiagram.continuous_sepOffset_weights {n : ℕ} (s : Fin n → Geometry.Plane) (i : Fin n) : Continuous fun (w : Fin n → ℝ) (j : Fin n) => sepOffset s w i j

Offsets move continuously with the weights. For fixed sites s, the whole offset vector j ↦ sepOffset s w i j depends continuously (indeed affinely) on the weights w.

theorem NRR.PowerDiagram.bodyCellSet_eq_finiteHalfspaceIntersection_offDiag {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : bodyCellSet K s w i = K.finiteHalfspaceIntersection (fun (j : { j : Fin n // j ≠ i }) => sepNormal s i ↑j) fun (j : { j : Fin n // j ≠ i }) => sepOffset s w i ↑j

theorem NRR.PowerDiagram.continuous_bodyCellArea_weights {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (i : Fin n) (hs : ∀ (j : Fin n), j ≠ i → s j ≠ s i) : Continuous fun (w : Fin n → ℝ) => bodyCellArea K s w i

Fixed‑site weight‑continuity of the restricted power‑cell area. With sites s fixed and pairwise distinct from s i (hs), the restricted cell area w ↦ bodyCellArea K s w i is continuous. The hypothesis hs is necessary (see the module docstring).