English
The Fourier integral of the n-th derivative of f is obtained by multiplying the Fourier integral of f by a fixed weight raised to the n-th power, reflecting the derivative order.
Русский
Фурье-интеграл n-й производной f получает умножение на фиксированный вес, возведённый в степень n, отражая порядок производной.
LaTeX
$$$$ \mathcal{F}\bigl( \mathrm{iteratedFDeriv}_{\mathbb{R}}^{n} f \bigr)(w) = \bigl( \text{weight}(w) \bigr)^{n} \; \mathcal{F}f(w) $$$$
Lean4
theorem fourierIntegral_iteratedDeriv {f : ℝ → E} {N : ℕ∞} {n : ℕ} (hf : ContDiff ℝ N f)
(h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedDeriv n f)) (hn : n ≤ N) :
𝓕 (iteratedDeriv n f) = fun (x : ℝ) ↦ (2 * π * I * x) ^ n • (𝓕 f x) :=
by
ext x : 1
have A : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) :=
by
intro n hn
rw [iteratedFDeriv_eq_equiv_comp]
exact (LinearIsometryEquiv.integrable_comp_iff _).2 (h'f n hn)
change 𝓕 (fun x ↦ iteratedDeriv n f x) x = _
simp_rw [iteratedDeriv, ← fourierIntegral_continuousMultilinearMap_apply (A n hn),
fourierIntegral_iteratedFDeriv hf A hn]
simp [← coe_smul, smul_smul, ← mul_pow]
