English
On the interval, the closure of polynomial functions equals the ambient subalgebra, i.e., polynomials are dense in continuous functions on [a,b].
Русский
На интервале замыкание полиномов совпадает с полным пространством: полиномы плотны в непрерывные функции на [a,b].
LaTeX
$$$\overline{\mathrm{polynomialFunctions}(I)} = \text{top}.$$$
Lean4
/-- The **Weierstrass Approximation Theorem**:
polynomials functions on `[a, b] ⊆ ℝ` are dense in `C([a,b],ℝ)`
(While we could deduce this as an application of the Stone-Weierstrass theorem,
our proof of that relies on the fact that `abs` is in the closure of polynomials on `[-M, M]`,
so we may as well get this done first.)
-/
theorem polynomialFunctions_closure_eq_top (a b : ℝ) : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤ :=
by
rcases lt_or_ge a b with h | h
· -- We can pullback continuous functions on `[a,b]` to continuous functions on `[0,1]`,
-- by precomposing with an affine map.
let W : C(Set.Icc a b, ℝ) →ₐ[ℝ] C(I, ℝ) := compRightAlgHom ℝ ℝ (iccHomeoI a b h).symm
let W' : C(Set.Icc a b, ℝ) ≃ₜ C(I, ℝ) := (iccHomeoI a b h).arrowCongr (.refl _)
have w : (W : C(Set.Icc a b, ℝ) → C(I, ℝ)) = W' := rfl
have p := polynomialFunctions_closure_eq_top'
apply_fun fun s => s.comap W at p
simp only [Algebra.comap_top] at p
rw [Subalgebra.topologicalClosure_comap_homeomorph _ W W' w] at p
rw [polynomialFunctions.comap_compRightAlgHom_iccHomeoI] at p
exact p
· -- Otherwise, `b ≤ a`, and the interval is a subsingleton,
subsingleton [(Set.subsingleton_Icc_of_ge h).coe_sort]
