Coulomb interactions

Electron and nuclear interactions, nearest-nucleus distances, and the electrostatic correction in Baxter’s inequality.

noncomputable def LiebThirring.coulombKernel (x y : Position) : ENNReal

Nonnegative Coulomb interaction, with infinite value at a collision.

Equations

• LiebThirring.coulombKernel x y = (ENNReal.ofReal ‖x - y‖)⁻¹

noncomputable def LiebThirring.electronRepulsion {N : ℕ} (x : Configuration N) : ENNReal

Sum the Coulomb interactions over each unordered pair of electrons.

Equations

• LiebThirring.electronRepulsion x = ∑ i : Fin N, ∑ j : Fin N with i < j, LiebThirring.coulombKernel (LiebThirring.particlePosition x i) (LiebThirring.particlePosition x j)

noncomputable def LiebThirring.attraction {N M : ℕ} (z : Fin M → NNReal) (R : Fin M → Position) (x : Configuration N) : ENNReal

Sum electron–nucleus Coulomb interactions weighted by the nuclear charges.

Equations

• LiebThirring.attraction z R x = ∑ i : Fin N, ∑ k : Fin M, ↑(z k) * LiebThirring.coulombKernel (LiebThirring.particlePosition x i) (R k)

noncomputable def LiebThirring.nuclearRepulsion {M : ℕ} (z : Fin M → NNReal) (R : Fin M → Position) : ENNReal

Sum the charge-weighted Coulomb interactions over unordered pairs of nuclei.

Equations

• LiebThirring.nuclearRepulsion z R = ∑ k : Fin M, ∑ l : Fin M with k < l, ↑(z k) * ↑(z l) * LiebThirring.coulombKernel (R k) (R l)

noncomputable def LiebThirring.nearestNucleusDistance {M : ℕ} (R : Fin M → Position) (x : Position) : ENNReal

The nearest nuclear distance, with infinite value when there are no nuclei.

Equations

• LiebThirring.nearestNucleusDistance R x = ⨅ (k : Fin M), ENNReal.ofReal ‖x - R k‖

noncomputable def LiebThirring.nearestOtherNucleusDistance {M : ℕ} (R : Fin M → Position) (k : Fin M) : ENNReal

The nearest distance to another nucleus, with infinite value for a single nucleus.

Equations

• LiebThirring.nearestOtherNucleusDistance R k = ⨅ (l : { l : Fin M // l ≠ k }), ENNReal.ofReal ‖R k - R ↑l‖

noncomputable def LiebThirring.nearestNucleusControl {N M : ℕ} (Z : NNReal) (R : Fin M → Position) (x : Configuration N) : ENNReal

Nearest-nucleus inverse-distance control with the electrostatic screening coefficient.

Equations

• LiebThirring.nearestNucleusControl Z R x = (2 * ↑Z + 1) * ∑ i : Fin N, (LiebThirring.nearestNucleusDistance R (LiebThirring.particlePosition x i))⁻¹

noncomputable def LiebThirring.baxterCorrection {M : ℕ} (Z : NNReal) (R : Fin M → Position) : ENNReal

The positive nearest-other-nucleus correction in Baxter’s inequality.

Equations

• LiebThirring.baxterCorrection Z R = ↑Z ^ 2 / 4 * ∑ k : Fin M, (LiebThirring.nearestOtherNucleusDistance R k)⁻¹

theorem LiebThirring.sum_ne_eq_two_sum_lt {α : Type u_1} [Fintype α] [LinearOrder α] (f : α → α → ENNReal) (hf : ∀ (i j : α), f i j = f j i) : (∑ i : α, ∑ j : α, if i ≠ j then f i j else 0) = 2 * ∑ i : α, ∑ j : α with i < j, f i j

An off-diagonal symmetric finite sum counts each upper-triangular term twice.

theorem LiebThirring.sum_eq_diag_add_two_sum_lt {α : Type u_1} [Fintype α] [LinearOrder α] (f : α → α → ENNReal) (hf : ∀ (i j : α), f i j = f j i) : ∑ i : α, ∑ j : α, f i j = ∑ i : α, f i i + 2 * ∑ i : α, ∑ j : α with i < j, f i j

A symmetric finite sum is its diagonal plus twice the upper triangle.