Scalar integrals for the half-space inverse-fourth mass

Primitive for the planar radial inverse-fourth integrand.

The radial primitive vanishes at infinity.

theorem LiebThirring.hasDerivAt_inverse_fourth_radial (s r : ℝ) (hs : 0 < s) : HasDerivAt (fun (t : ℝ) => -(s ^ 2 + t ^ 2)⁻¹ / 2) (r / (s ^ 2 + r ^ 2) ^ 2) r

Primitive for the planar radial inverse-fourth integrand.

theorem LiebThirring.tendsto_inverse_fourth_radial_primitive (s : ℝ) : Filter.Tendsto (fun (r : ℝ) => -(s ^ 2 + r ^ 2)⁻¹ / 2) Filter.atTop (nhds 0)

The radial primitive vanishes at infinity.

theorem LiebThirring.integrableOn_inverse_fourth_radial (s : ℝ) (hs : 0 < s) : MeasureTheory.IntegrableOn (fun (r : ℝ) => r / (s ^ 2 + r ^ 2) ^ 2) (Set.Ioi 0) MeasureTheory.volume

The radial inverse-fourth integrand is integrable for positive height.

theorem LiebThirring.lintegral_inverse_fourth_radial (s : ℝ) (hs : 0 < s) : ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (r / (s ^ 2 + r ^ 2) ^ 2) = ENNReal.ofReal (1 / (2 * s ^ 2))

Exact nonnegative radial inverse-fourth mass at a positive height.

theorem LiebThirring.hasDerivAt_inverse_square_height (s : ℝ) (hs : 0 < s) : HasDerivAt (fun (t : ℝ) => -Real.pi / t) (Real.pi / s ^ 2) s

Primitive for the positive-height inverse-square integral.

theorem LiebThirring.integrableOn_inverse_square_height (a : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (s : ℝ) => Real.pi / s ^ 2) (Set.Ioi a) MeasureTheory.volume

The inverse-square height integrand is integrable away from zero.

theorem LiebThirring.lintegral_inverse_square_height (a : ℝ) (ha : 0 < a) : ∫⁻ (s : ℝ) in Set.Ici a, ENNReal.ofReal (Real.pi / s ^ 2) = ENNReal.ofReal (Real.pi / a)

Exact nonnegative inverse-square height integral, including its lower endpoint.