# 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

• (Finset.range (n + 1)).sum (fun ν ↦ bernsteinPolynomial R n ν) = 1
• (Finset.range (n + 1)).sum (fun ν ↦ ν • bernsteinPolynomial R n ν) = n • X
• (Finset.range (n + 1)).sum (fun ν ↦ (ν * (ν-1)) • bernsteinPolynomial R n ν) = (n * (n-1)) • X^2

## 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) [] (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
• = (n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)
Instances For
theorem bernsteinPolynomial.eq_zero_of_lt (R : Type u_1) [] {n : } {ν : } (h : n < ν) :
= 0
@[simp]
theorem bernsteinPolynomial.map {R : Type u_1} [] {S : Type u_2} [] (f : R →+* S) (n : ) (ν : ) :
theorem bernsteinPolynomial.flip (R : Type u_1) [] (n : ) (ν : ) (h : ν n) :
().comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)
theorem bernsteinPolynomial.flip' (R : Type u_1) [] (n : ) (ν : ) (h : ν n) :
= (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)
theorem bernsteinPolynomial.eval_at_0 (R : Type u_1) [] (n : ) (ν : ) :
Polynomial.eval 0 () = if ν = 0 then 1 else 0
theorem bernsteinPolynomial.eval_at_1 (R : Type u_1) [] (n : ) (ν : ) :
Polynomial.eval 1 () = if ν = n then 1 else 0
theorem bernsteinPolynomial.derivative_succ_aux (R : Type u_1) [] (n : ) (ν : ) :
Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) = (n + 1) * ( - bernsteinPolynomial R n (ν + 1))
theorem bernsteinPolynomial.derivative_succ (R : Type u_1) [] (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) [] (n : ) :
Polynomial.derivative () = -n * bernsteinPolynomial R (n - 1) 0
theorem bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt (R : Type u_1) [] (n : ) {ν : } {k : } :
k < νPolynomial.eval 0 ((Polynomial.derivative)^[k] ()) = 0
@[simp]
theorem bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero (R : Type u_1) [] (n : ) (ν : ) :
Polynomial.eval 0 ((Polynomial.derivative)^[ν] (bernsteinPolynomial R n (ν + 1))) = 0
@[simp]
theorem bernsteinPolynomial.iterate_derivative_at_0 (R : Type u_1) [] (n : ) (ν : ) :
Polynomial.eval 0 ((Polynomial.derivative)^[ν] ()) = Polynomial.eval ((n - (ν - 1))) ()
theorem bernsteinPolynomial.iterate_derivative_at_0_ne_zero (R : Type u_1) [] [] (n : ) (ν : ) (h : ν n) :
Polynomial.eval 0 ((Polynomial.derivative)^[ν] ()) 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) [] (n : ) {ν : } {k : } :
k < n - νPolynomial.eval 1 ((Polynomial.derivative)^[k] ()) = 0
@[simp]
theorem bernsteinPolynomial.iterate_derivative_at_1 (R : Type u_1) [] (n : ) (ν : ) (h : ν n) :
Polynomial.eval 1 ((Polynomial.derivative)^[n - ν] ()) = (-1) ^ (n - ν) * Polynomial.eval (ν + 1) (ascPochhammer R (n - ν))
theorem bernsteinPolynomial.iterate_derivative_at_1_ne_zero (R : Type u_1) [] [] (n : ) (ν : ) (h : ν n) :
Polynomial.eval 1 ((Polynomial.derivative)^[n - ν] ()) 0
theorem bernsteinPolynomial.linearIndependent_aux (n : ) (k : ) (h : k n + 1) :
LinearIndependent fun (ν : Fin k) =>

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) [] (n : ) :
((Finset.range (n + 1)).sum fun (ν : ) => ) = 1
theorem bernsteinPolynomial.sum_smul (R : Type u_1) [] (n : ) :
((Finset.range (n + 1)).sum fun (ν : ) => ν ) = n Polynomial.X
theorem bernsteinPolynomial.sum_mul_smul (R : Type u_1) [] (n : ) :
((Finset.range (n + 1)).sum fun (ν : ) => (ν * (ν - 1)) ) = (n * (n - 1)) Polynomial.X ^ 2
theorem bernsteinPolynomial.variance (R : Type u_1) [] (n : ) :
((Finset.range (n + 1)).sum fun (ν : ) => (n Polynomial.X - ν) ^ 2 * ) = n Polynomial.X * (1 - Polynomial.X)

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