Lehmer's Mahler measure problem

DefinitionMahler measure of an integer polynomial#✓fully proved

The Mahler measure of \(f \in \mathbb{Z}[X]\) is the Mahler measure of its image in \(\mathbb{C}[X]\). It equals \(|a| \prod_i \max(1, |\alpha_i|)\), where \(a\) is the leading coefficient of \(f\) and the \(\alpha_i\) are the complex roots of \(f\) counted with multiplicity.

noncomputable def intMahlerMeasure (f : Polynomial ℤ) : ℝ :=
  f.mapMahlerMeasure (Int.castRingHom ℂ)

Used by 12

Used byMahler measure of Lehmer's polynomial · Mahler measure of a monic linear integer polynomial · Mahler measure of \(X - 1\) · Mahler measure of \(X - 2\) · Lehmer's question in terms of Lehmer's constant · Lehmer's constant bounds every Mahler measure above \(1\) · Lehmer's constant is at most \(2\) · Lehmer's question · Mahler measures above one · Nonzero integer polynomials have Mahler measure at least one · Lehmer's constant is at least one · Smyth's theorem for nonreciprocal polynomials

TheoremNonzero integer polynomials have Mahler measure at least one#✓fully proved

If \(f \in \mathbb{Z}[X]\) is a nonzero polynomial, then its Mahler measure satisfies \(M(f) \ge 1\).

Indeed, \(M(f) = |a| \prod_i \max(1, |\alpha_i|)\), where the leading coefficient \(a\) of \(f\) is a nonzero integer and the \(\alpha_i\) are the complex roots of \(f\) counted with multiplicity, so every factor is at least \(1\).

theorem one_le_intMahlerMeasure {f : Polynomial ℤ} (hf : f ≠ 0) :
    1 ≤ intMahlerMeasure f

Uses 1

Statement usesMahler measure of an integer polynomial

TheoremMahler measure of a monic linear integer polynomial#✓fully proved

For every integer \(a\), the Mahler measure of the integer polynomial \(X - a\) is \(\max(1, |a|)\).

theorem intMahlerMeasure_X_sub_C (a : ℤ) :
    intMahlerMeasure (X - C a) = max 1 ‖(a : ℝ)‖

Uses 1 · Used by 2

Statement usesMahler measure of an integer polynomial

Used byMahler measure of \(X - 1\) · Mahler measure of \(X - 2\)

TheoremMahler measure of \(X - 1\)#✓fully proved

The integer polynomial \(X - 1\) has Mahler measure \(1\).

Since \(1\) is not strictly larger than \(1\), this value is excluded from the set whose infimum is Lehmer's constant.

theorem intMahlerMeasure_X_sub_one :
    intMahlerMeasure (X - C (1 : ℤ)) = 1

Uses 2

Statement usesMahler measure of an integer polynomial

Proof usesMahler measure of a monic linear integer polynomial

TheoremMahler measure of \(X - 2\)#✓fully proved

The integer polynomial \(X - 2\) has Mahler measure \(2\).

Since \(2 > 1\), this value lies in the set whose infimum is Lehmer's constant.

theorem intMahlerMeasure_X_sub_two :
    intMahlerMeasure (X - C (2 : ℤ)) = 2

Uses 2 · Used by 3

Statement usesMahler measure of an integer polynomial

Proof usesMahler measure of a monic linear integer polynomial

Used byLehmer's question in terms of Lehmer's constant · Lehmer's constant is at most \(2\) · Lehmer's constant is at least one

DefinitionMahler measures above one#✓fully proved

This is the set of real numbers of the form \(M(f)\), where \(f \in \mathbb{Z}[X]\) is an integer polynomial whose Mahler measure \(M(f)\) is strictly larger than \(1\).

def mahlerMeasuresAboveOne : Set ℝ :=
  {y | ∃ f : Polynomial ℤ, 1 < intMahlerMeasure f ∧ y = intMahlerMeasure f}

Uses 1 · Used by 4

Statement usesMahler measure of an integer polynomial

Used byLehmer's constant · Lehmer's question in terms of Lehmer's constant · Lehmer's constant bounds every Mahler measure above \(1\) · Lehmer's constant is at least one

DefinitionLehmer's constant#✓fully proved

Writing \(M(f)\) for the Mahler measure of an integer polynomial \(f\), Lehmer's constant is \(C_{40a} = \inf \{M(f) : f \in \mathbb{Z}[X],\ M(f) > 1\}\), the infimum of the Mahler measures of integer polynomials that are strictly larger than \(1\).

noncomputable def lehmerConstant : ℝ :=
  sInf mahlerMeasuresAboveOne

Uses 1 · Used by 5

Statement usesMahler measures above one

Used byLehmer's question in terms of Lehmer's constant · Lehmer's constant bounds every Mahler measure above \(1\) · Lehmer's constant is at most \(2\) · Lehmer's upper bound for Lehmer's constant · Lehmer's constant is at least one

TheoremLehmer's constant bounds every Mahler measure above \(1\)#✓fully proved

For every integer polynomial \(f\) whose Mahler measure is strictly larger than \(1\), Lehmer's constant is at most the Mahler measure of \(f\).

theorem lehmerConstant_le_intMahlerMeasure {f : Polynomial ℤ}
    (hf : 1 < intMahlerMeasure f) : lehmerConstant ≤ intMahlerMeasure f

Uses 3 · Used by 2

Statement usesMahler measure of an integer polynomial · Lehmer's constant

Proof usesMahler measures above one

Used byLehmer's question in terms of Lehmer's constant · Lehmer's constant is at most \(2\)

TheoremLehmer's constant is at least one#✓fully proved

Lehmer's constant \(L\), the infimum of the Mahler measures strictly larger than \(1\) of polynomials in \(\mathbb{Z}[X]\), satisfies \(1 \le L\).

This is the lower bound recorded in the catalogue for the constant \(C_{40a}\).

theorem one_le_lehmerConstant : 1 ≤ lehmerConstant

Uses 4 · Used by 1

Statement usesLehmer's constant

Proof usesMahler measure of an integer polynomial · Mahler measure of \(X - 2\) · Mahler measures above one

Used byLehmer's question in terms of Lehmer's constant

TheoremLehmer's constant is at most \(2\)#✓fully proved

Lehmer's constant \(C_{40a}\) satisfies \(C_{40a} \le 2\).

The witness is the integer polynomial \(X - 2\), whose Mahler measure is \(2\).

theorem lehmerConstant_le_two : lehmerConstant ≤ 2

Uses 4

Statement usesLehmer's constant

Proof usesMahler measure of an integer polynomial · Mahler measure of \(X - 2\) · Lehmer's constant bounds every Mahler measure above \(1\)

DefinitionLehmer's question#✓fully proved

The proposition that there are integer polynomials with Mahler measure arbitrarily close to \(1\) from above: for every real \(\varepsilon > 0\) there is a polynomial \(f \in \mathbb{Z}[X]\) whose Mahler measure \(M(f)\) satisfies \(1 < M(f) < 1 + \varepsilon\).

Lehmer asked in 1933 whether this proposition holds.

def LehmerQuestion : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ f : Polynomial ℤ,
    1 < intMahlerMeasure f ∧ intMahlerMeasure f < 1 + ε

Uses 1 · Used by 1

Statement usesMahler measure of an integer polynomial

Used byLehmer's question in terms of Lehmer's constant

TheoremLehmer's question in terms of Lehmer's constant#✓fully proved

Lehmer's constant equals \(1\) if and only if Lehmer's question has a positive answer, that is, for every \(\varepsilon > 0\) there is an integer polynomial whose Mahler measure lies strictly between \(1\) and \(1 + \varepsilon\).

theorem lehmerConstant_eq_one_iff : lehmerConstant = 1 ↔ LehmerQuestion

Uses 7

Statement usesLehmer's question · Lehmer's constant

Proof usesMahler measure of an integer polynomial · Mahler measure of \(X - 2\) · Lehmer's constant bounds every Mahler measure above \(1\) · Mahler measures above one · Lehmer's constant is at least one

DefinitionLehmer's polynomial#✓fully proved

Lehmer's polynomial is the integer polynomial \(X^{10} + X^9 - X^7 - X^6 - X^5 - X^4 - X^3 + X + 1\).

Lehmer found it in 1933. Its Mahler measure \(1.176280\ldots\) is still the smallest known Mahler measure larger than \(1\).

noncomputable def lehmerPolynomial : Polynomial ℤ :=
  X ^ 10 + X ^ 9 - X ^ 7 - X ^ 6 - X ^ 5 - X ^ 4 - X ^ 3 + X + 1

Used by 1

Used byMahler measure of Lehmer's polynomial

DefinitionSmyth's polynomial#✓fully proved

Smyth's polynomial is \(X^3 - X - 1 \in \mathbb{Z}[X]\).

Its Mahler measure is the plastic number \(\theta_0 = 1.324717\ldots\), the real root of \(X^3 - X - 1\). Smyth proved in 1971 that every polynomial \(f \in \mathbb{Z}[X]\) with \(f(0) \neq 0\) that is nonreciprocal (reversing its coefficients gives neither \(f\) nor \(-f\)) has Mahler measure at least \(\theta_0\).

noncomputable def smythPolynomial : Polynomial ℤ :=
  X ^ 3 - X - 1

Used by 1

Used bySmyth's theorem for nonreciprocal polynomials

DefinitionReciprocal polynomial#✓fully proved

An integer polynomial \(f\) is reciprocal when reversing its coefficients gives \(f\) or \(-f\), that is, when \(X^d f(1/X) = f\) or \(X^d f(1/X) = -f\), where \(d\) is the degree of \(f\), taken to be \(0\) when \(f = 0\).

def IsReciprocal (f : Polynomial ℤ) : Prop :=
  f.reverse = f ∨ f.reverse = -f

Used by 1

Used bySmyth's theorem for nonreciprocal polynomials

TheoremMahler measure of Lehmer's polynomial#●ready to prove

The Mahler measure of Lehmer's polynomial is at most \(1176281/1000000 = 1.176281\).

theorem_wanted intMahlerMeasure_lehmerPolynomial_le :
    intMahlerMeasure lehmerPolynomial ≤ 1176281 / 1000000

Sources

• Lehmer (1933), the Mahler measure of Lehmer's polynomial is 1.176280818..., hence at most 1.176281. No root-location computation for the degree-ten example is formalized here.

Uses 2

Statement usesMahler measure of an integer polynomial · Lehmer's polynomial

TheoremLehmer's upper bound for Lehmer's constant#●ready to prove

Lehmer's constant is at most \(1176281/1000000 = 1.176281\).

theorem_wanted lehmer1933UpperBound_wanted :
    lehmerConstant ≤ 1176281 / 1000000

Sources

• Lehmer (1933), catalogue upper bound C₄₀ₐ ≤ 1.176280... from the Mahler measure of Lehmer's polynomial, rounded up at the sixth decimal place.

Uses 1

Statement usesLehmer's constant

TheoremSmyth's theorem for nonreciprocal polynomials#●ready to prove

Let \(f \in \mathbb{Z}[X]\) be an integer polynomial that is not reciprocal and whose constant term \(f(0)\) is nonzero. Then the Mahler measure of \(f\) is at least the Mahler measure of Smyth's polynomial \(X^3 - X - 1\).

theorem_wanted smyth1971Nonreciprocal_wanted (f : Polynomial ℤ)
    (hf : ¬ IsReciprocal f) (hf0 : Polynomial.eval 0 f ≠ 0) :
    intMahlerMeasure smythPolynomial ≤ intMahlerMeasure f

Sources

• Smyth (1971), as quoted in the catalogue: a nonreciprocal integer polynomial with nonzero constant term has Mahler measure at least that of X^3 - X - 1 (the plastic number 1.324717...).

Uses 3

Statement usesReciprocal polynomial · Mahler measure of an integer polynomial · Smyth's polynomial

15 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.