Integrated weak Baxter inequality

Testing nearest-nucleus control against a state yields the density integral.

The integrated weak Baxter bound, conditional on the exact Baxter proposition, for every normalized state and bounded-charge configuration.

theorem LiebThirring.Assembly.lintegral_nearestNucleusControl {N q M : ℕ} (Z : NNReal) (R : Fin M → Position) (ψ : State N q) : ∫⁻ (X : Configuration N), nearestNucleusControl Z R X * ↑‖↑↑ψ X‖₊ ^ 2 = (2 * ↑Z + 1) * ∫⁻ (x : Position), (nearestNucleusDistance R x)⁻¹ * density ψ x

Testing nearest-nucleus control against a state yields the density integral.

theorem LiebThirring.Assembly.integratedBaxter_of_baxter (hB : ∀ (N M : ℕ) (Z : NNReal) (R : Fin M → Position) (x : Configuration N), attraction (fun (x : Fin M) => Z) R x + baxterCorrection Z R ≤ electronRepulsion x + nuclearRepulsion (fun (x : Fin M) => Z) R + nearestNucleusControl Z R x) {N q M : ℕ} (Z : NNReal) (z : Fin M → NNReal) (R : Fin M → Position) (ψ : State N q) (hz : ∀ (k : Fin M), z k ≤ Z) (hψ : ‖ψ‖ = 1) : ∫⁻ (X : Configuration N), attraction z R X * ↑‖↑↑ψ X‖₊ ^ 2 ≤ (∫⁻ (X : Configuration N), electronRepulsion X * ↑‖↑↑ψ X‖₊ ^ 2) + nuclearRepulsion z R + (2 * ↑Z + 1) * ∫⁻ (x : Position), (nearestNucleusDistance R x)⁻¹ * density ψ x

The integrated weak Baxter bound, conditional on the exact Baxter proposition, for every normalized state and bounded-charge configuration.