Approximate identity from the regularized Coulomb density

Scaling of the fundamental solution's regularization density in physical dimension three.

The density pairing can be evaluated after dilating about its pole.

theorem LiebThirring.coulombApproximationDensity_smul {ε : ℝ} (hε : 0 < ε) (x : Position) : coulombApproximationDensity ε (ε • x) = (ε ^ 3)⁻¹ * coulombApproximationDensity 1 x

Scaling of the fundamental solution's regularization density in physical dimension three.

theorem LiebThirring.integral_coulombApproximationDensity_sub_mul {ε : ℝ} (hε : 0 < ε) (f : Position → ℝ) (y : Position) : ∫ (x : Position), coulombApproximationDensity ε (x - y) * f x = ∫ (x : Position), coulombApproximationDensity 1 x * f (y + ε • x)

The density pairing can be evaluated after dilating about its pole.

theorem LiebThirring.tendsto_integral_coulombApproximationDensity_sub_mul {f : Position → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) (y : Position) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : Position), coulombApproximationDensity ε (x - y) * f x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (4 * Real.pi * f y))

The regularized density converges to a point mass of weight 4π.