Geometry of power cells

Proves convexity, closedness, and covering of the ambient space by power cells. The definitions are in NRR.PowerDiagram.Defs, and the halfspace representation is in CellAlgebra.

@[simp]

theorem NRR.PowerDiagram.mem_cell {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) (i : Fin n) (x : E2) : x ∈ cell s w i ↔ ∀ (j : Fin n), powerDist s w i x ≤ powerDist s w j x

Membership in a power cell: x lies in cell s w i iff i is (weakly) power‑closest to x among all sites.

theorem NRR.PowerDiagram.cell_convex {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) (i : Fin n) : Convex ℝ (cell s w i)

Every power cell is convex: it is an intersection of convex half‑spaces.

theorem NRR.PowerDiagram.cell_isClosed {n : ℕ} (s : Fin n → E2) (w : Fin n → ℝ) (i : Fin n) : IsClosed (cell s w i)

Every power cell is closed: it is an intersection of closed half‑spaces.

theorem NRR.PowerDiagram.iUnion_cell {n : ℕ} [NeZero n] (s : Fin n → E2) (w : Fin n → ℝ) : ⋃ (i : Fin n), cell s w i = Set.univ

The power cells cover the whole plane. Requires at least one site ([NeZero n]): for each x, pick an index i minimizing the finite family j ↦ powerDist s w j x.