# Bernstein approximations and Weierstrass' theorem #

We prove that the Bernstein approximations

    ∑ k : Fin (n+1), (n.choose k * x^k * (1-x)^(n-k)) • f (k/n : ℝ)

for a continuous function `f : C([0,1], E)` taking values in a locally convex vector space converge uniformly to `f` as `n` tends to infinity. This statement directly applies to the cases when the codomain is a (semi)normed space or, more generally, has a topology defined by a family of seminorms.

Our proof follows [Richard Beals' Analysis, an introduction][beals-analysis], §7D. The original proof, due to Bernstein in 1912, is probabilistic, and relies on Bernoulli's theorem, which gives bounds for how quickly the observed frequencies in a Bernoulli trial approach the underlying probability.

The proof here does not directly rely on Bernoulli's theorem, but can also be given a probabilistic account.

- Consider a weighted coin which with probability `x` produces heads, and with probability `1-x` produces tails.
- The value of `bernstein n k x` is the probability that such a coin gives exactly `k` heads in a sequence of `n` tosses.
- If such an appearance of `k` heads results in a payoff of `f(k / n)`, the `n`-th Bernstein approximation for `f` evaluated at `x` is the expected payoff.
- The main estimate in the proof bounds the probability that the observed frequency of heads differs from `x` by more than some `δ`, obtaining a bound of `(4 * n * δ^2)⁻¹`, irrespective of `x`.
- This ensures that for `n` large, the Bernstein approximation is (uniformly) close to the payoff function `f`.

(You don't need to think in these terms to follow the proof below: it's a giant `calc` block!)

This result proves Weierstrass' theorem that polynomials are dense in `C([0,1], ℝ)`, although we defer an abstract statement of this until later.

source
def bernstein (n ν : ℕ) :
C(↑unitInterval, ℝ)

The Bernstein polynomials, as continuous functions on `[0,1]`.

Equations

- bernstein n ν = (bernsteinPolynomial ℝ n ν).toContinuousMapOn unitInterval

Instances For

source
theorem bernstein_apply (n ν : ℕ) (x : ↑unitInterval) :
(bernstein n ν) x = ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
source
@[simp]
theorem bernstein_nonneg {n ν : ℕ} {x : ↑unitInterval} :
0 ≤ (bernstein n ν) x
source
def Mathlib.Meta.Positivity.evalBernstein :
PositivityExt

Extension of the `positivity` tactic for Bernstein polynomials: they are always non-negative.

Equations

- One or more equations did not get rendered due to their size.

Instances For

We now give a slight reformulation of `bernsteinPolynomial.variance`.

source
def bernstein.z {n : ℕ} (k : Fin (n + 1)) :
↑unitInterval

Send `k : Fin (n+1)` to the equally spaced points `k/n` in the unit interval.

Equations

- bernstein.z k = ⟨↑↑k / ↑n, ⋯⟩

Instances For

source
@[simp]
theorem bernstein.z_zero {n : ℕ} :
z 0 = 0
source
@[simp]
theorem bernstein.z_last {n : ℕ} (hn : n ≠ 0) :
z (Fin.last n) = 1
source
@[simp]
theorem bernstein.probability (n : ℕ) (x : ↑unitInterval) :
∑ k : Fin (n + 1), (bernstein n ↑k) x = 1
source
theorem bernstein.variance {n : ℕ} (hn : n ≠ 0) (x : ↑unitInterval) :
∑ k : Fin (n + 1), (↑x - ↑(z k)) ^ 2 * (bernstein n ↑k) x = ↑x * (1 - ↑x) / ↑n
source
def bernsteinApproximation {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)) :
C(↑unitInterval, E)

The `n`-th approximation of a continuous function on `[0,1]` by Bernstein polynomials, given by `∑ k, bernstein n k x • f (k/n)`.

Equations

- bernsteinApproximation n f = ∑ k : Fin (n + 1), bernstein n ↑k • ContinuousMap.const (↑unitInterval) (f (bernstein.z k))

Instances For

We now set up some of the basic machinery of the proof that the Bernstein approximations converge uniformly.

A key player is the set `S f ε h n x`, for some function `f : C(I, E)`, `h : 0 < ε`, `n : ℕ` and `x : I`.

This is the set of points `k` in `Fin (n+1)` such that `k/n` is within `δ` of `x`, where `δ` is the modulus of uniform continuity for `f`, chosen so `‖f x - f y‖ < ε/2` when `|x - y| < δ`.

We show that if `k ∉ S`, then `1 ≤ δ^-2 * (x - k/n)^2`.

source
theorem bernsteinApproximation.apply {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)) (x : ↑unitInterval) :
(bernsteinApproximation n f) x = ∑ k : Fin (n + 1), (bernstein n ↑k) x • f (bernstein.z k)
source
@[simp]
theorem bernsteinApproximation.apply_zero {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)) :
(bernsteinApproximation n f) 0 = f 0
source
@[simp]
theorem bernsteinApproximation.apply_one {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] {n : ℕ} (hn : n ≠ 0) (f : C(↑unitInterval, E)) :
(bernsteinApproximation n f) 1 = f 1
source
theorem bernsteinApproximation_uniform {E : Type u_1} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] (f : C(↑unitInterval, E)) :
Filter.Tendsto (fun (n : ℕ) => bernsteinApproximation n f) Filter.atTop (nhds f)

The Bernstein approximations

    ∑ k : Fin (n+1), f (k/n : ℝ) * n.choose k * x^k * (1-x)^(n-k)

for a continuous function `f : C([0,1], ℝ)` converge uniformly to `f` as `n` tends to infinity.

This is the proof given in [Richard Beals' Analysis, an introduction][beals-analysis], §7D, and reproduced on wikipedia.