Exact kinetic layer cake

The Fourier density-field energy equals the kinetic energy and its extended high-field layer cake. The two half-line conventions differ only at the null zero cutoff.

theorem LiebThirring.kineticEnergy_eq_densityField_layerCake {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : kineticEnergy ψ = ∫⁻ (E : ℝ) in Set.Ici 0, ∫⁻ (x : Position), ‖highFourierField (densityField i ψ) E x‖ₑ ^ 2

the layer cake extended layer-cake identity on the nonnegative real half-line.

theorem LiebThirring.kineticEnergy_eq_densityField_layerCake_Ioi {N q : ℕ} (i : Fin N) (ψ : State N q) (hψ : antisymmetric ψ) : kineticEnergy ψ = ∫⁻ (E : ℝ) in Set.Ioi 0, ∫⁻ (x : Position), ‖highFourierField (densityField i ψ) E x‖ₑ ^ 2

The positive half-line convention consumed by the scalar Rumin integral.