English
For each 1 ≤ p < ∞, the span of Fourier monomials in Lp is dense in haarAddCircle: the closure of span {fourierLp p n} equals the entire Lp space.
Русский
Для каждого 1 ≤ p < ∞ линейный спан мономиал Фурье в Lp плотен в Haar-мере: замыкание span {fourierLp p n} равно всему пространству Lp.
LaTeX
$$(span ℂ (range (fourierLp p))).topologicalClosure = ⊤$$
Lean4
/-- For each `1 ≤ p < ∞`, the linear span of the monomials `fourier n` is dense in
`Lp ℂ p haarAddCircle`. -/
theorem span_fourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
(span ℂ (range (@fourierLp T _ p _))).topologicalClosure = ⊤ :=
by
convert
(ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
span_fourier_closure_eq_top
rw [map_span]
unfold fourierLp
rw [range_comp']
simp only [ContinuousLinearMap.coe_coe]
