Documentation

Mathlib.Analysis.Fourier.FourierTransformDeriv

Derivatives 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 also investigate higher derivatives: Assuming that ‖v‖^n * ‖f v‖ is integrable, we show that the Fourier transform of f is C^n.

We also study in a parallel way the Fourier transform of the derivative, which is obtained by tensoring the Fourier transform of the original function with the bilinear form. We also get results for iterated derivatives.

A consequence of these results is that, if a function is smooth and all its derivatives are integrable when multiplied by ‖v‖^k, then the same goes for its Fourier transform, with explicit bounds.

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 -2πI x * f x (or (-2πI x)^n * f x for higher derivatives).

Main definitions and results #

We introduce two convenience definitions:

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

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 (and iterated derivative) in Real.deriv_fourierIntegral and Real.iteratedDeriv_fourierIntegral.

theorem Real.hasDerivAt_fourierChar (x : ) :
HasDerivAt (fun (x : ) => (Real.fourierChar x)) (2 * Real.pi * Complex.I * (Real.fourierChar x)) x
theorem Real.differentiable_fourierChar :
Differentiable fun (x : ) => (Real.fourierChar x)
theorem Real.deriv_fourierChar (x : ) :
deriv (fun (x : ) => (Real.fourierChar x)) x = 2 * Real.pi * Complex.I * (Real.fourierChar x)
theorem Real.hasFDerivAt_fourierChar_neg_bilinear_right {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (v : V) (w : W) :
HasFDerivAt (fun (w : W) => (Real.fourierChar (-(L v) w))) ((-2 * Real.pi * Complex.I * (Real.fourierChar (-(L v) w))) Complex.ofRealCLM.comp (L v)) w
theorem Real.fderiv_fourierChar_neg_bilinear_right_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (v : V) (w : W) (y : W) :
(fderiv (fun (w : W) => (Real.fourierChar (-(L v) w))) w) y = -2 * Real.pi * Complex.I * ((L v) y) * (Real.fourierChar (-(L v) w))
theorem Real.differentiable_fourierChar_neg_bilinear_right {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (v : V) :
Differentiable fun (w : W) => (Real.fourierChar (-(L v) w))
theorem Real.hasFDerivAt_fourierChar_neg_bilinear_left {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (v : V) (w : W) :
HasFDerivAt (fun (v : V) => (Real.fourierChar (-(L v) w))) ((-2 * Real.pi * Complex.I * (Real.fourierChar (-(L v) w))) Complex.ofRealCLM.comp (L.flip w)) v
theorem Real.fderiv_fourierChar_neg_bilinear_left_apply {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (v : V) (y : V) (w : W) :
(fderiv (fun (v : V) => (Real.fourierChar (-(L v) w))) v) y = -2 * Real.pi * Complex.I * ((L y) w) * (Real.fourierChar (-(L v) w))
theorem Real.differentiable_fourierChar_neg_bilinear_left {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace V] [NormedAddCommGroup W] [NormedSpace W] (L : V →L[] W →L[] ) (w : W) :
Differentiable fun (v : V) => (Real.fourierChar (-(L v) w))

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
Instances For
    @[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 : VE) (v : V) (w : W) :
    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 : VE) (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.

    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.

    The Fourier integral of the derivative of a function is obtained by multiplying the Fourier integral of the original function by -L w v.

    The formal multilinear series whose n-th term is (w₁, ..., wₙ) ↦ (-2πI)^n * L v w₁ * ... * L v wₙ • f v, as a continuous multilinear map in the space W [×n]→L[ℝ] E.

    This is designed so that the Fourier transform of v ↦ fourierPowSMulRight L f v n is the n-th derivative of the Fourier transform of f.

    Equations
    Instances For
      @[simp]
      theorem VectorFourier.fourierPowSMulRight_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 : VE} {v : V} {n : } {m : Fin nW} :
      (VectorFourier.fourierPowSMulRight L f v n) m = (-(2 * Real.pi * Complex.I)) ^ n (∏ i : Fin n, (L v) (m i)) f v
      theorem VectorFourier.fourierPowSMulRight_eq_comp {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 : VE} {v : V} {n : } :
      VectorFourier.fourierPowSMulRight L f v n = (-(2 * Real.pi * Complex.I)) ^ n ((ContinuousMultilinearMap.smulRightL (fun (x : Fin n) => W) E) ((ContinuousMultilinearMap.mkPiAlgebra (Fin n) ).compContinuousLinearMapLRight fun (x : Fin n) => L v)) (f v)

      Decomposing fourierPowSMulRight L f v n as a composition of continuous bilinear and multilinear maps, to deduce easily its continuity and differentiability properties.

      theorem ContDiff.fourierPowSMulRight {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 : VE} {k : ℕ∞} (hf : ContDiff k f) (n : ) :
      theorem VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight {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 : VE} {K : ℕ∞} {C : } (hf : ContDiff K f) {n : } {k : } (hk : k K) {v : V} (hv : ik, jn, v ^ j * iteratedFDeriv i f v C) :
      iteratedFDeriv k (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) v (2 * Real.pi) ^ n * (2 * n + 2) ^ k * L ^ n * C

      The iterated derivative of a function multiplied by (L v ⬝) ^ n can be controlled in terms of the iterated derivatives of the initial function.

      If ‖v‖^n * ‖f v‖ is integrable for all n ≤ N, then the Fourier transform of f is C^N.

      If ‖v‖^n * ‖f v‖ is integrable for all n ≤ N, then the n-th derivative of the Fourier transform of f is the Fourier transform of fourierPowSMulRight L f v n, i.e., (L v ⬝) ^ n • f v.

      theorem VectorFourier.fourierIntegral_iteratedFDeriv {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 : VE} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (n : ), n NMeasureTheory.Integrable (iteratedFDeriv n f) μ) {n : } (hn : n N) :

      The Fourier integral of the n-th derivative of a function is obtained by multiplying the Fourier integral of the original function by (2πI L w ⬝ )^n.

      theorem VectorFourier.fourierPowSMulRight_iteratedFDeriv_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 : VE} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K : ℕ∞} {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (k n : ), k Kn NMeasureTheory.Integrable (fun (v : V) => v ^ k * iteratedFDeriv n f v) μ) {k : } {n : } (hk : k K) (hn : n N) {w : W} :

      The k-th derivative of the Fourier integral of f, multiplied by (L v w) ^ n, is the Fourier integral of the n-th derivative of (L v w) ^ k * f.

      theorem VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_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 : VE} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K : ℕ∞} {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (k n : ), k Kn NMeasureTheory.Integrable (fun (v : V) => v ^ k * iteratedFDeriv n f v) μ) {k : } {n : } (hk : k K) (hn : n N) {w : W} :
      VectorFourier.fourierPowSMulRight (-L.flip) (iteratedFDeriv k (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f)) w n (2 * Real.pi) ^ k * (2 * k + 2) ^ n * L ^ k * pFinset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), v ^ p.1 * iteratedFDeriv p.2 f vμ

      One can bound the k-th derivative of the Fourier integral of f, multiplied by (L v w) ^ n, in terms of integrals of iterated derivatives of f (of order up to n) multiplied by ‖v‖ ^ i (for i ≤ k). Auxiliary version in terms of the operator norm of fourierPowSMulRight (-L.flip) ⬝. For a version in terms of |L v w| ^ n * ⬝, see pow_mul_norm_iteratedFDeriv_fourierIntegral_le.

      theorem VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_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 : VE} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K : ℕ∞} {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (k n : ), k Kn NMeasureTheory.Integrable (fun (v : V) => v ^ k * iteratedFDeriv n f v) μ) {k : } {n : } (hk : k K) (hn : n N) (v : V) (w : W) :
      |(L v) w| ^ n * iteratedFDeriv k (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) w v ^ n * (2 * Real.pi * L) ^ k * (2 * k + 2) ^ n * pFinset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), v ^ p.1 * iteratedFDeriv p.2 f vμ

      One can bound the k-th derivative of the Fourier integral of f, multiplied by (L v w) ^ n, in terms of integrals of iterated derivatives of f (of order up to n) multiplied by ‖v‖ ^ i (for i ≤ k).

      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 : VE} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hvf_int : MeasureTheory.Integrable (fun (v : V) => v * f v) MeasureTheory.volume) (x : V) :

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

      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 : VE} (hf_int : MeasureTheory.Integrable f MeasureTheory.volume) (hvf_int : MeasureTheory.Integrable (fun (v : V) => v * f v) MeasureTheory.volume) :

      The Fourier integral of the Fréchet derivative of a function is obtained by multiplying the Fourier integral of the original function by 2πI ⟪v, w⟫.

      theorem Real.contDiff_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] {f : VE} {N : ℕ∞} (hf : ∀ (n : ), n NMeasureTheory.Integrable (fun (v : V) => v ^ n * f v) MeasureTheory.volume) :

      If ‖v‖^n * ‖f v‖ is integrable, then the Fourier transform of f is C^n.

      theorem Real.iteratedFDeriv_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] {f : VE} {N : ℕ∞} (hf : ∀ (n : ), n NMeasureTheory.Integrable (fun (v : V) => v ^ n * f v) MeasureTheory.volume) (h'f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) {n : } (hn : n N) :

      If ‖v‖^n * ‖f v‖ is integrable, then the n-th derivative of the Fourier transform of f is the Fourier transform of fun v ↦ (-2 * π * I) ^ n ⟪v, ⬝⟫^n f v.

      theorem Real.fourierIntegral_iteratedFDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] {f : VE} {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (n : ), n NMeasureTheory.Integrable (iteratedFDeriv n f) MeasureTheory.volume) {n : } (hn : n N) :

      The Fourier integral of the n-th derivative of a function is obtained by multiplying the Fourier integral of the original function by (2πI L w ⬝ )^n.

      theorem Real.pow_mul_norm_iteratedFDeriv_fourierIntegral_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [FiniteDimensional V] [MeasurableSpace V] [BorelSpace V] {f : VE} {K : ℕ∞} {N : ℕ∞} (hf : ContDiff N f) (h'f : ∀ (k n : ), k Kn NMeasureTheory.Integrable (fun (v : V) => v ^ k * iteratedFDeriv n f v) MeasureTheory.volume) {k : } {n : } (hk : k K) (hn : n N) (w : V) :
      w ^ n * iteratedFDeriv k (Real.fourierIntegral f) w (2 * Real.pi) ^ k * (2 * k + 2) ^ n * pFinset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), v ^ p.1 * iteratedFDeriv p.2 f v

      One can bound ‖w‖^n * ‖D^k (𝓕 f) w‖ in terms of integrals of the derivatives of f (or order at most n) multiplied by powers of v (of order at most k).

      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) :
      theorem Real.fourierIntegral_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : Differentiable f) (hf' : MeasureTheory.Integrable (deriv f) MeasureTheory.volume) :

      The Fourier integral of the Fréchet derivative of a function is obtained by multiplying the Fourier integral of the original function by 2πI x.

      theorem Real.iteratedDeriv_fourierIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {N : ℕ∞} {n : } (hf : ∀ (n : ), n NMeasureTheory.Integrable (fun (x : ) => x ^ n f x) MeasureTheory.volume) (hn : n N) :
      theorem Real.fourierIntegral_iteratedDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {N : ℕ∞} {n : } (hf : ContDiff N f) (h'f : ∀ (n : ), n NMeasureTheory.Integrable (iteratedDeriv n f) MeasureTheory.volume) (hn : n N) :