Nearest Voronoi face and boundary distance

Nearest-other nuclear distance determines the distance from a nucleus to its Voronoi boundary.

theorem LiebThirring.norm_bisectorNormal {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : ‖bisectorNormal R k l‖ = 1

theorem LiebThirring.mem_voronoiCell_iff_normal {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) (x : Position) : x ∈ voronoiCell R k ↔ ∀ (l : Fin M), l ≠ k → inner ℝ (bisectorNormal R k l) (x - R k) < ‖R l - R k‖ / 2

theorem LiebThirring.mem_bisectorPlane_iff_normal {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) (x : Position) : x ∈ bisectorPlane R k l ↔ inner ℝ (bisectorNormal R k l) (x - R k) = ‖R l - R k‖ / 2

theorem LiebThirring.exterior_halfSpace_subset_compl_voronoiCell {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {k l : Fin M} (hkl : k ≠ l) : {x : Position | ‖R l - R k‖ / 2 ≤ inner ℝ (bisectorNormal R k l) (x - R k)} ⊆ (voronoiCell R k)ᶜ

The direction n_kl points from C_k into its excluded half-space.

theorem LiebThirring.ball_subset_voronoiCell_of_bound {M : ℕ} (R : Fin M → Position) (k : Fin M) (r : ℝ) (hr : ∀ (l : Fin M), l ≠ k → 2 * r ≤ dist (R k) (R l)) : Metric.ball (R k) r ⊆ voronoiCell R k

Any radius below all half inter-nuclear distances gives a ball in the cell.