Analytic bounds for the positive Voronoi face measure

The explicit Voronoi face charge satisfies the finite-mass, energy, and decay bounds required by the potential argument.

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

The actual face potential is everywhere finite, including at face points.

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

Self-energy is finite as a consequence of the proved uniform potential bound.

theorem LiebThirring.continuous_toReal_coulombPotential_voronoiFaceMeasure {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : Continuous fun (x : Position) => (coulombPotential (voronoiFaceMeasure R hR Z) x).toReal

The finite potential, regarded as a real function, is also continuous.

noncomputable def LiebThirring.voronoiDecayCoefficient {M : ℕ} (R : Fin M → Position) (Z : ℝ) : ℝ

Explicit data-dependent coefficient in (6.2).

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.voronoiDecayCoefficient_nonneg {M : ℕ} (R : Fin M → Position) {Z : ℝ} (hZ : 0 ≤ Z) : 0 ≤ voronoiDecayCoefficient R Z

theorem LiebThirring.coulombPotential_nuclearFaceMeasure_decay {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (x : Position) : coulombPotential (nuclearFaceMeasure R hR Z k l hkl) x ≤ ENNReal.ofReal ((4 * Real.pi * nuclearFaceDensityBound R Z k l + 6 * Z + 16 * Real.pi * nuclearFaceDecayCoefficient R Z k l) / (1 + ‖x‖))

Apply cubic density decay and the exact planar kernel estimate to one face.

theorem LiebThirring.coulombPotential_voronoiFaceMeasure_decay {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (x : Position) : coulombPotential (voronoiFaceMeasure R hR Z) x ≤ ENNReal.ofReal (voronoiDecayCoefficient R Z / (1 + ‖x‖))

Equation (6.2), with an explicit coefficient depending only on the nuclei and charge.

theorem LiebThirring.tendsto_coulombPotential_voronoiFaceMeasure_zero {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : Filter.Tendsto (coulombPotential (voronoiFaceMeasure R hR Z)) (Bornology.cobounded Position) (nhds 0)

The decay at infinity used in the potential identity.

theorem LiebThirring.tendsto_toReal_coulombPotential_voronoiFaceMeasure_zero {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) : Filter.Tendsto (fun (x : Position) => (coulombPotential (voronoiFaceMeasure R hR Z) x).toReal) (Bornology.cobounded Position) (nhds 0)

The finite real-valued potential tends to zero at infinity as well.