The key inequality in the proof of Roth's theorem

Let α be a real number and let β ∈ ℚⁿ be a tuple of rational approximations of α with |βᵢ - α| ≤ H(βᵢ) ^ (-κ). Let P ∈ ℤ[X₁, …, Xₙ] be an auxiliary polynomial with partial degrees degreeOf i P ≤ rᵢ, coefficients at most exp (C₁ ∑ᵢ rᵢ) in absolute value, and weighted index at least (n / 2) (1 - ε) at the diagonal point (α, …, α). Suppose that the weighted index of P at β is at most 5 n ε / 2, as Roth's lemma guarantees for approximations of rapidly increasing heights.

Then a Hasse derivative Q of P does not vanish at β and still has index at least t = (1 / 2 - 3 ε) n at the diagonal point (TauCeti.exists_roth_hasseDeriv). Comparing the lower bound log |Q(β)| ≥ -∑ᵢ rᵢ log den(βᵢ) with the upper bound coming from the Taylor expansion of Q at the diagonal point (TauCeti.log_abs_eval_le_of_le_weightedIndex) gives the inequality

κ D' t ≤ n D + C₂ D / L, where C₂ = 4 C₁ + 2 log (2 max(1, |α|)) + 4,

whenever D' ≤ rᵢ h(βᵢ) ≤ D for all i and ∑ᵢ rᵢ ≤ 2 D / L. With rᵢ = ⌊D / h(βᵢ)⌋ the ratio D' / D tends to 1 as D grows, so for L large this forces κ (1 / 2 - 3 ε) ≤ 1 + o(1), which is false once κ > 2 and ε is small. This is the contradiction that proves Roth's theorem.

Main results

• TauCeti.roth_key_inequality_of_eval_ne_zero: for an integer polynomial Q with Q(β) ≠ 0 and weighted index at least t at a point a, κ D' t ≤ ∑ᵢ rᵢ h(βᵢ) + log B + ∑ᵢ rᵢ (log 2 + log max(1, |aᵢ|)) + 2 ∑ᵢ log (rᵢ + 1).
• TauCeti.roth_key_inequality: Pottmeyer's inequality (3.42) over ℚ, κ D' (1 / 2 - 3 ε) n ≤ n D + C₂ D / L, for an auxiliary polynomial of small index at β.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5.3 and §3.5.4, inequalities (3.40)–(3.42).

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

The key inequality for a nonvanishing polynomial. Let Q ∈ ℤ[X] have partial degrees degreeOf i Q ≤ r i, coefficients bounded by B in absolute value, and weighted index at least t at a ∈ ℝ^σ. If β ∈ ℚ^σ satisfies |βᵢ - aᵢ| ≤ H(βᵢ) ^ (-κ) and D ≤ rᵢ h(βᵢ), with κ, D ≥ 0, and Q(β) ≠ 0, then κ D t ≤ ∑ᵢ rᵢ h(βᵢ) + log B + ∑ᵢ rᵢ (log 2 + log max(1, |aᵢ|)) + 2 ∑ᵢ log (rᵢ + 1).

theorem TauCeti.roth_key_inequality {σ : Type u_1} [Fintype σ] {P : MvPolynomial σ ℤ} {r : σ → ℕ} (hdeg : ∀ (i : σ), MvPolynomial.degreeOf i P ≤ r i) {ε C₁ D L : ℝ} (hε : 0 ≤ ε) (hC₁ : Real.log 2 ≤ C₁) (hr : ∑ i : σ, ↑(r i) ≤ 2 * D / L) (hP : ∀ (μ : σ →₀ ℕ), |↑(P.coeff μ)| ≤ Real.exp (C₁ * ∑ i : σ, ↑(r i))) {α : ℝ} (hα : ENNReal.ofReal (↑(Fintype.card σ) / 2 * (1 - ε)) ≤ MvPolynomial.weightedIndex r (fun (x : σ) => α) ((MvPolynomial.map (Int.castRingHom ℝ)) P)) {β : σ → ℚ} (hβP : MvPolynomial.weightedIndex r β ((MvPolynomial.map (Int.castRingHom ℚ)) P) ≤ ENNReal.ofReal (5 * ↑(Fintype.card σ) * ε / 2)) {κ D' : ℝ} (hκ : 0 ≤ κ) (hD' : 0 ≤ D') (hβ : ∀ (i : σ), |↑(β i) - α| ≤ Height.mulHeight₁ (β i) ^ (-κ)) (hlow : ∀ (i : σ), D' ≤ ↑(r i) * Height.logHeight₁ (β i)) (hup : ∀ (i : σ), ↑(r i) * Height.logHeight₁ (β i) ≤ D) : κ * D' * ((1 / 2 - 3 * ε) * ↑(Fintype.card σ)) ≤ ↑(Fintype.card σ) * D + (4 * C₁ + 2 * Real.log (2 * max 1 |α|) + 4) * D / L

The key inequality in the proof of Roth's theorem (Pottmeyer, (3.42) over ℚ). Let P ∈ ℤ[X] have partial degrees degreeOf i P ≤ r i, where ∑ᵢ rᵢ ≤ 2 D / L, coefficients at most exp (C₁ ∑ᵢ rᵢ) in absolute value, where C₁ ≥ log 2, and weighted index at least (n / 2) (1 - ε) at the diagonal point (α, …, α), with 0 ≤ ε. Let β ∈ ℚ^σ satisfy |βᵢ - α| ≤ H(βᵢ) ^ (-κ) and D' ≤ rᵢ h(βᵢ) ≤ D, with κ, D' ≥ 0. If the weighted index of P at β is at most 5 n ε / 2, then κ D' (1 / 2 - 3 ε) n ≤ n D + (4 C₁ + 2 log (2 max(1, |α|)) + 4) D / L.