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 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 giantcalc
block!) This result proves Weierstrass' theorem that polynomials are dense inC([0,1], ℝ)
, although we defer an abstract statement of this until later.