Fiber Fourier transform and weighted currying

Fourier transform on every remaining-spin Hilbert component.

The full Fourier particle integral equals the weighted norm of its curried full Fourier transform, without any finite-energy assumption.

noncomputable def LiebThirring.restFourierLinearIsometryEquiv {N q : ℕ} (i : Fin N) : OneParticleFiber i q ≃ₗᵢ[ℂ] OneParticleFiber i q

Fourier transform on every remaining-spin Hilbert component.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.particleFourierEnergy_eq_currying_fullFourier {N q : ℕ} (i : Fin N) (ψ : State N q) : particleFourierEnergy ψ i = ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((oneParticleCurrying i) (FourierTransform.fourier ψ)) ξ‖₊ ^ 2

The full Fourier particle integral equals the weighted norm of its curried full Fourier transform, without any finite-energy assumption.