A formal study of Bernstein coefficients and polynomials

DOI10.1017/S0960129511000090MaRDI QIDQ3094174zbMATH OpenFDO

Authors Yves Bertot, Frédérique Guilhot, Assia Mahboubi

Publication date 21 October 2011

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0960129511000090

zbMATH Keywords

Bernstein coefficientsde Casteljau algorithmreal roots of polynomials

Mathematics Subject Classification ID

Orthogonal polynomials and functions of hypergeometric type (Jacobi, Laguerre, Hermite, Askey scheme, etc.) (33C45)

Recommendations

• scientific article; zbMATH DE number 5019917
• Uniform approximation and Bernstein polynomials with coefficients in the unit interval
• Matrix methods for the tensorial Bernstein form
• scientific article; zbMATH DE number 804609
• Algorithms for polynomials in Bernstein form

Cites work

• A Modular Formalisation of Finite Group Theory
• A monadic, functional implementation of real numbers
• A Short Presentation of Coq
• Algorithms in real algebraic geometry
• Certified Exact Transcendental Real Number Computation in Coq
• Efficient isolation of polynomial's real roots.
• Formal proofs for theoretical properties of Newton's method
• scientific article; zbMATH DE number 3986610 (Why is no real title available?)
• scientific article; zbMATH DE number 5019917 (Why is no real title available?)
• Implementing the cylindrical algebraic decomposition within the Coq system
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Cited in

(5)

• Formalization of Bernstein polynomials and applications to global optimization
• Theorem of three circles in Coq
• View of computer algebra data from Coq
• Uniform approximation and Bernstein polynomials with coefficients in the unit interval
• Safe smooth paths between straight line obstacles

Describes a project that uses

Uses Software

• Coq/SSReflect
• Coq
• METAFONT
• C-CoRN
• ISOLATE

This page was built for publication: A formal study of Bernstein coefficients and polynomials

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3094174)