Derivative of the Fourier transform

In this file we compute the Fréchet derivative of 𝓕 f, where f is a function such that both f and v ↦ ‖v‖ * ‖f v‖ are integrable. Here 𝓕 is understood as an operator (V → E) → (W → E), where V and W are normed ℝ-vector spaces and the Fourier transform is taken with respect to a continuous ℝ-bilinear pairing L : V × W → ℝ.

We also give a separate lemma for the most common case when V = W = ℝ and L is the obvious multiplication map.

theorem Real.hasDerivAt_fourierChar (x : ℝ) : HasDerivAt (fun (y : ℝ) => ↑(Real.fourierChar (Multiplicative.ofAdd y))) (2 * ↑Real.pi * Complex.I * ↑(Real.fourierChar (Multiplicative.ofAdd x))) x

def VectorFourier.mul_L {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) : W →L[ℝ] E

Send a function f : V → E to the function f : V → Hom (W, E) given by v ↦ (w ↦ -2 * π * I * L(v, w) • f v).

Equations

• VectorFourier.mul_L L f v = -(2 * ↑Real.pi * Complex.I) • ContinuousLinearMap.smulRight (L v) (f v)

theorem VectorFourier.hasFDerivAt_fourier_transform_integrand_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) : HasFDerivAt (fun (w' : W) => ↑(Real.fourierChar (Multiplicative.ofAdd (-(L v) w'))) • f v) (↑(Real.fourierChar (Multiplicative.ofAdd (-(L v) w))) • VectorFourier.mul_L L f v) w

The w-derivative of the Fourier transform integrand.

theorem VectorFourier.norm_fderiv_fourier_transform_integrand_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) : ‖↑(Real.fourierChar (Multiplicative.ofAdd (-(L v) w))) • VectorFourier.mul_L L f v‖ = 2 * Real.pi * ‖L v‖ * ‖f v‖

Norm of the w-derivative of the Fourier transform integrand.

theorem VectorFourier.norm_fderiv_fourier_transform_integrand_right_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) (w : W) : ‖↑(Real.fourierChar (Multiplicative.ofAdd (-(L v) w))) • VectorFourier.mul_L L f v‖ ≤ 2 * Real.pi * ‖L‖ * ‖v‖ * ‖f v‖

theorem VectorFourier.hasFDerivAt_fourier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [CompleteSpace E] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] (hf : MeasureTheory.Integrable f μ) (hf' : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) μ) (w : W) : HasFDerivAt (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) f) (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) (VectorFourier.mul_L L f) w) w

Main theorem of this section: if both f and x ↦ ‖x‖ * ‖f x‖ are integrable, then the Fourier transform of f has a Fréchet derivative (everywhere in its domain) and its derivative is the Fourier transform of mul_L L f.

@[inline, reducible]

abbrev VectorFourier.integralFourier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] (f : V → E) (μ : autoParam (MeasureTheory.Measure V) _auto✝) (w : V) : E

Notation for the Fourier transform on a real inner product space

Equations

• VectorFourier.integralFourier f μ = VectorFourier.fourierIntegral Real.fourierChar μ (innerₛₗ ℝ) f

theorem VectorFourier.InnerProductSpace.hasFDerivAt_fourier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [SecondCountableTopology V] [MeasurableSpace V] [BorelSpace V] [CompleteSpace E] {f : V → E} {μ : MeasureTheory.Measure V} (hf_int : MeasureTheory.Integrable f μ) (hvf_int : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) μ) (x : V) : HasFDerivAt (VectorFourier.integralFourier f μ) (VectorFourier.integralFourier (VectorFourier.mul_L (innerSL ℝ) f) μ x) x

The Fréchet derivative of the Fourier transform of f is the Fourier transform of fun v ↦ ((-2 * π * I) • f v) ⊗ (innerSL ℝ v).

theorem hasDerivAt_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℝ → E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hf' : MeasureTheory.Integrable (fun (x : ℝ) => x • f x) MeasureTheory.volume) (w : ℝ) : HasDerivAt (Real.fourierIntegral f) (Real.fourierIntegral (fun (x : ℝ) => (-2 * ↑Real.pi * Complex.I * ↑x) • f x) w) w