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.

source

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

polynomial R

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

bernstein_polynomial R n ν = ↑(n.choose ν) * polynomial.X ^ ν * (1 - polynomial.X) ^ (n - ν)

source

theorem bernstein_polynomial.eq_zero_of_lt (R : Type u_1) [comm_ring R] {n ν : ℕ} (h : n < ν) :

bernstein_polynomial R n ν = 0

source

@[simp]

theorem bernstein_polynomial.map {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] (f : R →+* S) (n ν : ℕ) :

polynomial.map f (bernstein_polynomial R n ν) = bernstein_polynomial S n ν

source

theorem bernstein_polynomial.flip (R : Type u_1) [comm_ring R] (n ν : ℕ) (h : ν ≤ n) :

(bernstein_polynomial R n ν).comp (1 - polynomial.X) = bernstein_polynomial R n (n - ν)

source

theorem bernstein_polynomial.flip' (R : Type u_1) [comm_ring R] (n ν : ℕ) (h : ν ≤ n) :

bernstein_polynomial R n ν = (bernstein_polynomial R n (n - ν)).comp (1 - polynomial.X)

source

theorem bernstein_polynomial.eval_at_0 (R : Type u_1) [comm_ring R] (n ν : ℕ) :

polynomial.eval 0 (bernstein_polynomial R n ν) = ite (ν = 0) 1 0

source

theorem bernstein_polynomial.eval_at_1 (R : Type u_1) [comm_ring R] (n ν : ℕ) :

polynomial.eval 1 (bernstein_polynomial R n ν) = ite (ν = n) 1 0

source

theorem bernstein_polynomial.derivative_succ_aux (R : Type u_1) [comm_ring R] (n ν : ℕ) :

⇑polynomial.derivative (bernstein_polynomial R (n + 1) (ν + 1)) = (↑n + 1) * (bernstein_polynomial R n ν - bernstein_polynomial R n (ν + 1))

source

theorem bernstein_polynomial.derivative_succ (R : Type u_1) [comm_ring R] (n ν : ℕ) :

⇑polynomial.derivative (bernstein_polynomial R n (ν + 1)) = ↑n * (bernstein_polynomial R (n - 1) ν - bernstein_polynomial R (n - 1) (ν + 1))

source

theorem bernstein_polynomial.derivative_zero (R : Type u_1) [comm_ring R] (n : ℕ) :

⇑polynomial.derivative (bernstein_polynomial R n 0) = -↑n * bernstein_polynomial R (n - 1) 0

source

theorem bernstein_polynomial.iterate_derivative_at_0_eq_zero_of_lt (R : Type u_1) [comm_ring R] (n : ℕ) {ν k : ℕ} :

k < ν → polynomial.eval 0 (⇑polynomial.derivative ^[k] (bernstein_polynomial R n ν)) = 0

source

@[simp]

theorem bernstein_polynomial.iterate_derivative_succ_at_0_eq_zero (R : Type u_1) [comm_ring R] (n ν : ℕ) :

polynomial.eval 0 (⇑polynomial.derivative ^[ν] (bernstein_polynomial R n (ν + 1))) = 0

source

@[simp]

theorem bernstein_polynomial.iterate_derivative_at_0 (R : Type u_1) [comm_ring R] (n ν : ℕ) :

polynomial.eval 0 (⇑polynomial.derivative ^[ν] (bernstein_polynomial R n ν)) = polynomial.eval ↑(n - (ν - 1)) (pochhammer R ν)

source

theorem bernstein_polynomial.iterate_derivative_at_0_ne_zero (R : Type u_1) [comm_ring R] [char_zero R] (n ν : ℕ) (h : ν ≤ n) :

polynomial.eval 0 (⇑polynomial.derivative ^[ν] (bernstein_polynomial R n ν)) ≠ 0

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

source

theorem bernstein_polynomial.iterate_derivative_at_1_eq_zero_of_lt (R : Type u_1) [comm_ring R] (n : ℕ) {ν k : ℕ} :

k < n - ν → polynomial.eval 1 (⇑polynomial.derivative ^[k] (bernstein_polynomial R n ν)) = 0

source

@[simp]

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

polynomial.eval 1 (⇑polynomial.derivative ^[n - ν] (bernstein_polynomial R n ν)) = (-1) ^ (n - ν) * polynomial.eval (↑ν + 1) (pochhammer R (n - ν))

source

theorem bernstein_polynomial.iterate_derivative_at_1_ne_zero (R : Type u_1) [comm_ring R] [char_zero R] (n ν : ℕ) (h : ν ≤ n) :

polynomial.eval 1 (⇑polynomial.derivative ^[n - ν] (bernstein_polynomial R n ν)) ≠ 0

source

theorem bernstein_polynomial.linear_independent_aux (n k : ℕ) (h : k ≤ n + 1) :

linear_independent ℚ (λ (ν : fin k), bernstein_polynomial ℚ n ↑ν)

source

theorem bernstein_polynomial.linear_independent (n : ℕ) :

linear_independent ℚ (λ (ν : fin (n + 1)), bernstein_polynomial ℚ 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.

source

theorem bernstein_polynomial.sum (R : Type u_1) [comm_ring R] (n : ℕ) :

(finset.range (n + 1)).sum (λ (ν : ℕ), bernstein_polynomial R n ν) = 1

source

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

source

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

source

theorem bernstein_polynomial.variance (R : Type u_1) [comm_ring R] (n : ℕ) :

(finset.range (n + 1)).sum (λ (ν : ℕ), (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.