Absolute height and Mahler measure

DefinitionPrimitive integral minimal polynomial#✓fully proved

Let \(K\) be a field that is an algebra over \(\mathbb{Q}\), let \(x \in K\), and let \(m_x \in \mathbb{Q}[X]\) be the minimal polynomial of \(x\) over \(\mathbb{Q}\), with \(m_x = 0\) when \(x\) is not algebraic over \(\mathbb{Q}\). Choose a nonzero integer \(b\) such that \(b\,m_x\) has integer coefficients. The primitive integral minimal polynomial \(P_x \in \mathbb{Z}[X]\) of \(x\) is the primitive part of \(b\,m_x\): when \(b\,m_x \neq 0\) it is \(b\,m_x\) divided by the nonnegative greatest common divisor of its coefficients, and when \(b\,m_x = 0\) it is \(1\).

Thus for algebraic \(x\), \(P_x\) is a primitive polynomial with integer coefficients that is a nonzero rational multiple of \(m_x\), determined up to sign, and for nonalgebraic \(x\), \(P_x = 1\). The sign is immaterial for applications to Mahler measure.

noncomputable def primitiveIntMinpoly (x : K) : ℤ[X] :=
  (IsLocalization.integerNormalization (nonZeroDivisors ℤ) (minpoly ℚ x)).primPart

Used by 14

Used byAbsolute logarithmic height from the algebraic Mahler measure · Logarithmic height from the roots of the minimal polynomial, for an integral element · Logarithmic height from the roots of the minimal polynomial, for an algebraic element · Logarithmic height from the roots of the minimal polynomial · Absolute multiplicative height as a Mahler measure · Multiplicative height as a Mahler measure, for an integral element · The sign normalization does not change the Mahler measure · Positive primitive integral minimal polynomial · An algebraic element is a root of its positive primitive integral minimal polynomial · The positive primitive integral minimal polynomial is primitive · The positive primitive integral minimal polynomial has positive leading coefficient · Sign normalization preserves the degree · The positive primitive integral minimal polynomial has the degree of the minimal polynomial · The positive primitive integral minimal polynomial is nonzero

TheoremLogarithmic height from the roots of the minimal polynomial, for an integral element#✓fully proved

Let \(K\) be a field of characteristic zero and let \(x \in K\) be integral over \(\mathbb{Q}\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(P_x \in \mathbb{Z}[X]\) be the primitive integral minimal polynomial of \(x\), with leading coefficient \(a\). Then the absolute logarithmic height of \(x\) is

\[h(x) = \frac{1}{d}\Big(\log |a| + \sum_{z} \log^+ |z|\Big),\]

where the sum runs over the complex roots \(z\) of \(P_x\), counted with multiplicity, and \(\log^+ t = \max(0, \log t)\).

public theorem absLogHeight₁_eq_log_leadingCoeff_add_sum_log_roots_of_isIntegral
    {K : Type*} [Field K] [CharZero K] [Algebra ℚ K] (x : K) (hx : IsIntegral ℚ x) :
    NumberField.absLogHeight₁ x =
      (Real.log
          ‖((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).leadingCoeff‖ +
        (((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).roots.map
          (fun z => Real.posLog ‖z‖)).sum) /
        ((minpoly ℚ x).natDegree : ℝ)

Uses 1 · Used by 2

Statement usesPrimitive integral minimal polynomial

Used byLogarithmic height from the roots of the minimal polynomial, for an algebraic element · Logarithmic height from the roots of the minimal polynomial

TheoremLogarithmic height from the roots of the minimal polynomial, for an algebraic element#✓fully proved

Let \(K\) be a field of characteristic zero and let \(x \in K\) be algebraic over \(\mathbb{Q}\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(P_x \in \mathbb{Z}[X]\) be the primitive integral minimal polynomial of \(x\), with leading coefficient \(a\). Then the absolute logarithmic height of \(x\) is

\[h(x) = \frac{1}{d}\Big(\log |a| + \sum_{z} \log^+ |z|\Big),\]

where the sum runs over the complex roots \(z\) of \(P_x\), counted with multiplicity, and \(\log^+ t = \max(0, \log t)\).

public theorem absLogHeight₁_eq_log_leadingCoeff_add_sum_log_roots_of_isAlgebraic
    {K : Type*} [Field K] [CharZero K] [Algebra ℚ K] (x : K) (hx : IsAlgebraic ℚ x) :
    NumberField.absLogHeight₁ x =
      (Real.log
          ‖((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).leadingCoeff‖ +
        (((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).roots.map
          (fun z => Real.posLog ‖z‖)).sum) /
        ((minpoly ℚ x).natDegree : ℝ)

Uses 2

Statement usesPrimitive integral minimal polynomial

Proof usesLogarithmic height from the roots of the minimal polynomial, for an integral element

TheoremLogarithmic height from the roots of the minimal polynomial#✓fully proved

Let \(K\) be a field of characteristic zero that is algebraic over \(\mathbb{Q}\), and let \(x \in K\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(P_x \in \mathbb{Z}[X]\) be the primitive integral minimal polynomial of \(x\), with leading coefficient \(a\). Then the absolute logarithmic height of \(x\) is

\[h(x) = \frac{1}{d}\Big(\log |a| + \sum_{z} \log^+ |z|\Big),\]

where the sum runs over the complex roots \(z\) of \(P_x\), counted with multiplicity, and \(\log^+ t = \max(0, \log t)\).

public theorem absLogHeight₁_eq_log_leadingCoeff_add_sum_log_roots
    {K : Type*} [Field K] [CharZero K] [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K] (x : K) :
    NumberField.absLogHeight₁ x =
      (Real.log
          ‖((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).leadingCoeff‖ +
        (((NumberField.primitiveIntMinpoly x).map (Int.castRingHom ℂ)).roots.map
          (fun z => Real.posLog ‖z‖)).sum) /
        ((minpoly ℚ x).natDegree : ℝ)

Sources

• arXiv:2608.15903; equivalent formulas occur in arXiv:2304.11607, 2309.11173, 2311.13047, 2311.14001, 2607.25168, 2608.04445, and 2608.20995.

Uses 2

Statement usesPrimitive integral minimal polynomial

Proof usesLogarithmic height from the roots of the minimal polynomial, for an integral element

TheoremMultiplicative height as a Mahler measure, for an integral element#✓fully proved

Let \(K\) be a field of characteristic zero and let \(x \in K\) be integral over \(\mathbb{Q}\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(P_x \in \mathbb{Z}[X]\) be the primitive integral minimal polynomial of \(x\). Then the absolute multiplicative height of \(x\) is \(H(x) = M(P_x)^{1/d}\), where \(M(P_x)\) is the Mahler measure of \(P_x\) regarded as a polynomial with complex coefficients.

public theorem absMulHeight₁_eq_mapMahlerMeasure_of_isIntegral
    {K : Type*} [Field K] [CharZero K] [Algebra ℚ K] (x : K) (hx : IsIntegral ℚ x) :
    NumberField.absMulHeight₁ x =
      (NumberField.primitiveIntMinpoly x).mapMahlerMeasure (Int.castRingHom ℂ) ^
        ((minpoly ℚ x).natDegree : ℝ)⁻¹

Uses 1 · Used by 2

Statement usesPrimitive integral minimal polynomial

Used byAbsolute logarithmic height from the algebraic Mahler measure · Absolute multiplicative height as a Mahler measure

TheoremAbsolute multiplicative height as a Mahler measure#✓fully proved

Let \(K\) be a field of characteristic zero that is algebraic over \(\mathbb{Q}\), and let \(x \in K\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(P_x \in \mathbb{Z}[X]\) be the primitive integral minimal polynomial of \(x\). Then the absolute multiplicative height of \(x\) is \(H(x) = M(P_x)^{1/d}\), where \(M(P_x)\) is the Mahler measure of \(P_x\) regarded as a polynomial with complex coefficients.

public theorem absMulHeight₁_eq_mapMahlerMeasure {K : Type*} [Field K] [CharZero K]
    [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K] (x : K) :
    NumberField.absMulHeight₁ x =
      (NumberField.primitiveIntMinpoly x).mapMahlerMeasure (Int.castRingHom ℂ) ^
        ((minpoly ℚ x).natDegree : ℝ)⁻¹

Sources

• arXiv:2608.15891, lines 205–217; equivalent formulations also occur in arXiv:2306.11331, 2307.11849, 2307.14915, 2312.04354, 2607.28857, 2607.29208, and 2608.11904.

Uses 2

Statement usesPrimitive integral minimal polynomial

Proof usesMultiplicative height as a Mahler measure, for an integral element

DefinitionPositive primitive integral minimal polynomial#✓fully proved

Let \(K\) be a field that is a \(\mathbb{Q}\)-algebra, let \(x \in K\), and let \(p\) be the canonical primitive integral minimal polynomial of \(x\). The positive primitive integral minimal polynomial of \(x\) is \(-p\) if the leading coefficient of \(p\) is negative, and \(p\) otherwise.

Since \(p\) is nonzero, the result has positive leading coefficient. When \(x\) is not algebraic over \(\mathbb{Q}\), \(p\) is the constant polynomial \(1\), and so is the result.

noncomputable def positivePrimitiveIntMinpoly (x : K) : Polynomial ℤ :=
  let p := primitiveIntMinpoly x
  if p.leadingCoeff < 0 then -p else p

Uses 1 · Used by 8

Statement usesPrimitive integral minimal polynomial

Used byAlgebraic Mahler measure · The algebraic Mahler measure is at least one · An algebraic element is a root of its positive primitive integral minimal polynomial · The positive primitive integral minimal polynomial is primitive · The positive primitive integral minimal polynomial has positive leading coefficient · Sign normalization preserves the degree · The positive primitive integral minimal polynomial has the degree of the minimal polynomial · The positive primitive integral minimal polynomial is nonzero

TheoremThe positive primitive integral minimal polynomial is primitive#✓fully proved

For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the positive primitive integral minimal polynomial of \(x\) is primitive: the greatest common divisor of its integer coefficients is \(1\).

theorem positivePrimitiveIntMinpoly_isPrimitive (x : K) :
    (positivePrimitiveIntMinpoly x).IsPrimitive

Uses 2

Statement usesPositive primitive integral minimal polynomial

Proof usesPrimitive integral minimal polynomial

TheoremThe positive primitive integral minimal polynomial is nonzero#✓fully proved

Let \(K\) be a field that is a \(\mathbb{Q}\)-algebra. For every \(x \in K\), the positive primitive integral minimal polynomial of \(x\) is not the zero polynomial.

theorem positivePrimitiveIntMinpoly_ne_zero (x : K) :
    positivePrimitiveIntMinpoly x ≠ 0

Uses 2

Statement usesPositive primitive integral minimal polynomial

Proof usesPrimitive integral minimal polynomial

TheoremThe positive primitive integral minimal polynomial has positive leading coefficient#✓fully proved

For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the leading coefficient of the positive primitive integral minimal polynomial of \(x\) is a strictly positive integer.

theorem positivePrimitiveIntMinpoly_leadingCoeff_pos (x : K) :
    0 < (positivePrimitiveIntMinpoly x).leadingCoeff

Uses 2 · Used by 1

Statement usesPositive primitive integral minimal polynomial

Proof usesPrimitive integral minimal polynomial

Used byThe algebraic Mahler measure is at least one

TheoremSign normalization preserves the degree#✓fully proved

For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the positive primitive integral minimal polynomial of \(x\) has the same degree as the primitive integral minimal polynomial of \(x\).

theorem positivePrimitiveIntMinpoly_natDegree (x : K) :
    (positivePrimitiveIntMinpoly x).natDegree = (primitiveIntMinpoly x).natDegree

Uses 2 · Used by 1

Statement usesPositive primitive integral minimal polynomial · Primitive integral minimal polynomial

Used byThe positive primitive integral minimal polynomial has the degree of the minimal polynomial

TheoremThe positive primitive integral minimal polynomial has the degree of the minimal polynomial#✓fully proved

The positive primitive integral minimal polynomial has the degree of the minimal polynomial. For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the positive primitive integral minimal polynomial of \(x\) has the same degree as the minimal polynomial of \(x\) over \(\mathbb{Q}\).

Degrees are natural numbers, the zero polynomial having degree \(0\); if \(x\) is not algebraic over \(\mathbb{Q}\), both degrees are \(0\).

theorem positivePrimitiveIntMinpoly_natDegree_eq (x : K) :
    (positivePrimitiveIntMinpoly x).natDegree = (minpoly ℚ x).natDegree

Uses 3

Statement usesPositive primitive integral minimal polynomial

Proof usesSign normalization preserves the degree · Primitive integral minimal polynomial

TheoremAn algebraic element is a root of its positive primitive integral minimal polynomial#✓fully proved

Let \(K\) be a field of characteristic zero that is an algebra over \(\mathbb{Q}\), and let \(x \in K\) be algebraic over \(\mathbb{Q}\). Then the positive primitive integral minimal polynomial of \(x\), with its integer coefficients mapped into \(K\), vanishes at \(x\).

theorem positivePrimitiveIntMinpoly_eval₂_at [CharZero K] (x : K) (hx : IsAlgebraic ℚ x) :
    Polynomial.eval₂ (Int.castRingHom K) x (positivePrimitiveIntMinpoly x) = 0

Uses 2

Statement usesPositive primitive integral minimal polynomial

Proof usesPrimitive integral minimal polynomial

DefinitionAlgebraic Mahler measure#✓fully proved

For an element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the algebraic Mahler measure \(M(x)\) is the Mahler measure of the positive primitive integral minimal polynomial of \(x\), regarded as a polynomial with complex coefficients. If \(x\) is not algebraic over \(\mathbb{Q}\), this polynomial is the constant \(1\), so \(M(x) = 1\).

noncomputable def algebraicMahlerMeasure (x : K) : ℝ :=
  (positivePrimitiveIntMinpoly x).mapMahlerMeasure (Int.castRingHom ℂ)

Uses 1 · Used by 10

Statement usesPositive primitive integral minimal polynomial

Used byAbsolute logarithmic height from the algebraic Mahler measure · The sign normalization does not change the Mahler measure · One plus the logarithm of a Mahler measure above one is below it · The algebraic Mahler measure is at least one · Blanksby–Montgomery lower bound for the Mahler measure · Asymptotic Dobrowolski coefficients · Coefficients are exactly the reals below the constant · Strict form of asymptotic Dobrowolski coefficients · Stewart's lower bound for the Mahler measure · Zero is an asymptotic Dobrowolski coefficient

TheoremThe sign normalization does not change the Mahler measure#✓fully proved

For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the algebraic Mahler measure of \(x\), that is the Mahler measure of the positive primitive integral minimal polynomial of \(x\), equals the Mahler measure of the primitive integral minimal polynomial of \(x\), both polynomials being regarded as polynomials with complex coefficients.

theorem algebraicMahlerMeasure_eq (x : K) :
    algebraicMahlerMeasure x = (primitiveIntMinpoly x).mapMahlerMeasure (Int.castRingHom ℂ)

Uses 2 · Used by 1

Statement usesAlgebraic Mahler measure · Primitive integral minimal polynomial

Used byAbsolute logarithmic height from the algebraic Mahler measure

TheoremThe algebraic Mahler measure is at least one#✓fully proved

For every element \(x\) of a field \(K\) that is an algebra over \(\mathbb{Q}\), the algebraic Mahler measure \(M(x)\) of \(x\) satisfies \(1 \le M(x)\).

This holds because the positive primitive integral minimal polynomial of \(x\) has a positive integer leading coefficient.

theorem one_le_algebraicMahlerMeasure (x : K) : 1 ≤ algebraicMahlerMeasure x

Uses 3 · Used by 2

Statement usesAlgebraic Mahler measure

Proof usesPositive primitive integral minimal polynomial · The positive primitive integral minimal polynomial has positive leading coefficient

Used byAbsolute logarithmic height from the algebraic Mahler measure · Zero is an asymptotic Dobrowolski coefficient

TheoremAbsolute logarithmic height from the algebraic Mahler measure#✓fully proved

Let \(K\) be a field of characteristic zero that is an algebra over \(\mathbb{Q}\), and let \(x \in K\) be algebraic over \(\mathbb{Q}\). Let \(d\) be the degree of the minimal polynomial of \(x\) over \(\mathbb{Q}\), and let \(M(x)\) be the algebraic Mahler measure of \(x\), the Mahler measure of the positive primitive integral minimal polynomial of \(x\) regarded as a complex polynomial. Then the absolute logarithmic height of \(x\) equals \(\log M(x) / d\).

theorem absLogHeight₁_eq_log_algebraicMahlerMeasure [CharZero K]
    (x : K) (hx : IsAlgebraic ℚ x) :
    absLogHeight₁ x = Real.log (algebraicMahlerMeasure x) / (minpoly ℚ x).natDegree

Uses 5

Statement usesAlgebraic Mahler measure

Proof usesMultiplicative height as a Mahler measure, for an integral element · The sign normalization does not change the Mahler measure · The algebraic Mahler measure is at least one · Primitive integral minimal polynomial

TheoremOne plus the logarithm of a Mahler measure above one is below it#✓fully proved

Let \(x\) be an element of a field \(K\) that is an algebra over \(\mathbb{Q}\), and let \(M(x)\) be its algebraic Mahler measure. If \(M(x) > 1\), then \(1 + \log M(x) < M(x)\).

Voutier uses this elementary inequality to pass from lower bounds for \(\log M(x)\) to lower bounds for \(M(x)\).

theorem log_algebraicMahlerMeasure_add_one_lt (x : K) (hM : 1 < algebraicMahlerMeasure x) :
    1 + Real.log (algebraicMahlerMeasure x) < algebraicMahlerMeasure x

Uses 1

Statement usesAlgebraic Mahler measure

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.