English
The subalgebra generated by mFourier n is exactly the complex span of the Fourier monomials: (mFourierSubalgebra d).toSubalgebra.toSubmodule = span_ℂ (range mFourier).
Русский
Подалгебра, порождённая mFourier n, совпадает с комплексной линейной оболочкой функций mFourier: (mFourierSubalgebra d).toSubalgebra.toSubmodule = span_ℂ (range mFourier).
LaTeX
$$$ (mFourierSubalgebra d).toSubalgebra.toSubmodule = \operatorname{span}_{\mathbb{C}}(\operatorname{range} mFourier) $$$
Lean4
/-- The star subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ` is in fact
the linear span of these functions. -/
theorem mFourierSubalgebra_coe : (mFourierSubalgebra d).toSubalgebra.toSubmodule = span ℂ (range mFourier) :=
by
apply adjoin_eq_span_of_subset
refine .trans (fun x ↦ Submonoid.closure_induction (fun _ ↦ id) ⟨0, ?_⟩ ?_) subset_span
· ext z
simp only [mFourier, Pi.zero_apply, fourier_zero, Finset.prod_const, one_pow, ContinuousMap.coe_mk,
ContinuousMap.one_apply]
· rintro _ _ _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
refine ⟨m + n, ?_⟩
ext z
simp only [mFourier, Pi.add_apply, fourier_apply, fourier_add', Finset.prod_mul_distrib, ContinuousMap.coe_mk,
ContinuousMap.mul_apply]
