mathlib3 documentation

topology.continuous_function.weierstrass

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
theorem polynomial_functions_closure_eq_top'  :
(polynomial_functions unit_interval).topological_closure = ⊤

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 polynomial_functions_closure_eq_top (a b : ℝ) :
(polynomial_functions (set.Icc a b)).topological_closure = ⊤

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 continuous_map_mem_polynomial_functions_closure (a b : ℝ) (f : C(↥(set.Icc a b), ℝ)) :
f ∈ (polynomial_functions (set.Icc a b)).topological_closure

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_continuous_map (a b : ℝ) (f : C(↥(set.Icc a b), ℝ)) (ε : ℝ) (pos : 0 < ε) :
∃ (p : polynomial ℝ), ‖p.to_continuous_map_on (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_continuous_on (a b : ℝ) (f : ℝ → ℝ) (c : continuous_on f (set.Icc a b)) (ε : ℝ) (pos : 0 < ε) :
∃ (p : polynomial ℝ), ∀ (x : ℝ), 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.