The absolute height and the Mahler measure

For an algebraic number x of degree d, the Mahler measure and the absolute multiplicative Weil height are related by M(x) = H(x) ^ d, equivalently log M(x) = d · h(x). This file proves this identity for elements of an arbitrary field of characteristic zero; at transcendental elements both sides are the junk value 1.

As a consequence, Northcott's theorem for the Mahler measure gives bounded-degree Northcott finiteness for the absolute height: in any field of characteristic zero there are only finitely many algebraic elements of bounded degree and bounded absolute height. The field is not required to be a number field, so this applies in ℂ or in an algebraic closure of ℚ.

Main results

• TauCeti.mahlerMeasure_eq_absMulHeight₁_pow: M(x) = H(x) ^ d.
• TauCeti.log_mahlerMeasure_eq_mul_absLogHeight₁: log M(x) = d · h(x).
• TauCeti.mahlerMeasure_inv: M(x⁻¹) = M(x).
• TauCeti.finite_setOf_absMulHeight₁_le: finiteness of the set of algebraic elements of degree at most d and absolute height at most B.

Implementation notes

The proof averages the relative height over the conjugates. Let L be a number field in which minpoly ℚ x splits, let D = [L : ℚ], and let a₀ be the leading coefficient of the primitive minimal polynomial F_x = a₀ ∏ (X - xᵢ) over L. Every conjugate xᵢ ∈ L has relative height H_L(xᵢ) = H(x) ^ D, so the product of these d heights is H(x) ^ (D d). Computing the same product place by place:

• at an infinite place, the conjugates are carried bijectively onto the complex roots of minpoly ℚ x, so each place contributes ∏ᵢ max(1, |xᵢ|) = M(x) / a₀, with multiplicity;
• at a finite place w, Gauss's lemma for the primitive polynomial F_x gives w(a₀) ∏ᵢ max(1, w(xᵢ)) = 1;
• by the product formula the finite-place values of a₀ multiply to a₀ ^ (-D).

Together the product is M(x) ^ D, and taking D-th roots gives the identity. The theorem uses the splitting field of minpoly ℚ x as L.

References

• C. Smyth, The Mahler measure of algebraic numbers: a survey (2008), §1.
• X. Wu, Diophantine geometry, week 08: arithmetic heights (2023), §3, Lemma 3.1, Proposition 3.1 and Theorem 3.4.

theorem TauCeti.mahlerMeasure_eq_absMulHeight₁_pow {F : Type u_1} [Field F] [CharZero F] (x : F) : mahlerMeasure x = NumberField.absMulHeight₁ x ^ (minpoly ℚ x).natDegree

Mahler measure and absolute height. For every element x of a field of characteristic zero, M(x) = H(x) ^ d with d = deg x, the degree of minpoly ℚ x. For transcendental x this reads 1 = 1 ^ 0.

theorem TauCeti.log_mahlerMeasure_eq_mul_absLogHeight₁ {F : Type u_1} [Field F] [CharZero F] (x : F) : Real.log (mahlerMeasure x) = ↑(minpoly ℚ x).natDegree * NumberField.absLogHeight₁ x

The logarithmic form of mahlerMeasure_eq_absMulHeight₁_pow: log M(x) = d · h(x) with d = deg x.

@[simp]

theorem TauCeti.mahlerMeasure_inv {F : Type u_1} [Field F] [CharZero F] (x : F) : mahlerMeasure x⁻¹ = mahlerMeasure x

Mahler measure of an inverse. M(x⁻¹) = M(x) for every element x of a field of characteristic zero. For x = 0 this reads M(0) = M(0), since 0⁻¹ = 0.

theorem TauCeti.finite_setOf_absMulHeight₁_le {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) : {x : F | IsAlgebraic ℚ x ∧ (minpoly ℚ x).natDegree ≤ d ∧ NumberField.absMulHeight₁ x ≤ B}.Finite

Northcott's theorem for the absolute height. In a field of characteristic zero there are only finitely many algebraic elements of degree at most d and absolute height at most B.