Bernstein approximations and Weierstrass' theorem

We prove that 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.

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.

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

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

Equations

• bernstein n ν = Polynomial.toContinuousMapOn (bernsteinPolynomial ℝ n ν) unitInterval

@[simp]

theorem bernstein_apply (n : ℕ) (ν : ℕ) (x : ↑unitInterval) : (bernstein n ν) x = ↑(Nat.choose n ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)

theorem bernstein_nonneg {n : ℕ} {ν : ℕ} {x : ↑unitInterval} : 0 ≤ (bernstein n ν) x

def Mathlib.Meta.Positivity.evalBernstein : Mathlib.Meta.Positivity.PositivityExt

Equations

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

We now give a slight reformulation of bernsteinPolynomial.variance.

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 = { val := ↑↑k / ↑n, property := ⋯ }

theorem bernstein.probability (n : ℕ) (x : ↑unitInterval) : (Finset.sum Finset.univ fun (k : Fin (n + 1)) => (bernstein n ↑k) x) = 1

theorem bernstein.variance {n : ℕ} (h : 0 < ↑n) (x : ↑unitInterval) : (Finset.sum Finset.univ fun (k : Fin (n + 1)) => (↑x - ↑(bernstein.z k)) ^ 2 * (bernstein n ↑k) x) = ↑x * (1 - ↑x) / ↑n

def bernsteinApproximation (n : ℕ) (f : C(↑unitInterval, ℝ)) : C(↑unitInterval, ℝ)

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

Equations

• bernsteinApproximation n f = Finset.sum Finset.univ fun (k : Fin (n + 1)) => f (bernstein.z k) • bernstein n ↑k

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

@[simp]

theorem bernsteinApproximation.apply (n : ℕ) (f : C(↑unitInterval, ℝ)) (x : ↑unitInterval) : (bernsteinApproximation n f) x = Finset.sum Finset.univ fun (k : Fin (n + 1)) => f (bernstein.z k) * (bernstein n ↑k) x

def bernsteinApproximation.δ (f : C(↑unitInterval, ℝ)) (ε : ℝ) (h : 0 < ε) : ℝ

The modulus of (uniform) continuity for f, chosen so |f x - f y| < ε/2 when |x - y| < δ.

Equations

• bernsteinApproximation.δ f ε h = ContinuousMap.modulus f (ε / 2) ⋯

theorem bernsteinApproximation.δ_pos {f : C(↑unitInterval, ℝ)} {ε : ℝ} {h : 0 < ε} : 0 < bernsteinApproximation.δ f ε h

def bernsteinApproximation.S (f : C(↑unitInterval, ℝ)) (ε : ℝ) (h : 0 < ε) (n : ℕ) (x : ↑unitInterval) : Finset (Fin (n + 1))

The set of points k so k/n is within δ of x.

Equations

• bernsteinApproximation.S f ε h n x = Set.toFinset {k : Fin (n + 1) | dist (bernstein.z k) x < bernsteinApproximation.δ f ε h}

theorem bernsteinApproximation.lt_of_mem_S {f : C(↑unitInterval, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : ↑unitInterval} {k : Fin (n + 1)} (m : k ∈ bernsteinApproximation.S f ε h n x) : |f (bernstein.z k) - f x| < ε / 2

If k ∈ S, then f(k/n) is close to f x.

theorem bernsteinApproximation.le_of_mem_S_compl {f : C(↑unitInterval, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : ↑unitInterval} {k : Fin (n + 1)} (m : k ∈ (bernsteinApproximation.S f ε h n x)ᶜ) : 1 ≤ bernsteinApproximation.δ f ε h ^ (-2) * (↑x - ↑(bernstein.z k)) ^ 2

If k ∉ S, then as δ ≤ |x - k/n|, we have the inequality 1 ≤ δ^-2 * (x - k/n)^2. This particular formulation will be helpful later.

theorem bernsteinApproximation_uniform (f : C(↑unitInterval, ℝ)) : 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.