Smooth cell representatives and harmonicity

The explicit smooth representative associated to a nearest-nucleus cell.

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

The explicit smooth representative associated to a nearest-nucleus cell.

Equations

• LiebThirring.screenedCellPotential Z R k x = ∑ p ∈ Finset.univ.erase k, ↑Z * ‖x - R p‖⁻¹

theorem LiebThirring.contDiffAt_screenedCellPotential {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) (n : WithTop ℕ∞) : ContDiffAt ℝ n (screenedCellPotential Z R k) x

theorem LiebThirring.screenedPotentialReal_eq_screenedCellPotential {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 = screenedCellPotential Z R k x

theorem LiebThirring.harmonicAt_inv_nuclear_distance (y x : Position) (hx : x ≠ y) : InnerProductSpace.HarmonicAt (fun (z : Position) => ‖z - y‖⁻¹) x

theorem LiebThirring.harmonicAt_screenedCellPotential {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : InnerProductSpace.HarmonicAt (screenedCellPotential Z R k) x