The choice of parameters in the proof of Roth's theorem

The proof of Roth's theorem evaluates an auxiliary polynomial at good rational approximations β₀, …, β_{n-1} of an algebraic number whose logarithmic heights h k = h(β_k) grow quickly: L ≤ h 0 and M * h k ≤ h (k + 1). For a real number D with 5 * h k ≤ D, the partial degrees of the auxiliary polynomial are bounded by r k = ⌊D / h k⌋₊. Such sequences of approximations exist by Northcott.exists_seq_mem_lt.

This file proves the elementary inequalities between these parameters which put the auxiliary polynomial in the range of Roth's index estimate. They are stated for an arbitrary real sequence h, which in the application is the sequence of heights of the approximations.

Main results

• TauCeti.sum_range_floor_div_le_two_mul_div: if M ≥ 2, then ∑_{k < n} r k ≤ 2 D / L.
• TauCeti.floor_div_le_mul_floor_div: if σ M ≥ 2, then r (k + 1) ≤ σ r k.
• TauCeti.inv_mul_add_le_floor_div_mul: if L ≥ σ⁻¹ (5 C₁ / 2 + 5 n) and a height H is at most C₁ ∑_{j < n} r j, then σ⁻¹ (H + 4 n r 0) ≤ r k h k.

The degree bounds are positive, 1 ≤ r k, by Nat.one_le_floor_iff and one_le_div.

References

• L. Pottmeyer, Diophantine Approximation (2022), §3.5.2.

theorem TauCeti.sum_range_floor_div_le_two_mul_div {n : ℕ} {h : ℕ → ℝ} {D L M : ℝ} (hD : 0 ≤ D) (hL : 0 < L) (hM : 2 ≤ M) (h₀ : L ≤ h 0) (hh : ∀ (k : ℕ), k + 1 < n → M * h k ≤ h (k + 1)) : ∑ k ∈ Finset.range n, ↑⌊D / h k⌋₊ ≤ 2 * D / L

If a sequence starts at h 0 ≥ L > 0 and grows by a factor M ≥ 2 at each of its first n terms, then the sum of ⌊D / h k⌋₊ over these terms is at most 2 D / L.

theorem TauCeti.floor_div_le_mul_floor_div {x y D M σ : ℝ} (hσ : 0 < σ) (hσM : 2 ≤ σ * M) (hx : 0 < x) (hxy : M * x ≤ y) (hD : 2 * x ≤ D) : ↑⌊D / y⌋₊ ≤ σ * ↑⌊D / x⌋₊

If y ≥ M x > 0, D ≥ 2 x and σ M ≥ 2, then ⌊D / y⌋₊ ≤ σ ⌊D / x⌋₊. Applied to consecutive terms of a quickly growing sequence, this makes consecutive degree bounds decrease by the factor σ.

theorem TauCeti.inv_mul_add_le_floor_div_mul {n k : ℕ} {h : ℕ → ℝ} {D L M σ C₁ H : ℝ} (hσ : 0 < σ) (hL : 0 < L) (hM : 2 ≤ M) (h₀ : L ≤ h 0) (hh : ∀ (j : ℕ), j + 1 < n → M * h j ≤ h (j + 1)) (hC₁ : 0 ≤ C₁) (hLC : σ⁻¹ * (5 * C₁ / 2 + 5 * ↑n) ≤ L) (hk : 0 < h k) (hD : 5 * h k ≤ D) (hH : H ≤ C₁ * ∑ j ∈ Finset.range n, ↑⌊D / h j⌋₊) : σ⁻¹ * (H + 4 * ↑n * ↑⌊D / h 0⌋₊) ≤ ↑⌊D / h k⌋₊ * h k

The height condition of Roth's index estimate for the degree bounds r j = ⌊D / h j⌋₊. Let h start at h 0 ≥ L ≥ σ⁻¹ (5 C₁ / 2 + 5 n) and grow by a factor M ≥ 2 along its first n terms. If 5 h k ≤ D and H ≤ C₁ ∑_{j < n} r j, then σ⁻¹ (H + 4 n r 0) ≤ r k h k.