Integral and L² Fourier representatives #
The raw Bochner Fourier integral represents the L² Fourier transform for integrable L² functions. Smooth compactly supported tests and tempered distributions identify the two representatives.
theorem
LiebThirring.Fourier.integral_fourier_smul_eq
{V : Type u_1}
{H : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(g : SchwartzMap V ℂ)
{f : V → H}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
:
Fourier integrals commute with Schwartz test-function pairings.
theorem
LiebThirring.Fourier.integral_fourierInv_smul_eq
{V : Type u_1}
{H : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(g : SchwartzMap V ℂ)
{f : V → H}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
:
∫ (x : V), (FourierTransformInv.fourierInv g) x • f x = ∫ (x : V), g x • FourierTransformInv.fourierInv f x
Inverse Fourier integrals commute with Schwartz test-function pairings.
theorem
LiebThirring.Fourier.fourier_toLp_ae_eq
{V : Type u_1}
{H : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
{f : V → H}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
The raw Fourier integral agrees almost everywhere with the L² Fourier transform.
theorem
LiebThirring.Fourier.fourierInv_toLp_ae_eq
{V : Type u_1}
{H : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
{f : V → H}
(hf : MeasureTheory.Integrable f MeasureTheory.volume)
(hf2 : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
The raw inverse Fourier integral agrees almost everywhere with the L² inverse transform.