exists_polynomial_near_of_continuousOn
theorem exists_polynomial_near_of_continuousOn :
∀ (a b : ℝ) (f : ℝ → ℝ),
ContinuousOn f (Set.Icc a b) → ∀ (ε : ℝ), 0 < ε → ∃ p, ∀ x ∈ Set.Icc a b, |Polynomial.eval x p - f x| < ε
This theorem is another form of Weierstrass's theorem, particularly useful for those who prefer dealing with epsilons rather than bundled continuous functions. It states that for any real-valued function `f` that is continuous on a closed interval `[a, b]`, for any positive real number `ε`, there exists a polynomial such that, for all `x` in the interval `[a, b]`, the absolute difference between the value of the polynomial at `x` and the value of the function `f` at `x` is less than `ε`. In other words, any continuous real-valued function on a closed interval can be approximated to within any given positive error bound on that interval by some polynomial.
More concisely: Given any continuous real-function `f` on a closed interval `[a, b]` and any positive real `ε`, there exists a polynomial approximating `f` such that the maximum absolute error is less than `ε`.
|
exists_polynomial_near_continuousMap
theorem exists_polynomial_near_continuousMap :
∀ (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)) (ε : ℝ), 0 < ε → ∃ p, ‖p.toContinuousMapOn (Set.Icc a b) - f‖ < ε
This theorem is an alternative statement of Weierstrass' theorem. It states that for any continuous function `f` that maps from a closed interval `[a, b]` to the real numbers, and for any real number `ε` greater than `0`, there exists a polynomial `p` such that the norm of the difference between `p` mapped on the interval `[a, b]` and `f` is less than `ε`. This theorem essentially states that we can approximate any real-valued continuous function on a closed interval with a polynomial within any given precision.
More concisely: Given a continuous real-valued function `f` on a closed interval `[a, b]` and any real `ε > 0`, there exists a polynomial `p` such that `∥p(x) - f(x)∥ < ε` for all `x ∈ [a, b]`.
|
continuousMap_mem_polynomialFunctions_closure
theorem continuousMap_mem_polynomialFunctions_closure :
∀ (a b : ℝ) (f : C(↑(Set.Icc a b), ℝ)), f ∈ (polynomialFunctions (Set.Icc a b)).topologicalClosure
This is an alternative statement of Weierstrass' theorem. The theorem asserts that for any real-valued continuous function `f` defined on a closed interval `[a, b]`, the function `f` is a uniform limit of polynomials. In other words, `f` belongs to the topological closure of the subalgebra of polynomial functions defined on the same interval `[a, b]`. This theorem is a fundamental result in real analysis and the theory of approximation.
More concisely: For any continuous real-valued function on a closed interval, it is uniformly approximated by polynomials.
|
polynomialFunctions_closure_eq_top
theorem polynomialFunctions_closure_eq_top : ∀ (a b : ℝ), (polynomialFunctions (Set.Icc a b)).topologicalClosure = ⊤
The **Weierstrass Approximation Theorem** states that for any real numbers `a` and `b`, the closure of the subalgebra of polynomial functions on the closed interval `[a, b]` is dense in the space of continuous functions from `[a, b]` to the real numbers, symbolized as `C([a,b],ℝ)`. In other words, for any continuous function from `[a, b]` to the real numbers, and for any positive `ε`, there exists a polynomial function on `[a, b]` that is within `ε` of the continuous function everywhere on `[a, b]`. This theorem could be derived as an application of the Stone-Weierstrass theorem, although the proof of that involves the fact that the absolute value function is in the closure of polynomials on any interval `[-M, M]`.
More concisely: The Weierstrass Approximation Theorem asserts that the closure of the algebra of polynomial functions is dense in the space of continuous functions on a closed interval.
|
polynomialFunctions_closure_eq_top'
theorem polynomialFunctions_closure_eq_top' : (polynomialFunctions unitInterval).topologicalClosure = ⊤
This theorem is a special case of the Weierstrass approximation theorem for the unit interval in the real numbers, which ranges from 0 to 1 (inclusive). It states that the topological closure of the set of polynomial functions on this unit interval is the entire set of continuous functions on the unit interval. The proof relies on the definitions of polynomial functions and unit interval, as well as the application of Bernstein approximations.
More concisely: The topological closure of the set of polynomial functions on the unit interval [0, 1] equals the set of all continuous functions on that interval.
|