Integrable boundary majorant for the exterior inverse-square flux

Exact planar radial inverse-fourth mass with its flux numerator.

Exact whole-plane integral of the positive inverse-square flux density.

theorem LiebThirring.lintegral_planar_inverse_fourth_flux (a : ℝ) (ha : 0 < a) : ∫⁻ (q : Planar), ENNReal.ofReal (a / (‖q‖ ^ 2 + a ^ 2) ^ 2) = ENNReal.ofReal (Real.pi / a)

Exact planar radial inverse-fourth mass with its flux numerator.

theorem LiebThirring.lintegral_plane_inverse_fourth_flux (n b c : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (ha : 0 < planeHeight n b c) : ∫⁻ (y : Position), ENNReal.ofReal (planeHeight n b c / ‖y - c‖ ^ 4) ∂planeMeasure F = ENNReal.ofReal (Real.pi / planeHeight n b c)

Exact whole-plane integral of the positive inverse-square flux density.

theorem LiebThirring.integrable_plane_inverse_fourth_flux (n b c : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (ha : 0 < planeHeight n b c) : MeasureTheory.Integrable (fun (y : Position) => planeHeight n b c / ‖y - c‖ ^ 4) (planeMeasure F)

The full-plane flux majorant is Bochner integrable.