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.

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_logMahelerMeasure {p q : Polynomial ℂ} (hpq : p * q ≠ 0) : (p * q).logMahlerMeasure = p.logMahlerMeasure + q.logMahlerMeasure