Approximation by algebraic numbers of bounded degree

DefinitionHeight of a real algebraic number#✓fully proved

Let \(\alpha\) be a real algebraic number, let \(p\) be its monic minimal polynomial over \(\mathbb{Q}\), and let \(D\) be the least common multiple of the denominators of the nonzero coefficients of \(p\). The height \(H(\alpha)\) is the largest absolute value of a coefficient of the integer polynomial \(D p\). For a real number that is not algebraic over \(\mathbb{Q}\), the height is \(0\).

Equivalently, \(H(\alpha)\) is the largest absolute value of a coefficient of the minimal polynomial of \(\alpha\) scaled to have coprime integer coefficients.

noncomputable def height (α : ℝ) : ℕ :=
  -- Let `p` be the minimal polynomial of `α`, defined to be monic and over `ℚ`.
  letI p := minpoly ℚ α
  -- Now let `D` be the LCM of the denominators of the nonzero coefficients.
  letI D := Multiset.lcm (Multiset.map (fun i ↦ (p.coeff i).den) p.support.val)
  -- The height of `α` is the supremum of the finite set of `|n|`, where `n` runs
  -- through the numerators of the nonzero coefficients of `D * p`.
  Finset.sup p.support (fun i ↦ (D * p.coeff i).num.natAbs)

Used by 1

Used byApproximation exponents admitting infinitely many solutions

DefinitionReal algebraic numbers of bounded degree#✓fully proved

For a natural number \(n\), this is the type of real numbers \(\alpha\) that are algebraic over \(\mathbb{Q}\) and whose minimal polynomial over \(\mathbb{Q}\) has degree at most \(n\).

def AlgebraicDegLE (n : ℕ) : Type :=
  {α : ℝ // IsAlgebraic ℚ α ∧ Polynomial.natDegree (minpoly ℚ α) ≤ n}

Sources

the lean-eval source ranged over ℂ; the classical exponent in Poëls' theorem uses real algebraic approximants, so this is restricted to ℝ (recorded as a Lean variant).

Used by 1

Used byApproximation exponents admitting infinitely many solutions

DefinitionApproximation exponents admitting infinitely many solutions#✓fully proved

Let \(n\) be a natural number, \(\xi\) a real number, and \(H(\alpha)\) the height of a real algebraic number \(\alpha\). This is the set of real numbers \(\omega > 0\) for which there are infinitely many real algebraic numbers \(\alpha\) of degree at most \(n\) with \(0 < |\xi - \alpha| \le H(\alpha)^{-\omega - 1}\).

When \(n \ge 1\) and \(\xi\) is irrational, this set contains the interval \((0, 1)\) by Dirichlet's theorem.

def ω_stars (n : ℕ) (ξ : ℝ) : Set ℝ≥0 :=
  {ω : ℝ≥0 | 0 < ω ∧
    {α : AlgebraicDegLE n | 0 < ‖ξ - α.1‖ ∧ ‖ξ - α.1‖ ≤ (height α.1) ^ (- (ω : ℝ) - 1)}.Infinite}

def AlgebraicDegLE (n : ℕ) : Type :=
  {α : ℝ // IsAlgebraic ℚ α ∧ Polynomial.natDegree (minpoly ℚ α) ≤ n}

WantedExt/NumberTheory/OnApproximationOfRealsWanted.lean:73

noncomputable def height (α : ℝ) : ℕ :=
  -- Let `p` be the minimal polynomial of `α`, defined to be monic and over `ℚ`.
  letI p := minpoly ℚ α
  -- Now let `D` be the LCM of the denominators of the nonzero coefficients.
  letI D := Multiset.lcm (Multiset.map (fun i ↦ (p.coeff i).den) p.support.val)
  -- The height of `α` is the supremum of the finite set of `|n|`, where `n` runs
  -- through the numerators of the nonzero coefficients of `D * p`.
  Finset.sup p.support (fun i ↦ (D * p.coeff i).num.natAbs)

WantedExt/NumberTheory/OnApproximationOfRealsWanted.lean:60

Sources

ω here is ω⋆ in the paper.

Uses 2 · Used by 1

Statement usesReal algebraic numbers of bounded degree · Height of a real algebraic number

Used byClassical exponent of approximation by algebraic numbers

DefinitionClassical exponent of approximation by algebraic numbers#✓fully proved

For a natural number \(n\) and a real number \(\xi\), let \(H(\alpha)\) denote the height of a real algebraic number \(\alpha\). The classical exponent \(\omega^*_n(\xi)\) is the supremum in \([0, \infty]\) of the set of real numbers \(\omega > 0\) for which there are infinitely many real algebraic numbers \(\alpha\) of degree at most \(n\) with \(0 < |\xi - \alpha| \le H(\alpha)^{-\omega - 1}\). It is \(0\) when this set is empty.

noncomputable def classicalExponent (n : ℕ) (ξ : ℝ) : ℝ≥0∞ :=
  sSup (((↑) : ℝ≥0 → ℝ≥0∞) '' (ω_stars n ξ))

def ω_stars (n : ℕ) (ξ : ℝ) : Set ℝ≥0 :=
  {ω : ℝ≥0 | 0 < ω ∧
    {α : AlgebraicDegLE n | 0 < ‖ξ - α.1‖ ∧ ‖ξ - α.1‖ ≤ (height α.1) ^ (- (ω : ℝ) - 1)}.Infinite}

WantedExt/NumberTheory/OnApproximationOfRealsWanted.lean:81

Uses 1 · Used by 1

Statement usesApproximation exponents admitting infinitely many solutions

Used byPoëls' lower bound for the classical exponent

TheoremPoëls' lower bound for the classical exponent#●ready to prove

Let \(n \ge 2\) be an integer and let \(a = 1/(2 - \log 2)\). For every real number \(\xi\) that is transcendental over \(\mathbb{Q}\), the classical exponent of approximation to \(\xi\) by real algebraic numbers of degree at most \(n\) satisfies \(\omega^*_n(\xi) \ge a n\).

public theorem_wanted theorem_1_1 (n : ℕ) (hn : n ≥ 2) (ξ : ℝ) (hξ : Transcendental ℚ ξ) :
    letI a : ℝ := 1 / (2 - Real.log 2)
    (ω⋆ n ξ : EReal) ≥ (a : EReal) * n

Sources

A. Poëls, On approximation to a real number by algebraic numbers of bounded degree, Annals of Math, 201 (1) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_on_approximation_of_reals of the lean-eval benchmark.

Uses 1

Statement usesClassical exponent of approximation by algebraic numbers

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.