# 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 = ⊤`

source
theorem polynomialFunctions_closure_eq_top' :
(polynomialFunctions unitInterval).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.

source
theorem polynomialFunctions_closure_eq_top (a b : ℝ) :
(polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤

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

source
theorem continuousMap_mem_polynomialFunctions_closure (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)) :
f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure

An alternative statement of Weierstrass' theorem.

Every real-valued continuous function on `[a,b]` is a uniform limit of polynomials.

source
theorem exists_polynomial_near_continuousMap (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)) (ε : ℝ) (pos : 0 < ε) :
∃ (p : Polynomial ℝ), ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε

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.

source
theorem exists_polynomial_near_of_continuousOn (a b : ℝ) (f : ℝ → ℝ) (c : ContinuousOn f (Set.Icc a b)) (ε : ℝ) (pos : 0 < ε) :
∃ (p : Polynomial ℝ), ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε

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.