Finiteness and continuity of the screened potential

The extended screened potential and its real representative agree on their finite locus.

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

The real form of the shared extended screened potential.

Equations

• LiebThirring.screenedPotentialReal Z R x = (LiebThirring.screenedPotential Z R x).toReal

theorem LiebThirring.nuclear_separation_le_twice_dist {M : ℕ} (R : Fin M → Position) (k p : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : ‖R p - R k‖ ≤ 2 * ‖x - R p‖

Every retained pole is separated from a closed nearest-nucleus cell.

theorem LiebThirring.ne_nucleus_of_mem_closedVoronoiCell {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k p : Fin M) (hpk : p ≠ k) {x : Position} (hx : x ∈ closedVoronoiCell R k) : x ≠ R p

theorem LiebThirring.screenedPotential_eq_on_closedVoronoiCell {M : ℕ} (Z : NNReal) (R : Fin M → Position) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : screenedPotential Z R x = ∑ p ∈ Finset.univ.erase k, ↑Z * coulombKernel x (R p)

The shared minimum is the explicit formula on every closed cell.

theorem LiebThirring.screenedPotential_ne_top {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (x : Position) : screenedPotential Z R x ≠ ⊤

Distinct nuclei make the screened potential finite even at a nucleus.

theorem LiebThirring.continuous_screenedPotential {M : ℕ} (Z : NNReal) (R : Fin M → Position) : Continuous (screenedPotential Z R)

Extended continuity also holds without separation of the nuclei.

theorem LiebThirring.continuous_screenedPotentialReal {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) : Continuous (screenedPotentialReal Z R)

theorem LiebThirring.screenedPotentialReal_eq_on_closedVoronoiCell {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, ↑Z * ‖x - R p‖⁻¹

The real closed-cell formula has no singular retained denominators.

theorem LiebThirring.screenedPotentialReal_nonneg {M : ℕ} (Z : NNReal) (R : Fin M → Position) (x : Position) : 0 ≤ screenedPotentialReal Z R x