mathlib3 documentation

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

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 < ν) :
@[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 ν : ) :

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

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