English
A variant of the iterated derivative result with a slightly adjusted indexing, showing the equality for the nth iterated derivative of FourierIntegral in terms of FourierPowSMulRight.
Русский
Вариант результата об итеративной производной с немного изменённой индексацией, демонстрирующий равенство для n-й итерационной производной FourierIntegral через FourierPowSMulRight.
LaTeX
$$$\\text{iteratedFDeriv}_{\\mathbb{R}}^n (\\text{fourierIntegral}) = \\text{fourierIntegral}( \\text{fourierPowSMulRight } L f v n)$$$
Lean4
/-- If `‖v‖^n * ‖f v‖` is integrable for all `n ≤ N`, then the `n`-th derivative of the Fourier
transform of `f` is the Fourier transform of `fourierPowSMulRight L f v n`,
i.e., `(L v ⬝) ^ n • f v`. -/
theorem iteratedFDeriv_fourierIntegral {N : ℕ∞} (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ)
(h'f : AEStronglyMeasurable f μ) {n : ℕ} (hn : n ≤ N) :
iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) =
fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun v ↦ fourierPowSMulRight L f v n) :=
by
ext w : 1
exact ((hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f).eq_iteratedFDeriv (mod_cast hn) w).symm
