Fourier transform on Schwartz functions #
This file constructs the Fourier transform as a continuous linear map acting on Schwartz
functions, in fourierTransformCLM
. It is also given as a continuous linear equiv, in
fourierTransformCLE
.
noncomputable def
SchwartzMap.fourierTransformCLM
(π : Type u_1)
[RCLike π]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
[NormedSpace π E]
[SMulCommClass β π E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
:
The Fourier transform on a real inner product space, as a continuous linear map on the Schwartz space.
Equations
- SchwartzMap.fourierTransformCLM π = SchwartzMap.mkCLM (fun (x : SchwartzMap V E) => Real.fourierIntegral βx) β― β― β― β―
Instances For
@[simp]
theorem
SchwartzMap.fourierTransformCLM_apply
(π : Type u_1)
[RCLike π]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
[NormedSpace π E]
[SMulCommClass β π E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
@[simp]
theorem
SchwartzMap.fourier_inversion
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
(f : SchwartzMap V E)
(x : V)
:
@[simp]
theorem
SchwartzMap.fourier_inversion_inv
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
(f : SchwartzMap V E)
(x : V)
:
theorem
SchwartzMap.integral_bilin_fourierIntegral_eq
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace β F]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace β G]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E βL[β] F βL[β] G)
:
β« (ΞΎ : V), (M (Real.fourierIntegral (βf) ΞΎ)) (g ΞΎ) = β« (x : V), (M (f x)) (Real.fourierIntegral (βg) x)
The Fourier transform satisfies β« π f * g = β« f * π g
, i.e., it is self-adjoint.
Version where the multiplication is replaced by a general bilinear form M
.
theorem
SchwartzMap.integral_sesq_fourierIntegral_eq
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace β F]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace β G]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E βLβ[β] F βL[β] G)
:
β« (ΞΎ : V), (M (Real.fourierIntegral (βf) ΞΎ)) (g ΞΎ) = β« (x : V), (M (f x)) (Real.fourierIntegralInv (βg) x)
theorem
SchwartzMap.integral_sesq_fourier_fourier
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace β F]
{G : Type u_7}
[NormedAddCommGroup G]
[NormedSpace β G]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E βLβ[β] F βL[β] G)
:
β« (ΞΎ : V), (M (Real.fourierIntegral (βf) ΞΎ)) (Real.fourierIntegral (βg) ΞΎ) = β« (x : V), (M (f x)) (g x)
Plancherel's theorem for Schwartz functions.
Version where the multiplication is replaced by a general bilinear form M
.
theorem
SchwartzMap.integral_inner_fourier_fourier
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_8}
[NormedAddCommGroup H]
[InnerProductSpace β H]
[CompleteSpace H]
(f g : SchwartzMap V H)
:
Plancherel's theorem for Schwartz functions.
theorem
SchwartzMap.integral_norm_sq_fourier
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_8}
[NormedAddCommGroup H]
[InnerProductSpace β H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
theorem
SchwartzMap.inner_fourierTransformCLM_toL2_eq
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_8}
[NormedAddCommGroup H]
[InnerProductSpace β H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
inner β (((fourierTransformCLM β) f).toLp 2 MeasureTheory.volume)
(((fourierTransformCLM β) f).toLp 2 MeasureTheory.volume) = inner β (f.toLp 2 MeasureTheory.volume) (f.toLp 2 MeasureTheory.volume)
theorem
SchwartzMap.norm_fourierTransformCLM_toL2_eq
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_8}
[NormedAddCommGroup H]
[InnerProductSpace β H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
noncomputable def
SchwartzMap.fourierTransformCLE
(π : Type u_1)
[RCLike π]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
[NormedSpace π E]
[SMulCommClass β π E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
:
The Fourier transform on a real inner product space, as a continuous linear equiv on the Schwartz space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SchwartzMap.fourierTransformCLE_apply
(π : Type u_1)
[RCLike π]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
[NormedSpace π E]
[SMulCommClass β π E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
(f : SchwartzMap V E)
:
@[simp]
theorem
SchwartzMap.fourierTransformCLE_symm_apply
(π : Type u_1)
[RCLike π]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace β E]
[NormedSpace π E]
[SMulCommClass β π E]
{V : Type u_5}
[NormedAddCommGroup V]
[InnerProductSpace β V]
[FiniteDimensional β V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
(f : SchwartzMap V E)
: