Local planar Coulomb integration

The truncated radial inverse-distance integrand is Borel measurable.

Exact planar Coulomb integral with arbitrary nonnegative normal height.

theorem LiebThirring.measurable_truncated_planar_coulomb (h ε : ℝ) : Measurable fun (r : ℝ) => if √(r ^ 2 + h ^ 2) < ε then (ENNReal.ofReal √(r ^ 2 + h ^ 2))⁻¹ else 0

The truncated radial inverse-distance integrand is Borel measurable.

theorem LiebThirring.lintegral_planar_coulomb_cutoff (h ε : ℝ) (hh : 0 ≤ h) : (∫⁻ (q : Planar), if √(‖q‖ ^ 2 + h ^ 2) < ε then (ENNReal.ofReal √(‖q‖ ^ 2 + h ^ 2))⁻¹ else 0) = ENNReal.ofReal (2 * Real.pi * max (ε - h) 0)

Exact planar Coulomb integral with arbitrary nonnegative normal height.

theorem LiebThirring.lintegral_coulombKernel_ball_planeMeasure_eq (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) (ε : ℝ) : ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂planeMeasure F = ENNReal.ofReal (2 * Real.pi * max (ε - planeHeight n b x) 0)

Exact local Coulomb mass in a plane at any centre, on or off the plane.

theorem LiebThirring.lintegral_coulombKernel_ball_planeMeasure_le (n b x : Position) (hn : ‖n‖ = 1) (F : PlaneFrame (affinePlane n b)) {ε : ℝ} (hε : 0 < ε) : ∫⁻ (y : Position) in Metric.ball x ε, coulombKernel x y ∂planeMeasure F ≤ ENNReal.ofReal (2 * Real.pi * ε)

The local planar Coulomb bound, including off-plane centres and the infinite diagonal value of the Coulomb kernel.