The Weierstrass approximation theorem for continuous functions on
We've already proved the Weierstrass approximation theorem
in the sense that we've shown that the Bernstein approximations
to a continuous function on
[0,1] converge uniformly.
Here we rephrase this more abstractly as
polynomial_functions_closure_eq_top' : (polynomial_functions I).topological_closure = ⊤
and then, by precomposing with suitable affine functions,
polynomial_functions_closure_eq_top : (polynomial_functions (set.Icc a b)).topological_closure = ⊤
The Weierstrass approximation theorem:
polynomials functions on
[a, b] ⊆ ℝ are dense in
(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
so we may as well get this done first.)
An alternative statement of Weierstrass' theorem, for those who like their epsilons.
Every real-valued continuous function on
[a,b] is within any
ε > 0 of some polynomial.
Another alternative statement of Weierstrass's theorem, for those who like epsilons, but not bundled continuous functions.
Every real-valued function
ℝ → ℝ which is continuous on
can be approximated to within any
ε > 0 on
[a,b] by some polynomial.