English
The subalgebra generated by the Fourier monomials corresponds exactly to the span of those monomials; its underlying subspace is the linear span of {f_n}.
Русский
Порождённая Фурье-мононимиалами подалгебра соответствует линейному спану этих функций; её основание — линейный спан {f_n}.
LaTeX
$$Subalgebra.toSubmodule (@fourierSubalgebra T).toSubalgebra = span ℂ (range fourier).$$
Lean4
/-- The star subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` is in fact the
linear span of these functions. -/
theorem fourierSubalgebra_coe :
Subalgebra.toSubmodule (@fourierSubalgebra T).toSubalgebra = span ℂ (range (@fourier T)) :=
by
apply adjoin_eq_span_of_subset
refine Subset.trans ?_ Submodule.subset_span
intro x hx
refine Submonoid.closure_induction (fun _ => id) ⟨0, ?_⟩ ?_ hx
· ext1 z; exact fourier_zero
· rintro - - - - ⟨m, rfl⟩ ⟨n, rfl⟩
refine ⟨m + n, ?_⟩
ext1 z
exact fourier_add
