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.
• Polynomial.mapMahlerMeasure p v: the (exponential) Mahler measure of a polynomial p over a ring A whose coefficients are mapped to ℂ via v : A →+* ℂ

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.
• mahlerMeasure_le_sqrt_sum_sq_norm_coeff: Landau's inequality — the Mahler measure is at most the ℓ² norm of the coefficient vector.
• norm_coeff_le_choose_mul_mahlerMeasure_of_one_le_mahlerMeasure: Mignotte's coefficient bound — if f = g * h with M(h) ≥ 1, then ‖g.coeff n‖ ≤ C(deg g, n) · M(f).

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.leadingCoeff_le_mahlerMeasure (p : Polynomial ℂ) : ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

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

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

Alias of Polynomial.leadingCoeff_le_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.one_le_mahlerMeasure_of_one_le_norm_leadingCoeff {p : Polynomial ℂ} (hlc : 1 ≤ ‖p.leadingCoeff‖) : 1 ≤ p.mahlerMeasure

If the leading coefficient of a polynomial has norm at least 1, then its Mahler measure is at least 1. This holds in particular for nonzero polynomials with integer coefficients, since their leading coefficient is a nonzero integer.

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.mahlerMeasure_le_sqrt_sum_sq_norm_coeff (p : Polynomial ℂ) : p.mahlerMeasure ≤ √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2)

Landau's inequality: the Mahler measure of a polynomial is at most the ℓ² norm of its coefficient vector, √(∑ ‖coeff i‖²).

This is the classical inequality due to Landau (1905). Combined with the multiplicativity of the Mahler measure (mahlerMeasure_mul), it gives the Mignotte bound on coefficients of polynomial factors.

TODO: restate using a dedicated polynomial ℓ² norm once one is defined (see the TODO in Mathlib.Analysis.Polynomial.Norm).

theorem Polynomial.mahlerMeasure_le_sqrt_natDegree_add_one_mul_supNorm (p : Polynomial ℂ) : p.mahlerMeasure ≤ √(↑p.natDegree + 1) * p.supNorm

The Mahler measure of a polynomial is at most the sup norm of the polynomial times the square root of its degree plus one.

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

theorem Polynomial.supNorm_le_choose_natDegree_div_two_mul_mahlerMeasure (p : Polynomial ℂ) : p.supNorm ≤ ↑(p.natDegree.choose (p.natDegree / 2)) * p.mahlerMeasure

The Mignotte bound

theorem Polynomial.norm_coeff_le_choose_mul_mahlerMeasure_of_one_le_mahlerMeasure (n : ℕ) (g h : Polynomial ℂ) (hh : 1 ≤ h.mahlerMeasure) : ‖g.coeff n‖ ≤ ↑(g.natDegree.choose n) * (g * h).mahlerMeasure

Mignotte's coefficient bound: if f = g * h and h has Mahler measure at least 1 (which holds in particular when h has integer coefficients with nonzero leading coefficient), then the coefficients of g are bounded by a binomial coefficient times the Mahler measure of g * h.

Combined with mahlerMeasure_le_sqrt_sum_sq_norm_coeff (Landau's inequality), this gives the classical Mignotte bound ‖g.coeff n‖ ≤ C(deg g, n) · √(∑ i ∈ f.support, ‖f.coeff i‖ ^ 2) used in polynomial factorization algorithms (Berlekamp–Zassenhaus).

Mahler Measure on Other Rings

While the Mahler measure is an inherently Complex concept, we often want to work with it for polynomials with coefficients in subrings of ℂ. To do so, we introduce mapMahlerMeasure. This takes a RingHom A ℂ which takes the polynomial from A[X] to ℂ[X].

Some lemmas require the RingHom to also preserve the norm on the base ring, e.g., leadingCoeff_le_mapMahlerMeasure. Those will come below.

noncomputable def Polynomial.mapMahlerMeasure {A : Type u_1} [Semiring A] (p : Polynomial A) (v : A →+* ℂ) : ℝ

The Mahler measure for polynomials on rings other than ℂ. Most theorems will require A to be a NormedRing and v to be an isometry. See, e.g., mapMahlerMeasure_const

Equations

• p.mapMahlerMeasure v = (Polynomial.map v p).mahlerMeasure

theorem Polynomial.mapMahlerMeasure_eq {A : Type u_1} [Semiring A] (p : Polynomial A) (v : A →+* ℂ) : p.mapMahlerMeasure v = (map v p).mahlerMeasure

theorem Polynomial.mapMahlerMeasure_mul {A : Type u_1} [Semiring A] (v : A →+* ℂ) (f g : Polynomial A) : (f * g).mapMahlerMeasure v = f.mapMahlerMeasure v * g.mapMahlerMeasure v

theorem Polynomial.mapMahlerMeasure_nonneg {A : Type u_1} [Semiring A] (p : Polynomial A) (v : A →+* ℂ) : 0 ≤ p.mapMahlerMeasure v

@[simp]

theorem Polynomial.mapMahlerMeasure_zero {A : Type u_1} [Semiring A] (v : A →+* ℂ) : mapMahlerMeasure 0 v = 0

@[simp]

theorem Polynomial.mapMahlerMeasure_one {A : Type u_1} [Semiring A] (v : A →+* ℂ) : mapMahlerMeasure 1 v = 1

theorem Polynomial.mapMahlerMeasure_const {A : Type u_2} [NormedRing A] (v : A →+* ℂ) (hv : Isometry ⇑v) (z : A) : (C z).mapMahlerMeasure v = ‖z‖

theorem Polynomial.leadingCoeff_le_mapMahlerMeasure {A : Type u_2} [NormedRing A] (p : Polynomial A) (v : A →+* ℂ) (hv : Isometry ⇑v) : ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v

theorem Polynomial.Monic.one_le_mapMahlerMeasure {A : Type u_2} [NormedRing A] {p : Polynomial A} (v : A →+* ℂ) [NormOneClass A] (hv : Isometry ⇑v) (hp : p.Monic) : 1 ≤ p.mapMahlerMeasure v

theorem Polynomial.mapMahlerMeasure_pos_of_ne_zero {A : Type u_2} [NormedRing A] {p : Polynomial A} (v : A →+* ℂ) (hv : Isometry ⇑v) (hp : p ≠ 0) : 0 < p.mapMahlerMeasure v

theorem Polynomial.mapMahlerMeasure_le_sum_norm_coeff {A : Type u_2} [NormedRing A] (p : Polynomial A) (v : A →+* ℂ) (hv : Isometry ⇑v) : p.mapMahlerMeasure v ≤ p.sum fun (x : ℕ) (a : A) => ‖a‖

theorem Polynomial.norm_coeff_le_choose_mul_mapMahlerMeasure {A : Type u_2} [NormedRing A] (v : A →+* ℂ) (hv : Isometry ⇑v) (n : ℕ) (p : Polynomial A) : ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mapMahlerMeasure v