span_mFourier_closure_eq_top — Mathlib

English

The complex span of Fourier monomials is dense in the full function space: span mFourier is dense in C(UnitAddTorus d, ℂ).

Русский

Комплексная линейная оболочка мономиалов Фурье плотна в полном пространстве функций: span mFourier плотно в C(UnitAddTorus d, ℂ).

LaTeX

$$$ \operatorname{topClosure}_{\mathbb{C}}(\operatorname{span}(\{mFourier(n) : n \in \mathbb{Z}^d\})) = ⊤ $$$

Lean4

/-- The linear span of the monomials `mFourier n` is dense in `C(UnitAddTorus d, ℂ)`. -/
theorem span_mFourier_closure_eq_top : (span ℂ (range <| mFourier (d := d))).topologicalClosure = ⊤ :=
  by
  rw [← mFourierSubalgebra_coe]
  exact congr_arg (Subalgebra.toSubmodule <| StarSubalgebra.toSubalgebra ·) mFourierSubalgebra_closure_eq_top

Похожие утверждения