Fixed high-field representatives #
The high field uses the same chosen L² representative at every cutoff.
Joint strong measurability holds for this fixed representative.
noncomputable def
LiebThirring.highFourierField
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume))
(E : ℝ)
(x : Position)
:
H
The high field uses the same chosen L² representative at every cutoff.
Equations
- LiebThirring.highFourierField h E x = ↑↑h x - LiebThirring.lowFourierField h E x
Instances For
theorem
LiebThirring.stronglyMeasurable_highFourierField_canonical
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume))
:
MeasureTheory.StronglyMeasurable fun (p : ℝ × Position) => highFourierField h p.1 p.2
Joint strong measurability holds for this fixed representative.
theorem
LiebThirring.highFourierField_ae
{H : Type u_1}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume))
(E : ℝ)
(hE : 0 ≤ E)
:
↑↑(FourierTransformInv.fourierInv (highFrequencyClass h E)) =ᵐ[MeasureTheory.volume] highFourierField h E
Each nonnegative cutoff's high field represents its exact inverse L² class.