English
The Fourier transform 𝓕 f has a Fréchet derivative at a point x, given by the derivative of the transformed function with respect to the original function, i.e., HasFDerivAt(𝓕 f) at x equals the action of the differential of the Fourier operator on f.
Русский
Фурье-преобразование 𝓕 f имеет предел-фредхелеву производную в точке x; производная Фурье-оператора действует на f аналогично дифференциалу преобразования.
LaTeX
$$$$ \text{HasFDerivAt} \, (\mathcal{F} f) \, \bigl( \mathcal{F}(\mathrm{fourierSMulRight}(\mathrm{innerSL}\, \mathbb{R}) f) \bigr) (x) $$$$
Lean4
/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of
`fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`. -/
theorem hasFDerivAt_fourierIntegral (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) (x : V) :
HasFDerivAt (𝓕 f) (𝓕 (fourierSMulRight (innerSL ℝ) f) x) x :=
VectorFourier.hasFDerivAt_fourierIntegral (innerSL ℝ) hf_int hvf_int x
