const_mul — Mathlib

English

Analogous to the previous result, for f:ℝ→ℂ and c∈ℂ, the Fourier coefficients on the interval satisfy fourierCoeffOn hab (c•f) n = c • fourierCoeffOn hab f n.

Русский

Аналогично, для f:ℝ→ℂ и скаляра c коэффициенты Фурье на отрезке удовлетворяют fourierCoeffOn hab (c•f) n = c • fourierCoeffOn hab f n.

LaTeX

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

Lean4

theorem const_mul {a b : ℝ} (f : ℝ → ℂ) (c : ℂ) (n : ℤ) (hab : a < b) :
    fourierCoeffOn hab (fun x => c * f x) n = c * fourierCoeffOn hab f n :=
  fourierCoeffOn.const_smul _ _ _ _

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