Density bounds and local Coulomb integrals of the face measure

Uniform bound of the density on one plane.

Domination by bounded-density surface measure, with its literal coefficient.

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

Uniform bound of the density on one plane.

Equations

• LiebThirring.nuclearFaceDensityBound R Z k l = Z / (2 * Real.pi * LiebThirring.nuclearHalfDistance R k l ^ 2)

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

theorem LiebThirring.nuclearFaceDensity_le_bound {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) {k l : Fin M} (hkl : k ≠ l) {y : Position} (hy : y ∈ bisectorPlane R k l) : nuclearFaceDensity R Z k l y ≤ nuclearFaceDensityBound R Z k l

theorem LiebThirring.voronoiFaceDensity_le_bound {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (y : Position) : voronoiFaceDensity R Z k l y ≤ ENNReal.ofReal (nuclearFaceDensityBound R Z k l)

theorem LiebThirring.nuclearFaceMeasure_le_smul_surface {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 ≤ ENNReal.ofReal (nuclearFaceDensityBound R Z k l) • bisectorSurfaceMeasure R hR k l hkl

Domination by bounded-density surface measure, with its literal coefficient.

theorem LiebThirring.lintegral_coulombKernel_ball_nuclearFaceMeasure_le {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (k l : Fin M) (hkl : k ≠ l) (x : Position) {ε : ℝ} (hε : 0 < ε) : ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂nuclearFaceMeasure R hR Z k l hkl ≤ ENNReal.ofReal (2 * Real.pi * ε * nuclearFaceDensityBound R Z k l)

The local estimate includes off-plane centres and the infinite kernel value.

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

The coefficient in the uniform local singular-integral bound (6.4).

Equations

• LiebThirring.voronoiLocalCoefficient R Z = 2 * Real.pi * ∑ p : LiebThirring.NuclearPair M, LiebThirring.nuclearFaceDensityBound R Z (↑p).1 (↑p).2

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

theorem LiebThirring.lintegral_coulombKernel_ball_voronoiFaceMeasure_le {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) {Z : ℝ} (hZ : 0 ≤ Z) (x : Position) {ε : ℝ} (hε : 0 < ε) : ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂voronoiFaceMeasure R hR Z ≤ ENNReal.ofReal (voronoiLocalCoefficient R Z * ε)

Equation (6.4) for the actual unordered-face measure.