differentiable_fourierIntegral — Mathlib

English

If f is integrable and its Fourier transform is integrable, then 𝓕 f is differentiable (indeed C^1 under mild conditions).

Русский

Если f интегрируема и её Фурье-преобразование интегрируемо, то 𝓕 f дифференцируема (при умеренных условиях даже C^1).

LaTeX

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

Lean4

theorem differentiable_fourierIntegral (hf_int : Integrable f) (hvf_int : Integrable (fun v ↦ ‖v‖ * ‖f v‖)) :
    Differentiable ℝ (𝓕 f) :=
  VectorFourier.differentiable_fourierIntegral (innerSL ℝ) hf_int hvf_int

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