mathlib

dac1da3a - feat(analysis/special_functions/bernstein): Weierstrass' theorem: polynomials are dense in C([0,1]) (#6497)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>