Energies, comparison, and regularity of spherical shells

Interacting with a point charge evaluates the potential at that point.

A point charge in the first energy argument also evaluates the potential.

theorem LiebThirring.coulombPotential_shell_le_kernel (a : Position) {r : ℝ} (hr : 0 < r) (x : Position) : coulombPotential (shell a r) x ≤ coulombKernel x a

Newton's potential is no greater than the potential of the center point.

theorem LiebThirring.coulombPotential_shell_of_radius_le (a : Position) {r : ℝ} (hr : 0 < r) (x : Position) (hx : r ≤ ‖x - a‖) : coulombPotential (shell a r) x = coulombKernel x a

Outside or on the shell, its potential equals the point-charge potential.

theorem LiebThirring.coulombEnergy_shell_self (a : Position) {r : ℝ} (hr : 0 < r) : coulombEnergy (shell a r) (shell a r) = (ENNReal.ofReal r)⁻¹

The self-energy has no factor 1/2, in accordance with the shared definition.

theorem LiebThirring.coulombEnergy_shell_le_kernel (a b : Position) {r s : ℝ} (hr : 0 < r) (hs : 0 < s) : coulombEnergy (shell a r) (shell b s) ≤ coulombKernel a b

Spherical smearing decreases mutual Coulomb energy, even for coincident centers.