English
The star-subalgebra of continuous functions on AddCircle(T) generated by the Fourier monomials f_n (n ∈ ℤ) is precisely the smallest star-subalgebra containing all f_n, i.e., the adjoint-closure of the span of {f_n}.
Русский
Звёзд-подалгебра непрерывных функций на AddCircle(T), порождённая мономиалами Фурье f_n (n ∈ ℤ), есть наименьшая звёздовая подалгебра, содержащая все f_n (замкнутость по операции сопряжения).
LaTeX
$$Fourier Subalgebra = Algebra.adjoin_ℂ (range fourier).$$
Lean4
/-- The star subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` . -/
def fourierSubalgebra : StarSubalgebra ℂ C(AddCircle T, ℂ)
where
toSubalgebra := Algebra.adjoin ℂ (range fourier)
star_mem' :=
by
change Algebra.adjoin ℂ (range (fourier (T := T))) ≤ star (Algebra.adjoin ℂ (range (fourier (T := T))))
refine adjoin_le ?_
rintro - ⟨n, rfl⟩
exact subset_adjoin ⟨-n, ext fun _ => fourier_neg⟩
