Theorems · Theorem · complex analysis

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).

Defined in

Mathlib.Analysis.Polynomial.MahlerMeasure

Cited by

1 results in Mathlib

Foundations

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