Electron-pair expectations from the one-body Coulomb estimate

One-body Coulomb estimates and particle slicing control electron-pair expectations by the selected particle’s Fourier energy.

theorem LiebThirring.Assembly.instFactNeENNRealOfNatTop_leanPool_1 : Fact (2 ≠ ⊤)

theorem LiebThirring.Assembly.realForm_particlePosition_insert_ne {N : ℕ} (i j : Fin N) (hij : i ≠ j) (x : Position) (y : OtherConfiguration i) : particlePosition (insertParticle i x y) j = particlePosition (insertParticle i 0 y) j

Inserting one particle does not move any other particle.

theorem LiebThirring.Assembly.realForm_pair_lintegral_eq_slices {N q : ℕ} (i j : Fin N) (hij : i ≠ j) (ψ : State N q) : ∫⁻ (X : Configuration N), coulombKernel (particlePosition X i) (particlePosition X j) * ↑‖↑↑ψ X‖₊ ^ 2 = ∫⁻ (y : OtherConfiguration i) (x : Position), coulombKernel x (particlePosition (insertParticle i 0 y) j) * ↑‖↑↑(↑↑(realFormSwapCurrying (realFormParticleCurrying i ψ)) y) x‖₊ ^ 2

A pair expectation is the integral of the one-body expectations on the remaining-coordinate slices, with centre at the other particle.

theorem LiebThirring.Assembly.lintegral_pair_coulomb_le_of_one_body_bound {N q : ℕ} (hHardy : ∀ (c : Position) (u : ↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume)), ∫⁻ (x : Position), coulombKernel x c * ↑‖↑↑u x‖₊ ^ 2 ≤ ↑‖u‖₊ ^ 2 + 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (SpinAmplitudes N q)) u) ξ‖₊ ^ 2) (i j : Fin N) (hij : i ≠ j) (ψ : State N q) : ∫⁻ (X : Configuration N), coulombKernel (particlePosition X i) (particlePosition X j) * ↑‖↑↑ψ X‖₊ ^ 2 ≤ ↑‖ψ‖₊ ^ 2 + 4 * particleFourierEnergy ψ i

Conditional pair estimate: the input is the exact Hardy one-body Fourier Coulomb bound, specialized to the full finite spin space.

theorem LiebThirring.Assembly.realForm_particleFourierEnergy_le {N q : ℕ} (i : Fin N) (ψ : State N q) : particleFourierEnergy ψ i ≤ kineticEnergy ψ

Each particle energy is dominated by the total kinetic energy.

theorem LiebThirring.Assembly.lintegral_electronRepulsion_lt_top_of_one_body_bound {N q : ℕ} (hHardy : ∀ (c : Position) (u : ↥(MeasureTheory.Lp (SpinAmplitudes N q) 2 MeasureTheory.volume)), ∫⁻ (x : Position), coulombKernel x c * ↑‖↑↑u x‖₊ ^ 2 ≤ ↑‖u‖₊ ^ 2 + 4 * ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (SpinAmplitudes N q)) u) ξ‖₊ ^ 2) (ψ : State N q) (hT : kineticEnergy ψ < ⊤) : ∫⁻ (x : Configuration N), electronRepulsion x * ↑‖↑↑ψ x‖₊ ^ 2 < ⊤

Conditional finiteness of the electron repulsion on the finite kinetic form domain, with no symmetry or normalization required.