Exact inverse-fourth mass of an exterior half-space

The inverse-fourth planar slice has mass π/s² at positive normal height.

In the volume-preserving height coordinates the inverse-fourth kernel has its literal radial denominator.

theorem LiebThirring.lintegral_planar_inverse_fourth (s : ℝ) (hs : 0 < s) : ∫⁻ (q : Planar), ENNReal.ofReal ((s ^ 2 + ‖q‖ ^ 2) ^ 2)⁻¹ = ENNReal.ofReal (Real.pi / s ^ 2)

The inverse-fourth planar slice has mass π/s² at positive normal height.

theorem LiebThirring.inverse_fourth_sphereHeightSplit (p : ℝ × Planar) : ‖sphereHeightSplit.symm p‖ ^ 4 = (p.1 ^ 2 + ‖p.2‖ ^ 2) ^ 2

In the volume-preserving height coordinates the inverse-fourth kernel has its literal radial denominator.

theorem LiebThirring.lintegral_inverse_fourth_coordinate_halfSpace {a : ℝ} (ha : 0 < a) : ∫⁻ (x : Position) in {x : Position | a ≤ x.ofLp 2}, ENNReal.ofReal (‖x‖ ^ 4)⁻¹ = ENNReal.ofReal (Real.pi / a)

Exact inverse-fourth volume integral in the canonical coordinate half-space.

theorem LiebThirring.lintegral_inverse_fourth_halfSpace (n c : Position) (hn : ‖n‖ = 1) {a : ℝ} (ha : 0 < a) : ∫⁻ (x : Position) in {x : Position | a ≤ inner ℝ n (x - c)}, ENNReal.ofReal (‖x - c‖ ^ 4)⁻¹ = ENNReal.ofReal (Real.pi / a)

Exact inverse-fourth volume mass of an exterior half-space with arbitrary unit normal and arbitrary centre. This is the energy deficit, equation.

theorem LiebThirring.lintegral_inverse_fourth_halfSpace_le_of_subset (n c : Position) (hn : ‖n‖ = 1) {a : ℝ} (ha : 0 < a) (E : Set Position) (hE : {x : Position | a ≤ inner ℝ n (x - c)} ⊆ E) : ENNReal.ofReal (Real.pi / a) ≤ ∫⁻ (x : Position) in E, ENNReal.ofReal (‖x - c‖ ^ 4)⁻¹

The exact mass supplies the lower bound used by the nearest-nucleus argument.