The scalar Newton angular integral

The elementary height integral used to evaluate the potential of a spherical shell.

theorem LiebThirring.intervalIntegrable_newton_rpow {u r : ℝ} (hu : 0 < u) (hr : 0 < r) : IntervalIntegrable (fun (t : ℝ) => (u ^ 2 + r ^ 2 - 2 * u * r * t) ^ (-(1 / 2))) MeasureTheory.volume (-1) 1

Integrability of the real power after the Newton affine substitution.

theorem LiebThirring.integral_newton_rpow {u r : ℝ} (hu : 0 < u) (hr : 0 < r) : ∫ (t : ℝ) in -1..1, (u ^ 2 + r ^ 2 - 2 * u * r * t) ^ (-(1 / 2)) = 2 / max u r

Real-valued angular integral for a positive observation radius.

theorem LiebThirring.newton_polynomial_pos {u r t : ℝ} (hu : 0 < u) (hr : 0 < r) (ht : t < 1) : 0 < u ^ 2 + r ^ 2 - 2 * u * r * t

The squared distance is positive before the possibly singular right endpoint.

theorem LiebThirring.lintegral_newton_rpow {u r : ℝ} (hu : 0 < u) (hr : 0 < r) : ∫⁻ (t : ℝ) in Set.Icc (-1) 1, (ENNReal.ofReal √(u ^ 2 + r ^ 2 - 2 * u * r * t))⁻¹ = ENNReal.ofReal (2 / max u r)

Evaluation of the extended integral, retaining its possibly infinite endpoint value.

theorem LiebThirring.newton_angular_integral {u r : ℝ} (hu : 0 ≤ u) (hr : 0 < r) : (ENNReal.ofReal 2)⁻¹ * ∫⁻ (t : ℝ) in Set.Icc (-1) 1, (ENNReal.ofReal √(u ^ 2 + r ^ 2 - 2 * u * r * t))⁻¹ = (ENNReal.ofReal (max u r))⁻¹

The one-dimensional Newton average, including the singular endpoint when u = r.