The everywhere nearest-nucleus cutoff

The extended nearest-distance cutoff, infinite at nuclei when a > 0.

The nearest-distance cutoff is measurable.

noncomputable def LiebThirring.Assembly.nearestNucleusCutoff {M : ℕ} (a r : ℝ) (R : Fin M → Position) (x : Position) : ENNReal

The extended nearest-distance cutoff, infinite at nuclei when a > 0.

Equations

• LiebThirring.Assembly.nearestNucleusCutoff a r R x = if LiebThirring.nearestNucleusDistance R x < ENNReal.ofReal r then ENNReal.ofReal a * (LiebThirring.nearestNucleusDistance R x)⁻¹ else 0

theorem LiebThirring.Assembly.nearestNucleusInverse_le_cutoff {M : ℕ} (a r : ℝ) (hr : 0 < r) (R : Fin M → Position) (x : Position) : ENNReal.ofReal a * (nearestNucleusDistance R x)⁻¹ ≤ nearestNucleusCutoff a r R x + ENNReal.ofReal (a / r)

The cutoff plus its constant tail controls the inverse nearest distance everywhere.

theorem LiebThirring.Assembly.nearestNucleusCutoff_rpow_le_sum {M : ℕ} (a r : ℝ) (hr : 0 < r) (R : Fin M → Position) (x : Position) : nearestNucleusCutoff a r R x ^ (5 / 2) ≤ ∑ k : Fin M, nucleusCutoff a r (R k) x ^ (5 / 2)

A nearest-distance cutoff power is bounded pointwise by the sum of one-center powers.

theorem LiebThirring.Assembly.lintegral_nearestNucleusCutoff_rpow_le {M : ℕ} (a r : ℝ) (ha : 0 ≤ a) (hr : 0 < r) (R : Fin M → Position) : ∫⁻ (x : Position), nearestNucleusCutoff a r R x ^ (5 / 2) ≤ ENNReal.ofReal (8 * Real.pi * ↑M * a ^ (5 / 2) * √r)

The cutoff power integral of the nearest-nucleus cutoff, uniformly over all nuclear configurations.