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.lean, which defines the Bernstein approximations of a continuous function f : C([0,1], ℝ), and shows that these converge uniformly to f.

noncomputable def bernsteinPolynomial (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial R

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

• bernsteinPolynomial R n ν = ↑(n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)

theorem bernsteinPolynomial.eq_zero_of_lt (R : Type u_1) [CommRing R] {n ν : ℕ} (h : n < ν) : bernsteinPolynomial R n ν = 0

@[simp]

theorem bernsteinPolynomial.map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (n ν : ℕ) : Polynomial.map f (bernsteinPolynomial R n ν) = bernsteinPolynomial S n ν

theorem bernsteinPolynomial.flip (R : Type u_1) [CommRing R] (n ν : ℕ) (h : ν ≤ n) : (bernsteinPolynomial R n ν).comp (1 - Polynomial.X) = bernsteinPolynomial R n (n - ν)

theorem bernsteinPolynomial.flip' (R : Type u_1) [CommRing R] (n ν : ℕ) (h : ν ≤ n) : bernsteinPolynomial R n ν = (bernsteinPolynomial R n (n - ν)).comp (1 - Polynomial.X)

theorem bernsteinPolynomial.eval_at_0 (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial.eval 0 (bernsteinPolynomial R n ν) = if ν = 0 then 1 else 0

theorem bernsteinPolynomial.eval_at_1 (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial.eval 1 (bernsteinPolynomial R n ν) = if ν = n then 1 else 0

theorem bernsteinPolynomial.derivative_succ_aux (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial.derivative (bernsteinPolynomial R (n + 1) (ν + 1)) = (↑n + 1) * (bernsteinPolynomial R n ν - bernsteinPolynomial R n (ν + 1))

theorem bernsteinPolynomial.derivative_succ (R : Type u_1) [CommRing R] (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) [CommRing R] (n : ℕ) : Polynomial.derivative (bernsteinPolynomial R n 0) = -↑n * bernsteinPolynomial R (n - 1) 0

theorem bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt (R : Type u_1) [CommRing R] (n : ℕ) {ν k : ℕ} : k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0

@[simp]

theorem bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n (ν + 1))) = 0

@[simp]

theorem bernsteinPolynomial.iterate_derivative_at_0 (R : Type u_1) [CommRing R] (n ν : ℕ) : Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) = Polynomial.eval (↑(n - (ν - 1))) (ascPochhammer R ν)

theorem bernsteinPolynomial.iterate_derivative_at_0_ne_zero (R : Type u_1) [CommRing R] [CharZero R] (n ν : ℕ) (h : ν ≤ n) : Polynomial.eval 0 ((⇑Polynomial.derivative)^[ν] (bernsteinPolynomial R n ν)) ≠ 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) [CommRing R] (n : ℕ) {ν k : ℕ} : k < n - ν → Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0

@[simp]

theorem bernsteinPolynomial.iterate_derivative_at_1 (R : Type u_1) [CommRing R] (n ν : ℕ) (h : ν ≤ n) : Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) = (-1) ^ (n - ν) * Polynomial.eval (↑ν + 1) (ascPochhammer R (n - ν))

theorem bernsteinPolynomial.iterate_derivative_at_1_ne_zero (R : Type u_1) [CommRing R] [CharZero R] (n ν : ℕ) (h : ν ≤ n) : Polynomial.eval 1 ((⇑Polynomial.derivative)^[n - ν] (bernsteinPolynomial R n ν)) ≠ 0

theorem bernsteinPolynomial.linearIndependent_aux (n k : ℕ) (h : k ≤ n + 1) : LinearIndependent ℚ fun (ν : Fin k) => bernsteinPolynomial ℚ n ↑ν

theorem bernsteinPolynomial.linearIndependent (n : ℕ) : LinearIndependent ℚ fun (ν : Fin (n + 1)) => bernsteinPolynomial ℚ n ↑ν

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) [CommRing R] (n : ℕ) : ∑ ν ∈ Finset.range (n + 1), bernsteinPolynomial R n ν = 1

theorem bernsteinPolynomial.sum_smul (R : Type u_1) [CommRing R] (n : ℕ) : ∑ ν ∈ Finset.range (n + 1), ν • bernsteinPolynomial R n ν = n • Polynomial.X

theorem bernsteinPolynomial.sum_mul_smul (R : Type u_1) [CommRing R] (n : ℕ) : ∑ ν ∈ Finset.range (n + 1), (ν * (ν - 1)) • bernsteinPolynomial R n ν = (n * (n - 1)) • Polynomial.X ^ 2

theorem bernsteinPolynomial.variance (R : Type u_1) [CommRing R] (n : ℕ) : ∑ ν ∈ Finset.range (n + 1), (n • Polynomial.X - ↑ν) ^ 2 * bernsteinPolynomial R n ν = n • Polynomial.X * (1 - Polynomial.X)

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