Radial integration on the Euclidean carrier

Radial integration in physical Euclidean three-space, for nonnegative Borel functions.

theorem LiebThirring.lintegral_norm (g : ℝ → ENNReal) (hg : Measurable g) : ∫⁻ (x : Position), g ‖x‖ = ENNReal.ofReal (4 * Real.pi) * ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal (r ^ 2) * g r

Radial integration in physical Euclidean three-space, for nonnegative Borel functions.