Documentation

Mathlib.RingTheory.Polynomial.Bernstein

Bernstein polynomials #

The definition of the Bernstein polynomials

bernsteinPolynomial (R : Type*) [CommRing R] (n ν : ℕ) : R[X] :=
(choose n ν) * X^ν * (1 - X)^(n - ν)

and the fact that for ν : fin (n+1) these are linearly independent over .

We prove the basic identities

Notes #

See also Mathlib.Analysis.SpecialFunctions.Bernstein, which defines the Bernstein approximations of a continuous function f : C([0,1], ℝ), and shows that these converge uniformly to f.

def bernsteinPolynomial (R : Type u_1) [CommRing R] (n : ) (ν : ) :

bernsteinPolynomial R n ν is (choose n ν) * X^ν * (1 - X)^(n - ν).

Although the coefficients are integers, it is convenient to work over an arbitrary commutative ring.

Equations
Instances For
    theorem bernsteinPolynomial.eq_zero_of_lt (R : Type u_1) [CommRing R] {n : } {ν : } (h : n < ν) :
    @[simp]
    theorem bernsteinPolynomial.map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (n : ) (ν : ) :
    theorem bernsteinPolynomial.flip (R : Type u_1) [CommRing R] (n : ) (ν : ) (h : ν n) :
    (bernsteinPolynomial R n ν).comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)
    theorem bernsteinPolynomial.flip' (R : Type u_1) [CommRing R] (n : ) (ν : ) (h : ν n) :
    bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)
    theorem bernsteinPolynomial.eval_at_0 (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0
    theorem bernsteinPolynomial.eval_at_1 (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0
    theorem bernsteinPolynomial.derivative_succ_aux (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) = (n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))
    theorem bernsteinPolynomial.derivative_succ (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.derivative (bernsteinPolynomial R n (ν + 1)) = n * (bernsteinPolynomial R (n - 1) ν - bernsteinPolynomial R (n - 1) (ν + 1))
    theorem bernsteinPolynomial.derivative_zero (R : Type u_1) [CommRing R] (n : ) :
    Polynomial.derivative (bernsteinPolynomial R n 0) = -n * bernsteinPolynomial R (n - 1) 0
    theorem bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt (R : Type u_1) [CommRing R] (n : ) {ν : } {k : } :
    k < νPolynomial.eval 0 ((Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
    @[simp]
    theorem bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.eval 0 ((Polynomial.derivative)^[ν] (bernsteinPolynomial R n (ν + 1))) = 0
    @[simp]
    theorem bernsteinPolynomial.iterate_derivative_at_0 (R : Type u_1) [CommRing R] (n : ) (ν : ) :
    Polynomial.eval 0 ((Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) = Polynomial.eval ((n - (ν - 1))) (ascPochhammer R ν)
    theorem bernsteinPolynomial.iterate_derivative_at_0_ne_zero (R : Type u_1) [CommRing R] [CharZero R] (n : ) (ν : ) (h : ν n) :
    Polynomial.eval 0 ((Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) 0

    Rather than redoing the work of evaluating the derivatives at 1, we use the symmetry of the Bernstein polynomials.

    theorem bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt (R : Type u_1) [CommRing R] (n : ) {ν : } {k : } :
    k < n - νPolynomial.eval 1 ((Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
    @[simp]
    theorem bernsteinPolynomial.iterate_derivative_at_1 (R : Type u_1) [CommRing R] (n : ) (ν : ) (h : ν n) :
    Polynomial.eval 1 ((Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * Polynomial.eval (ν + 1) (ascPochhammer R (n - ν))
    theorem bernsteinPolynomial.iterate_derivative_at_1_ne_zero (R : Type u_1) [CommRing R] [CharZero R] (n : ) (ν : ) (h : ν n) :
    Polynomial.eval 1 ((Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) 0

    The Bernstein polynomials are linearly independent.

    We prove by induction that the collection of bernsteinPolynomial n ν for ν = 0, ..., k are linearly independent. The inductive step relies on the observation that the (n-k)-th derivative, evaluated at 1, annihilates bernsteinPolynomial n ν for ν < k, but has a nonzero value at ν = k.

    theorem bernsteinPolynomial.sum (R : Type u_1) [CommRing R] (n : ) :
    νFinset.range (n + 1), bernsteinPolynomial R n ν = 1
    theorem bernsteinPolynomial.sum_smul (R : Type u_1) [CommRing R] (n : ) :
    νFinset.range (n + 1), ν bernsteinPolynomial R n ν = n Polynomial.X
    theorem bernsteinPolynomial.sum_mul_smul (R : Type u_1) [CommRing R] (n : ) :
    νFinset.range (n + 1), (ν * (ν - 1)) bernsteinPolynomial R n ν = (n * (n - 1)) Polynomial.X ^ 2
    theorem bernsteinPolynomial.variance (R : Type u_1) [CommRing R] (n : ) :
    νFinset.range (n + 1), (n Polynomial.X - ν) ^ 2 * bernsteinPolynomial R n ν = n Polynomial.X * (1 - Polynomial.X)

    A certain linear combination of the previous three identities, which we'll want later.