English
The star subalgebra of C(UnitAddTorus d, ℂ) generated by all mFourier n is the smallest star subalgebra containing these Fourier monomials; equivalently it is Algebra.adjoin ℂ (range mFourier).
Русский
Звёздовая подалгебра в C(UnitAddTorus d, ℂ), генерируемая всеми mFourier n, есть наименьшая звёздовая подалгебра, содержащая эти мономиалы Фурье; эквивалентно она равна Algebra.adjoin ℂ (range mFourier).
LaTeX
$$$ \text{StarSubalgebra}(\\mathbb{C}, C(UnitAddTorus d, \\mathbb{C})) = \\text{Algebra.adjoin }\\mathbb{C}(\mathrm{range}\\, mFourier) $$$
Lean4
/-- The star subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ`. -/
def mFourierSubalgebra (d : Type*) [Fintype d] : StarSubalgebra ℂ C(UnitAddTorus d, ℂ)
where
toSubalgebra := Algebra.adjoin ℂ (range mFourier)
star_mem' := by
change Algebra.adjoin ℂ (range mFourier) ≤ star (Algebra.adjoin ℂ (range mFourier))
refine adjoin_le ?_
rintro _ ⟨n, rfl⟩
refine subset_adjoin ⟨-n, ?_⟩
ext1 x
simp only [mFourier_neg, starRingEnd_apply, ContinuousMap.star_apply]
