Global bounds for the screened potential

An explicit finite bound valid throughout space, including at nuclei.

The nuclear configuration fits inside a ball of some nonnegative radius.

theorem LiebThirring.screenedPotentialReal_le_cell_bound {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : screenedPotentialReal Z R x ≤ ∑ p ∈ Finset.univ.erase k, 2 * ↑Z / ‖R p - R k‖

theorem LiebThirring.screenedPotentialReal_le_global_bound {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (x : Position) : screenedPotentialReal Z R x ≤ ∑ k : Fin M, ∑ p ∈ Finset.univ.erase k, 2 * ↑Z / ‖R p - R k‖

An explicit finite bound valid throughout space, including at nuclei.

theorem LiebThirring.bounded_screenedPotentialReal {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : ∃ (C : ℝ), ∀ (x : Position), |screenedPotentialReal Z R x| ≤ C

theorem LiebThirring.exists_nuclear_radius {M : ℕ} (R : Fin M → Position) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ (k : Fin M), ‖R k‖ ≤ A

The nuclear configuration fits inside a ball of some nonnegative radius.

theorem LiebThirring.half_norm_le_nuclear_distance {M : ℕ} (R : Fin M → Position) {A : ℝ} (hA : ∀ (k : Fin M), ‖R k‖ ≤ A) {x : Position} (hx : 2 * A ≤ ‖x‖) (k : Fin M) : ‖x‖ / 2 ≤ ‖x - R k‖

Outside twice a ball containing the nuclei, every denominator is large.

theorem LiebThirring.screenedPotentialReal_le_decay {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) {A : ℝ} (hA : ∀ (k : Fin M), ‖R k‖ ≤ A) {x : Position} (hx : 2 * A ≤ ‖x‖) (hxpos : 0 < ‖x‖) : screenedPotentialReal Z R x ≤ 2 * ↑(M - 1) * ↑Z / ‖x‖

The explicit O(1/|x|) estimate of screened-potential regularity.

theorem LiebThirring.exists_screenedPotentialReal_le_one_add_norm {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Position), |screenedPotentialReal Z R x| ≤ C / (1 + ‖x‖)

A global version of the decay estimate, with denominator 1 + |x|.