Derivative of the Fourier transform

In this file we compute the Fréchet derivative of the Fourier transform of f, where f is a function such that both f and v ↦ ‖v‖ * ‖f v‖ are integrable. Here the Fourier transform 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 → ℝ and a given reference measure μ.

We give specialized versions of these results on inner product spaces (where L is the scalar product) and on the real line, where we express the one-dimensional derivative in more concrete terms, as the Fourier transform of x * f x.

Main definitions and results

We introduce one convenience definition:

• VectorFourier.fourierSMulRight L f: given f : V → E and L a bilinear pairing between V and W, then this is the function fun v ↦ -(2 * π * I) (L v ⬝) • f v, from V to Hom (W, E). This is essentially ContinousLinearMap.smulRight, up to the factor - 2πI designed to make sure that the Fourier integral of fourierSMulRight L f is the derivative of the Fourier integral of f.

With this definition, the statements read as follows, first in a general context (arbitrary L and μ):

• VectorFourier.hasFDerivAt_fourierIntegral: the Fourier integral of f is differentiable, with derivative the Fourier integral of fourierSMulRight L f.
• VectorFourier.differentiable_fourierIntegral: the Fourier integral of f is differentiable.
• VectorFourier.fderiv_fourierIntegral: formula for the derivative of the Fourier integral of f.

These statements are then specialized to the case of the usual Fourier transform on finite-dimensional inner product spaces with their canonical Lebesgue measure (covering in particular the case of the real line), replacing the namespace VectorFourier by the namespace Real in the above statements.

We also give specialized versions of the one-dimensional real derivative in Real.deriv_fourierIntegral.

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

def VectorFourier.fourierSMulRight {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). This is designed so that the Fourier transform of fourierSMulRight L f is the derivative of the Fourier transform of f.

Equations

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

@[simp]

theorem VectorFourier.fourierSMulRight_apply {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) : (VectorFourier.fourierSMulRight L f v) w = -(2 * ↑Real.pi * Complex.I) • (L v) w • f v

theorem VectorFourier.hasFDerivAt_fourierChar_smul {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 (-(L v) w') • f v) (Real.fourierChar (-(L v) w) • VectorFourier.fourierSMulRight L f v) w

The w-derivative of the Fourier transform integrand.

theorem VectorFourier.norm_fourierSMulRight {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) : ‖VectorFourier.fourierSMulRight L f v‖ = 2 * Real.pi * ‖L v‖ * ‖f v‖

theorem VectorFourier.norm_fourierSMulRight_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) : ‖VectorFourier.fourierSMulRight L f v‖ ≤ 2 * Real.pi * ‖L‖ * ‖v‖ * ‖f v‖

theorem MeasureTheory.AEStronglyMeasurable.fourierSMulRight {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} {W : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] [SecondCountableTopologyEither V (W →L[ℝ] ℝ)] [MeasurableSpace V] [BorelSpace V] {L : V →L[ℝ] W →L[ℝ] ℝ} {f : V → E} {μ : MeasureTheory.Measure V} (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.AEStronglyMeasurable (fun (v : V) => VectorFourier.fourierSMulRight L f v) μ

theorem VectorFourier.hasFDerivAt_fourierIntegral {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} [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : MeasureTheory.Measure V} (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.fourierSMulRight 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 smulRight L f.

theorem VectorFourier.fderiv_fourierIntegral {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} [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : MeasureTheory.Measure V} (hf : MeasureTheory.Integrable f μ) (hf' : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) μ) (w : W) : fderiv ℝ (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) f) w = VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) (VectorFourier.fourierSMulRight L f) w

theorem VectorFourier.differentiable_fourierIntegral {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} [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : MeasureTheory.Measure V} (hf : MeasureTheory.Integrable f μ) (hf' : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) μ) : Differentiable ℝ (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) f)

theorem Real.hasFDerivAt_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → E} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hvf_int : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) MeasureTheory.volume) (x : V) : HasFDerivAt (Real.fourierIntegral f) (Real.fourierIntegral (VectorFourier.fourierSMulRight (innerSL ℝ) f) x) x

The Fréchet derivative of the Fourier transform of f is the Fourier transform of fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v.

theorem Real.fderiv_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → E} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hvf_int : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) MeasureTheory.volume) (x : V) : fderiv ℝ (Real.fourierIntegral f) x = Real.fourierIntegral (VectorFourier.fourierSMulRight (innerSL ℝ) f) x

The Fréchet derivative of the Fourier transform of f is the Fourier transform of fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v.

theorem Real.differentiable_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {f : V → E} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hvf_int : MeasureTheory.Integrable (fun (v : V) => ‖v‖ * ‖f v‖) MeasureTheory.volume) : Differentiable ℝ (Real.fourierIntegral f)

theorem Real.hasDerivAt_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ 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

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