fourierIntegral_const_smul — Mathlib

English

Scaling the input function by a constant factor r scales the Fourier integral by the same factor r.

Русский

Умножение входной функции на константу r тождественно масштабирует преобразование Фурье на r.

LaTeX

$$$$ \\mathrm{fourierIntegral}(e, μ, r\\cdot f) = r \\cdot \\mathrm{fourierIntegral}(e, μ, f). $$$$

Lean4

theorem fourierIntegral_const_smul (e : AddChar 𝕜 𝕊) (μ : Measure 𝕜) (f : 𝕜 → E) (r : ℂ) :
    fourierIntegral e μ (r • f) = r • fourierIntegral e μ f :=
  VectorFourier.fourierIntegral_const_smul _ _ _ _ _

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