Full and partial Fourier factorization #
Outer Fourier transform acts on the spatial factor of a curried tensor.
Rest-coordinate Fourier transforms act on the remaining factor of a tensor.
theorem
LiebThirring.fourier_tensorInsertion
{N q : ℕ}
(i : Fin N)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
(v : ↥(RestState i q))
:
Outer Fourier transform acts on the spatial factor of a curried tensor.
theorem
LiebThirring.restFourier_tensorInsertion
{N q : ℕ}
(i : Fin N)
(f : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume))
(v : ↥(RestState i q))
:
(↑↑(restFourierLinearIsometryEquiv i)).compLp ((tensorInsertion f) v) = (tensorInsertion f) (FourierTransform.fourier v)
Rest-coordinate Fourier transforms act on the remaining factor of a tensor.
theorem
LiebThirring.oneParticleCurrying_fourier_insertion_toLp
{N q : ℕ}
(i : Fin N)
(f : SchwartzMap Position (EuclideanSpace ℂ (Fin q)))
(v : SchwartzMap (OtherConfiguration i) (EuclideanSpace ℂ (OtherSpinLabels i q)))
:
(oneParticleCurrying i)
(FourierTransform.fourier
((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume))) = (↑↑(restFourierLinearIsometryEquiv i)).compLp
(FourierTransform.fourier
((oneParticleCurrying i)
((oneParticleInsertion i (f.toLp 2 MeasureTheory.volume)) (v.toLp 2 MeasureTheory.volume))))
The full/partial factorization on the smooth tensor core.
theorem
LiebThirring.oneParticleCurrying_fourier
{N q : ℕ}
(i : Fin N)
(ψ : State N q)
:
(oneParticleCurrying i) (FourierTransform.fourier ψ) = (↑↑(restFourierLinearIsometryEquiv i)).compLp (FourierTransform.fourier ((oneParticleCurrying i) ψ))
Exact unweighted Fourier factorization factorization as an equality of L² classes.
theorem
LiebThirring.norm_oneParticleCurrying_fourier_ae
{N q : ℕ}
(i : Fin N)
(ψ : State N q)
:
∀ᵐ (ξ : Position), ‖↑↑((oneParticleCurrying i) (FourierTransform.fourier ψ)) ξ‖₊ = ‖↑↑(FourierTransform.fourier ((oneParticleCurrying i) ψ)) ξ‖₊
Currying the full Fourier transform and partial Fourier have identical fiber norms a.e.
theorem
LiebThirring.particleFourierEnergy_eq_partialFourier
{N q : ℕ}
(i : Fin N)
(ψ : State N q)
:
particleFourierEnergy ψ i = ∫⁻ (ξ : Position), ENNReal.ofReal ((2 * Real.pi) ^ 2) * ↑‖ξ‖₊ ^ 2 * ↑‖↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position (OneParticleFiber i q)) ((oneParticleCurrying i) ψ)) ξ‖₊ ^ 2
The particle energy equals the partial Fourier kinetic integral, including infinite energy.