Bernstein polynomials #
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
.
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 - ν)
Rather than redoing the work of evaluating the derivatives at 1, we use the symmetry of the Bernstein polynomials.
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
.
A certain linear combination of the previous three identities, which we'll want later.