English
There is a Fréchet derivative for the Fourier transform 𝓕 f at a point, given by the derivative of the transformed function with respect to the input via the smoothed action.
Русский
Существуют Фреше-дифференциалы для Фурье-преобразования 𝓕 f в точке; производная выражается через дифференциал преобразования при действии сглаженных данных.
LaTeX
$$$$ \text{HasDerivAt}\,(\mathcal{F}f)(x) = \mathcal{F}\bigl( (2\pi i x) f(x) \bigr) $$$$
Lean4
theorem hasDerivAt_fourierIntegral {f : ℝ → E} (hf : Integrable f) (hf' : Integrable (fun x : ℝ ↦ x • f x)) (w : ℝ) :
HasDerivAt (𝓕 f) (𝓕 (fun x : ℝ ↦ (-2 * π * I * x) • f x) w) w :=
by
have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using hf'.norm
let L := ContinuousLinearMap.mul ℝ ℝ |>.flip
have h_int : Integrable fun v ↦ fourierSMulRight L f v :=
by
suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
convert
((ContinuousLinearMap.ring_lmap_equiv_self ℝ
E).symm.toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp
hf' using
2 with _ v
apply ContinuousLinearMap.ext_ring
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul_apply', one_mul,
ContinuousLinearMap.map_smul]
exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm
rw [← VectorFourier.fourierIntegral_convergent_iff continuous_fourierChar L.continuous₂ w] at h_int
convert (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1
erw [ContinuousLinearMap.integral_apply h_int]
simp_rw [ContinuousLinearMap.smul_apply, fourierSMulRight, ContinuousLinearMap.smul_apply,
ContinuousLinearMap.smulRight_apply, L, ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul_apply', one_mul, ←
neg_mul, mul_smul]
rfl
