Thue–Siegel–Roth theorem

TheoremRoth's theorem with divisibility conditions#✓fully proved

Let \(\alpha\) be a real algebraic number, let \(0 < \varepsilon \le 1\), and let \(S\) be a finite index set carrying, for each \(l \in S\), a natural number \(p_l\) and reals \(\mu_l, \nu_l \ge 0\) with \(\sigma = \sum_{l \in S} (\mu_l + \nu_l)\) less than \(2 + \varepsilon\). Then there are only finitely many rationals \(q\), written in lowest terms with numerator \(n\) and denominator \(d \ge 1\), such that \(|\alpha - q| < 1/d^{2 + \varepsilon - \sigma}\) and there are exponents \(a_l, b_l \in \mathbb{N}\) for \(l \in S\) with \(\prod_{l \in S} p_l^{a_l}\) dividing \(n\), \(\prod_{l \in S} p_l^{b_l}\) dividing \(d\), and \(d^{\mu_l} \le p_l^{a_l}\) and \(d^{\nu_l} \le p_l^{b_l}\) for every \(l \in S\).

Taking \(S\) empty gives the usual archimedean approximation statement.

MathlibExt.NumberTheory.RothAuxiliary.finite_of_divisible_approximations · 15 lines 
public theorem finite_of_divisible_approximations
    (α : ℝ) (hα : IsAlgebraic ℚ α)
    (ε : ℝ) (hε : 0 < ε) (hεone : ε ≤ 1)
    {ι : Type*} (S : Finset ι) (p : ι → ℕ) (μ ν : ι → ℝ)
    (hμ : ∀ l ∈ S, 0 ≤ μ l) (hν : ∀ l ∈ S, 0 ≤ ν l)
    (hσ : ∑ l ∈ S, (μ l + ν l) < 2 + ε) :
    Set.Finite {q : ℚ |
      |α - (q : ℝ)| <
          1 / Real.rpow (q.den : ℝ) (2 + ε - ∑ l ∈ S, (μ l + ν l)) ∧
        ∃ a b : ι → ℕ,
          ((∏ l ∈ S, p l ^ a l : ℕ) : ℤ) ∣ q.num ∧
          (∏ l ∈ S, p l ^ b l) ∣ q.den ∧
          ∀ l ∈ S,
            Real.rpow (q.den : ℝ) (μ l) ≤ (p l : ℝ) ^ a l ∧
            Real.rpow (q.den : ℝ) (ν l) ≤ (p l : ℝ) ^ b l}
Used by 2
Used byRidout's \(p\)-adic extension of Roth's theorem · Thue–Siegel–Roth theorem

TheoremRidout's \(p\)-adic extension of Roth's theorem#✓fully proved

Let \(\xi\) be an irrational real algebraic number, let \(\varepsilon > 0\), and let \(S\) be a finite set of primes. For a rational number \(r\), write \(r = p/q\) in lowest terms with \(p \in \mathbb{Z}\) and \(q \ge 1\), and let \(H(r) = \max(|p|, q)\) be its height. For a prime \(\ell\), let \(|\cdot|_\ell\) be the \(\ell\)-adic absolute value on \(\mathbb{Q}\), normalized by \(|\ell|_\ell = \ell^{-1}\). Then only finitely many rationals \(r = p/q\) satisfy

\[\Bigl(\prod_{\ell \in S} |p|_\ell |q|_\ell\Bigr) |\xi - r| < \frac{1}{H(r)^{2 + \varepsilon}}.\]

The source prints the right side as \(1/q^{2 + \varepsilon}\). Over all rationals that bound fails: with \(2 \in S\) and \(\xi = \sqrt{2}\), every \(r = 2^k\) with \(k \ge 1\) gives left side \(1 - \sqrt{2}/2^k < 1\), so the height \(H(r)\) is used instead.

Proof: The proof follows Roth's auxiliary-polynomial and index route, with the S-adic integrality step supplied by valuation divisibility and a finite pigeonhole.

theorem ridout_padic_roth (ξ : ℝ) (hξ : IsAlgebraic ℚ ξ) (hξi : Irrational ξ)
    (ε : ℝ) (hε : 0 < ε)
    (S : Finset Nat.Primes) :
    Set.Finite {r : ℚ |
      ((∏ ℓ ∈ S, padicNorm ℓ.1 (r.num : ℚ) * padicNorm ℓ.1 (r.den : ℚ) : ℚ) : ℝ) *
          |ξ - (r : ℝ)| <
        (((max r.num.natAbs r.den : ℕ) : ℝ) ^ (2 + ε))⁻¹}
Sources
Uses 1
Proof usesRoth's theorem with divisibility conditions

TheoremThue–Siegel–Roth theorem#✓fully proved

Let \(\alpha\) be an irrational real number that is algebraic over \(\mathbb{Q}\), and let \(\varepsilon > 0\) be real. Then only finitely many rational numbers \(q\) satisfy \(|\alpha - q| < 1 / b^{2 + \varepsilon}\), where \(b\) is the denominator of \(q\) in lowest terms.

Proof: The proof constructs Siegel's auxiliary polynomial, bounds its index at rational approximation points by a Taylor estimate, and contradicts the inductive Roth lemma.

public theorem thue_siegel_roth :
    ∀ (α : ℝ), IsAlgebraic ℚ α → Irrational α →
      ∀ (ε : ℝ), 0 < ε →
        Set.Finite { q : ℚ | |α - (q : ℝ)| < 1 / Real.rpow (q.den : ℝ) (2 + ε) }
Sources
  • K. F. Roth, Rational approximations to algebraic numbers, Mathematika 2 (1955) 1–20; predecessors Thue 1909 and Siegel 1921; textbook in Schmidt, Diophantine Approximation
Uses 1
Proof usesRoth's theorem with divisibility conditions
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.