Cubic decay of the actual Voronoi face densities

Explicit cubic decay estimates for the Voronoi face densities.

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

The explicit coefficient of the cubic decay bound in face charge.

Equations

• LiebThirring.nuclearFaceDecayCoefficient R Z k l = Z * LiebThirring.nuclearHalfDistance R k l / (2 * Real.pi) * (1 + (1 + ‖R k‖) / LiebThirring.nuclearHalfDistance R k l) ^ 3

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

theorem LiebThirring.nuclearFaceDensity_le_decay {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 ≤ nuclearFaceDecayCoefficient R Z k l / (1 + ‖y‖) ^ 3

The lower separation on a bisector converts inverse cubic nuclear distance into inverse cubic distance from the origin.

theorem LiebThirring.voronoiFaceDensity_le_decay {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 (nuclearFaceDecayCoefficient R Z k l / (1 + ‖y‖) ^ 3)

The genuine-face indicator preserves the cubic decay bound everywhere.