Mahler measure of integer polynomials

The main purpose of this file is to prove 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.

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 + 1 ∧ ∀ (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.