One-particle test vectors for low Fourier fields

Literal Fourier-side spin test with negative phase.

The Fourier-side test has the norm of a constant unit-spin indicator.

noncomputable def LiebThirring.lowMomentumTestFourierFunction {q : ℕ} (E : ℝ) (x : Position) (s : Fin q) : Position → EuclideanSpace ℂ (Fin q)

Literal Fourier-side spin test with negative phase.

Equations

• LiebThirring.lowMomentumTestFourierFunction E x s = (LiebThirring.lowMomentumRegion E).indicator fun (ξ : LiebThirring.Position) => EuclideanSpace.single s ↑(Real.fourierChar (-inner ℝ ξ x))

theorem LiebThirring.norm_lowMomentumTestFourierFunction {q : ℕ} (E : ℝ) (x ξ : Position) (s : Fin q) : ‖lowMomentumTestFourierFunction E x s ξ‖ = ‖(lowMomentumRegion E).indicator (fun (x : Position) => EuclideanSpace.single s 1) ξ‖

The Fourier-side test has the norm of a constant unit-spin indicator.

theorem LiebThirring.stronglyMeasurable_lowMomentumTestFourierFunction {q : ℕ} (E : ℝ) (x : Position) (s : Fin q) : MeasureTheory.StronglyMeasurable (lowMomentumTestFourierFunction E x s)

Every Fourier-side test is strongly measurable.

theorem LiebThirring.memLp_lowMomentumTestFourierFunction {q : ℕ} (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : MeasureTheory.MemLp (lowMomentumTestFourierFunction E x s) 2 MeasureTheory.volume

Finite low-region volume makes the literal Fourier-side test an L² function.

noncomputable def LiebThirring.lowMomentumTestFrequencyClass {q : ℕ} (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)

The exact Fourier-side L² class of the cutoff spin test.

Equations

• LiebThirring.lowMomentumTestFrequencyClass E hE x s = MeasureTheory.MemLp.toLp (LiebThirring.lowMomentumTestFourierFunction E x s) ⋯

noncomputable def LiebThirring.lowMomentumTest {q : ℕ} (E : ℝ) (x : Position) (s : Fin q) (hE : 0 ≤ E) : ↥(MeasureTheory.Lp (EuclideanSpace ℂ (Fin q)) 2 MeasureTheory.volume)

The spatial one-particle cutoff test is inverse L² Fourier of its literal frequency class.

Equations

• LiebThirring.lowMomentumTest E x s hE = FourierTransformInv.fourierInv (LiebThirring.lowMomentumTestFrequencyClass E hE x s)

theorem LiebThirring.fourier_lowMomentumTest {q : ℕ} (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : FourierTransform.fourier (lowMomentumTest E x s hE) = lowMomentumTestFrequencyClass E hE x s

Fourier of the test is exactly the prescribed cutoff frequency class.

theorem LiebThirring.lowMomentumTest_fourier_ae {q : ℕ} (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : ↑↑(FourierTransform.fourier (lowMomentumTest E x s hE)) =ᵐ[MeasureTheory.volume] lowMomentumTestFourierFunction E x s

One common literal negative-phase Fourier representative for the test.

theorem LiebThirring.lowMomentumTest_norm_sq {q : ℕ} (E : ℝ) (hE : 0 ≤ E) (x : Position) (s : Fin q) : ‖lowMomentumTest E x s hE‖ ^ 2 = (MeasureTheory.volume (lowMomentumRegion E)).toReal

The test has squared norm equal to the finite low-region volume.