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.
Main statements #
SchwartzMap.fderivCLM_fourier_eq: The derivative of the Fourier transform is given by the Fourier transform of the multiplication with-(2 * π * Complex.I) • innerSL ℝ.SchwartzMap.lineDerivOp_fourier_eq: The line derivative of the Fourier transform is given by the Fourier transform of the multiplication with-(2 * π * Complex.I) • (inner ℝ · m).SchwartzMap.integral_bilin_fourier_eq: The Fourier transform is self-adjoint.SchwartzMap.integral_inner_fourier_fourier: Plancherel's theorem for Schwartz functions.
def
SchwartzMap.fourierTransformCLM
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[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.
This definition is only to define the Fourier transform, use FourierTransform.fourierCLM instead.
Equations
Instances For
instance
SchwartzMap.instFourierTransform
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierTransform (SchwartzMap V E) (SchwartzMap V E)
Equations
instance
SchwartzMap.instFourierAdd
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierAdd (SchwartzMap V E) (SchwartzMap V E)
instance
SchwartzMap.instFourierSMul
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierSMul 𝕜 (SchwartzMap V E) (SchwartzMap V E)
instance
SchwartzMap.instContinuousFourier
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
ContinuousFourier (SchwartzMap V E) (SchwartzMap V E)
theorem
SchwartzMap.fourier_coe
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
@[simp]
theorem
SchwartzMap.fourierTransformCLM_apply
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
instance
SchwartzMap.instFourierTransformInv
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierTransformInv (SchwartzMap V E) (SchwartzMap V E)
Equations
instance
SchwartzMap.instFourierInvAdd
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierInvAdd (SchwartzMap V E) (SchwartzMap V E)
instance
SchwartzMap.instFourierInvSMul
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
FourierInvSMul 𝕜 (SchwartzMap V E) (SchwartzMap V E)
instance
SchwartzMap.instContinuousFourierInv
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
:
ContinuousFourierInv (SchwartzMap V E) (SchwartzMap V E)
theorem
SchwartzMap.fourierInv_coe
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
theorem
SchwartzMap.fourierInv_apply_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
instance
SchwartzMap.instFourierPair
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
:
FourierPair (SchwartzMap V E) (SchwartzMap V E)
instance
SchwartzMap.instFourierInvPair
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
[CompleteSpace E]
:
FourierInvPair (SchwartzMap V E) (SchwartzMap V E)
@[deprecated FourierPair.fourierInv_fourier_eq (since := "2025-11-13")]
theorem
SchwartzMap.fourier_inversion
{E : Type u_5}
{F : Type u_6}
{inst✝ : FourierTransform E F}
{inst✝¹ : FourierTransformInv F E}
[self : FourierPair E F]
(f : E)
:
Alias of FourierPair.fourierInv_fourier_eq.
@[deprecated FourierInvPair.fourier_fourierInv_eq (since := "2025-11-13")]
theorem
SchwartzMap.fourier_inversion_inv
{E : Type u_5}
{F : Type u_6}
{inst✝ : FourierTransform F E}
{inst✝¹ : FourierTransformInv E F}
[self : FourierInvPair E F]
(f : E)
:
Alias of FourierInvPair.fourier_fourierInv_eq.
@[deprecated FourierTransform.fourierCLE (since := "2026-01-06")]
def
SchwartzMap.fourierTransformCLE
(R : Type u_5)
(E : Type u_6)
{F : Type u_7}
[Semiring R]
[AddCommMonoid E]
[AddCommMonoid F]
[Module R E]
[Module R F]
[FourierTransform E F]
[FourierAdd E F]
[FourierSMul R E F]
[FourierTransformInv F E]
[FourierPair E F]
[FourierInvPair F E]
[TopologicalSpace E]
[TopologicalSpace F]
[ContinuousFourier E F]
[ContinuousFourierInv F E]
:
Alias of FourierTransform.fourierCLE.
Equations
Instances For
@[deprecated FourierTransform.fourierCLE_apply (since := "2026-01-06")]
theorem
SchwartzMap.fourierTransformCLE_apply
{R : Type u_5}
{E : Type u_6}
{F : Type u_7}
[Semiring R]
[AddCommMonoid E]
[AddCommMonoid F]
[Module R E]
[Module R F]
[FourierTransform E F]
[FourierAdd E F]
[FourierSMul R E F]
[FourierTransformInv F E]
[FourierPair E F]
[FourierInvPair F E]
[TopologicalSpace E]
[TopologicalSpace F]
[ContinuousFourier E F]
[ContinuousFourierInv F E]
(f : E)
:
Alias of FourierTransform.fourierCLE_apply.
@[deprecated FourierTransform.fourierCLE_symm_apply (since := "2026-01-06")]
theorem
SchwartzMap.fourierTransformCLE_symm_apply
{R : Type u_5}
{E : Type u_6}
{F : Type u_7}
[Semiring R]
[AddCommMonoid E]
[AddCommMonoid F]
[Module R E]
[Module R F]
[FourierTransform E F]
[FourierAdd E F]
[FourierSMul R E F]
[FourierTransformInv F E]
[FourierPair E F]
[FourierInvPair F E]
[TopologicalSpace E]
[TopologicalSpace F]
[ContinuousFourier E F]
[ContinuousFourierInv F E]
(f : F)
:
Alias of FourierTransform.fourierCLE_symm_apply.
theorem
SchwartzMap.fourier_evalCLM_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(𝕜' : Type u_4)
[NormedField 𝕜']
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{G : Type u_6}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[NormedSpace 𝕜' G]
[SMulCommClass ℝ 𝕜' G]
(f : SchwartzMap V (F →L[ℝ] G))
(m : F)
:
FourierTransform.fourier ((SchwartzMap.evalCLM 𝕜' V G m) f) = (SchwartzMap.evalCLM 𝕜' V G m) (FourierTransform.fourier f)
theorem
SchwartzMap.fderivCLM_fourier_eq
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
(fderivCLM 𝕜 V E) (FourierTransform.fourier f) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) f)
The derivative of the Fourier transform is given by the Fourier transform of the multiplication
with -(2 * π * Complex.I) • innerSL ℝ.
theorem
SchwartzMap.fourier_fderivCLM_eq
(𝕜 : Type u_1)
[RCLike 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
[NormedSpace 𝕜 E]
[SMulCommClass ℂ 𝕜 E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
:
FourierTransform.fourier ((fderivCLM 𝕜 V E) f) = (2 * ↑Real.pi * Complex.I) • (smulRightCLM ℂ E (innerSL ℝ)) (FourierTransform.fourier f)
The Fourier transform of the derivative is given by multiplication of
(2 * π * Complex.I) • innerSL ℝ with the Fourier transform.
theorem
SchwartzMap.lineDerivOp_fourier_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
(m : V)
:
LineDeriv.lineDerivOp m (FourierTransform.fourier f) = FourierTransform.fourier (-(2 * ↑Real.pi * Complex.I) • (smulLeftCLM E fun (x : V) => inner ℝ x m) f)
theorem
SchwartzMap.fourier_lineDerivOp_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
(m : V)
:
FourierTransform.fourier (LineDeriv.lineDerivOp m f) = (2 * ↑Real.pi * Complex.I) • (smulLeftCLM E fun (x : V) => inner ℝ x m) (FourierTransform.fourier f)
theorem
SchwartzMap.lineDerivOp_fourierInv_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
(m : V)
:
LineDeriv.lineDerivOp m (FourierTransformInv.fourierInv f) = FourierTransformInv.fourierInv ((2 * ↑Real.pi * Complex.I) • (smulLeftCLM E fun (x : V) => inner ℝ x m) f)
theorem
SchwartzMap.fourierInv_lineDerivOp_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f : SchwartzMap V E)
(m : V)
:
FourierTransformInv.fourierInv (LineDeriv.lineDerivOp m f) = -(2 * ↑Real.pi * Complex.I) • (smulLeftCLM E fun (x : V) => inner ℝ x m) (FourierTransformInv.fourierInv f)
theorem
SchwartzMap.integral_bilin_fourier_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransform.fourier 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.
@[deprecated SchwartzMap.integral_bilin_fourier_eq (since := "2025-11-16")]
theorem
SchwartzMap.integral_bilin_fourierIntegral_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransform.fourier g) x)
Alias of SchwartzMap.integral_bilin_fourier_eq.
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_fourier_smul_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[CompleteSpace F]
(f : SchwartzMap V ℂ)
(g : SchwartzMap V F)
:
The Fourier transform satisfies ∫ 𝓕 f • g = ∫ f • 𝓕 g, i.e., it is self-adjoint.
theorem
SchwartzMap.integral_fourier_mul_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f g : SchwartzMap V ℂ)
:
The Fourier transform satisfies ∫ 𝓕 f * g = ∫ f * 𝓕 g, i.e., it is self-adjoint.
theorem
SchwartzMap.integral_bilin_fourierInv_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransformInv.fourierInv f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)
The inverse 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_fourierInv_smul_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
[CompleteSpace F]
(f : SchwartzMap V ℂ)
(g : SchwartzMap V F)
:
∫ (ξ : V), (FourierTransformInv.fourierInv f) ξ • g ξ = ∫ (x : V), f x • (FourierTransformInv.fourierInv g) x
The inverse Fourier transform satisfies ∫ 𝓕⁻ f • g = ∫ f • 𝓕⁻ g, i.e., it is self-adjoint.
theorem
SchwartzMap.integral_fourierInv_mul_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
(f g : SchwartzMap V ℂ)
:
∫ (ξ : V), (FourierTransformInv.fourierInv f) ξ * g ξ = ∫ (x : V), f x * (FourierTransformInv.fourierInv g) x
The inverse Fourier transform satisfies ∫ 𝓕⁻ f * g = ∫ f * 𝓕⁻ g, i.e., it is self-adjoint.
theorem
SchwartzMap.integral_sesq_fourier_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L⋆[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)
@[deprecated SchwartzMap.integral_sesq_fourier_eq (since := "2025-11-16")]
theorem
SchwartzMap.integral_sesq_fourierIntegral_eq
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L⋆[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)
Alias of SchwartzMap.integral_sesq_fourier_eq.
theorem
SchwartzMap.integral_sesq_fourier_fourier
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℂ F]
{G : Type u_5}
[NormedAddCommGroup G]
[NormedSpace ℂ G]
[CompleteSpace E]
[CompleteSpace F]
(f : SchwartzMap V E)
(g : SchwartzMap V F)
(M : E →L⋆[ℂ] F →L[ℂ] G)
:
∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) ((FourierTransform.fourier g) ξ) = ∫ (x : V), (M (f x)) (g x)
Plancherel's theorem for Schwartz functions.
Version where the inner product is replaced by a general sesquilinear form M.
@[simp]
theorem
SchwartzMap.integral_inner_fourier_fourier
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[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_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
theorem
SchwartzMap.inner_fourier_toL2_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(f g : SchwartzMap V H)
:
inner ℂ ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume)
((FourierTransform.fourier g).toLp 2 MeasureTheory.volume) = inner ℂ (f.toLp 2 MeasureTheory.volume) (g.toLp 2 MeasureTheory.volume)
@[deprecated SchwartzMap.inner_fourier_toL2_eq (since := "2025-11-13")]
theorem
SchwartzMap.inner_fourierTransformCLM_toL2_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(f g : SchwartzMap V H)
:
inner ℂ ((FourierTransform.fourier f).toLp 2 MeasureTheory.volume)
((FourierTransform.fourier g).toLp 2 MeasureTheory.volume) = inner ℂ (f.toLp 2 MeasureTheory.volume) (g.toLp 2 MeasureTheory.volume)
Alias of SchwartzMap.inner_fourier_toL2_eq.
@[simp]
theorem
SchwartzMap.norm_fourier_toL2_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
@[deprecated SchwartzMap.norm_fourier_toL2_eq (since := "2025-11-13")]
theorem
SchwartzMap.norm_fourierTransformCLM_toL2_eq
{V : Type u_3}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[FiniteDimensional ℝ V]
[MeasurableSpace V]
[BorelSpace V]
{H : Type u_4}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
(f : SchwartzMap V H)
:
Alias of SchwartzMap.norm_fourier_toL2_eq.