# The Weierstrass approximation theorem for continuous functions on `[a,b]`

#

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
`polynomialFunctions_closure_eq_top' : (polynomialFunctions I).topologicalClosure = ⊤`

and then, by precomposing with suitable affine functions,
`polynomialFunctions_closure_eq_top : (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤`

The special case of the Weierstrass approximation theorem for the interval `[0,1]`

.
This is just a matter of unravelling definitions and using the Bernstein approximations.

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.)

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 `[a,b]`

can be approximated to within any `ε > 0`

on `[a,b]`

by some polynomial.