Heights and Mahler measure

Absolute heights of algebraic numbers, Mahler measure, Lehmer's problem, Dobrowolski bounds, Schinzel–Zassenhaus, house and trace problems.

• Absolute height and Mahler measure
• Asymptotic Dobrowolski constant
• Cyclotomic integers of small house
• Lehmer's Mahler measure problem
• Multivariable Mahler measure
• Pisot numbers
• Schur–Siegel–Smyth trace problem

TheoremDimitrov's lower bound for the house of an algebraic integer#●ready to prove

Let \(K\) be a number field and let \(\alpha \in K\) be a nonzero algebraic integer that is not a root of unity. Let \(d'\) be the number of distinct values of the argument \(\arg \sigma(\alpha)\) as \(\sigma\) ranges over the ring homomorphisms \(K \to \mathbb{C}\). Then the house of \(\alpha\), the maximum of \(|\sigma(\alpha)|\) over these \(\sigma\), is at least \(2^{1/(4d')}\).

public theorem_wanted dimitrov {K : Type*} [Field K] [NumberField K]
    (α : K)
    (α_int : IsIntegral ℤ α)
    (α_ne_zero : α ≠ 0)
    (α_not_rootOfUnity : ¬ IsOfFinOrder α) :
    (2 : ℝ) ^ (1 / (4 * (Finset.univ.image fun σ : K →+* ℂ ↦ (σ α).arg).card) : ℝ) ≤
      NumberField.house α

Sources

• James McKee and Chris Smyth, Around the Unit Circle, Chapter 4, Theorem 4.1; Vesselin Dimitrov (2019). Problem dimitrov of the lean-eval benchmark.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.