Commit 2021-04-22 01:02 dac1da3aView on Github →
feat(analysis/special_functions/bernstein): Weierstrass' theorem: polynomials are dense in C([0,1]) (#6497)
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
n tends to infinity.
Our proof follows Richard Beals' Analysis, an introduction, §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
xproduces heads, and with probability
- The value of
bernstein n k xis the probability that such a coin gives exactly
kheads in a sequence of
- If such an appearance of
kheads results in a payoff of
f(k / n), the
n-th Bernstein approximation for
xis the expected payoff.
- The main estimate in the proof bounds the probability that
the observed frequency of heads differs from
xby more than some
δ, obtaining a bound of
(4 * n * δ^2)⁻¹, irrespective of
- This ensures that for
nlarge, 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
calcblock!) This result proves Weierstrass' theorem that polynomials are dense in
C([0,1], ℝ), although we defer an abstract statement of this until later.