A formal study of Bernstein coefficients and polynomials
Yves Bertot, Frédérique Guilhot, Assia Mahboubi · Mathematical Structures in Computer Science · 2011
Bernstein coefficients provide a discrete approximation of the behaviour of a polynomial inside an interval. This can be used, for example, to isolate the real roots of polynomials. We prove formally a criterion for the existence of a single root in an interval and the correctness of the de Casteljau algorithm for computing Bernstein coefficients efficiently.