A formal study of Bernstein coefficients and polynomials

Yves Bertot (1) , Frédérique Guilhot (1) , Assia Mahboubi (2, 3)

1 MARELLE - Mathematical, Reasoning and Software
2 TYPICAL - Types, Logic and computing
3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

Bernstein coefficients provide a discrete approximation of the behavior of a polynomial inside an interval. This can be used for example to isolate real roots of polynomials. We prove a criterion for the existence of a single root in an interval and the correctness of the de Casteljau algorithm to compute efficiently Bernstein coefficients.

Domaines: Logique en informatique [cs.LO]

Yves Bertot, Frédérique Guilhot, Assia Mahboubi. A formal study of Bernstein coefficients and polynomials. Mathematical Structures in Computer Science, 2011, 21 (04), pp.731-761. ⟨10.1017/S0960129511000090⟩. ⟨inria-00503017v2⟩