The volume majorant for the exterior cutoff limit

Exact radial mass outside the closed positive-radius threshold.

Translation-invariant exact inverse-fourth mass outside a positive-radius ball.

theorem LiebThirring.lintegral_inverse_fourth_outside_origin_ball (a : ℝ) (ha : 0 < a) : (∫⁻ (x : Position), if a ≤ ‖x‖ then ENNReal.ofReal (1 / ‖x‖ ^ 4) else 0) = ENNReal.ofReal (4 * Real.pi / a)

Exact radial mass outside the closed positive-radius threshold.

theorem LiebThirring.lintegral_inverse_fourth_outside_ball (c : Position) (a : ℝ) (ha : 0 < a) : ∫⁻ (x : Position) in (Metric.ball c a)ᶜ, ENNReal.ofReal (1 / ‖x - c‖ ^ 4) = ENNReal.ofReal (4 * Real.pi / a)

Translation-invariant exact inverse-fourth mass outside a positive-radius ball.

theorem LiebThirring.integrableOn_inverse_fourth_outside_ball (c : Position) (a : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (x : Position) => 1 / ‖x - c‖ ^ 4) (Metric.ball c a)ᶜ MeasureTheory.volume

Integrability of the inverse-fourth kernel outside a positive-radius ball.

theorem LiebThirring.integrableOn_inverse_fourth_exterior_of_ball_subset {M : ℕ} (R : Fin M → Position) (k : Fin M) (a : ℝ) (ha : 0 < a) (hball : Metric.ball (R k) a ⊆ voronoiCell R k) : MeasureTheory.IntegrableOn (fun (x : Position) => 1 / ‖x - R k‖ ^ 4) (voronoiCell R k)ᶜ MeasureTheory.volume

Any ball contained in a Voronoi cell gives the exterior volume majorant.