Mahler measure of integer polynomials

The main purpose of this file is to prove some facts about the Mahler measure of integer polynomials, in particular Northcott's Theorem for the Mahler measure.

Main results

• Polynomial.finite_mahlerMeasure_le: Northcott's Theorem: the set of integer polynomials of degree at most n and Mahler measure at most B is finite.
• Polynomial.card_mahlerMeasure_le_prod: an upper bound on the number of integer polynomials of degree at most n and Mahler measure at most B.
• Polynomial.cyclotomic_mahlerMeasure_eq_one: the Mahler measure of a cyclotomic polynomial is 1.

theorem Polynomial.one_le_mahlerMeasure_of_ne_zero {p : Polynomial ℤ} (hp : p ≠ 0) : 1 ≤ (map (Int.castRingHom ℂ) p).mahlerMeasure

theorem Polynomial.card_eq_of_natDegree_le_of_coeff_le {n : ℕ} {B₁ B₂ : Fin (n + 1) → ℝ} : {p : Polynomial ℤ | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), B₁ i ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ B₂ i}.ncard = ∏ i : Fin (n + 1), (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

theorem Polynomial.finite_mahlerMeasure_le (n : ℕ) (B : NNReal) : {p : Polynomial ℤ | p.natDegree ≤ n ∧ (map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite

Northcott's Theorem: the set of integer polynomials of degree at most n and Mahler measure at most B is finite.

theorem Polynomial.card_mahlerMeasure_le_prod (n : ℕ) (B : NNReal) : {p : Polynomial ℤ | p.natDegree ≤ n ∧ (map (Int.castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i : Fin (n + 1), (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

An upper bound on the number of integer polynomials of degree at most n and Mahler measure at most B.

theorem Polynomial.cyclotomic_mahlerMeasure_eq_one {R : Type u_1} [CommRing R] [Algebra R ℂ] (n : ℕ) : (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

The Mahler measure of a cyclotomic polynomial is 1.