Scalar radial mass integral for a planar face charge

Radial integration of r / (sqrt (r² + a²))³ at positive height gives the planar mass calculation.

theorem LiebThirring.hasDerivAt_faceDensity_primitive (a r : ℝ) (ha : 0 < a) : HasDerivAt (fun (t : ℝ) => -(√(t ^ 2 + a ^ 2))⁻¹) (r / √(r ^ 2 + a ^ 2) ^ 3) r

The primitive of the radial planar face density.

theorem LiebThirring.tendsto_faceDensity_primitive_atTop (a : ℝ) : Filter.Tendsto (fun (r : ℝ) => -(√(r ^ 2 + a ^ 2))⁻¹) Filter.atTop (nhds 0)

The radial primitive tends to zero at infinity.

theorem LiebThirring.integrableOn_faceDensity_radial (a : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r / √(r ^ 2 + a ^ 2) ^ 3) (Set.Ioi 0) MeasureTheory.volume

The radial planar face density is integrable on the positive half-line.

theorem LiebThirring.integral_faceDensity_radial (a : ℝ) (ha : 0 < a) : ∫ (r : ℝ) in Set.Ioi 0, r / √(r ^ 2 + a ^ 2) ^ 3 = a⁻¹

Exact real radial mass integral at positive height.

theorem LiebThirring.lintegral_faceDensity_radial (a : ℝ) (ha : 0 < a) : ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (r / √(r ^ 2 + a ^ 2) ^ 3) = ENNReal.ofReal a⁻¹

Exact extended nonnegative radial mass integral at positive height.