English
If a suitable integrability condition holds for all required derivatives, then the Fourier transform is continuously differentiable (C^N) as a function of its spatial variable.
Русский
Если выполнены условия интегрируемости для всех требуемых производных, Фурье-преобразование является непрерывно дифференцируемым (C^N) по пространственной переменной.
LaTeX
$$$\\text{ContDiff}_{\\mathbb{R}}\\; N\\; (\\text{fourierIntegral})$$$
Lean4
/-- Variant of `hasFTaylorSeriesUpTo_fourierIntegral` in which the smoothness index is restricted
to `ℕ∞` (and so are the inequalities in the assumption `hf`). Avoids normcasting in some
applications. -/
theorem hasFTaylorSeriesUpTo_fourierIntegral' {N : ℕ∞} (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ)
(h'f : AEStronglyMeasurable f μ) :
HasFTaylorSeriesUpTo N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
(fun w n ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun v ↦ fourierPowSMulRight L f v n) w) :=
hasFTaylorSeriesUpTo_fourierIntegral _ (fun n hn ↦ hf n (mod_cast hn)) h'f
