mathlib documentation

ring_theory.polynomial.bernstein

Bernstein polynomials #

The definition of the Bernstein polynomials

bernstein_polynomial (R : Type*) [comm_ring R] (n ν : ) : polynomial R :=
(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 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.

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 < ν) :
@[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) :
theorem bernstein_polynomial.flip' (R : Type u_1) [comm_ring R] (n ν : ) (h : ν n) :
theorem bernstein_polynomial.eval_at_0 (R : Type u_1) [comm_ring R] (n ν : ) :
theorem bernstein_polynomial.eval_at_1 (R : Type u_1) [comm_ring R] (n ν : ) :
theorem bernstein_polynomial.derivative_succ (R : Type u_1) [comm_ring R] (n ν : ) :

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

@[simp]
theorem bernstein_polynomial.iterate_derivative_at_1 (R : Type u_1) [comm_ring R] (n ν : ) (h : ν n) :

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 : ) :
∑ (ν : ) in finset.range (n + 1), bernstein_polynomial R n ν = 1
theorem bernstein_polynomial.sum_smul (R : Type u_1) [comm_ring R] (n : ) :
∑ (ν : ) in finset.range (n + 1), ν bernstein_polynomial R n ν = n polynomial.X
theorem bernstein_polynomial.sum_mul_smul (R : Type u_1) [comm_ring R] (n : ) :
∑ (ν : ) in finset.range (n + 1), * - 1)) bernstein_polynomial R n ν = (n * (n - 1)) polynomial.X ^ 2
theorem bernstein_polynomial.variance (R : Type u_1) [comm_ring R] (n : ) :
∑ (ν : ) in finset.range (n + 1), ((n polynomial.X - ν) ^ 2) * bernstein_polynomial R n ν = (n polynomial.X) * (1 - polynomial.X)

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