Voronoi boundary decomposition and volume partition

Strict faces partition each Voronoi boundary up to triple-tie strata.

theorem LiebThirring.exists_tie_of_mem_closed_not_mem_cell {M : ℕ} (R : Fin M → Position) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) (hn : x ∉ voronoiCell R k) : ∃ (l : Fin M), l ≠ k ∧ dist x (R k) = dist x (R l)

A closest nucleus fails to be uniquely closest exactly when another nucleus ties it.

theorem LiebThirring.closedVoronoiCells_cover {M : ℕ} (R : Fin M → Position) (hM : 0 < M) : ⋃ (k : Fin M), closedVoronoiCell R k = Set.univ

theorem LiebThirring.exists_nearest_tie_of_not_mem_cells {M : ℕ} (R : Fin M → Position) (hM : 0 < M) {x : Position} (hx : x ∉ ⋃ (k : Fin M), voronoiCell R k) : ∃ (k : Fin M) (l : Fin M), k ≠ l ∧ x ∈ closedVoronoiCell R k ∧ dist x (R k) = dist x (R l)

Outside all open cells, two closest nuclei tie.

theorem LiebThirring.volume_bisectorPlane {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : MeasureTheory.volume ↑(bisectorPlane R k l) = 0

theorem LiebThirring.volume_compl_voronoiCells {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 0 < M) : MeasureTheory.volume (⋃ (k : Fin M), voronoiCell R k)ᶜ = 0

The disjoint open cells cover ambient space up to a volume-null set.