differentiable_fourierIntegral — Mathlib

English

If both the function f and the unit-scaled derivatives ‖v‖^n‖f(v)‖ satisfy integrability, then the Fourier integral is differentiable with respect to the spatial variables.

Русский

Если функция f и условно нормированные производные удовлетворяют интегрируемости, то Фурье-интеграл является дифференцируемым по пространственным переменным.

LaTeX

$$$\\text{Differentiable}_{\\mathbb{R}}( \\text{fourierIntegral} )$$$

Lean4

theorem differentiable_fourierIntegral [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V}
    (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) :
    Differentiable ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) := fun w ↦
  (hasFDerivAt_fourierIntegral L hf hf' w).differentiableAt

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