Radial normalization of the regularized Coulomb density

The elementary radial antiderivative in the fundamental solution's normalization argument, at unit scale.

The radial primitive tends to one at infinity.

theorem LiebThirring.hasDerivAt_coulomb_radial_primitive (r : ℝ) : HasDerivAt (fun (t : ℝ) => t ^ 3 * (t ^ 2 + 1) ^ (-(3 / 2))) (3 * r ^ 2 * (r ^ 2 + 1) ^ (-(5 / 2))) r

The elementary radial antiderivative in the fundamental solution's normalization argument, at unit scale.

theorem LiebThirring.tendsto_coulomb_radial_primitive : Filter.Tendsto (fun (r : ℝ) => r ^ 3 * (r ^ 2 + 1) ^ (-(3 / 2))) Filter.atTop (nhds 1)

The radial primitive tends to one at infinity.

theorem LiebThirring.coulomb_radial_integrable_integral : MeasureTheory.IntegrableOn (fun (r : ℝ) => 3 * r ^ 2 * (r ^ 2 + 1) ^ (-(5 / 2))) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (r : ℝ) in Set.Ioi 0, 3 * r ^ 2 * (r ^ 2 + 1) ^ (-(5 / 2)) = 1

The radial Jacobian times the unit density is integrable and has integral one.

theorem LiebThirring.integrable_coulombApproximationDensity_one : MeasureTheory.Integrable (coulombApproximationDensity 1) MeasureTheory.volume

The unit-scale regularization density is integrable on physical three-space.

theorem LiebThirring.integral_coulombApproximationDensity_one : ∫ (x : Position), coulombApproximationDensity 1 x = 4 * Real.pi

The regularization density has the exact Coulomb normalization 4π at unit scale.