Documentation

Mathlib.Analysis.SpecialFunctions.Bernstein

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.

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

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

Equations
theorem bernstein_apply (n ν : ) (x : unitInterval) :
(bernstein n ν) x = (n.choose ν) * x ^ ν * (1 - x) ^ (n - ν)
@[simp]
theorem bernstein_nonneg {n ν : } {x : unitInterval} :
0 (bernstein n ν) x

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.

We now give a slight reformulation of bernsteinPolynomial.variance.

def bernstein.z {n : } (k : Fin (n + 1)) :

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

Equations
@[simp]
theorem bernstein.z_zero {n : } :
z 0 = 0
@[simp]
theorem bernstein.z_last {n : } (hn : n 0) :
z (Fin.last n) = 1
@[simp]
theorem bernstein.probability (n : ) (x : unitInterval) :
k : Fin (n + 1), (bernstein n k) x = 1
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

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

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.

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.