Documentation

Mathlib.Analysis.SpecialFunctions.Bernstein

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][beals-analysis], §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.

(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.

def bernstein (n : ) (ν : ) :

The Bernstein polynomials, as continuous functions on [0,1].

Equations
Instances For
    @[simp]
    theorem bernstein_apply (n : ) (ν : ) (x : unitInterval) :
    (bernstein n ν) x = (Nat.choose n ν) * x ^ ν * (1 - x) ^ (n - ν)
    theorem bernstein_nonneg {n : } {ν : } {x : unitInterval} :
    0 (bernstein n ν) x
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      We now give a slight reformulation of bernsteinPolynomial.variance.

      def bernstein.z {n : } (k : Fin (n + 1)) :

      Send k : Fin (n+1) to the equally spaced points k/n in the unit interval.

      Equations
      Instances For
        theorem bernstein.probability (n : ) (x : unitInterval) :
        (Finset.sum Finset.univ fun (k : Fin (n + 1)) => (bernstein n k) x) = 1
        theorem bernstein.variance {n : } (h : 0 < n) (x : unitInterval) :
        (Finset.sum Finset.univ fun (k : Fin (n + 1)) => (x - (bernstein.z k)) ^ 2 * (bernstein n k) x) = x * (1 - x) / n

        The n-th approximation of a continuous function on [0,1] by Bernstein polynomials, given by ∑ k, f (k/n) * bernstein n k x.

        Equations
        Instances For

          We now set up some of the basic machinery of the proof that the Bernstein approximations converge uniformly.

          A key player is the set S f ε h n x, for some function f : C(I, ℝ), h : 0 < ε, n : ℕ and x : I.

          This is the set of points k in Fin (n+1) such that k/n is within δ of x, where δ is the modulus of uniform continuity for f, chosen so |f x - f y| < ε/2 when |x - y| < δ.

          We show that if k ∉ S, then 1 ≤ δ^-2 * (x - k/n)^2.

          @[simp]
          theorem bernsteinApproximation.apply (n : ) (f : C(unitInterval, )) (x : unitInterval) :
          (bernsteinApproximation n f) x = Finset.sum Finset.univ fun (k : Fin (n + 1)) => f (bernstein.z k) * (bernstein n k) x
          def bernsteinApproximation.δ (f : C(unitInterval, )) (ε : ) (h : 0 < ε) :

          The modulus of (uniform) continuity for f, chosen so |f x - f y| < ε/2 when |x - y| < δ.

          Equations
          Instances For
            def bernsteinApproximation.S (f : C(unitInterval, )) (ε : ) (h : 0 < ε) (n : ) (x : unitInterval) :
            Finset (Fin (n + 1))

            The set of points k so k/n is within δ of x.

            Equations
            Instances For
              theorem bernsteinApproximation.lt_of_mem_S {f : C(unitInterval, )} {ε : } {h : 0 < ε} {n : } {x : unitInterval} {k : Fin (n + 1)} (m : k bernsteinApproximation.S f ε h n x) :
              |f (bernstein.z k) - f x| < ε / 2

              If k ∈ S, then f(k/n) is close to f x.

              theorem bernsteinApproximation.le_of_mem_S_compl {f : C(unitInterval, )} {ε : } {h : 0 < ε} {n : } {x : unitInterval} {k : Fin (n + 1)} (m : k (bernsteinApproximation.S f ε h n x)) :
              1 bernsteinApproximation.δ f ε h ^ (-2) * (x - (bernstein.z k)) ^ 2

              If k ∉ S, then as δ ≤ |x - k/n|, we have the inequality 1 ≤ δ^-2 * (x - k/n)^2. This particular formulation will be helpful later.

              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.

              This is the proof given in [Richard Beals' Analysis, an introduction][beals-analysis], §7D, and reproduced on wikipedia.