Theorems · Theorem · complex analysis

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.

Defined in

Mathlib.Analysis.Polynomial.MahlerMeasure

Cited by

1 results in Mathlib

Foundations

Depth 296 from the axioms · uses propext, Classical.choice, Quot.sound