Theorems · Theorem · harmonic analysis

Real.fourier_fderiv

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E},
  MeasureTheory.Integrable f MeasureTheory.volume →
    Differentiable ℝ f →
      MeasureTheory.Integrable (fderiv ℝ f) MeasureTheory.volume →
        FourierTransform.fourier (fderiv ℝ f) = VectorFourier.fourierSMulRight (-innerSL ℝ) (FourierTransform.fourier 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⟫.

Defined in

Mathlib.Analysis.Fourier.FourierTransformDeriv

Cited by

2 results in Mathlib

Foundations

Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupInnerProductSpaceFiniteDimensionalMeasurableSpaceBorelSpace