const_smul — Mathlib

English

For hab with a<b and f:ℝ→E, the map f↦fourierCoeffOn hab f is linear with respect to scalar multiplication: fourierCoeffOn hab (c•f) n = c•fourierCoeffOn hab f n.

Русский

Для hab с a<b и f:ℝ→E коэффициенты Фурье на отрезке линейны по отношению к скаляру: fourierCoeffOn hab (c•f) n = c•fourierCoeffOn hab f n.

LaTeX

$$$$ \\widehat{f}_{[a,b],n}^{\\text{On}}(c\\cdot f) = c\\cdot \\widehat{f}_{[a,b],n}^{\\text{On}}(f) $$$$

Lean4

theorem const_smul {a b : ℝ} (f : ℝ → E) (c : ℂ) (n : ℤ) (hab : a < b) :
    fourierCoeffOn hab (c • f) n = c • fourierCoeffOn hab f n :=
  by
  haveI := Fact.mk (by linarith : 0 < b - a)
  apply fourierCoeff.const_smul

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