Lower bounds for cross evaluations at rational points #
For integer polynomials P, Q of degree at most N, a nonzero value
P(x) - y Q(x) at rational points cannot be smaller than
(den(x)^N den(y))⁻¹. This is the arithmetic lower bound used when auxiliary
polynomials give a small rational linear form in two approximants.
The proof applies Mathlib's one_le_pow_mul_abs_eval_div to
den(y) P - num(y) Q; it does not require either polynomial to be nonzero.
theorem
TauCeti.one_le_den_pow_mul_abs_aeval_sub_mul
{P Q : Polynomial ℤ}
{N : ℕ}
(hP : P.natDegree ≤ N)
(hQ : Q.natDegree ≤ N)
{x y : ℚ}
(hne : (Polynomial.aeval x) P - y * (Polynomial.aeval x) Q ≠ 0)
:
For a nonzero cross evaluation of integer polynomials of degree at most N,
1 ≤ den(x)^N den(y) |P(x) - y Q(x)|.