integrable_fourierPowSMulRight — Mathlib

English

A variant stating that the Fourier integral is differentiable under certain integrability hypotheses, with the derivative given by the corresponding FourierPowSMulRight term.

Русский

Вариант утверждает, что Фурье-интеграл дифференцируем при определённых условиях интегрируемости, а производная выражается через соответствующий член FourierPowSMulRight.

LaTeX

$$$\\text{ContDiff} \\; \\mathbb{R} \\; \\text{(FourierIntegral value)}$$$

Lean4

theorem integrable_fourierPowSMulRight {n : ℕ} (hf : Integrable (fun v ↦ ‖v‖ ^ n * ‖f v‖) μ)
    (h'f : AEStronglyMeasurable f μ) : Integrable (fun v ↦ fourierPowSMulRight L f v n) μ :=
  by
  refine (hf.const_mul ((2 * π * ‖L‖) ^ n)).mono' (h'f.fourierPowSMulRight L n) ?_
  filter_upwards with v
  exact (norm_fourierPowSMulRight_le L f v n).trans (le_of_eq (by ring))

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