Polynomial Interpolation

Title:	Polynomial Interpolation
Authors:	René Thiemann and Akihisa Yamada
Submission date:	2016-01-29
Abstract:	We formalized three algorithms for polynomial interpolation over arbitrary fields: Lagrange's explicit expression, the recursive algorithm of Neville and Aitken, and the Newton interpolation in combination with an efficient implementation of divided differences. Variants of these algorithms for integer polynomials are also available, where sometimes the interpolation can fail; e.g., there is no linear integer polynomial p such that p(0) = 0 and p(2) = 1. Moreover, for the Newton interpolation for integer polynomials, we proved that all intermediate results that are computed during the algorithm must be integers. This admits an early failure detection in the implementation. Finally, we proved the uniqueness of polynomial interpolation. The development also contains improved code equations to speed up the division of integers in target languages.
BibTeX:	@article{Polynomial_Interpolation-AFP, author = {René Thiemann and Akihisa Yamada}, title = {Polynomial Interpolation}, journal = {Archive of Formal Proofs}, month = jan, year = 2016, note = {\url{http://isa-afp.org/entries/Polynomial_Interpolation.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Sqrt_Babylonian
Used by:	Deep_Learning, Gauss_Sums, Polynomial_Factorization
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry