Stream: new members
Topic: Computing with polynomials
Amos Turchet (Aug 11 2020 at 10:23):
I'm trying to prove the following lemma about lower bound for the value of a polynomial with integral coefficients evaluated at a rational number at a rational which is not a root of the polynomial. And I'm getting stuck and a bit worried:
import data.polynomial import data.rat notation α`[X]` := polynomial α /- The Lemma gives a lower bound on the absolute value of a polynomial f with integral coefficients evaluated at a rational number q which is not a root of f -/ lemma poly_not_zero_low_bound (x : ℚ) (p : ℤ [X]) (hx : x.denom > 0) (hpx : polynomial.aeval x p ≠ 0) : abs(polynomial.aeval x p) ≥ 1 / (x.denom)^(p.nat_degree) : begin calc abs(polynomial.aeval x p) = abs((polynomial.aeval x p).num / (polynomial.aeval x p).denom) : by rw rat.num_denom (polynomial.aeval x p) ... = abs(polynomial.aeval x p).num / abs(polynomial.aeval x p).denom : by rw abs_div ... ≥ 1 / (abs(polynomial.aeval x p)).denom : by sorry --rw [hx, rat.mk_eq_zero, int.nat_abs_ne_zero_of_ne_zero] ... ≥ 1 / (x.denom)^(p.nat_degree) : by sorry end
This was proven (a bit more generally) by @Jujian Zhang and it takes more than 100 lines of codes. To me it seems that the only actual computation to be done should be the last step which ideally would take less than that.
But before that it looks like I have issues with using
rat.num_denom as well as showing that given
hpx the numerator is a non-zero integer and therefore its absolute value is at least 1 (what David Masser calls the "Fundamental Theorem of Trascendence").
Last updated: May 13 2021 at 21:12 UTC