Globally smooth extensions of screened cell representatives

Small inner bumps remove the retained Coulomb poles. Their transition balls lie strictly outside the associated closed cell, so the extension agrees with the cell representative on a neighborhood of each point of that cell.

noncomputable def LiebThirring.screenedInnerBump (c : Position) (d : ℝ) (hd : 0 < d) : ContDiffBump c

Smooth cutoff around a nuclear position for removing its Coulomb singularity.

Equations

• LiebThirring.screenedInnerBump c d hd = { rIn := d / 8, rOut := d / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def LiebThirring.screenedSmoothInverse (c : Position) (d : ℝ) (hd : 0 < d) (x : Position) : ℝ

A smooth replacement of the inverse distance near a nuclear position.

Equations

• LiebThirring.screenedSmoothInverse c d hd x = (1 - ↑(LiebThirring.screenedInnerBump c d hd) x) * ‖x - c‖⁻¹

theorem LiebThirring.contDiff_screenedSmoothInverse (c : Position) (d : ℝ) (hd : 0 < d) : ContDiff ℝ (↑⊤) (screenedSmoothInverse c d hd)

theorem LiebThirring.eventuallyEq_screenedSmoothInverse (c x : Position) (d : ℝ) (hd : 0 < d) (hx : d / 4 < ‖x - c‖) : screenedSmoothInverse c d hd =ᶠ[nhds x] fun (y : Position) => ‖y - c‖⁻¹

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

Smooth extension of the screened potential from a closed Voronoi cell.

Equations

• LiebThirring.screenedCellSmooth Z R hR k x = ∑ p : { p : Fin M // p ≠ k }, ↑Z * LiebThirring.screenedSmoothInverse (R ↑p) ‖R ↑p - R k‖ ⋯ x

theorem LiebThirring.contDiff_screenedCellSmooth {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) : ContDiff ℝ (↑⊤) (screenedCellSmooth Z R hR k)

theorem LiebThirring.eventuallyEq_screenedCellSmooth {M : ℕ} (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (k : Fin M) {x : Position} (hx : x ∈ closedVoronoiCell R k) : screenedCellSmooth Z R hR k =ᶠ[nhds x] screenedCellPotential Z R k