Cutoff integrals represent the L² projections

The literal low-frequency part of the L² Fourier transform.

The spatial low projection is inverse L² Fourier of the cutoff class.

noncomputable def LiebThirring.lowFrequencyClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

The literal low-frequency part of the L² Fourier transform.

Equations

• LiebThirring.lowFrequencyClass h E = MeasureTheory.MemLp.toLp ((LiebThirring.lowMomentumRegion E).indicator ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ LiebThirring.Position H) h)) ⋯

noncomputable def LiebThirring.lowFourierProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

The spatial low projection is inverse L² Fourier of the cutoff class.

Equations

• LiebThirring.lowFourierProjection h E = FourierTransformInv.fourierInv (LiebThirring.lowFrequencyClass h E)

theorem LiebThirring.lowFourierProjection_ae {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (hE : 0 ≤ E) : ↑↑(lowFourierProjection h E) =ᵐ[MeasureTheory.volume] lowFourierField h E

The continuous raw low field represents the exact inverse L² projection.

noncomputable def LiebThirring.highFrequencyClass {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

The literal complementary high-frequency class.

Equations

• LiebThirring.highFrequencyClass h E = MeasureTheory.MemLp.toLp ((LiebThirring.lowMomentumRegion E)ᶜ.indicator ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ LiebThirring.Position H) h)) ⋯

theorem LiebThirring.highFrequencyClass_eq_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) : highFrequencyClass h E = FourierTransform.fourier h - lowFrequencyClass h E

The complementary frequency class is Fourier minus its low-frequency part.

theorem LiebThirring.highFourierProjection_ae {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (hE : 0 ≤ E) (f : Position → H) (hf : ↑↑h =ᵐ[MeasureTheory.volume] f) : ↑↑(FourierTransformInv.fourierInv (highFrequencyClass h E)) =ᵐ[MeasureTheory.volume] fun (x : Position) => f x - lowFourierField h E x

The fixed representative difference represents inverse L² high projection.