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 probability1-x
produces tails. - The value of
bernstein n k x
is the probability that such a coin gives exactlyk
heads in a sequence ofn
tosses. - If such an appearance of
k
heads results in a payoff off(k / n)
, then
-th Bernstein approximation forf
evaluated atx
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 ofx
. - This ensures that for
n
large, the Bernstein approximation is (uniformly) close to the payoff functionf
.
(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
We now give a slight reformulation of bernstein_polynomial.variance
.
Send k : fin (n+1)
to the equally spaced points k/n
in the unit interval.
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
- bernstein_approximation n f = finset.univ.sum (λ (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
.
The modulus of (uniform) continuity for f
, chosen so |f x - f y| < ε/2
when |x - y| < δ
.
Equations
- bernstein_approximation.δ f ε h = f.modulus (ε / 2) _
The set of points k
so k/n
is within δ
of x
.
Equations
- bernstein_approximation.S f ε h n x = {k : fin (n + 1) | has_dist.dist (bernstein.z k) x < bernstein_approximation.δ f ε h}.to_finset
If k ∈ S
, then f(k/n)
is close to f x
.
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.
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.