NRR.EMP.VariableBody.HalfspaceCoefficients — moving halfspace coefficients

For a variable planar body C : BodySpace K A, a configuration of sites s : Config n, and a weight vector w : Fin n → ℝ, the restricted power cell of site i is the body C intersected with finitely many closed lower halfspaces. The j‑th halfspace has

• normal sepNormal s i j = 2 • (sⱼ - sᵢ), depending only on the sites, and
• offset sepOffset s w i j = ‖sⱼ‖² - ‖sᵢ‖² - wⱼ + wᵢ, depending affinely on sites and weights.

These are thin wrappers over the fixed-site coefficients PowerDiagram.sepNormal and PowerDiagram.sepOffset evaluated at s.pts. Their continuity in the configuration (for the normal) and jointly in configuration and weights (for the offset) follows from continuity of the site map Config.continuous_pts. The off-diagonal normals are nonzero by injectivity of the sites.

The cell-algebra identities re-express cellSet hA C s w i as the parent body C.body intersected with the intersection of these halfspaces, both over all j and over the off-diagonal j ≠ i (the diagonal term is the whole plane and drops out). Keeping the parent as C.body lets later indicator-convergence arguments apply the subbody membership-stability theorem directly.

noncomputable def NRR.EMP.VariableBody.sepNormal {n : ℕ} (s : Config n) (i j : Fin n) : Geometry.Plane

The separating normal of the pair (i, j) for a configuration s, as the fixed-site separating normal PowerDiagram.sepNormal evaluated at the sites s.pts.

Equations

• NRR.EMP.VariableBody.sepNormal s i j = NRR.PowerDiagram.sepNormal s.pts i j

noncomputable def NRR.EMP.VariableBody.sepOffset {n : ℕ} (s : Config n) (w : Fin n → ℝ) (i j : Fin n) : ℝ

The separating offset of the pair (i, j) for a configuration s and weights w, as the fixed-site separating offset PowerDiagram.sepOffset evaluated at the sites s.pts.

Equations

• NRR.EMP.VariableBody.sepOffset s w i j = NRR.PowerDiagram.sepOffset s.pts w i j

theorem NRR.EMP.VariableBody.continuous_sepNormal {n : ℕ} (i j : Fin n) : Continuous fun (s : Config n) => sepNormal s i j

The separating normal varies continuously with the configuration.

theorem NRR.EMP.VariableBody.continuous_sepOffset {n : ℕ} (i j : Fin n) : Continuous fun (z : Config n × (Fin n → ℝ)) => sepOffset z.1 z.2 i j

The separating offset varies continuously with the configuration and the weights jointly.

theorem NRR.EMP.VariableBody.sepNormal_ne_zero {n : ℕ} (s : Config n) {i j : Fin n} (hij : i ≠ j) : sepNormal s i j ≠ 0

Off-diagonal separating normals are nonzero, from injectivity of the sites.

theorem NRR.EMP.VariableBody.cellSet_eq_iInter_halfspace {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) : cellSet hA C s w i = ↑C.body.body ∩ ⋂ (j : Fin n), Geometry.lowerClosedHalfspace (sepNormal s i j) (sepOffset s w i j)

Full halfspace representation. The restricted power cell of site i inside the variable body C equals the parent body C.body intersected with the closed lower halfspaces over all j.

theorem NRR.EMP.VariableBody.cellSet_eq_offDiag_halfspaces {K : Geometry.ConvexBody Geometry.Plane} {A : ℝ} {n : ℕ} (hA : 0 < A) (C : BodySpace K A) (s : Config n) (w : Fin n → ℝ) (i : Fin n) : cellSet hA C s w i = ↑C.body.body ∩ ⋂ (j : { j : Fin n // j ≠ i }), Geometry.lowerClosedHalfspace (sepNormal s i ↑j) (sepOffset s w i ↑j)

Off-diagonal halfspace representation. The diagonal term j = i is the whole plane, so it can be dropped, leaving the intersection over j ≠ i.