Unconditional integrability on the actual Voronoi exteriors and faces

The literal half nearest-other ball is contained in the open cell.

The positive-height exclusion applies to the actual nuclear configuration.

theorem LiebThirring.ball_nearestOther_half_subset_voronoiCell {M : ℕ} (R : Fin M → Position) (hM : 2 ≤ M) (k : Fin M) : Metric.ball (R k) ((nearestOtherNucleusDistance R k).toReal / 2) ⊆ voronoiCell R k

The literal half nearest-other ball is contained in the open cell.

theorem LiebThirring.integrableOn_inverse_fourth_voronoiExterior {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (hM : 2 ≤ M) (k : Fin M) : MeasureTheory.IntegrableOn (fun (x : Position) => 1 / ‖x - R k‖ ^ 4) (voronoiCell R k)ᶜ MeasureTheory.volume

The positive-height exclusion applies to the actual nuclear configuration.

theorem LiebThirring.integrable_bisector_inverse_fourth_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : MeasureTheory.Integrable (fun (y : Position) => nuclearHalfDistance R k l / ‖y - R k‖ ^ 4) (bisectorSurfaceMeasure R hR k l hkl)

The inverse-fourth flux density is integrable on the whole bisector plane.

theorem LiebThirring.integrableOn_voronoiFace_inverse_fourth_flux {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) : MeasureTheory.IntegrableOn (fun (y : Position) => nuclearHalfDistance R k l / ‖y - R k‖ ^ 4) (voronoiFace R k l) (bisectorSurfaceMeasure R hR k l hkl)

In particular the actual, potentially unbounded genuine face is integrable.