fourierIntegral_const_smul — Mathlib

English

Linearity holds for the Fourier transform when the input is multiplied by a scalar from the field and when the function is vector-valued, i.e., the transform distributes over addition and scalar multiplication.

Русский

Линейность преобразования Фурье сохраняется для векторнозначных функций: преобразование распределяется по сложению и умножению на скаляры.

LaTeX

$$$$ \\mathrm{fourierIntegral}(e, \\mu, L, f + g) = \\mathrm{fourierIntegral}(e, \\mu, L, f) + \\mathrm{fourierIntegral}(e, \\mu, L, g) $$$$

Lean4

theorem fourierIntegral_const_smul (e : AddChar 𝕜 𝕊) (μ : Measure V) (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (r : ℂ) :
    fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f :=
  by
  ext1 w
  simp only [Pi.smul_apply, fourierIntegral, smul_comm _ r, integral_smul]

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