Lehmer's Mahler measure problem

Reference: Wikipedia

def LehmerMahlerMeasureProblem.mahlerMeasure (f : Polynomial ℂ) : ℝ

The Mahler measure of f(X) is defined as ‖a‖ ∏ᵢ max(1,‖αᵢ‖), where f(X)=a(X-α₁)(X-α₂)...(X-αₙ).

Equations

• LehmerMahlerMeasureProblem.mahlerMeasure f = ‖f.leadingCoeff‖ * (Multiset.map (fun (x : ℂ) => 1 ⊔ ‖x‖) f.roots).prod

def LehmerMahlerMeasureProblem.mahlerMeasureZ (f : Polynomial ℤ) : ℝ

Equations

• LehmerMahlerMeasureProblem.mahlerMeasureZ f = LehmerMahlerMeasureProblem.mahlerMeasure (Polynomial.map (algebraMap ℤ ℂ) f)

theorem LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem : ∃ (μ : ℝ), ∀ (f : Polynomial ℤ), μ > 1 ∧ (mahlerMeasureZ f > 1 → mahlerMeasureZ f ≥ μ)

Let M(f) denote the Mahler measure of f. There exists a constant μ>1 such that for any f(x)∈ℤ[x], M(f)>1 → M(f)≥μ.

def LehmerMahlerMeasureProblem.lehmerPolynomial : Polynomial ℤ

Equations

• One or more equations did not get rendered due to their size.

theorem LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.best (f : Polynomial ℤ) (hf : mahlerMeasureZ f > 1) : mahlerMeasureZ f ≥ mahlerMeasureZ lehmerPolynomial

μ=M(X^10 + X^9 - X^7 - X^6 - X^5 - X^4 - X^3 + X + 1) is the best value for lehmer_mahler_measure_problem.

theorem LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.not_reciprocal (f : Polynomial ℤ) (hf : mahlerMeasureZ f > 1) (hf' : f.reverse ≠ f) : mahlerMeasureZ f ≥ mahlerMeasureZ (Polynomial.X ^ 3 - Polynomial.X - 1)

If f is not reciprocal and M(f)>1 then M(f) ≥ M(X^3 - X - 1).

def LehmerMahlerMeasureProblem.Polynomial.HasOddCoeffs (f : Polynomial ℤ) : Prop

Polynomial.HasOddCoeffs f means that all coefficients of f : Polynomial ℤ are odd.

Equations

• LehmerMahlerMeasureProblem.Polynomial.HasOddCoeffs f = ∀ i ∈ f.support, Odd (f.coeff i)

theorem LehmerMahlerMeasureProblem.lehmer_mahler_measure_problem.variants.odd (f : Polynomial ℤ) (hf : mahlerMeasureZ f > 1) (hf' : Polynomial.HasOddCoeffs f) : mahlerMeasureZ f ≥ mahlerMeasureZ (Polynomial.X ^ 2 - Polynomial.X - 1)

If all the coefficients of f are odd and M(f)>1, M(f) ≥ M(X^2 - X - 1).