Documentation

Mathlib.Analysis.Distribution.FourierSchwartz

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
Instances For
    @[simp]

    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.

    Plancherel's theorem for Schwartz functions.

    Version where the multiplication is replaced by a general bilinear form M.

    Plancherel's theorem for Schwartz functions.

    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