Exact density-field Fourier energy

Extended multiplier in the same factorization as the energy.

Fourier of the scaled density field has exactly N times the squared norm.

theorem LiebThirring.ofReal_fourierKineticMultiplier (ξ : Position) : ENNReal.ofReal ((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2) = ENNReal.ofReal ((2 * Real.pi) ^ 2) * ‖ξ‖ₑ ^ 2

Extended multiplier in the same factorization as the energy.

theorem LiebThirring.densityField_fourier_enorm_sq_ae {N q : ℕ} (i : Fin N) (ψ : State N q) : ∀ᵐ (ξ : Position), ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (OneParticleFiber i q)) (densityField i ψ)) ξ‖ₑ ^ 2 = ↑N * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (OneParticleFiber i q)) ((oneParticleCurrying i) ψ)) ξ‖ₑ ^ 2

Fourier of the scaled density field has exactly N times the squared norm.

theorem LiebThirring.kineticEnergy_eq_densityField_fourier {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : kineticEnergy ψ = ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2) * ‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (OneParticleFiber i q)) (densityField i ψ)) ξ‖ₑ ^ 2

The literal density-field Fourier energy is the full kinetic energy.