Mahler measure of integer polynomials

The main purpose of this file is to prove some facts about the Mahler measure of integer polynomials, in particular Northcott's Theorem for the Mahler measure.

Main results

• Polynomial.finite_mahlerMeasure_le: Northcott's Theorem: the set of integer polynomials of degree at most n and Mahler measure at most B is finite.
• Polynomial.card_mahlerMeasure_le_prod: an upper bound on the number of integer polynomials of degree at most n and Mahler measure at most B.
• Polynomial.cyclotomic_mahlerMeasure_eq_one: the Mahler measure of a cyclotomic polynomial is 1.
• Polynomial.pow_eq_one_of_mahlerMeasure_eq_one: if an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are roots of unity.
• Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_one: if an integer non-constant polynomial has Mahler measure equal to 1 and is not a multiple of X, then it is divisible by a cyclotomic polynomial.

theorem Polynomial.one_le_mahlerMeasure_of_ne_zero {p : Polynomial ℤ} (hp : p ≠ 0) : 1 ≤ (map (Int.castRingHom ℂ) p).mahlerMeasure

def Polynomial.boxPoly (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ) : Set (Polynomial ℤ)

The set of polynomials whose coefficients are bounded between B₁ and B₂. This construction is used as part of our proof of Northcott's theorem.

Equations

• Polynomial.boxPoly n B₁ B₂ = {p : Polynomial ℤ | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), B₁ i ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ B₂ i}

theorem Polynomial.ncard_boxPoly (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ) : (boxPoly n B₁ B₂).ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

@[deprecated Polynomial.ncard_boxPoly (since := "2026-02-02")]

theorem Polynomial.card_eq_of_natDegree_le_of_coeff_le (n : ℕ) (B₁ B₂ : Fin (n + 1) → ℝ) : (boxPoly n B₁ B₂).ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Alias of Polynomial.ncard_boxPoly.

theorem Polynomial.finite_mahlerMeasure_le (n : ℕ) (B : NNReal) : {p : Polynomial ℤ | p.natDegree ≤ n ∧ (map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite

Northcott's Theorem: the set of integer polynomials of degree at most n and Mahler measure at most B is finite.

theorem Polynomial.card_mahlerMeasure_le_prod (n : ℕ) (B : NNReal) : {p : Polynomial ℤ | p.natDegree ≤ n ∧ (map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i : Fin (n + 1), (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

An upper bound on the number of integer polynomials of degree at most n and Mahler measure at most B.

theorem Polynomial.cyclotomic_mahlerMeasure_eq_one {R : Type u_1} [CommRing R] [Algebra R ℂ] (n : ℕ) : (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

The Mahler measure of a cyclotomic polynomial is 1.

theorem Polynomial.norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) : ‖(map (Int.castRingHom ℂ) p).leadingCoeff‖ = 1

theorem Polynomial.abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) : |p.leadingCoeff| = 1

theorem Polynomial.isIntegral_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) {z : ℂ} (hz : z ∈ p.aroots ℂ) : IsIntegral ℤ z

If an integer polynomial has Mahler measure equal to 1, then all its complex roots are integral over ℤ.

theorem Polynomial.norm_root_le_one_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) {z : ℂ} (hz : z ∈ p.aroots ℂ) : ‖z‖ ≤ 1

If an integer polynomial has Mahler measure equal to 1, then all its complex roots have norm at most 1.

theorem Polynomial.pow_eq_one_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) {z : ℂ} (hz₀ : z ≠ 0) (hz : z ∈ p.aroots ℂ) : ∃ (n : ℕ), 0 < n ∧ z ^ n = 1

If an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are roots of unity.

theorem Polynomial.isPrimitiveRoot_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) {z : ℂ} (hz₀ : z ≠ 0) (hz : z ∈ p.aroots ℂ) : ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n

If an integer polynomial has Mahler measure equal to 1, then all its complex nonzero roots are roots of unity.

theorem Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_one {p : Polynomial ℤ} (h : (map (Int.castRingHom ℂ) p).mahlerMeasure = 1) (hX : ¬X ∣ p) (hpdeg : p.degree ≠ 0) : ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p

If an integer non-constant polynomial has Mahler measure equal to 1 and is not a multiple of X, then it is divisible by a cyclotomic polynomial.