English
The n-th iterated derivative of the Fourier integral equals the Fourier integral of the n-th Fourier power-smulRight term, i.e., iteratedFDeriv f = FourierPowSMulRight L f v n inside the integral framework.
Русский
n-я итерационная производная Фурье-интеграла равна Фурье-интегралу от n-й степени 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 Fourier transform of `f` is `C^N`. -/
theorem contDiff_fourierIntegral {N : ℕ∞} (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ) :
ContDiff ℝ N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) :=
by
by_cases h'f : Integrable f μ
· exact (hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff
· have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by ext w; simp [fourierIntegral, integral, h'f]
simpa [this] using contDiff_const
