Nearest-nucleus geometry for the energy deficit

A finite configuration with at least two nuclei has a nearest other index.

The finite minimum agrees with the extended nearest-other distance.

theorem LiebThirring.exists_nearest_other_nucleus {M : ℕ} (R : Fin M → Position) (hM : 2 ≤ M) (k : Fin M) : ∃ (l : Fin M), l ≠ k ∧ ∀ (p : Fin M), p ≠ k → ‖R k - R l‖ ≤ ‖R k - R p‖

A finite configuration with at least two nuclei has a nearest other index.

theorem LiebThirring.nearestOtherNucleusDistance_eq_of_nearest {M : ℕ} (R : Fin M → Position) {k l : Fin M} (hkl : l ≠ k) (hl : ∀ (p : Fin M), p ≠ k → ‖R k - R l‖ ≤ ‖R k - R p‖) : nearestOtherNucleusDistance R k = ENNReal.ofReal ‖R k - R l‖

The finite minimum agrees with the extended nearest-other distance.

theorem LiebThirring.nearestOtherNucleusDistance_pos {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : 0 < nearestOtherNucleusDistance R k

theorem LiebThirring.nearestOtherNucleusDistance_lt_top {M : ℕ} (R : Fin M → Position) (hM : 2 ≤ M) (k : Fin M) : nearestOtherNucleusDistance R k < ⊤

theorem LiebThirring.nearestOtherNucleusDistance_toReal_pos {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : 0 < (nearestOtherNucleusDistance R k).toReal

theorem LiebThirring.exists_nearest_exterior_halfSpace {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : ∃ (l : Fin M), l ≠ k ∧ nearestOtherNucleusDistance R k = ENNReal.ofReal ‖R l - R k‖ ∧ {x : Position | (nearestOtherNucleusDistance R k).toReal / 2 ≤ inner ℝ (bisectorNormal R k l) (x - R k)} ⊆ (voronoiCell R k)ᶜ

The nearest-other half-space lies in the cell exterior, with the radius.

theorem LiebThirring.nearestNucleusDistance_eq_of_mem_voronoiFace {M : ℕ} (R : Fin M → Position) {k l : Fin M} {x : Position} (hx : x ∈ voronoiFace R k l) : nearestNucleusDistance R x = ENNReal.ofReal ‖x - R k‖

Every genuine face has either incident nucleus as a nearest one.