Coefficient bounds for interpolation polynomials #
A polynomial assembled by polynomialOfCoefficients from an integer coefficient vector
bounded by R has every coefficient bounded by R. The Bombieri–Vaaler auxiliary
constructions of the determinant method use this to bound the coefficients of the auxiliary
polynomial. Nondivisibility by the defining polynomial is a separate step, proved from the
global determinant lower bound in Section 3.3.
theorem
CCDN.abs_coefficient_polynomialOfCoefficients_le
{n N : ℕ}
(mon : Fin N → Fin n →₀ ℕ)
(hmon : Function.Injective mon)
(v : Fin N → ℤ)
{R : ℝ}
(hR : 0 ≤ R)
(hv : InBox v R)
(e : Fin n →₀ ℕ)
:
If the monomials mon are distinct and the integer coefficient vector v lies in the box
of radius R ≥ 0, then every coefficient of polynomialOfCoefficients mon v has absolute
value at most R.