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.