Newton's shell potential theorem

Newton’s shell formula holds at every observation point, including points on the shell. The proof uses normalized sphere measure and its height distribution.

theorem LiebThirring.coulombPotential_shell_center (a : Position) {r : ℝ} (hr : 0 ≤ r) : coulombPotential (shell a r) a = (ENNReal.ofReal r)⁻¹

The value at the shell center, including the infinite value at radius zero.

theorem LiebThirring.coulombKernel_shell_direction (a x : Position) {r : ℝ} (hr : 0 ≤ r) (hz : 0 < ‖x - a‖) (ω : ↑(Metric.sphere 0 1)) : coulombKernel x (a + r • ↑ω) = (ENNReal.ofReal √(‖x - a‖ ^ 2 + r ^ 2 - 2 * ‖x - a‖ * r * inner ℝ (↑ω) (‖x - a‖⁻¹ • (x - a))))⁻¹

The squared-distance reduction in the direction from the shell center to x.

theorem LiebThirring.coulombPotential_shell_angular (a : Position) {r : ℝ} (hr : 0 < r) (x : Position) : coulombPotential (shell a r) x = (ENNReal.ofReal 2)⁻¹ * ∫⁻ (t : ℝ) in Set.Icc (-1) 1, (ENNReal.ofReal √(‖x - a‖ ^ 2 + r ^ 2 - 2 * ‖x - a‖ * r * t))⁻¹

The shell potential is the Archimedes angular average, including zero observation radius.

theorem LiebThirring.coulombPotential_shell (a : Position) {r : ℝ} (hr : 0 < r) (x : Position) : coulombPotential (shell a r) x = (ENNReal.ofReal (max ‖x - a‖ r))⁻¹

Newton's formula for every point, including the center and the singular sphere.