Upper and lower bounds for the value of an auxiliary polynomial at a rational point

In the proof of Roth's theorem, an auxiliary polynomial Q in n variables with partial degrees degreeOf i Q ≤ r i is evaluated at a point β ∈ ℚⁿ whose coordinates are very good rational approximations of an algebraic number α. Two estimates for |Q(β)| then contradict each other.

• Lower bound. If Q has integer coefficients and Q(β) ≠ 0, then ∏ᵢ den(βᵢ) ^ rᵢ • Q(β) is a nonzero integer, so log |Q(β)| ≥ -∑ᵢ rᵢ log den(βᵢ).
• Upper bound. Expand Q(β) = ∑_d (∂^d Q)(a) (β - a)^d by Taylor's formula at a point a where Q has weighted index at least t with respect to the weights r. The terms of weight ∑ᵢ dᵢ / rᵢ < t vanish. If |βᵢ - aᵢ| ≤ H(βᵢ) ^ (-κ) and rᵢ h(βᵢ) ≥ D, each of the remaining terms has ∏ᵢ |βᵢ - aᵢ| ^ dᵢ ≤ exp(-κ D t), while the Hasse jets (∂^d Q)(a) are bounded in terms of the coefficients of Q. For coefficients bounded by B this gives |Q(β)| ≤ B (∏ᵢ (rᵢ + 1))² ∏ᵢ (2 max(1, |aᵢ|)) ^ rᵢ exp(-κ D t).

Here H and h are Mathlib's multiplicative and logarithmic heights Height.mulHeight₁ and Height.logHeight₁ on ℚ. In Roth's theorem a is the diagonal point (α, …, α).

Main results

• TauCeti.one_le_prod_den_pow_mul_abs_eval: 1 ≤ ∏ᵢ den(βᵢ) ^ rᵢ * |Q(β)| for Q ∈ ℤ[X] with Q(β) ≠ 0.
• TauCeti.neg_sum_mul_log_den_le_log_abs_eval: its logarithmic form -∑ᵢ rᵢ log den(βᵢ) ≤ log |Q(β)|.
• TauCeti.prod_abs_sub_pow_le_exp: ∏ᵢ |βᵢ - aᵢ| ^ dᵢ ≤ exp(-κ D t) for a multi-index d ≤ r of weight at least t.
• TauCeti.abs_eval_le_of_le_weightedIndex: the upper bound for a real polynomial of weighted index at least t at a.
• TauCeti.log_abs_eval_le_of_le_weightedIndex: its logarithmic form log |Q(β)| ≤ log B + ∑ᵢ rᵢ (log 2 + log max(1, |aᵢ|)) + 2 ∑ᵢ log(rᵢ + 1) - κ D t.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5.3 and Exercise 3.10.

The lower bound

theorem TauCeti.one_le_prod_den_pow_mul_abs_eval {σ : Type u_1} [Fintype σ] {Q : MvPolynomial σ ℤ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i Q ≤ r i) (β : σ → ℚ) (hQ : (MvPolynomial.eval β) ((MvPolynomial.map (Int.castRingHom ℚ)) Q) ≠ 0) : 1 ≤ (∏ i : σ, ↑(β i).den ^ r i) * |(MvPolynomial.eval β) ((MvPolynomial.map (Int.castRingHom ℚ)) Q)|

Lower bound for an integer polynomial at a rational point. If Q ∈ ℤ[X] has partial degrees degreeOf i Q ≤ r i and does not vanish at β ∈ ℚ^σ, then 1 ≤ ∏ᵢ den(βᵢ) ^ rᵢ * |Q(β)|: clearing denominators turns Q(β) into a nonzero integer.

theorem TauCeti.neg_sum_mul_log_den_le_log_abs_eval {σ : Type u_1} [Fintype σ] {Q : MvPolynomial σ ℤ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i Q ≤ r i) (β : σ → ℚ) (hQ : (MvPolynomial.eval fun (i : σ) => ↑(β i)) ((MvPolynomial.map (Int.castRingHom ℝ)) Q) ≠ 0) : -∑ i : σ, ↑(r i) * Real.log ↑(β i).den ≤ Real.log |(MvPolynomial.eval fun (i : σ) => ↑(β i)) ((MvPolynomial.map (Int.castRingHom ℝ)) Q)|

Lower bound for an integer polynomial at a rational point, logarithmic form: if Q ∈ ℤ[X] has partial degrees degreeOf i Q ≤ r i and Q(β) ≠ 0 for β ∈ ℚ^σ, then -∑ᵢ rᵢ log den(βᵢ) ≤ log |Q(β)|.

The upper bound

theorem TauCeti.prod_abs_sub_pow_le_exp {σ : Type u_1} [Fintype σ] {r : σ → ℕ} {a : σ → ℝ} {β : σ → ℚ} {κ D t : ℝ} (hκ : 0 ≤ κ) (hD : 0 ≤ D) (hβ : ∀ (i : σ), |↑(β i) - a i| ≤ Height.mulHeight₁ (β i) ^ (-κ)) (hr : ∀ (i : σ), D ≤ ↑(r i) * Height.logHeight₁ (β i)) {d : σ →₀ ℕ} (hdr : ∀ (i : σ), d i ≤ r i) (ht : t ≤ ∑ i : σ, ↑(d i) / ↑(r i)) : ∏ i : σ, |↑(β i) - a i| ^ d i ≤ Real.exp (-(κ * D * t))

Smallness of a high-weight monomial in the approximation errors. If β ∈ ℚ^σ satisfies |βᵢ - aᵢ| ≤ H(βᵢ) ^ (-κ) and D ≤ rᵢ h(βᵢ) for all i, with κ, D ≥ 0, then every multi-index d ≤ r of weight ∑ᵢ dᵢ / rᵢ ≥ t has ∏ᵢ |βᵢ - aᵢ| ^ dᵢ ≤ exp(-κ D t).

theorem TauCeti.abs_eval_le_of_le_weightedIndex {σ : Type u_1} [Fintype σ] {P : MvPolynomial σ ℝ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i P ≤ r i) {B : ℝ} (hB : ∀ (μ : σ →₀ ℕ), |P.coeff μ| ≤ B) {a : σ → ℝ} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex r a P) {β : σ → ℚ} {κ D : ℝ} (hκ : 0 ≤ κ) (hD : 0 ≤ D) (hβ : ∀ (i : σ), |↑(β i) - a i| ≤ Height.mulHeight₁ (β i) ^ (-κ)) (hr : ∀ (i : σ), D ≤ ↑(r i) * Height.logHeight₁ (β i)) : |(MvPolynomial.eval fun (i : σ) => ↑(β i)) P| ≤ (B * (∏ i : σ, (↑(r i) + 1)) ^ 2 * ∏ i : σ, (2 * max 1 |a i|) ^ r i) * Real.exp (-(κ * D * t))

Upper bound for an auxiliary polynomial at a rational point. Let P be a real polynomial with partial degrees degreeOf i P ≤ r i, coefficients bounded by B, and weighted index at least t at a with respect to the weights r. If β ∈ ℚ^σ satisfies |βᵢ - aᵢ| ≤ H(βᵢ) ^ (-κ) and D ≤ rᵢ h(βᵢ) for all i, with κ, D ≥ 0, then |P(β)| ≤ B (∏ᵢ (rᵢ + 1))² ∏ᵢ (2 max(1, |aᵢ|)) ^ rᵢ exp(-κ D t).

theorem TauCeti.log_abs_eval_le_of_le_weightedIndex {σ : Type u_1} [Fintype σ] {P : MvPolynomial σ ℝ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i P ≤ r i) {B : ℝ} (hB : ∀ (μ : σ →₀ ℕ), |P.coeff μ| ≤ B) {a : σ → ℝ} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex r a P) {β : σ → ℚ} {κ D : ℝ} (hκ : 0 ≤ κ) (hD : 0 ≤ D) (hβ : ∀ (i : σ), |↑(β i) - a i| ≤ Height.mulHeight₁ (β i) ^ (-κ)) (hr : ∀ (i : σ), D ≤ ↑(r i) * Height.logHeight₁ (β i)) (hP : (MvPolynomial.eval fun (i : σ) => ↑(β i)) P ≠ 0) : Real.log |(MvPolynomial.eval fun (i : σ) => ↑(β i)) P| ≤ Real.log B + ∑ i : σ, ↑(r i) * (Real.log 2 + Real.log (max 1 |a i|)) + 2 * ∑ i : σ, Real.log (↑(r i) + 1) - κ * D * t

Upper bound for an auxiliary polynomial at a rational point, logarithmic form: under the hypotheses of TauCeti.abs_eval_le_of_le_weightedIndex, if moreover P(β) ≠ 0, then log |P(β)| ≤ log B + ∑ᵢ rᵢ (log 2 + log max(1, |aᵢ|)) + 2 ∑ᵢ log(rᵢ + 1) - κ D t.