NRR.EMP.PowerPartitionPieces — equal‑area power cells as convex bodies

Given a configuration s : Config n of pairwise‑distinct sites in a convex body K with 0 < K.area and 0 < n, we bundle each restricted power (Laguerre) cell of the canonical normalized equal‑area weight EMP.normalizedWeight as a Geometry.ConvexBody.

Nonempty interior — required to form a ConvexBody — is supplied by the theorem PowerDiagram.bodyCellSet_interior_nonempty_of_equalArea, using that the normalized weight is equal‑area (EMP.normalizedWeight_isEqualArea).

Public API

• EMP.powerPartitionPiece — the i‑th equal‑area restricted power cell bundled as a convex body.
• EMP.powerPartitionPiece_carrier — its carrier is the restricted cell set.
• EMP.powerPartitionPiece_area — its area equals the set‑level bodyCellArea.
• EMP.powerPartitionPiece_area_eq — each piece has area exactly K.area / n.

The full partition (disjointness / covering of K) is out of scope here.

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

Equal‑area power‑cell piece. The i‑th restricted power cell of the canonical normalized equal‑area weight EMP.normalizedWeight K s.pts hn s.injective_pts, bundled as a Geometry.ConvexBody. Nonempty interior is provided by PowerDiagram.bodyCellSet_interior_nonempty_of_equalArea (the existing theorem).

Equations

• NRR.EMP.powerPartitionPiece K s hn hK i = NRR.PowerDiagram.bodyCellBody K s.pts (NRR.EMP.normalizedWeight K s.pts hn ⋯) i ⋯

@[simp]

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

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

theorem NRR.EMP.powerPartitionPiece_area {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) (i : Fin n) : (powerPartitionPiece K s hn hK i).area = PowerDiagram.bodyCellArea K s.pts (normalizedWeight K s.pts hn ⋯) i

The area of the equal‑area power‑cell piece equals the set‑level bodyCellArea of the normalized weight.

theorem NRR.EMP.powerPartitionPiece_area_eq {n : ℕ} (K : Geometry.ConvexBody Geometry.Plane) (s : Config n) (hn : 0 < n) (hK : 0 < K.area) (i : Fin n) : (powerPartitionPiece K s hn hK i).area = K.area / ↑n

Equal area. Each equal‑area power‑cell piece has area exactly the average K.area / n, because the normalized weight is an equal‑area weight (EMP.normalizedWeight_isEqualArea).