The screened nuclear potential and the basic electrostatic inequality

screenedPotential Z R x omits a nearest nucleus. The basic electrostatic inequality for positive finite-energy measures connects the Voronoi face-charge argument with shell assembly.

noncomputable def LiebThirring.screenedPotential {M : ℕ} (Z : NNReal) (R : Fin M → Position) (x : Position) : ENNReal

The potential of all nuclei except a nearest one: min_k Σ_{p ≠ k} Z |x - R_p|⁻¹.

Equations

• LiebThirring.screenedPotential Z R x = ⨅ (k : Fin M), ∑ p ∈ Finset.univ.erase k, ↑Z * LiebThirring.coulombKernel x (R p)

def LiebThirring.BasicElectrostaticInequality {M : ℕ} (Z : NNReal) (R : Fin M → Position) : Prop

the basic electrostatic inequality,, for positive finite measures of finite Coulomb energy: ∫ Φ dμ + C_R ≤ D(μ, μ) + U.

Equations

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