Trivial cases of the energy deficit

The square-completion deficit input is unconditional when the charge is zero.

The square-completion deficit input for one nucleus is entirely unconditional.

@[simp]

theorem LiebThirring.baxterCorrection_one (Z : NNReal) (R : Fin 1 → Position) : baxterCorrection Z R = 0

@[simp]

theorem LiebThirring.nuclearRepulsion_one (Z : NNReal) (R : Fin 1 → Position) : nuclearRepulsion (fun (x : Fin 1) => Z) R = 0

theorem LiebThirring.energyDeficit_one (Z : NNReal) (R : Fin 1 → Position) (hR : Function.Injective R) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + baxterCorrection Z R ≤ nuclearRepulsion (fun (x : Fin 1) => Z) R

The square-completion deficit input for one nucleus is entirely unconditional.