English
The iterated derivative of the Fourier transform satisfies a closed-form in terms of iterated derivatives of f with corresponding polynomial weights.
Русский
Итерированная производная Фурье-преобразования удовлетворяет замкнутой формуле в терминах итерированных производных f с соответствующими полиномиальными весами.
LaTeX
$$$$ \mathrm{iteratedFDeriv}_{\mathbb{R}}^{k}(\mathcal{F} f) = \mathcal{F}\bigl( \mathrm{iteratedFDeriv}_{\mathbb{R}}^{k}(f) \bigr) $$$$
Lean4
theorem iteratedDeriv_fourierIntegral {f : ℝ → E} {N : ℕ∞} {n : ℕ}
(hf : ∀ (n : ℕ), n ≤ N → Integrable (fun x ↦ x ^ n • f x)) (hn : n ≤ N) :
iteratedDeriv n (𝓕 f) = 𝓕 (fun x : ℝ ↦ (-2 * π * I * x) ^ n • f x) :=
by
ext x : 1
have A (n : ℕ) (hn : n ≤ N) : Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) :=
by
convert (hf n hn).norm with x
simp [norm_smul]
have B : AEStronglyMeasurable f := by simpa using (hf 0 (zero_le _)).1
rw [iteratedDeriv, iteratedFDeriv_fourierIntegral A B hn,
fourierIntegral_continuousMultilinearMap_apply (integrable_fourierPowSMulRight _ (A n hn) B), fourierIntegral_eq,
fourierIntegral_eq]
congr with y
suffices (-(2 * π * I)) ^ n • y ^ n • f y = (-(2 * π * I * y)) ^ n • f y by simpa [innerSL_apply _]
simp only [← neg_mul, ← coe_smul, smul_smul, mul_pow, ofReal_pow, mul_assoc]
