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:

• 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 ContinuousLinearMap.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.
• VectorFourier.fourierPowSMulRight is the higher order analogue for higher derivatives: fourierPowSMulRight L f v n is informally (-(2 * π * I))^n (L v ⬝)^n • f v, in the space of continuous multilinear maps W [×n]→L[ℝ] E.

With these definitions, 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.
• VectorFourier.fourierIntegral_fderiv: formula for the Fourier integral of the derivative of f.
• VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral: under suitable integrability conditions, the Fourier integral of f has an explicit Taylor series up to order N, given by the Fourier integrals of fun v ↦ fourierPowSMulRight L f v n.
• VectorFourier.contDiff_fourierIntegral: under suitable integrability conditions, the Fourier integral of f is C^n.
• VectorFourier.iteratedFDeriv_fourierIntegral: under suitable integrability conditions, explicit formula for the n-th derivative of the Fourier integral of f, as the Fourier integral of fun v ↦ fourierPowSMulRight L f v n.
• VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le: explicit bounds for the n-th derivative of the Fourier integral, multiplied by a power function, in terms of corresponding integrals for the original function.

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 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 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))

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) • (L v).smulRight (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 μ L.toLinearMap₂ f) (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (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‖) μ) : fderiv ℝ (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) = VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (VectorFourier.fourierSMulRight L f)

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 μ L.toLinearMap₂ f)

theorem VectorFourier.fourierIntegral_fderiv {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] [FiniteDimensional ℝ V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] (hf : MeasureTheory.Integrable f μ) (h'f : Differentiable ℝ f) (hf' : MeasureTheory.Integrable (fderiv ℝ f) μ) : VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (fderiv ℝ f) = VectorFourier.fourierSMulRight (-L.flip) (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ 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.

def VectorFourier.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 : V → E) (v : V) : FormalMultilinearSeries ℝ W E

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

• VectorFourier.fourierPowSMulRight L f v n = (-(2 * ↑Real.pi * Complex.I)) ^ n • (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (f v)).compContinuousLinearMap fun (x : Fin n) => L v

@[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 : V → E} {v : V} {n : ℕ} {m : Fin n → W} : (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 : V → E} {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 Continuous.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 : V → E} (hf : Continuous f) (n : ℕ) : Continuous fun (v : V) => VectorFourier.fourierPowSMulRight L f v n

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 : V → E} {k : WithTop ℕ∞} (hf : ContDiff ℝ k f) (n : ℕ) : ContDiff ℝ k fun (v : V) => VectorFourier.fourierPowSMulRight L f v n

theorem VectorFourier.norm_fourierPowSMulRight_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) (n : ℕ) : ‖VectorFourier.fourierPowSMulRight L f v n‖ ≤ (2 * Real.pi * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

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 : V → E} {K : WithTop ℕ∞} {C : ℝ} (hf : ContDiff ℝ K f) {n k : ℕ} (hk : ↑k ≤ K) {v : V} (hv : ∀ i ≤ k, ∀ j ≤ n, ‖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.

theorem MeasureTheory.AEStronglyMeasurable.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 : V → E} [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] (hf : MeasureTheory.AEStronglyMeasurable f μ) (n : ℕ) : MeasureTheory.AEStronglyMeasurable (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) μ

theorem VectorFourier.integrable_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 : V → E} [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] {n : ℕ} (hf : MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) μ) (h'f : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.Integrable (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) μ

theorem VectorFourier.hasFTaylorSeriesUpTo_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] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] {N : WithTop ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) μ) (h'f : MeasureTheory.AEStronglyMeasurable f μ) : HasFTaylorSeriesUpTo N (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) fun (w : W) (n : ℕ) => VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) w

theorem VectorFourier.hasFTaylorSeriesUpTo_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] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] {N : ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) μ) (h'f : MeasureTheory.AEStronglyMeasurable f μ) : HasFTaylorSeriesUpTo (↑N) (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) fun (w : W) (n : ℕ) => VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) w

Variant of hasFTaylorSeriesUpTo_fourierIntegral in which the smoothness index is restricted to ℕ∞ (and so are the inequalities in the assumption hf). Avoids normcasting in some applications.

theorem VectorFourier.contDiff_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] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] {N : ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) μ) : ContDiff ℝ (↑N) (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f)

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

theorem VectorFourier.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 : V → E} [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} [SecondCountableTopology V] {N : ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) μ) (h'f : MeasureTheory.AEStronglyMeasurable f μ) {n : ℕ} (hn : ↑n ≤ N) : iteratedFDeriv ℝ n (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) = VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ fun (v : V) => VectorFourier.fourierPowSMulRight L f v 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 : V → E} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) μ) {n : ℕ} (hn : ↑n ≤ N) : VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun (w : W) => VectorFourier.fourierPowSMulRight (-L.flip) (VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ f) w 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 : V → E} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.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 = VectorFourier.fourierIntegral Real.fourierChar μ L.toLinearMap₂ (iteratedFDeriv ℝ n fun (v : V) => VectorFourier.fourierPowSMulRight L f v k) 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 : V → E} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.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 * ∑ p ∈ Finset.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 : V → E} [MeasurableSpace V] [BorelSpace V] [FiniteDimensional ℝ V] {μ : MeasureTheory.Measure V} [μ.IsAddHaarMeasure] {K N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.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 * ∑ p ∈ Finset.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 : 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) : fderiv ℝ (Real.fourierIntegral f) = Real.fourierIntegral (VectorFourier.fourierSMulRight (innerSL ℝ) f)

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.fourierIntegral_fderiv {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 : MeasureTheory.Integrable f MeasureTheory.volume) (h'f : Differentiable ℝ f) (hf' : MeasureTheory.Integrable (fderiv ℝ f) MeasureTheory.volume) : Real.fourierIntegral (fderiv ℝ f) = VectorFourier.fourierSMulRight (-innerSL ℝ) (Real.fourierIntegral f)

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 : V → E} {N : ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume) : ContDiff ℝ (↑N) (Real.fourierIntegral f)

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 : V → E} {N : ℕ∞} (hf : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun (v : V) => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume) (h'f : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) {n : ℕ} (hn : ↑n ≤ N) : iteratedFDeriv ℝ n (Real.fourierIntegral f) = Real.fourierIntegral fun (v : V) => VectorFourier.fourierPowSMulRight (innerSL ℝ) f v 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 : V → E} {N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedFDeriv ℝ n f) MeasureTheory.volume) {n : ℕ} (hn : ↑n ≤ N) : Real.fourierIntegral (iteratedFDeriv ℝ n f) = fun (w : V) => VectorFourier.fourierPowSMulRight (-innerSL ℝ) (Real.fourierIntegral f) w 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 : V → E} {K N : ℕ∞} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → MeasureTheory.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 * ∑ p ∈ Finset.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) : deriv (Real.fourierIntegral f) = Real.fourierIntegral fun (x : ℝ) => (-2 * ↑Real.pi * Complex.I * ↑x) • f x

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) : Real.fourierIntegral (deriv f) = fun (x : ℝ) => (2 * ↑Real.pi * Complex.I * ↑x) • Real.fourierIntegral f x

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 ≤ N → MeasureTheory.Integrable (fun (x : ℝ) => x ^ n • f x) MeasureTheory.volume) (hn : ↑n ≤ N) : iteratedDeriv n (Real.fourierIntegral f) = Real.fourierIntegral fun (x : ℝ) => (-2 * ↑Real.pi * Complex.I * ↑x) ^ n • f x

theorem Real.fourierIntegral_iteratedDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℝ → E} {N : ℕ∞} {n : ℕ} (hf : ContDiff ℝ (↑N) f) (h'f : ∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (iteratedDeriv n f) MeasureTheory.volume) (hn : ↑n ≤ N) : Real.fourierIntegral (iteratedDeriv n f) = fun (x : ℝ) => (2 * ↑Real.pi * Complex.I * ↑x) ^ n • Real.fourierIntegral f x