Polar integration on the Euclidean plane

Planar polar integration for the singular Coulomb kernel.

theorem LiebThirring.lintegral_planar_norm (g : ℝ → ENNReal) (hg : Measurable g) : ∫⁻ (q : Planar), g ‖q‖ = ENNReal.ofReal (2 * Real.pi) * ∫⁻ (r : ℝ) in Set.Ioi 0, ENNReal.ofReal r * g r

Nonnegative radial integration on the Euclidean plane, with angular mass 2π.