Low Fourier cutoff fields

The Fourier kinetic multiplier with the normalization.

The closed low momentum region at real energy E.

noncomputable def LiebThirring.fourierKineticMultiplier (ξ : Position) : ℝ

The Fourier kinetic multiplier with the normalization.

Equations

• LiebThirring.fourierKineticMultiplier ξ = (2 * Real.pi) ^ 2 * ‖ξ‖ ^ 2

noncomputable def LiebThirring.lowMomentumRegion (E : ℝ) : Set Position

The closed low momentum region at real energy E.

Equations

• LiebThirring.lowMomentumRegion E = {ξ : LiebThirring.Position | LiebThirring.fourierKineticMultiplier ξ ≤ E}

theorem LiebThirring.continuous_fourierKineticMultiplier : Continuous fourierKineticMultiplier

theorem LiebThirring.measurableSet_lowMomentumRegion (E : ℝ) : MeasurableSet (lowMomentumRegion E)

theorem LiebThirring.lowMomentumRegion_eq_closedBall (E : ℝ) (hE : 0 ≤ E) : lowMomentumRegion E = Metric.closedBall 0 (√E / (2 * Real.pi))

The low region is exactly the ball of radius sqrt E / (2π).

theorem LiebThirring.volume_lowMomentumRegion_ne_top (E : ℝ) (hE : 0 ≤ E) : MeasureTheory.volume (lowMomentumRegion E) ≠ ⊤

Every low momentum region at nonnegative energy has finite volume.

theorem LiebThirring.volume_lowMomentumRegion (E : ℝ) (hE : 0 ≤ E) : MeasureTheory.volume (lowMomentumRegion E) = ENNReal.ofReal (1 / (6 * Real.pi ^ 2) * E ^ (3 / 2))

Exact three-dimensional phase-space volume, including E = 0.

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

The same raw inverse Fourier integral is used for every real energy and point.

Equations

• LiebThirring.lowFourierField h E x = FourierTransformInv.fourierInv ((LiebThirring.lowMomentumRegion E).indicator ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ LiebThirring.Position H) h)) x

theorem LiebThirring.integrable_lowFourierRepresentative {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (hE : 0 ≤ E) : MeasureTheory.Integrable ((lowMomentumRegion E).indicator ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position H) h)) MeasureTheory.volume

The supported Fourier representative is integrable, with no finite-energy premise.

theorem LiebThirring.integrable_lowFourierField {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (hE : 0 ≤ E) (x : Position) : MeasureTheory.Integrable (fun (ξ : Position) => Real.fourierChar (inner ℝ ξ x) • (lowMomentumRegion E).indicator (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position H) h)) ξ) MeasureTheory.volume

Each inverse Fourier integrand defining the low field is Bochner integrable.

theorem LiebThirring.lowFourierField_eq_integral {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (E : ℝ) (x : Position) : lowFourierField h E x = ∫ (ξ : Position) in lowMomentumRegion E, Real.fourierChar (inner ℝ ξ x) • ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Position H) h) ξ

The defining integral has the positive inverse Fourier phase from Fourier cutoff.

theorem LiebThirring.stronglyMeasurable_lowFourierField {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : MeasureTheory.StronglyMeasurable fun (p : ℝ × Position) => lowFourierField h p.1 p.2

One fixed Fourier representative gives joint strong measurability for all energies.

theorem LiebThirring.stronglyMeasurable_highFourierField {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (h : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) (f : Position → H) (hf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.StronglyMeasurable fun (p : ℝ × Position) => f p.2 - lowFourierField h p.1 p.2

Subtracting the low integral from any fixed strongly measurable representative preserves joint strong measurability.