# mathlib3documentation

ring_theory.polynomial.bernstein

# Bernstein polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The definition of the Bernstein polynomials

bernstein_polynomial (R : Type*) [comm_ring 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 (λ ν, bernstein_polynomial R n ν) = 1
• (finset.range (n + 1)).sum (λ ν, ν • bernstein_polynomial R n ν) = n • X
• (finset.range (n + 1)).sum (λ ν, (ν * (ν-1)) • bernstein_polynomial R n ν) = (n * (n-1)) • X^2

## Notes #

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

noncomputable def bernstein_polynomial (R : Type u_1) [comm_ring R] (n ν : ) :

bernstein_polynomial 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
theorem bernstein_polynomial.eq_zero_of_lt (R : Type u_1) [comm_ring R] {n ν : } (h : n < ν) :
ν = 0
@[simp]
theorem bernstein_polynomial.map {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (f : R →+* S) (n ν : ) :
ν) = ν
theorem bernstein_polynomial.flip (R : Type u_1) [comm_ring R] (n ν : ) (h : ν n) :
ν).comp = (n - ν)
theorem bernstein_polynomial.flip' (R : Type u_1) [comm_ring R] (n ν : ) (h : ν n) :
ν = (n - ν)).comp
theorem bernstein_polynomial.eval_at_0 (R : Type u_1) [comm_ring R] (n ν : ) :
ν) = ite = 0) 1 0
theorem bernstein_polynomial.eval_at_1 (R : Type u_1) [comm_ring R] (n ν : ) :
ν) = ite = n) 1 0
theorem bernstein_polynomial.derivative_succ_aux (R : Type u_1) [comm_ring R] (n ν : ) :
polynomial.derivative (n + 1) + 1)) = (n + 1) * ν - + 1))
theorem bernstein_polynomial.derivative_succ (R : Type u_1) [comm_ring R] (n ν : ) :
polynomial.derivative + 1)) = n * (n - 1) ν - (n - 1) + 1))
theorem bernstein_polynomial.derivative_zero (R : Type u_1) [comm_ring R] (n : ) :
= -n * (n - 1) 0
@[simp]
theorem bernstein_polynomial.iterate_derivative_at_0 (R : Type u_1) [comm_ring R] (n ν : ) :
= polynomial.eval (n - - 1)) ν)
theorem bernstein_polynomial.iterate_derivative_at_0_ne_zero (R : Type u_1) [comm_ring R] [char_zero R] (n ν : ) (h : ν n) :
0

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

theorem bernstein_polynomial.iterate_derivative_at_1_eq_zero_of_lt (R : Type u_1) [comm_ring R] (n : ) {ν k : } :
k < n - ν = 0
@[simp]
theorem bernstein_polynomial.iterate_derivative_at_1 (R : Type u_1) [comm_ring R] (n ν : ) (h : ν n) :
ν)) = (-1) ^ (n - ν) * polynomial.eval (ν + 1) (n - ν))
theorem bernstein_polynomial.iterate_derivative_at_1_ne_zero (R : Type u_1) [comm_ring R] [char_zero R] (n ν : ) (h : ν n) :
ν)) 0
theorem bernstein_polynomial.linear_independent_aux (n k : ) (h : k n + 1) :
(λ (ν : fin k),
theorem bernstein_polynomial.linear_independent (n : ) :
(λ (ν : fin (n + 1)),

The Bernstein polynomials are linearly independent.

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

theorem bernstein_polynomial.sum (R : Type u_1) [comm_ring R] (n : ) :
(finset.range (n + 1)).sum (λ (ν : ), ν) = 1
theorem bernstein_polynomial.sum_smul (R : Type u_1) [comm_ring R] (n : ) :
(finset.range (n + 1)).sum (λ (ν : ), ν ν) =
theorem bernstein_polynomial.sum_mul_smul (R : Type u_1) [comm_ring R] (n : ) :
(finset.range (n + 1)).sum (λ (ν : ), * - 1)) ν) = (n * (n - 1))
theorem bernstein_polynomial.variance (R : Type u_1) [comm_ring R] (n : ) :
(finset.range (n + 1)).sum (λ (ν : ), - ν) ^ 2 * ν) = *

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