Mahler measure of complex polynomials

In this file we define the Mahler measure of a polynomial over ℂ[X] and prove some basic properties.

Main definitions

• Polynomial.logMahlerMeasure p: the logarithmic Mahler measure of a polynomial p defined as (2 * π)⁻¹ * ∫ x ∈ (0, 2 * π), log ‖p (e ^ (i * x))‖.
• Polynomial.mahlerMeasure p: the (exponential) Mahler measure of a polynomial p, which is equal to e ^ p.logMahlerMeasure if p is nonzero, and 0 otherwise.

Main results

• Polynomial.mahlerMeasure_mul: the Mahler measure of the product of two polynomials is the product of their Mahler measures.
• mahlerMeasure_eq_leadingCoeff_mul_prod_roots: the Mahler measure of a polynomial is the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk.

noncomputable def Polynomial.logMahlerMeasure (p : Polynomial ℂ) : ℝ

The logarithmic Mahler measure of a polynomial p defined as (2 * π)⁻¹ * ∫ x ∈ (0, 2 * π), log ‖p (e ^ (i * x))‖

Equations

• p.logMahlerMeasure = Real.circleAverage (fun (x : ℂ) => Real.log ‖Polynomial.eval x p‖) 0 1

theorem Polynomial.logMahlerMeasure_def (p : Polynomial ℂ) : p.logMahlerMeasure = Real.circleAverage (fun (x : ℂ) => Real.log ‖eval x p‖) 0 1

@[simp]

theorem Polynomial.logMahlerMeasure_zero : logMahlerMeasure 0 = 0

@[simp]

theorem Polynomial.logMahlerMeasure_one : logMahlerMeasure 1 = 0

@[simp]

theorem Polynomial.logMahlerMeasure_const (z : ℂ) : (C z).logMahlerMeasure = Real.log ‖z‖

@[simp]

theorem Polynomial.logMahlerMeasure_X : X.logMahlerMeasure = 0

@[simp]

theorem Polynomial.logMahlerMeasure_monomial (n : ℕ) (z : ℂ) : ((monomial n) z).logMahlerMeasure = Real.log ‖z‖

noncomputable def Polynomial.mahlerMeasure (p : Polynomial ℂ) : ℝ

The Mahler measure of a polynomial p defined as e ^ (logMahlerMeasure p) if p is nonzero and 0 otherwise

Equations

• p.mahlerMeasure = if p ≠ 0 then Real.exp p.logMahlerMeasure else 0

theorem Polynomial.mahlerMeasure_def_of_ne_zero {p : Polynomial ℂ} (hp : p ≠ 0) : p.mahlerMeasure = Real.exp ((2 * Real.pi)⁻¹ * ∫ (x : ℝ) in 0..2 * Real.pi, Real.log ‖eval (circleMap 0 1 x) p‖)

theorem Polynomial.logMahlerMeasure_eq_log_MahlerMeasure {p : Polynomial ℂ} : p.logMahlerMeasure = Real.log p.mahlerMeasure

@[simp]

theorem Polynomial.mahlerMeasure_zero : mahlerMeasure 0 = 0

@[simp]

theorem Polynomial.mahlerMeasure_one : mahlerMeasure 1 = 1

@[simp]

theorem Polynomial.mahlerMeasure_const (z : ℂ) : (C z).mahlerMeasure = ‖z‖

theorem Polynomial.mahlerMeasure_nonneg (p : Polynomial ℂ) : 0 ≤ p.mahlerMeasure

theorem Polynomial.mahlerMeasure_pos_of_ne_zero {p : Polynomial ℂ} (hp : p ≠ 0) : 0 < p.mahlerMeasure

@[simp]

theorem Polynomial.mahlerMeasure_eq_zero_iff (p : Polynomial ℂ) : p.mahlerMeasure = 0 ↔ p = 0

theorem Polynomial.intervalIntegrable_mahlerMeasure (p : Polynomial ℂ) : IntervalIntegrable (fun (x : ℝ) => Real.log ‖eval (circleMap 0 1 x) p‖) MeasureTheory.volume 0 (2 * Real.pi)

The Mahler measure of the product of two polynomials is the product of their Mahler measures

theorem Polynomial.mahlerMeasure_mul (p q : Polynomial ℂ) : (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

@[simp]

theorem Polynomial.prod_mahlerMeasure_eq_mahlerMeasure_prod (s : Multiset (Polynomial ℂ)) : s.prod.mahlerMeasure = (Multiset.map (fun (p : Polynomial ℂ) => p.mahlerMeasure) s).prod

theorem Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure {p q : Polynomial ℂ} (hpq : p * q ≠ 0) : (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure

@[deprecated Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure (since := "2025-11-17")]

theorem Polynomial.logMahlerMeasure_mul_eq_add_logMahelerMeasure {p q : Polynomial ℂ} (hpq : p * q ≠ 0) : (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure

Alias of Polynomial.logMahlerMeasure_mul_eq_add_logMahlerMeasure.

theorem Polynomial.logMahlerMeasure_C_mul {a : ℂ} (ha : a ≠ 0) {p : Polynomial ℂ} (hp : p ≠ 0) : (C a * p).logMahlerMeasure = Real.log ‖a‖ + p.logMahlerMeasure

@[simp]

theorem Polynomial.logMahlerMeasure_X_sub_C (z : ℂ) : (X - C z).logMahlerMeasure = ‖z‖.posLog

The logarithmic Mahler measure of X - C z is the log⁺ of the absolute value of z.

@[simp]

theorem Polynomial.logMahlerMeasure_X_add_C (z : ℂ) : (X + C z).logMahlerMeasure = ‖z‖.posLog

theorem Polynomial.logMahlerMeasure_C_mul_X_add_C {a : ℂ} (ha : a ≠ 0) (b : ℂ) : (C a * X + C b).logMahlerMeasure = Real.log ‖a‖ + ‖a⁻¹ * b‖.posLog

theorem Polynomial.logMahlerMeasure_of_degree_eq_one {p : Polynomial ℂ} (h : p.degree = 1) : p.logMahlerMeasure = Real.log ‖p.coeff 1‖ + ‖(p.coeff 1)⁻¹ * p.coeff 0‖.posLog

@[simp]

theorem Polynomial.mahlerMeasure_X_sub_C (z : ℂ) : (X - C z).mahlerMeasure = max 1 ‖z‖

The Mahler measure of X - C z equals max 1 ‖z‖.

@[simp]

theorem Polynomial.mahlerMeasure_X_add_C (z : ℂ) : (X + C z).mahlerMeasure = max 1 ‖z‖

@[simp]

theorem Polynomial.mahlerMeasure_C_mul_X_add_C {a : ℂ} (ha : a ≠ 0) (b : ℂ) : (C a * X + C b).mahlerMeasure = max ‖a‖ ‖b‖

theorem Polynomial.mahlerMeasure_of_degree_eq_one {p : Polynomial ℂ} (h : p.degree = 1) : p.mahlerMeasure = max ‖p.coeff 1‖ ‖p.coeff 0‖

theorem Polynomial.logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots (p : Polynomial ℂ) : p.logMahlerMeasure = Real.log ‖p.leadingCoeff‖ + (Multiset.map (fun (a : ℂ) => ‖a‖.posLog) p.roots).sum

The logarithmic Mahler measure of a polynomial is the log of the absolute value of its leading coefficient plus the sum of the logs of the absolute values of its roots lying outside the unit disk.

theorem Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots (p : Polynomial ℂ) : p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun (a : ℂ) => max 1 ‖a‖) p.roots).prod

The Mahler measure of a polynomial is the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk.

Estimates for the Mahler measure

theorem Polynomial.one_le_prod_max_one_norm_roots (p : Polynomial ℂ) : 1 ≤ (Multiset.map (fun (a : ℂ) => max 1 ‖a‖) p.roots).prod

theorem Polynomial.leading_coeff_le_mahlerMeasure (p : Polynomial ℂ) : ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

theorem Polynomial.prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff {p : Polynomial ℂ} (hlc : 1 ≤ ‖p.leadingCoeff‖) : (Multiset.map (fun (a : ℂ) => max 1 ‖a‖) p.roots).prod ≤ p.mahlerMeasure

theorem Polynomial.mahlerMeasure_le_sum_norm_coeff (p : Polynomial ℂ) : p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) => ‖a‖

The Mahler measure of a polynomial is bounded above by the sum of the norms of its coefficients.

theorem Polynomial.norm_coeff_le_choose_mul_mahlerMeasure (n : ℕ) (p : Polynomial ℂ) : ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure