fderiv_fourierIntegral — Mathlib

English

The Fréchet derivative of the Fourier integral is given by the Fourier transform of the derivative-perturbed integrand, with a minus flip of L.

Русский

Фретше-производная Фурье-интеграла задаётся Фурье-преобразованием производной изменённого интегранта, с минус-флипом L.

LaTeX

$$$\\text{fderiv}\\_\u211d(\\text{fourierIntegral}) = \\text{fourierIntegral}\\_\u211d( -L.flip , f)$$$

Lean4

theorem fderiv_fourierIntegral [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] {μ : Measure V}
    (hf : Integrable f μ) (hf' : Integrable (fun v : V ↦ ‖v‖ * ‖f v‖) μ) :
    fderiv ℝ (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) = fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) :=
  by
  ext w : 1
  exact (hasFDerivAt_fourierIntegral L hf hf' w).fderiv

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