English
A variant of the Fréchet derivative formula for the Fourier transform, highlighting the structure of the derivative with respect to the transform input.
Русский
Вариант формулы Фреше-производной Фурье-преобразования, подчёркивающий структуру производной по входу преобразования.
LaTeX
$$$$ \text{HasFDerivAt}(\mathcal{F} f) = \mathcal{F}\bigl( \text{smoothed version of } f \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 x`. -/
theorem fourierIntegral_deriv {f : ℝ → E} (hf : Integrable f) (h'f : Differentiable ℝ f) (hf' : Integrable (deriv f)) :
𝓕 (deriv f) = fun (x : ℝ) ↦ (2 * π * I * x) • (𝓕 f x) :=
by
ext x
have I : Integrable (fun x ↦ fderiv ℝ f x) := by
simpa only [← deriv_fderiv] using (ContinuousLinearMap.smulRightL ℝ ℝ E 1).integrable_comp hf'
have : 𝓕 (deriv f) x = 𝓕 (fderiv ℝ f) x 1 := by simp only [fourierIntegral_continuousLinearMap_apply I, fderiv_deriv]
rw [this, fourierIntegral_fderiv hf h'f I]
simp only [fourierSMulRight_apply, ContinuousLinearMap.neg_apply, innerSL_apply, smul_smul, RCLike.inner_apply',
conj_trivial, mul_one, neg_smul, smul_neg, neg_neg, neg_mul, ← coe_smul]
