English
The derivative of the Fourier integral equals the Fourier integral of a derivative of the integrand with a factor of (2π i) times the variable.
Русский
Производная по переменной Фурье-интеграла равна Фурье-интегралу от производной подинтегранного выражения с множителем (2π i)·x.
LaTeX
$$$$ \frac{d}{dx} \mathcal{F}f(x) = \mathcal{F}\bigl( (2\pi i x) f(x) \bigr) $$$$
Lean4
/-- 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 fourierIntegral_fderiv (hf : Integrable f) (h'f : Differentiable ℝ f) (hf' : Integrable (fderiv ℝ f)) :
𝓕 (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f) :=
by
rw [← innerSL_real_flip V]
exact VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'
