Finite mass of the Voronoi face measure

Integrating the displayed density on the full bisector plane gives Z.

Restricting the whole-plane charge to the genuine face decreases its mass.

theorem LiebThirring.lintegral_bisector_nuclearFaceDensity {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) : ∫⁻ (y : Position), ENNReal.ofReal (nuclearFaceDensity R Z k l y) ∂bisectorSurfaceMeasure R hR k l hkl = ENNReal.ofReal Z

Integrating the displayed density on the full bisector plane gives Z.

theorem LiebThirring.nuclearFaceMeasure_mass_le {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) : (nuclearFaceMeasure R hR Z k l hkl) Set.univ ≤ ENNReal.ofReal Z

Restricting the whole-plane charge to the genuine face decreases its mass.

theorem LiebThirring.card_nuclearPair (M : ℕ) : Fintype.card (NuclearPair M) = M.choose 2

theorem LiebThirring.voronoiFaceMeasure_mass_le {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : (voronoiFaceMeasure R hR Z) Set.univ ≤ ↑(M.choose 2) * ENNReal.ofReal Z

The preliminary mass bound in face charge; exact mass belongs to the potential identity.

theorem LiebThirring.voronoiFaceMeasure_mass_lt_top {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : (voronoiFaceMeasure R hR Z) Set.univ < ⊤

theorem LiebThirring.isFiniteMeasure_voronoiFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : MeasureTheory.IsFiniteMeasure (voronoiFaceMeasure R hR Z)

Finiteness is proved from the explicit density, without a potential identity.