### 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.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Polynomial_Interpolation

- Is_Rat_To_Rat
- Divmod_Int
- Improved_Code_Equations
- Ring_Hom
- Missing_Unsorted
- Missing_Polynomial
- Ring_Hom_Poly
- Newton_Interpolation
- Lagrange_Interpolation
- Neville_Aitken_Interpolation
- Polynomial_Interpolation

### Depends on

- Computing N-th Roots using the Babylonian Method

### Used by

- Chebyshev Polynomials
- A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
- The Theorem of Three Circles
- Formal Puiseux Series
- Gauss Sums and the Pólya–Vinogradov Inequality
- Count the Number of Complex Roots
- Expressiveness of Deep Learning
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Polynomial Factorization
- The Sturm–Tarski Theorem

### Auto-related entries

- Interpolation Polynomials (in HOL-Algebra)
- A verified factorization algorithm for integer polynomials with polynomial complexity
- The Factorization Algorithm of Berlekamp and Zassenhaus

## Cite

×

Polynomial_Interpolation-AFP

    @article{Polynomial_Interpolation-AFP,
      author  = {René Thiemann and Akihisa Yamada},
      title   = {Polynomial Interpolation},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Polynomial_Interpolation.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016