The Mahler measure of an algebraic number

For an element x of a field of characteristic zero, the Mahler measure M(x) is the Mahler measure of its primitive minimal polynomial F_x ∈ ℤ[X], mapped to ℂ[X]. For algebraic x of degree d with conjugates x⁽¹⁾, …, x⁽ᵈ⁾ ∈ ℂ this is M(x) = a₀ ∏ᵢ max(1, |x⁽ⁱ⁾|): the positive integer leading coefficient a₀ of F_x times the product of max(1, |x⁽ⁱ⁾|) over the conjugates. Keeping the leading coefficient gives M(p/q) = max(|p|, q) for a rational number in lowest terms. For transcendental x the value is 1.

The definition needs no complex embedding of the ambient field: only the polynomial F_x is mapped to ℂ. Consequently M(x) is constant on conjugacy classes and invariant under field embeddings. Together with the naive and absolute heights, the Mahler measure is one of the classical size functions on algebraic numbers used in Liouville- and Roth-type approximation estimates and in Northcott finiteness.

Main definitions

• TauCeti.mahlerMeasure x: the Mahler measure of x.

Main results

• TauCeti.mahlerMeasure_eq_leadingCoeff_mul_prod: M(x) = a₀ ∏ max(1, |z|) over the complex roots z of minpoly ℚ x, counted with multiplicity.
• TauCeti.leadingCoeff_le_mahlerMeasure, TauCeti.one_le_mahlerMeasure: 1 ≤ a₀ ≤ M(x).
• TauCeti.mahlerMeasure_ratCast: M(p/q) = max(|p|, q), the multiplicative height of p/q.
• TauCeti.mahlerMeasure_map, TauCeti.mahlerMeasure_eq_of_minpoly_eq: invariance under field embeddings and conjugation.
• TauCeti.mahlerMeasure_eq_one_iff: Kronecker's theorem, for algebraic x, M(x) = 1 exactly when x is zero or a root of unity.
• TauCeti.finite_setOf_mahlerMeasure_le: Northcott's theorem for the Mahler measure; in every field of characteristic zero there are only finitely many algebraic elements of bounded degree and bounded Mahler measure.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, §6.1 and Theorem 6.1.
• C. Smyth, The Mahler measure of algebraic numbers: a survey (2008), §1.

noncomputable def TauCeti.mahlerMeasure {F : Type u_1} [Field F] [CharZero F] (x : F) : ℝ

The Mahler measure M(x) of x: the Mahler measure of its primitive minimal polynomial F_x, mapped to ℂ[X]. For algebraic x this is a₀ ∏ max(1, |x⁽ⁱ⁾|) over the complex conjugates of x (mahlerMeasure_eq_leadingCoeff_mul_prod); for transcendental x it is 1.

theorem TauCeti.mahlerMeasure_def {F : Type u_1} [Field F] [CharZero F] (x : F) : mahlerMeasure x = (Polynomial.map (Int.castRingHom ℂ) (primitiveMinpoly x)).mahlerMeasure

The Mahler measure of x is the Mahler measure of F_x mapped to ℂ[X].

theorem TauCeti.mahlerMeasure_eq_of_minpoly_eq {F : Type u_1} [Field F] [CharZero F] {F' : Type u_2} [Field F'] [CharZero F'] {x : F} {y : F'} (h : minpoly ℚ x = minpoly ℚ y) : mahlerMeasure x = mahlerMeasure y

The Mahler measure depends only on minpoly ℚ x: conjugates, possibly lying in different fields, have equal Mahler measure.

@[simp]

theorem TauCeti.mahlerMeasure_map {F : Type u_1} [Field F] [CharZero F] {F' : Type u_2} [Field F'] [CharZero F'] (f : F →+* F') (x : F) : mahlerMeasure (f x) = mahlerMeasure x

Field embeddings preserve the Mahler measure.

@[simp]

theorem TauCeti.mahlerMeasure_of_not_isAlgebraic {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : ¬IsAlgebraic ℚ x) : mahlerMeasure x = 1

Transcendental elements have Mahler measure 1.

theorem TauCeti.mahlerMeasure_eq_leadingCoeff_mul_prod {F : Type u_1} [Field F] [CharZero F] (x : F) : mahlerMeasure x = ↑(primitiveMinpoly x).leadingCoeff * (Multiset.map (fun (z : ℂ) => max 1 ‖z‖) ((minpoly ℚ x).aroots ℂ)).prod

The Mahler measure of x is a₀ ∏ max(1, |z|), the product running over the complex roots z of minpoly ℚ x counted with multiplicity, where a₀ is the leading coefficient of F_x. For transcendental x both sides are 1.

theorem TauCeti.leadingCoeff_le_mahlerMeasure {F : Type u_1} [Field F] [CharZero F] (x : F) : ↑(primitiveMinpoly x).leadingCoeff ≤ mahlerMeasure x

The leading coefficient a₀ of F_x is at most the Mahler measure of x.

theorem TauCeti.one_le_mahlerMeasure {F : Type u_1} [Field F] [CharZero F] (x : F) : 1 ≤ mahlerMeasure x

The Mahler measure of every element is at least 1.

@[simp]

theorem TauCeti.mahlerMeasure_ratCast {F : Type u_1} [Field F] [CharZero F] (q : ℚ) : mahlerMeasure ↑q = max ↑q.num.natAbs ↑q.den

The Mahler measure of a rational number q is the maximum of the absolute value of its numerator and its denominator, independently of the field containing q.

theorem TauCeti.mahlerMeasure_ratCast_eq_mulHeight₁ {F : Type u_1} [Field F] [CharZero F] (q : ℚ) : mahlerMeasure ↑q = Height.mulHeight₁ q

On rational numbers the Mahler measure is the multiplicative Weil height.

@[simp]

theorem TauCeti.mahlerMeasure_zero {F : Type u_1} [Field F] [CharZero F] : mahlerMeasure 0 = 1

The Mahler measure of 0 is 1.

@[simp]

theorem TauCeti.mahlerMeasure_one {F : Type u_1} [Field F] [CharZero F] : mahlerMeasure 1 = 1

The Mahler measure of 1 is 1.

theorem TauCeti.mahlerMeasure_eq_one_iff {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsAlgebraic ℚ x) : mahlerMeasure x = 1 ↔ x = 0 ∨ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Kronecker's theorem. An algebraic element has Mahler measure 1 exactly when it is zero or a root of unity.

theorem TauCeti.finite_setOf_mahlerMeasure_le {F : Type u_1} [Field F] [CharZero F] (d : ℕ) (B : ℝ) : {z : F | IsAlgebraic ℚ z ∧ (minpoly ℚ z).natDegree ≤ d ∧ mahlerMeasure z ≤ B}.Finite

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

Examples