English
The Fréchet derivative of the Fourier transform 𝓕 f exists under integrability assumptions, and equals the Fourier transform of the smoothed function f with respect to the inner product with w.
Русский
Существование Фредхелевой (Фрéше) производной Фурье-преобразования 𝓕 f при условии интегрируемости; она равна Фурье-преобразованию сглаженной функции по внутреннему произведению.
LaTeX
$$$$ fderiv(\mathcal{F} f) = \mathcal{F}\bigl( fourierSMulRight (innerSL \mathbb{R}) f \bigr) $$$$
Lean4
/-- The Fréchet derivative of the Fourier transform of `f` is the Fourier transform of
`fun v ↦ -2 * π * I ⟪v, ⬝⟫ f v`. -/
theorem fderiv_fourierIntegral (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) :
fderiv ℝ (𝓕 f) = 𝓕 (fourierSMulRight (innerSL ℝ) f) :=
VectorFourier.fderiv_fourierIntegral (innerSL ℝ) hf_int hvf_int
