Skip to content

Bernstein polynomials

4 fully proved

Bernstein

TheoremFirst central moment of the Bernstein weights#✓fully proved

For n ≠ 0, ∑ k : Fin (n + 1), (x - k / n) * bernstein n k x = 0: the binomial frequency S / n has mean x.

theorem mean {n : ℕ} (hn : n ≠ 0) (x : I) :
    (∑ k : Fin (n + 1), ((x : ℝ) - z k) * bernstein n k x) = 0
Used by 1
Used byVoronovskaya's theorem (1932)

TheoremFourth central moment of the Bernstein weights#✓fully proved

For n ≠ 0, ∑ k : Fin (n + 1), (x - k / n) ^ 4 * bernstein n k x = x (1 - x) (1 + 3 (n - 2) x (1 - x)) / n³, i.e. E[(S - n x) ^ 4] = n x (1 - x) (1 + 3 (n - 2) x (1 - x)) for S ~ Bin(n, x).

theorem fourth_moment {n : ℕ} (hn : n ≠ 0) (x : I) :
    (∑ k : Fin (n + 1), ((x : ℝ) - z k) ^ 4 * bernstein n k x) =
      (x : ℝ) * (1 - x) * (1 + 3 * ((n : ℝ) - 2) * x * (1 - x)) / (n : ℝ) ^ 3
Used by 1
Used byFourth central moment bound for Bernstein weights

TheoremFourth central moment bound for Bernstein weights#✓fully proved

The fourth central moment of the Bernstein weights is at most 1 / n ^ 2, uniformly in x ∈ [0, 1].

theorem fourth_moment_le {n : ℕ} (hn : n ≠ 0) (x : I) :
    (∑ k : Fin (n + 1), ((x : ℝ) - z k) ^ 4 * bernstein n k x) ≤ 1 / (n : ℝ) ^ 2
Uses 1 · Used by 1
Proof usesFourth central moment of the Bernstein weights
Used byVoronovskaya's theorem (1932)

Bernstein Approximation

TheoremVoronovskaya's theorem (1932)#✓fully proved

For f : ℝ → ℝ of class C² and x ∈ [0, 1], the Bernstein approximations of f on [0, 1] satisfy n · (bernsteinApproximation n f x - f x) → x (1 - x) / 2 · f''(x) as n → ∞.

theorem tendsto_voronovskaya {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (x : I) :
    Tendsto (fun n : ℕ => (n : ℝ) *
        (bernsteinApproximation n ((⟨f, hf.continuous⟩ : C(ℝ, ℝ)).restrict I) x - f x))
      atTop (𝓝 ((x : ℝ) * (1 - x) / 2 * deriv (deriv f) x))
Sources
  • Voronovskaya (1932); Lorentz, Bernstein Polynomials (1953), Chapter 1.
Uses 2 · Used by 1
Proof usesFourth central moment bound for Bernstein weights · First central moment of the Bernstein weights
Used byWright–Fisher diffusion limit, generator form (Feller 1951; Voronovskaya 1932)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.