The scalar radial Coulomb integral in a plane

The Coulomb radial primitive is differentiable at every point for positive height.

The real radial Coulomb integral at positive height.

theorem LiebThirring.hasDerivAt_sqrt_sq_add_sq (h x : ℝ) (hh : 0 < h) : HasDerivAt (fun (ρ : ℝ) => √(ρ ^ 2 + h ^ 2)) (x / √(x ^ 2 + h ^ 2)) x

The Coulomb radial primitive is differentiable at every point for positive height.

theorem LiebThirring.integral_coulomb_radial_of_pos (h R : ℝ) (hh : 0 < h) : ∫ (ρ : ℝ) in 0..R, ρ / √(ρ ^ 2 + h ^ 2) = √(R ^ 2 + h ^ 2) - h

The real radial Coulomb integral at positive height.

theorem LiebThirring.lintegral_coulomb_radial_Ioo (h R : ℝ) (hh : 0 ≤ h) (hR : 0 ≤ R) : ∫⁻ (ρ : ℝ) in Set.Ioo 0 R, ENNReal.ofReal ρ * (ENNReal.ofReal √(ρ ^ 2 + h ^ 2))⁻¹ = ENNReal.ofReal (√(R ^ 2 + h ^ 2) - h)

Exact nonnegative radial integral on an open interval, including zero height.

theorem LiebThirring.le_sqrt_sq_add_sq (h ρ : ℝ) (hh : 0 ≤ h) : h ≤ √(ρ ^ 2 + h ^ 2)

Distance from a point of the plane to a centre at height h is at least h.

theorem LiebThirring.lintegral_coulomb_radial (h ε : ℝ) (hh : 0 ≤ h) : (∫⁻ (ρ : ℝ) in Set.Ioi 0, ENNReal.ofReal ρ * if √(ρ ^ 2 + h ^ 2) < ε then (ENNReal.ofReal √(ρ ^ 2 + h ^ 2))⁻¹ else 0) = ENNReal.ofReal (max (ε - h) 0)

Exact truncated radial Coulomb integral for every nonnegative height.

This includes centres outside the ball (ε ≤ h), whose contribution is zero, and centres in the plane (h = 0), whose kernel is infinite at the origin. The radial origin is excluded by Ioi 0, as in planar polar coordinates.