English
Let f be a suitably smooth function with finite-dimensional domain; the Fourier transform of the n-th derivative of f is obtained by multiplying the Fourier transform of f by a polynomial factor determined by the linear map L and the variable w. In particular, 𝓕(D^n f)(w) = (2π i L w)^{n} 𝓕(f)(w) in the appropriate setting.
Русский
Пусть f задана на конечномерном пространстве, достаточно гладкая; Фурье-преобразование n-й производной f получается умножением Фурье-преобразования f на степенной множитель, зависящий от линейного отображения L и переменной w: 𝓕(D^n f)(w) = (2π i L w)^{n} 𝓕(f)(w).
LaTeX
$$$\mathcal{F}\bigl(\mathrm{iteratedFDeriv}_{\mathbb{R}}^{n} f\bigr)(w) = \bigl( (2\pi i) \, L(w) \bigr)^{n} \; \mathcal{F}f(w)$$$
Lean4
/-- The Fourier integral of the `n`-th derivative of a function is obtained by multiplying the
Fourier integral of the original function by `(2πI L w ⬝ )^n`. -/
theorem fourierIntegral_iteratedFDeriv [FiniteDimensional ℝ V] {μ : Measure V} [Measure.IsAddHaarMeasure μ] {N : ℕ∞}
(hf : ContDiff ℝ N f) (h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ) {n : ℕ} (hn : n ≤ N) :
fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ n f) =
(fun w ↦ fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w n) :=
by
induction n with
| zero =>
ext w m
simp only [iteratedFDeriv_zero_apply, fourierPowSMulRight_apply, pow_zero, Finset.univ_eq_empty,
ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply, Finset.prod_empty, one_smul,
fourierIntegral_continuousMultilinearMap_apply' ((h'f 0 bot_le))]
| succ n ih =>
ext w m
have J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ :=
by
specialize h'f (n + 1) hn
rwa [iteratedFDeriv_succ_eq_comp_left, Function.comp_def,
LinearIsometryEquiv.integrable_comp_iff (𝕜 := ℝ) (φ := fderiv ℝ (iteratedFDeriv ℝ n f))] at h'f
suffices H :
(fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0) (Fin.tail m) =
(-(2 * π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -L (m x) w) • ∫ v, 𝐞 (-L v w) • f v ∂μ
by
rw [fourierIntegral_continuousMultilinearMap_apply' (h'f _ hn)]
simp only [iteratedFDeriv_succ_apply_left, fourierPowSMulRight_apply, ContinuousLinearMap.neg_apply,
ContinuousLinearMap.flip_apply]
rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)), ←
fourierIntegral_continuousLinearMap_apply' J]
exact H
have h'n : n < N := (Nat.cast_lt.mpr n.lt_succ_self).trans_le hn
rw [fourierIntegral_fderiv _ (h'f n h'n.le) (hf.differentiable_iteratedFDeriv (mod_cast h'n)) J]
simp only [ih h'n.le, fourierSMulRight_apply, ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply,
neg_smul, smul_neg, neg_neg, smul_apply, fourierPowSMulRight_apply, ← coe_smul (E := E), smul_smul]
congr 1
simp only [ofReal_prod, ofReal_neg, pow_succ, mul_neg, Fin.prod_univ_succ, neg_mul, ofReal_mul, neg_neg,
Fin.tail_def]
ring
