NRR.PowerDiagram.BodyCells — restricted power cells as sets

Restricted power (Laguerre) cells of a convex body K, kept at the set level:

• bodyCellSet K s w i = (K : Set Plane) ∩ cell s w i — the restricted cell as a plain set.
• bodyCellArea K s w i — its area (real‑valued Lebesgue measure), defined unconditionally.

Set‑level geometry (bodyCellSet_subset_body, bodyCellSet_convex, bodyCellSet_isCompact) is available without any nondegeneracy assumption.

Bundling a restricted cell as a Geometry.ConvexBody (which requires nonempty interior by construction) is only possible when explicit interior evidence is supplied, via bodyCellBody K s w i hInt. There is deliberately no unconditional bodyCell: a restricted cell can be empty or lower‑dimensional, so it need not be a solid convex body.

Partition properties of the family i ↦ bodyCellSet K s w i are out of scope here.

def NRR.PowerDiagram.bodyCellSet {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : Set Geometry.Plane

Restricted power cell as a set: the intersection of the body K with the power cell of site i. Kept at the set level (no bundling, no nondegeneracy hypothesis).

Equations

• NRR.PowerDiagram.bodyCellSet K s w i = K.carrier ∩ NRR.PowerDiagram.cell s w i

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

Area of a restricted power cell: the real‑valued Lebesgue measure of bodyCellSet. Defined unconditionally (no nonempty‑interior hypothesis).

Equations

• NRR.PowerDiagram.bodyCellArea K s w i = (MeasureTheory.volume (NRR.PowerDiagram.bodyCellSet K s w i)).toReal

@[simp]

theorem NRR.PowerDiagram.bodyCellSet_def {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : bodyCellSet K s w i = K.carrier ∩ cell s w i

Definitional unfolding of bodyCellSet.

theorem NRR.PowerDiagram.bodyCellSet_subset_body {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : bodyCellSet K s w i ⊆ K.carrier

A restricted power cell is contained in the body K.

theorem NRR.PowerDiagram.bodyCellSet_convex {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : Convex ℝ (bodyCellSet K s w i)

A restricted power cell is convex (intersection of two convex sets).

theorem NRR.PowerDiagram.bodyCellSet_isCompact {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) : IsCompact (bodyCellSet K s w i)

A restricted power cell is compact: the body is compact and the power cell is closed.

noncomputable def NRR.PowerDiagram.bodyCellBody {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) (hInt : (interior (bodyCellSet K s w i)).Nonempty) : Geometry.ConvexBody Geometry.Plane

Bundled restricted power cell, requiring explicit nonempty‑interior evidence hInt. The carrier is bodyCellSet K s w i; convexity and compactness are automatic, and solidity is exactly the supplied hypothesis.

Equations

• NRR.PowerDiagram.bodyCellBody K s w i hInt = { carrier := NRR.PowerDiagram.bodyCellSet K s w i, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := hInt }

@[simp]

theorem NRR.PowerDiagram.bodyCellBody_carrier {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) (hInt : (interior (bodyCellSet K s w i)).Nonempty) : (bodyCellBody K s w i hInt).carrier = bodyCellSet K s w i

The carrier of bodyCellBody is the restricted cell set.

theorem NRR.PowerDiagram.bodyCellBody_area {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Fin n → Geometry.Plane) (w : Fin n → ℝ) (i : Fin n) (hInt : (interior (bodyCellSet K s w i)).Nonempty) : (bodyCellBody K s w i hInt).area = bodyCellArea K s w i

The area of the bundled restricted cell equals the set‑level bodyCellArea.