Fourier transform on Schwartz functions

This file will construct the Fourier transform as a continuous linear map acting on Schwartz functions.

For now, it only contains the fact that the Fourier transform of a Schwartz function is differentiable, with an explicit derivative given by a Fourier transform. See SchwartzMap.hasFDerivAt_fourier.

def VectorFourier.fourierSMulRightSchwartz {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : D →L[ℝ] E →L[ℝ] ℝ) : SchwartzMap D V →L[ℝ] SchwartzMap D (E →L[ℝ] V)

Multiplication by a linear map on Schwartz space: for f : D → V a Schwartz function and L a bilinear map from D × E to ℝ, we define a new Schwartz function on D taking values in the space of linear maps from E to V, given by (VectorFourier.fourierSMulRightSchwartz L f) (v) = -(2 * π * I) • L (v, ⬝) • f v. The point of this definition is that the derivative of the Fourier transform of f is the Fourier transform of VectorFourier.fourierSMulRightSchwartz L f.

Equations

• VectorFourier.fourierSMulRightSchwartz L = -(2 * ↑Real.pi * Complex.I) • SchwartzMap.bilinLeftCLM (ContinuousLinearMap.flip (ContinuousLinearMap.smulRightL ℝ E V)) ⋯

@[simp]

theorem VectorFourier.fourierSMulRightSchwartz_apply {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : D →L[ℝ] E →L[ℝ] ℝ) (f : SchwartzMap D V) (d : D) : ((VectorFourier.fourierSMulRightSchwartz L) f) d = -(2 * ↑Real.pi * Complex.I) • ContinuousLinearMap.smulRight (L d) (f d)

theorem SchwartzMap.hasFDerivAt_fourierIntegral {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] (L : D →L[ℝ] E →L[ℝ] ℝ) [MeasurableSpace D] [BorelSpace D] {μ : MeasureTheory.Measure D} [SecondCountableTopology D] [MeasureTheory.Measure.HasTemperateGrowth μ] (f : SchwartzMap D V) (w : E) : HasFDerivAt (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) ⇑f) (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) (⇑((VectorFourier.fourierSMulRightSchwartz L) f)) w) w

The Fourier transform of a Schwartz map f has a Fréchet derivative (everywhere in its domain) and its derivative is the Fourier transform of the Schwartz map mul_L_schwartz L f.