NRR.EMP.PartitionFromPowerDiagram — the canonical equal‑area power partition

Given a configuration s : Config n of pairwise‑distinct sites inside a convex body K with 0 < K.area and 0 < n, this module assembles the equal‑area restricted power (Laguerre) cells EMP.powerPartitionPiece into an honest ConvexPartition K n.

The three partition obligations are discharged from the set‑level power‑diagram API:

• subset — PowerDiagram.bodyCellSet_subset;
• covers — PowerDiagram.iUnion_bodyCellSet (needs [NeZero n], supplied from hn);
• nullOverlap — PowerDiagram.bodyCellSet_inter_null, using site injectivity from Config.

Public API

• EMP.powerPartition — the canonical equal‑area power partition of K.
• EMP.powerPartition_piece_carrier — the carrier of the i‑th piece is the restricted cell set of the canonical normalized equal‑area weight.
• EMP.powerPartition_isEqualArea — every piece has the same area (= K.area / n).
• EMP.powerPartition_covers — the pieces cover K.
• EMP.powerPartition_nullOverlap — distinct pieces overlap only on a null set.

noncomputable def NRR.EMP.powerPartition {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : ConvexPartition K n

Canonical equal‑area power partition. The restricted power cells of the canonical normalized equal‑area weight EMP.normalizedWeight K s.pts hn s.injective_pts, bundled as a ConvexPartition K n. Covering comes from PowerDiagram.iUnion_bodyCellSet; null overlap of distinct pieces comes from PowerDiagram.bodyCellSet_inter_null via Config site injectivity.

Equations

• NRR.EMP.powerPartition K s hn hK = { piece := fun (i : Fin n) => NRR.EMP.powerPartitionPiece K s hn hK i, subset := ⋯, covers := ⋯, nullOverlap := ⋯ }

theorem NRR.EMP.powerPartition_piece_carrier {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) (i : Fin n) : ((powerPartition K s hn hK).piece i).carrier = PowerDiagram.bodyCellSet K s.pts (normalizedWeight K s.pts hn ⋯) i

The carrier of the i‑th piece of the canonical equal‑area power partition is the restricted power cell set of the canonical normalized equal‑area weight.

theorem NRR.EMP.powerPartition_isEqualArea {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : (powerPartition K s hn hK).IsEqualArea

Equal area. Every piece of the canonical equal‑area power partition has the same area (each equal to the average K.area / n), because the underlying normalized weight is an equal‑area weight.

theorem NRR.EMP.powerPartition_covers {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) : K.carrier ⊆ ⋃ (i : Fin n), ((powerPartition K s hn hK).piece i).carrier

Cover. The pieces of the canonical equal‑area power partition cover K.

theorem NRR.EMP.powerPartition_nullOverlap {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) (i j : Fin n) (hij : i ≠ j) : MeasureTheory.volume (((powerPartition K s hn hK).piece i).carrier ∩ ((powerPartition K s hn hK).piece j).carrier) = 0

Null overlap. Distinct pieces of the canonical equal‑area power partition overlap only on a Lebesgue‑null set.