Asymptotic Dobrowolski constant

DefinitionDobrowolski scale#✓fully proved

For a natural number \(d\), the Dobrowolski scale is

\[\left(\frac{\log \log d}{\log d}\right)^3,\]

with natural logarithms and the conventions \(\log 0 = 0\) and \(x / 0 = 0\), so that it is \(0\) for \(d \le 1\).

It is used only for degrees \(d \ge 3\) in the definition of asymptotic Dobrowolski coefficients.

noncomputable def dobrowolskiScale (d : ℕ) : ℝ :=
  (Real.log (Real.log d) / Real.log d) ^ 3

Used by 5

Used byPositivity of the Dobrowolski scale · Asymptotic Dobrowolski coefficients · Coefficients are exactly the reals below the constant · Strict form of asymptotic Dobrowolski coefficients · Zero is an asymptotic Dobrowolski coefficient

TheoremPositivity of the Dobrowolski scale#✓fully proved

For every natural number \(d \ge 3\), the Dobrowolski scale \(\left(\frac{\log \log d}{\log d}\right)^3\) is strictly positive.

theorem dobrowolskiScale_pos {d : ℕ} (hd : 3 ≤ d) : 0 < dobrowolskiScale d

Uses 1 · Used by 3

Statement usesDobrowolski scale

Used byCoefficients are exactly the reals below the constant · Strict form of asymptotic Dobrowolski coefficients · Zero is an asymptotic Dobrowolski coefficient

DefinitionAsymptotic Dobrowolski coefficients#✓fully proved

A real number \(c\) is an asymptotic Dobrowolski coefficient if for every \(\varepsilon > 0\) there is a natural number \(D \ge 3\) such that every nonzero algebraic number \(\alpha \in \mathbb{C}\) that is not a root of unity and whose minimal polynomial over \(\mathbb{Q}\) has degree \(d \ge D\) satisfies

\[1 + (c - \varepsilon) \left(\frac{\log \log d}{\log d}\right)^3 \le M(\alpha),\]

where \(M(\alpha)\) is the Mahler measure of \(\alpha\).

The degree threshold \(D\) may depend on \(\varepsilon\) but is uniform over all such \(\alpha\).

def IsAsymptoticDobrowolskiCoefficient (c : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ D : ℕ, 3 ≤ D ∧
    ∀ α : ℂ, IsAlgebraic ℚ α → α ≠ 0 → ¬IsOfFinOrder α →
      D ≤ (minpoly ℚ α).natDegree →
        1 + (c - ε) * dobrowolskiScale (minpoly ℚ α).natDegree ≤
          algebraicMahlerMeasure α

Uses 2 · Used by 6

Statement usesDobrowolski scale · Algebraic Mahler measure

Used byAsymptotic Dobrowolski constant · Upper bounds for the asymptotic Dobrowolski constant · Coefficients are bounded by the asymptotic Dobrowolski constant · Coefficients are exactly the reals below the constant · Strict form of asymptotic Dobrowolski coefficients · Zero is an asymptotic Dobrowolski coefficient

DefinitionAsymptotic Dobrowolski constant#✓fully proved

The asymptotic Dobrowolski constant is the supremum, in the extended real numbers \([-\infty, +\infty]\), of the set of all real asymptotic Dobrowolski coefficients.

The supremum would be \(-\infty\) if there were no coefficient and is \(+\infty\) if the coefficients are unbounded above; neither attainment nor a finite upper bound is assumed.

noncomputable def asymptoticDobrowolskiConstant : EReal :=
  sSup {x : EReal | ∃ c : ℝ, IsAsymptoticDobrowolskiCoefficient c ∧ x = c}

Uses 1 · Used by 8

Statement usesAsymptotic Dobrowolski coefficients

Used byUpper bounds for the asymptotic Dobrowolski constant · Trivial upper bound for the asymptotic Dobrowolski constant · The asymptotic Dobrowolski constant is nonnegative · Cantor–Straus lower bound for the asymptotic Dobrowolski constant · Coefficients are bounded by the asymptotic Dobrowolski constant · Dobrowolski's lower bound for the asymptotic Dobrowolski constant · Coefficients are exactly the reals below the constant · Louboutin's lower bound for the asymptotic Dobrowolski constant

TheoremCoefficients are bounded by the asymptotic Dobrowolski constant#✓fully proved

Every real asymptotic Dobrowolski coefficient \(c\) satisfies \(c \le\) the asymptotic Dobrowolski constant, as extended real numbers.

theorem coe_le_asymptoticDobrowolskiConstant {c : ℝ}
    (hc : IsAsymptoticDobrowolskiCoefficient c) :
    (c : EReal) ≤ asymptoticDobrowolskiConstant

Uses 2 · Used by 3

Statement usesAsymptotic Dobrowolski coefficients · Asymptotic Dobrowolski constant

Used byUpper bounds for the asymptotic Dobrowolski constant · The asymptotic Dobrowolski constant is nonnegative · Coefficients are exactly the reals below the constant

TheoremZero is an asymptotic Dobrowolski coefficient#✓fully proved

The real number \(0\) is an asymptotic Dobrowolski coefficient: for every real \(\varepsilon > 0\) there is a natural number \(D \ge 3\) such that every nonzero algebraic number \(\alpha \in \mathbb{C}\) that is not a root of unity and whose minimal polynomial over \(\mathbb{Q}\) has degree \(d \ge D\) satisfies \(1 - \varepsilon \left(\frac{\log \log d}{\log d}\right)^3 \le M(\alpha)\), where \(M(\alpha)\) is the Mahler measure of the primitive integer minimal polynomial of \(\alpha\) with positive leading coefficient.

theorem zero_isAsymptoticDobrowolskiCoefficient : IsAsymptoticDobrowolskiCoefficient 0

Uses 5 · Used by 1

Statement usesAsymptotic Dobrowolski coefficients

Proof usesDobrowolski scale · Positivity of the Dobrowolski scale · Algebraic Mahler measure · The algebraic Mahler measure is at least one

Used byThe asymptotic Dobrowolski constant is nonnegative

TheoremUpper bounds for the asymptotic Dobrowolski constant#✓fully proved

For every extended real number \(b\), the asymptotic Dobrowolski constant is at most \(b\) if and only if every real asymptotic Dobrowolski coefficient \(c\) satisfies \(c \le b\).

theorem asymptoticDobrowolskiConstant_le_iff {b : EReal} :
    asymptoticDobrowolskiConstant ≤ b ↔
      ∀ c : ℝ, IsAsymptoticDobrowolskiCoefficient c → (c : EReal) ≤ b

Uses 3

Statement usesAsymptotic Dobrowolski coefficients · Asymptotic Dobrowolski constant

Proof usesCoefficients are bounded by the asymptotic Dobrowolski constant

TheoremCoefficients are exactly the reals below the constant#✓fully proved

A real number \(c\) is an asymptotic Dobrowolski coefficient if and only if \(c\) is at most the asymptotic Dobrowolski constant, as extended real numbers.

The \(\varepsilon\) in the definition makes the set of coefficients closed, so a finite constant is itself a coefficient; this also covers the case where the coefficients are unbounded above.

theorem isAsymptoticDobrowolskiCoefficient_iff {c : ℝ} :
    IsAsymptoticDobrowolskiCoefficient c ↔ (c : EReal) ≤ asymptoticDobrowolskiConstant

Uses 6

Statement usesAsymptotic Dobrowolski coefficients · Asymptotic Dobrowolski constant

Proof usesCoefficients are bounded by the asymptotic Dobrowolski constant · Dobrowolski scale · Positivity of the Dobrowolski scale · Algebraic Mahler measure

TheoremStrict form of asymptotic Dobrowolski coefficients#✓fully proved

A real number \(c\) is an asymptotic Dobrowolski coefficient if and only if for every \(\varepsilon > 0\) there is a natural number \(D \ge 3\) such that every nonzero algebraic number \(\alpha \in \mathbb{C}\) that is not a root of unity and whose minimal polynomial over \(\mathbb{Q}\) has degree \(d \ge D\) satisfies

\[1 + (c - \varepsilon) \left(\frac{\log \log d}{\log d}\right)^3 < M(\alpha),\]

where \(M(\alpha)\) is the Mahler measure of \(\alpha\).

So the strict bounds are equivalent to the non-strict bounds in the definition.

theorem isAsymptoticDobrowolskiCoefficient_iff_strict {c : ℝ} :
    IsAsymptoticDobrowolskiCoefficient c ↔
      ∀ ε : ℝ, 0 < ε → ∃ D : ℕ, 3 ≤ D ∧
        ∀ α : ℂ, IsAlgebraic ℚ α → α ≠ 0 → ¬IsOfFinOrder α →
          D ≤ (minpoly ℚ α).natDegree →
            1 + (c - ε) * dobrowolskiScale (minpoly ℚ α).natDegree <
              algebraicMahlerMeasure α

Uses 4

Statement usesAsymptotic Dobrowolski coefficients · Dobrowolski scale · Algebraic Mahler measure

Proof usesPositivity of the Dobrowolski scale

TheoremThe asymptotic Dobrowolski constant is nonnegative#✓fully proved

The asymptotic Dobrowolski constant is at least \(0\).

The bound comes from the coefficient \(0\), which is an asymptotic Dobrowolski coefficient because every Mahler measure is at least \(1\).

theorem asymptoticDobrowolskiConstant_nonneg : 0 ≤ asymptoticDobrowolskiConstant

Uses 3

Statement usesAsymptotic Dobrowolski constant

Proof usesCoefficients are bounded by the asymptotic Dobrowolski constant · Zero is an asymptotic Dobrowolski coefficient

TheoremTrivial upper bound for the asymptotic Dobrowolski constant#✓fully proved

The asymptotic Dobrowolski constant is at most \(+\infty\).

This is only the trivial bound in the extended reals, not a finite estimate.

theorem asymptoticDobrowolskiConstant_le_top : asymptoticDobrowolskiConstant ≤ ⊤

Uses 1

Statement usesAsymptotic Dobrowolski constant

TheoremDobrowolski's lower bound for the asymptotic Dobrowolski constant#●ready to prove

The asymptotic Dobrowolski constant is at least \(1\), as an extended real number.

theorem_wanted dobrowolski_one_le_asymptoticConstant :
    (1 : EReal) ≤ asymptoticDobrowolskiConstant

Sources

• Dobrowolski (1979), as reported by Voutier, coefficient 1.

Uses 1

Statement usesAsymptotic Dobrowolski constant

TheoremCantor–Straus lower bound for the asymptotic Dobrowolski constant#●ready to prove

The asymptotic Dobrowolski constant is at least \(2\), as an extended real number.

theorem_wanted cantorStraus_two_le_asymptoticConstant :
    (2 : EReal) ≤ asymptoticDobrowolskiConstant

Sources

• Cantor--Straus (1982), as reported by Voutier, coefficient 2.

Uses 1

Statement usesAsymptotic Dobrowolski constant

TheoremLouboutin's lower bound for the asymptotic Dobrowolski constant#●ready to prove

The asymptotic Dobrowolski constant is at least \(9/4\), as an extended real number.

theorem_wanted louboutin_nine_fourths_le_asymptoticConstant :
    ((9 : ℝ) / 4 : EReal) ≤ asymptoticDobrowolskiConstant

Sources

• Louboutin (1983), as reported by Voutier, coefficient 9/4.

Uses 1

Statement usesAsymptotic Dobrowolski constant

TheoremBlanksby–Montgomery lower bound for the Mahler measure#●ready to prove

Let \(\alpha\) be a nonzero complex number that is algebraic over \(\mathbb{Q}\) and is not a root of unity, and let \(d\) be the degree of its minimal polynomial over \(\mathbb{Q}\). If \(d \ge 2\), then the algebraic Mahler measure \(M(\alpha)\) satisfies \(M(\alpha) > 1 + \frac{1}{52\, d \log(6d)}\), with \(\log\) the natural logarithm.

theorem_wanted blanksbyMontgomery_degreeBound (α : ℂ)
    (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) (hroot : ¬IsOfFinOrder α)
    (hd : 2 ≤ (minpoly ℚ α).natDegree) :
    1 + 1 / (52 * (minpoly ℚ α).natDegree * Real.log (6 * (minpoly ℚ α).natDegree)) <
      algebraicMahlerMeasure α

Sources

• Blanksby--Montgomery, the strict degree-dependent bound quoted by Voutier.

Uses 1

Statement usesAlgebraic Mahler measure

TheoremStewart's lower bound for the Mahler measure#●ready to prove

Let \(\alpha\) be a nonzero complex number that is algebraic over \(\mathbb{Q}\) and is not a root of unity, and let \(d\) be the degree of its minimal polynomial over \(\mathbb{Q}\). If \(d \ge 2\), then the algebraic Mahler measure \(M(\alpha)\) satisfies \(M(\alpha) > 1 + \frac{1}{10000\, d \log d}\), with \(\log\) the natural logarithm.

theorem_wanted stewart_degreeBound (α : ℂ)
    (hα : IsAlgebraic ℚ α) (hα0 : α ≠ 0) (hroot : ¬IsOfFinOrder α)
    (hd : 2 ≤ (minpoly ℚ α).natDegree) :
    1 + 1 / (10000 * (minpoly ℚ α).natDegree * Real.log (minpoly ℚ α).natDegree) <
      algebraicMahlerMeasure α

Sources

• Stewart (1978), the strict degree-dependent bound quoted by Voutier.

Uses 1

Statement usesAlgebraic Mahler measure

11 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.