Conditional bounded-charge Baxter inequality #
Weak Baxter for arbitrary bounded nonnegative charges, conditional only on the exact equal-charge Baxter proposition.
theorem
LiebThirring.Assembly.weakBaxter_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 M : ℕ)
(Z : NNReal)
(z : Fin M → NNReal)
(R : Fin M → Position)
(x : Configuration N)
(hz : ∀ (k : Fin M), z k ≤ Z)
:
Weak Baxter for arbitrary bounded nonnegative charges, conditional only on the exact equal-charge Baxter proposition.