English
For any p with 1 ≤ p < ∞, the span of Fourier monomials is dense in the Lp space of functions on UnitAddTorus: closure equals top.
Русский
Для любого p с 1 ≤ p < ∞ линейная оболочка мономиалов Фурье плотна в Lp-пространстве функций на UnitAddTorus; замыкание равно всему пространству.
LaTeX
$$$ (\operatorname{span}_{\mathbb{C}} \{mFourierLp(p, n) : n\})^{\text{topClosure}} = ⊤ \quad (1 \le p < ∞) $$$
Lean4
/-- The family of monomials `mFourier n`, parametrized by `n : ℤᵈ` and considered as
elements of the `Lp` space of functions `UnitAddTorus d → ℂ`. -/
abbrev mFourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : d → ℤ) : Lp ℂ p (volume : Measure (UnitAddTorus d)) :=
ContinuousMap.toLp (E := ℂ) p volume ℂ (mFourier n)
