English
For each p between 1 and ∞, the span of the Fourier monomials mFourierLp(·) is dense in the Lp space on UnitAddTorus d.
Русский
Для каждого p в диапазоне 1 ≤ p < ∞ линейная оболочка монофицирующих функций Фурье mFourierLp(·) плотно заполнит пространство Lp на UnitAddTorus d.
LaTeX
$$$$\\big(\\operatorname{span}\\mathbb{C}\\;\\operatorname{range}(mFourierLp(d,\\,2,\\,\\cdot))\\big)_{\\text{topologicalClosure}} = \\top$$
Lean4
/-- For each `1 ≤ p < ∞`, the linear span of the monomials `mFourier n` is dense in the `Lᵖ` space
of functions on `UnitAddTorus d`. -/
theorem span_mFourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
(span ℂ (range (@mFourierLp d _ p _))).topologicalClosure = ⊤ := by
simpa only [map_span, ContinuousLinearMap.coe_coe, ← range_comp, Function.comp_def] using
(ContinuousMap.toLp_denseRange ℂ volume ℂ hp).topologicalClosure_map_submodule span_mFourier_closure_eq_top
