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 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 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.
• 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.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.

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

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

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

• One or more equations did not get rendered due to their size.

@[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 • (Finset.prod Finset.univ fun (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.compContinuousLinearMapLRight (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)) 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 : ℕ∞} (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 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} [SecondCountableTopology V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure 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} [SecondCountableTopology V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure 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} [SecondCountableTopology V] [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure 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 μ (ContinuousLinearMap.toLinearMap₂ L) f) fun (w : W) (n : ℕ) => VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₂ L) (fun (v : V) => VectorFourier.fourierPowSMulRight L f v n) w

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