# Commit 2021-04-22 01:02 dac1da3a

View 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 `f`

as `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
`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.