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.mul_L_schwartz {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.mul_L_schwartz 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.mul_L_schwartz L f.

Equations

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

theorem VectorFourier.mul_L_schwartz_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.mul_L_schwartz L) f) d = VectorFourier.mul_L L (⇑f) d

theorem SchwartzMap.integrable_pow_mul {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] [MeasurableSpace D] [BorelSpace D] [FiniteDimensional ℝ D] (f : SchwartzMap D V) {μ : MeasureTheory.Measure D} (k : ℕ) [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.Integrable (fun (x : D) => ‖x‖ ^ k * ‖f x‖) μ

theorem SchwartzMap.integrable {D : Type u_1} [NormedAddCommGroup D] [NormedSpace ℝ D] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℂ V] [MeasurableSpace D] [BorelSpace D] [FiniteDimensional ℝ D] (f : SchwartzMap D V) {μ : MeasureTheory.Measure D} [MeasureTheory.Measure.IsAddHaarMeasure μ] : MeasureTheory.Integrable (⇑f) μ

theorem SchwartzMap.hasFDerivAt_fourier {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[ℝ] ℝ) [CompleteSpace V] [MeasurableSpace D] [BorelSpace D] {μ : MeasureTheory.Measure D} [FiniteDimensional ℝ D] [MeasureTheory.Measure.IsAddHaarMeasure μ] (f : SchwartzMap D V) (w : E) : HasFDerivAt (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) ⇑f) (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) (⇑((VectorFourier.mul_L_schwartz 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.