Denominators of evaluation of polynomials at ratios

Let i : R → K be a homomorphism of semirings. Assume that K is commutative. If a and b are elements of R such that i b ∈ K is invertible, then for any polynomial f ∈ R[X] the "mathematical" expression b ^ f.natDegree * f (a / b) ∈ K is in the image of the homomorphism i.

def DenomsClearable {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] (a b : R) (N : ℕ) (f : Polynomial R) (i : R →+* K) : Prop

denomsClearable formalizes the property that b ^ N * f (a / b) does not have denominators, if the inequality f.natDegree ≤ N holds.

The definition asserts the existence of an element D of R and an element bi = 1 / i b of K such that clearing the denominators of the fraction equals i D.

Equations

• DenomsClearable a b N f i = ∃ (D : R) (bi : K), bi * i b = 1 ∧ i D = i b ^ N * Polynomial.eval (i a * bi) (Polynomial.map i f)

theorem denomsClearable_zero {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ℕ) (a : R) (bu : bi * i b = 1) : DenomsClearable a b N 0 i

theorem denomsClearable_C_mul_X_pow {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {i : R →+* K} {b : R} {bi : K} {N : ℕ} (a : R) (bu : bi * i b = 1) {n : ℕ} (r : R) (nN : n ≤ N) : DenomsClearable a b N (Polynomial.C r * Polynomial.X ^ n) i

theorem DenomsClearable.add {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {i : R →+* K} {a b : R} {N : ℕ} {f g : Polynomial R} : DenomsClearable a b N f i → DenomsClearable a b N g i → DenomsClearable a b N (f + g) i

theorem denomsClearable_of_natDegree_le {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {i : R →+* K} {b : R} {bi : K} (N : ℕ) (a : R) (bu : bi * i b = 1) (f : Polynomial R) : f.natDegree ≤ N → DenomsClearable a b N f i

theorem denomsClearable_natDegree {R : Type u_1} {K : Type u_2} [Semiring R] [CommSemiring K] {b : R} {bi : K} (i : R →+* K) (f : Polynomial R) (a : R) (bu : bi * i b = 1) : DenomsClearable a b f.natDegree f i

If i : R → K is a ring homomorphism, f is a polynomial with coefficients in R, a, b are elements of R, with i b invertible, then there is a D ∈ R such that b ^ f.natDegree * f (a / b) equals i D.

theorem one_le_pow_mul_abs_eval_div {K : Type u_1} [LinearOrderedField K] {f : Polynomial ℤ} {a b : ℤ} (b0 : 0 < b) (fab : Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f) ≠ 0) : 1 ≤ ↑b ^ f.natDegree * |Polynomial.eval (↑a / ↑b) (Polynomial.map (algebraMap ℤ K) f)|

Evaluating a polynomial with integer coefficients at a rational number and clearing denominators, yields a number greater than or equal to one. The target can be any LinearOrderedField K. The assumption on K could be weakened to LinearOrderedCommRing assuming that the image of the denominator is invertible in K.