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.

noncomputable 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] : SchwartzMap V E →L[𝕜] SchwartzMap V E

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

• SchwartzMap.fourierTransformCLM 𝕜 = SchwartzMap.mkCLM (fun (x : SchwartzMap V E) => FourierTransform.fourier ⇑x) ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable 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

• SchwartzMap.instFourierTransform = { fourier := fun (f : SchwartzMap V E) => (SchwartzMap.fourierTransformCLM ℂ) f }

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) : ⇑(FourierTransform.fourier f) = FourierTransform.fourier ⇑f

@[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) : (fourierTransformCLM 𝕜) f = FourierTransform.fourier f

@[instance_reducible]

noncomputable 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

• SchwartzMap.instFourierTransformInv = { fourierInv := ⇑(SchwartzMap.compCLMOfContinuousLinearEquiv ℂ ↑(LinearIsometryEquiv.neg ℝ) ∘SL SchwartzMap.fourierTransformCLM ℂ) }

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) : ⇑(FourierTransformInv.fourierInv f) = FourierTransformInv.fourierInv ⇑f

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) : FourierTransformInv.fourierInv f = (compCLMOfContinuousLinearEquiv ℂ ↑(LinearIsometryEquiv.neg ℝ)) (FourierTransform.fourier f)

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)

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)

The line derivative in direction m of the Fourier transform is given by the Fourier transform of the multiplication with -(2 * π * Complex.I) • (inner ℝ · m).

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)

The Fourier transform of line derivative in direction m is given by multiplication of (2 * π * Complex.I) • (inner ℝ · m) with the Fourier transform.

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)

The line derivative in direction m of the inverse Fourier transform is given by the inverse Fourier transform of the multiplication with (2 * π * Complex.I) • (inner ℝ · m).

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)

The inverse Fourier transform of line derivative in direction m is given by multiplication of -(2 * π * Complex.I) • (inner ℝ · m) with the inverse Fourier transform.

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.

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) : ∫ (ξ : V), (FourierTransform.fourier f) ξ • g ξ = ∫ (x : V), f x • (FourierTransform.fourier g) x

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 ℂ) : ∫ (ξ : V), (FourierTransform.fourier f) ξ * g ξ = ∫ (x : V), f x * (FourierTransform.fourier g) x

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)

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.

theorem SchwartzMap.norm_fourier_apply_le_toLp_one {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : SchwartzMap V F) (x : V) : ‖(FourierTransform.fourier f) x‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖

theorem SchwartzMap.norm_fourier_toBoundedContinuousFunction_le_toLp_one {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : SchwartzMap V F) : ‖(FourierTransform.fourier f).toBoundedContinuousFunction‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖

theorem SchwartzMap.norm_fourier_Lp_top_leq_toLp_one {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℂ F] (f : SchwartzMap V F) : ‖(FourierTransform.fourier f).toLp ⊤ MeasureTheory.volume‖ ≤ ‖f.toLp 1 MeasureTheory.volume‖

@[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) : ∫ (ξ : V), inner ℂ ((FourierTransform.fourier f) ξ) ((FourierTransform.fourier g) ξ) = ∫ (x : V), inner ℂ (f x) (g x)

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) : ∫ (ξ : V), ‖(FourierTransform.fourier f) ξ‖ ^ 2 = ∫ (x : V), ‖f x‖ ^ 2

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)

@[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) : ‖(FourierTransform.fourier f).toLp 2 MeasureTheory.volume‖ = ‖f.toLp 2 MeasureTheory.volume‖