Hostname: page-component-74656f9884-54qdv Total loading time: 0 Render date: 2026-11-10T05:27:40.857Z Has data issue: false hasContentIssue false
  • English
  • Français

A formal study of Bernstein coefficients and polynomials†

Published online by Cambridge University Press:  01 July 2011

YVES BERTOT ,
FRÉDÉRIQUE GUILHOT  and
ASSIA MAHBOUBI
YVES BERTOT
Affiliation:
INRIA Sophia Antipolis - Méditerranée, 2004, route des Lucioles - BP 93, 06902 Sophia Antipolis Cedex, France Email: Yves.Bertot.Guilhot@inria.fr; Frederique.Guilhot@inria.fr
FRÉDÉRIQUE GUILHOT
Affiliation:
INRIA Sophia Antipolis - Méditerranée, 2004, route des Lucioles - BP 93, 06902 Sophia Antipolis Cedex, France Email: Yves.Bertot.Guilhot@inria.fr; Frederique.Guilhot@inria.fr
ASSIA MAHBOUBI
Affiliation:
Inria Saclay – Île-de-France, Laboratoire d'Informatique de l'École Polytechnique (LIX), Parc Orsay Université, 4, rue Jacques Monod, 91893 Orsay cedex, France and École polytechnique Laboratoire d'informatique (LIX), 91128 Palaiseau Cedex, France Email: Assia.Mahboubi@inria.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

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.

References

Basu, S., Pollack, R. and Roy, M.-F. (2006) Algorithms in Real ALgebraic Geometry, second edition, Algorithms and Computations in Mathematics 10, Springer-Verlag.CrossRefGoogle Scholar
Bertot, Y. and Castéran, P. (2004) Interactive Theorem Proving and Program Development, Coq'Art: the Calculus of Inductive Constructions, Springer-Verlag.CrossRefGoogle Scholar
Bertot, Y., Gonthier, G., Ould Biha, S. and Paşca, I. (2008) Canonical Big Operators. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 517012–16. (Available at http://hal.inria.fr/inria-00331193/.)Google Scholar
Bézier, P. (1986) Courbes et Surfaces, Hermès.Google Scholar
Cohen, C. (2010) Formalizing real analysis for polynomials. Technical report, Inria. (Available at http://hal.inria.fr/inria-00545778/en/.)Google Scholar
Cruz-Filipe, L., Geuvers, H. and Wiedijk, F. (2004) C-CoRN, the Constructive Coq Repository at Nijmegen. In: Asperti, A., Bancerek, G. and Trybulec, A. (eds.) Proceedings Mathematical Knowledge Management, Third International Conference, MKM 2004. Springer-Verlag Lecture Notes in Computer Science 311988–103.Google Scholar
de Castleljau, P. (1985) Formes à pôles, Hermès.Google Scholar
Descartes, R. (1969) Géométrie (1636) A source book in Mathematics, Harvard University Press.Google Scholar
Gonthier, G. and Mahboubi, A. (2008) A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, INRIA. (Available at http://hal.inria.fr/inria-00258384/en/.)Google Scholar
Gonthier, G. and Mahboubi, A. (2010) An introduction to small scale reflection in Coq. Technical report, INRIA.Google Scholar
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E. and Théry, L. (2007) A modular formalisation of finite group theory. In: Schneider, K. and Brandt, J. (eds.) Proceedings Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007. Springer-Verlag Lecture Notes in Computer Science 473286–101.Google Scholar
Knuth, D. (1986) Metafont: the Program, Addison Wesley.Google Scholar
Mahboubi, A. (2007) Implementing the cylindrical algebraic decomposition within the Coq system. Mathematical Structures in Computer Science 17 (1)99–127.CrossRefGoogle Scholar
Mourrain, B., Rouillier, F. and Roy, M.-F. (2005) Bernstein's basis and real root isolation, Mathematical Sciences Research Institute Publications.Google Scholar
O'Connor, R. (2007) A monadic, functional implementation of real numbers. Mathematical Structures in Computer Science 17 (1)129–159.CrossRefGoogle Scholar
O'Connor, R. (2008) Certified exact transcendental real number computation in Coq. In: Mohamed, O. A., Muñoz, C. and Tahar, S. (eds.) Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). Springer-Verlag Lecture Notes in Computer Science 5170246–261.Google Scholar
Paşca, I. (2011) Formal proofs for theoretical properties of Newton's method. Mathematical Structures in Computer Science 21 (4)683–714.CrossRefGoogle Scholar
Rouillier, F. and Zimmermann, P. (2003) Efficient isolation of polynomial real roots. Journal of Computational and Applied Mathematics 162 (1)33–50.CrossRefGoogle Scholar
Troelstra, A. S. and van Dalen, D. (1988) Constructivism in Mathematics, an introduction 1, North-Holland.Google Scholar
Uspensky, J. V. (1948) Theory of Equations, MacGraw-Hill.Google Scholar
Zumkeller, R. (2008) Global Optimization in Type Theory, Ph.D. thesis, École Polytechnique.Google Scholar