Pointwise low fields and one-particle contraction #
The negative Fourier phase in the one-spin test becomes the positive inverse phase under the adjoint contraction. The equality is in the Hilbert fiber at every spatial point, without pointwise claims about state slices.
theorem
LiebThirring.lowFourierField_component_eq_of_fourier_ae
{ι : Type u_1}
{H : Type u_2}
[Fintype ι]
[DecidableEq ι]
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(h : ↥(MeasureTheory.Lp (PiLp 2 fun (x : ι) => H) 2 MeasureTheory.volume))
(E : ℝ)
(hE : 0 ≤ E)
(x : Position)
(s : ι)
(g : ↥(MeasureTheory.Lp (EuclideanSpace ℂ ι) 2 MeasureTheory.volume))
(hg :
↑↑(FourierTransform.fourier g) =ᵐ[MeasureTheory.volume]
(lowMomentumRegion E).indicator fun (ξ : Position) => EuclideanSpace.single s ↑(Real.fourierChar (-inner ℝ ξ x)))
:
A one-spin negative-phase Fourier test contracts to the continuous low field component. The representative premise characterizes the test, rather than assuming a low-momentum estimate.
theorem
LiebThirring.lowFourierField_density_component_eq
{N q : ℕ}
(i : Fin N)
(ψ : State N q)
(E : ℝ)
(hE : 0 ≤ E)
(x : Position)
(s : Fin q)
:
(lowFourierField (densityField i ψ) E x).ofLp s = ↑√↑N • (oneParticleContraction i (lowMomentumTest E x s hE)) ψ
The exact the low-momentum bound test contracts to the scaled density-field component.
theorem
LiebThirring.lowFourierField_density_component_norm_sq
{N q : ℕ}
(i : Fin N)
(ψ : State N q)
(E : ℝ)
(hE : 0 ≤ E)
(x : Position)
(s : Fin q)
:
‖(lowFourierField (densityField i ψ) E x).ofLp s‖ ^ 2 = ↑N * ‖(oneParticleContraction i (lowMomentumTest E x s hE)) ψ‖ ^ 2
Squared component norm in the exact normalization used by the Pauli bound.