contDiff_fourierIntegral — Mathlib

English

If all low-order derivatives of f are integrable with polynomial weights, then 𝓕 f is C^N (i.e., has continuous derivatives up to order N).

Русский

Если для всех порядков до N справедлива интегрируемость с весами, то 𝓕 f имеет непрерывные производные до порядка N.

LaTeX

$$$$ \text{ContDiff}_{\mathbb{R}}(N)(\mathcal{F}f) $$$$

Lean4

/-- If `‖v‖^n * ‖f v‖` is integrable, 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 (𝓕 f) :=
  VectorFourier.contDiff_fourierIntegral (innerSL ℝ) hf

Похожие утверждения