The Fourier transform on $L^p$

In this file we define the Fourier transform on $L^2$ as a linear isometry equivalence.

Main definitions

• MeasureTheory.Lp.fourierTransformₗᵢ: The Fourier transform on $L^2$ as a linear isometry equivalence.

Main statements

• SchwartzMap.toLp_fourier_eq: The Fourier transform on 𝓢(E, F) agrees with the Fourier transform on $L^2$.
• MeasureTheory.Lp.fourier_toTemperedDistribution_eq: The Fourier transform on $L^2$ agrees with the Fourier transform on 𝓢'(E, F).

noncomputable def MeasureTheory.Lp.fourierTransformₗᵢ (E : Type u_1) (F : Type u_2) [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : ↥(Lp F 2 volume) ≃ₗᵢ[ℂ] ↥(Lp F 2 volume)

The Fourier transform on L2 as a linear isometry equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MeasureTheory.Lp.instFourierTransform {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierTransform ↥(Lp F 2 volume) ↥(Lp F 2 volume)

Equations

• MeasureTheory.Lp.instFourierTransform = { fourier := ⇑(MeasureTheory.Lp.fourierTransformₗᵢ E F) }

instance MeasureTheory.Lp.instFourierAdd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierAdd ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instFourierSMul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierSMul ℂ ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instContinuousFourier {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : ContinuousFourier ↥(Lp F 2 volume) ↥(Lp F 2 volume)

@[instance_reducible]

noncomputable instance MeasureTheory.Lp.instFourierTransformInv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierTransformInv ↥(Lp F 2 volume) ↥(Lp F 2 volume)

Equations

• MeasureTheory.Lp.instFourierTransformInv = { fourierInv := ⇑(MeasureTheory.Lp.fourierTransformₗᵢ E F).symm }

instance MeasureTheory.Lp.instFourierInvAdd {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierInvAdd ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instFourierInvSMul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierInvSMul ℂ ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instContinuousFourierInv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : ContinuousFourierInv ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instFourierPair {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierPair ↥(Lp F 2 volume) ↥(Lp F 2 volume)

instance MeasureTheory.Lp.instFourierPairInv {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : FourierInvPair ↥(Lp F 2 volume) ↥(Lp F 2 volume)

@[simp]

theorem MeasureTheory.Lp.norm_fourier_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : ↥(Lp F 2 volume)) : ‖FourierTransform.fourier f‖ = ‖f‖

Plancherel's theorem for L2 functions.

@[simp]

theorem MeasureTheory.Lp.inner_fourier_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : ↥(Lp F 2 volume)) (g : ↥(Lp F 2 volume)) : inner ℂ (FourierTransform.fourier f) (FourierTransform.fourier g) = inner ℂ f g

@[simp]

theorem SchwartzMap.toLp_fourier_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : SchwartzMap E F) : FourierTransform.fourier (f.toLp 2 MeasureTheory.volume) = (FourierTransform.fourier f).toLp 2 MeasureTheory.volume

@[simp]

theorem SchwartzMap.toLp_fourierInv_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : SchwartzMap E F) : FourierTransformInv.fourierInv (f.toLp 2 MeasureTheory.volume) = (FourierTransformInv.fourierInv f).toLp 2 MeasureTheory.volume

theorem MeasureTheory.Lp.fourier_toTemperedDistribution_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : ↥(Lp F 2 volume)) : FourierTransform.fourier (toTemperedDistribution f) = toTemperedDistribution (FourierTransform.fourier f)

The 𝓢'-Fourier transform and the L2-Fourier transform coincide on L2.

theorem MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (f : ↥(Lp F 2 volume)) : FourierTransformInv.fourierInv (toTemperedDistribution f) = toTemperedDistribution (FourierTransformInv.fourierInv f)

The 𝓢'-inverse Fourier transform and the L2-inverse Fourier transform coincide on L2.