English
Let f be a function on the circle AddCircle T with values in a normed space E, and c be a complex scalar. The nth Fourier coefficient is linear in the function: the coefficient of c·f is c times the coefficient of f.
Русский
Пусть f — функция на кольце AddCircle T со значениями в нормированном пространстве E, а c — комплексный скаляр. Тогда коэффициент Фурье n линейен по отношению к умножению функции на скаляр: коэффициент к функции c·f равен c на коэффициент f.
LaTeX
$$$$ \\widehat{(c\\cdot f)}_n = c\\cdot \\widehat{f}_n $$$$
Lean4
theorem const_smul (f : AddCircle T → E) (c : ℂ) (n : ℤ) : fourierCoeff (c • f :) n = c • fourierCoeff f n := by
simp_rw [fourierCoeff, Pi.smul_apply, ← smul_assoc, smul_eq_mul, mul_comm, ← smul_eq_mul, smul_assoc, integral_smul]
