The positive measure of genuine Voronoi faces

Unordered nuclear pairs, represented by their increasing ordering.

The real density on a bisector plane, as prescribed in.

@[reducible, inline]

abbrev LiebThirring.NuclearPair (M : ℕ) : Type

Unordered nuclear pairs, represented by their increasing ordering.

Equations

• LiebThirring.NuclearPair M = { p : Fin M × Fin M // p.1 < p.2 }

noncomputable def LiebThirring.nuclearFaceDensity {M : ℕ} (R : Fin M → Position) (Z : ℝ) (k l : Fin M) (y : Position) : ℝ

The real density on a bisector plane, as prescribed in (6.1).

Equations

• LiebThirring.nuclearFaceDensity R Z k l y = Z * LiebThirring.nuclearHalfDistance R k l / (2 * Real.pi * ‖y - R k‖ ^ 3)

noncomputable def LiebThirring.voronoiFaceDensity {M : ℕ} (R : Fin M → Position) (Z : ℝ) (k l : Fin M) : Position → ENNReal

Extend the nonnegative density by zero off the genuine face.

Equations

• LiebThirring.voronoiFaceDensity R Z k l = (LiebThirring.voronoiFace R k l).indicator fun (y : LiebThirring.Position) => ENNReal.ofReal (LiebThirring.nuclearFaceDensity R Z k l y)

noncomputable def LiebThirring.nuclearFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (Z : ℝ) (k l : Fin M) (hkl : k ≠ l) : MeasureTheory.Measure Position

One genuine face, equipped with its surface charge.

Equations

• LiebThirring.nuclearFaceMeasure R hR Z k l hkl = (LiebThirring.bisectorSurfaceMeasure R hR k l hkl).withDensity (LiebThirring.voronoiFaceDensity R Z k l)

noncomputable def LiebThirring.voronoiFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (Z : ℝ) : MeasureTheory.Measure Position

The positive measure ν of (6.1); each genuine face occurs once.

Equations

• LiebThirring.voronoiFaceMeasure R hR Z = ∑ p : LiebThirring.NuclearPair M, LiebThirring.nuclearFaceMeasure R hR Z (↑p).1 (↑p).2 ⋯

theorem LiebThirring.measurable_nuclearFaceDensity {M : ℕ} (R : Fin M → Position) (Z : ℝ) (k l : Fin M) : Measurable (nuclearFaceDensity R Z k l)

theorem LiebThirring.measurable_voronoiFaceDensity {M : ℕ} (R : Fin M → Position) (Z : ℝ) (k l : Fin M) : Measurable (voronoiFaceDensity R Z k l)

theorem LiebThirring.nuclearFaceDensity_nonneg {M : ℕ} (R : Fin M → Position) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (y : Position) : 0 ≤ nuclearFaceDensity R Z k l y

theorem LiebThirring.lintegral_nuclearFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (Z : ℝ) (k l : Fin M) (hkl : k ≠ l) (h : Position → ENNReal) (hh : Measurable h) : ∫⁻ (y : Position), h y ∂nuclearFaceMeasure R hR Z k l hkl = ∫⁻ (y : Position) in voronoiFace R k l, ENNReal.ofReal (nuclearFaceDensity R Z k l y) * h y ∂bisectorSurfaceMeasure R hR k l hkl

The defining nonnegative Borel integral formula, with explicit face restriction.

@[simp]

theorem LiebThirring.voronoiFaceMeasure_one (R : Fin 1 → Position) (hR : Function.Injective R) (Z : ℝ) : voronoiFaceMeasure R hR Z = 0