Assembly of the energy deficit from the potential and exterior-flux identities

The exterior flux identity, cutoff passage, geometric lower bound, and charge coefficients combine with the screened-potential identity to give the energy deficit.

theorem LiebThirring.half_energy_add_exterior_integrals_eq_repulsion_of_potential_eq_and_exterior_flux {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) (hFlux : ∀ (k : Fin M), ∫⁻ (x : Position) in (voronoiCell R k)ᶜ, ENNReal.ofReal (‖x - R k‖ ^ 4)⁻¹ = ∑ l : { l : Fin M // l ≠ k }, ∫⁻ (y : Position) in voronoiFace R k ↑l, ENNReal.ofReal (nuclearHalfDistance R k ↑l / ‖y - R k‖ ^ 4) ∂bisectorSurfaceMeasure R hR k ↑l ⋯) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + ENNReal.ofReal (↑Z ^ 2 / (8 * Real.pi)) * ∑ k : Fin M, ∫⁻ (x : Position) in (voronoiCell R k)ᶜ, ENNReal.ofReal (‖x - R k‖ ^ 4)⁻¹ = nuclearRepulsion (fun (x : Fin M) => Z) R

The exact exterior expression once the potential identity and the exterior flux calculation are supplied. This is a conditional assembly helper.

theorem LiebThirring.energyDeficit_of_potential_eq_and_exterior_flux {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) (hFlux : 2 ≤ M → ∀ (k : Fin M), ∫⁻ (x : Position) in (voronoiCell R k)ᶜ, ENNReal.ofReal (‖x - R k‖ ^ 4)⁻¹ = ∑ l : { l : Fin M // l ≠ k }, ∫⁻ (y : Position) in voronoiFace R k ↑l, ENNReal.ofReal (nuclearHalfDistance R k ↑l / ‖y - R k‖ ^ 4) ∂bisectorSurfaceMeasure R hR k ↑l ⋯) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + baxterCorrection Z R ≤ nuclearRepulsion (fun (x : Fin M) => Z) R

The exact square-completion input conditional on the potential and exterior-flux identities. The extra exterior-flux premise is displayed in the name and statement.

theorem LiebThirring.energyDeficit_of_potential_eq_and_compact_flux {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) (hCompactFlux : ∀ (k : Fin M) (V : Position → Position), ContDiff ℝ 1 V → HasCompactSupport V → ∫ (x : Position) in (voronoiCell R k)ᶜ, positionDivergence V x = -∑ l : { l : Fin M // l ≠ k }, ∫ (y : Position) in voronoiFace R k ↑l, inner ℝ (bisectorNormal R k ↑l) (V y) ∂bisectorSurfaceMeasure R hR k ↑l ⋯) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + baxterCorrection Z R ≤ nuclearRepulsion (fun (x : Fin M) => Z) R

A reusable assembly of the square-completion input from potential equality and a compact-field flux identity.

theorem LiebThirring.energyDeficit_of_potential_eq {M : ℕ} (hM : 1 ≤ M) (Z : NNReal) (R : Fin M → Position) (hR : Function.Injective R) (hPhi : ∀ (x : Position), screenedPotential Z R x = coulombPotential (voronoiFaceMeasure R hR ↑Z) x) : coulombEnergy (voronoiFaceMeasure R hR ↑Z) (voronoiFaceMeasure R hR ↑Z) / 2 + baxterCorrection Z R ≤ nuclearRepulsion (fun (x : Fin M) => Z) R

The nearest-nucleus energy deficit used in square completion. The potential identity is the only analytic hypothesis; compact-field flux, the cutoff limit and the half-space lower bound are supplied by proved theorems. The one-nucleus case is included.