Mahler measure

Stream: mathlib4

[Fabrizio Barroero]

#26035 introduces the Mahler measure of a complex polynomial and proves its multiplicativity using recent work by @Stefan Kebekus

[Fabrizio Barroero]

This is the first PR of hopefully many as I have the full proof of Northcott's Theorem: there are at most finitely many integer polynomials of bounded degree and Mahler measure.

[Fabrizio Barroero]

The only thing missing is Jensen's formula which has been formalized by Stefan but it's not yet in Mathlib.

[Stefan Kebekus]

This is great news. :congratulations:

[Stefan Kebekus]

I am currently cleaning my code and feeding it into MathLib. Harmonic functions are next, but the Jensen formula will probably not arrive in the library until the end of summer.

[Fabrizio Barroero]

Thanks! No problem, there’s no rush! Thanks for your work!

[Stefan Kebekus]

@Fabrizio Barroero FYI: The Jensen Formula has landed in Mathlib a few minutes ago, thanks to the help of @Sébastien Gouëzel and others. I'd be glad if you found it useful.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/JensenFormula.html

[Fabrizio Barroero]

Stefan Kebekus said:

Fabrizio Barroero FYI: The Jensen Formula has landed in Mathlib a few minutes ago, thanks to the help of Sébastien Gouëzel and others. I'd be glad if you found it useful.

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/JensenFormula.html

That’s great news! Thanks for your work and thanks to the reviewers as well

[Fabrizio Barroero]

In #30548 Jensen's formula is applied to get the usual formula for the Mahler measure:
The Mahler measure of a polynomial is the the absolute value of its leading coefficient times the product of the absolute values of its roots lying outside the unit disk.

[Kevin Wilson]

Hi all! I was attempting to use the Mahler measure with integer polynomials, but it requires the coefficients be in C. This leads to a bunch of tracking of casts.

I wondered if it's possible to define the Mahler measure over a smaller algebra instead?

[Johan Commelin]

I don't know much about the Mahler measure, but Mathlib has more examples where an explicit ring of coefficients is added as "bookkeeping", exactly to avoid casts.

[Filippo A. E. Nuccio]

@Fabrizio Barroero

[Fabrizio Barroero]

In #31732 I added Nothcott's Theorem

theorem finite_mahlerMeasure_le (n : ℕ) (B : ℝ≥0) :
    Set.Finite {p : ℤ[X] | p.natDegree ≤ n ∧ (p.map (Int.castRingHom ℂ)).mahlerMeasure ≤ B}

and I have to say it was a little painful to juggle the casts around, although not as painful as I anticipated.

In any case, I suppose one could define the Mahler Measure of a polynomial with coefficient in any subring of C. Something like this

import Mathlib

namespace Polynomial

variable (R : Type*) [CommSemiring R] [Algebra R ℂ] (p : R[X])

noncomputable def mahlerMeasure' := (p.map (algebraMap R ℂ)).mahlerMeasure

example : (X : ℤ[X]).mahlerMeasure' = 1 := by simp [mahlerMeasure', mahlerMeasure]

end Polynomial

This could go at the beginning the NumberTheory/MahlerMeasure file and one can then simplify the notation of what comes after.
I don't know it this is the right way of defining it...

[Fabrizio Barroero]

Kevin Wilson said:

Hi all! I was attempting to use the Mahler measure with integer polynomials, but it requires the coefficients be in C. This leads to a bunch of tracking of casts.

I wondered if it's possible to define the Mahler measure over a smaller algebra instead?

By the way, I would be very interested to know about your plans of using the Polynomial.mahlerMeasure.

[Kevin Wilson]

I was going about proving some results in arithmetic statistics, and as a warm up, a standard one is "The number of reducible polynomials of height H and degree d >= 3 is bounded by H^(d - 1)." The proof is essentially "apply Mahler measure and its relationship to height + dyadic intervals."

So I needed Mahler measure on Z :-)

I essentially setup your example, but then I ended up copy/pasting a bunch of the lemmas as they basically all hold true, and it felt a bit wasteful.

[Fabrizio Barroero]

Kevin Wilson said:

I was going about proving some results in arithmetic statistics, and as a warm up, a standard one is "The number of reducible polynomials of height H and degree d >= 3 is bounded by H^(d - 1)." The proof is essentially "apply Mahler measure and its relationship to height + dyadic intervals."

So I needed Mahler measure on Z :-)

I essentially setup your example, but then I ended up copy/pasting a bunch of the lemmas as they basically all hold true, and it felt a bit wasteful.

Nice! That seem like a good warm up!

[Kevin Wilson]

Johan Commelin said:

I don't know much about the Mahler measure, but Mathlib has more examples where an explicit ring of coefficients is added as "bookkeeping", exactly to avoid casts.

I would love an example here!

[Kevin Buzzard]

Group cohomology is developed not for abelian groups (as is traditional in the literature) but for $R$-modules, with the output cohomology groups also being $R$-modules.

[Riccardo Brasca]

For a simpler example: we have cyclotomic polynomial over any ring R (that is of course just the image of the polynomials over ℤ).

[Johan Commelin]

@Kevin Wilson :up: is the kind of example I was thinking of (-;

[Fabrizio Barroero]

In this case though, the definition needs to depend on how one embeds the ring into C. Something like this also works

import Mathlib

namespace Polynomial

variable {R : Type*} [CommSemiring R] (p : R[X])

noncomputable def mahlerMeasure' (f : R →+* ℂ) := (p.map f).mahlerMeasure

example : (X : ℤ[X]).mahlerMeasure' (Int.castRingHom ℂ) = 1 := by simp [mahlerMeasure', mahlerMeasure]

end Polynomial

but I think one does not gain much cause the map has to be carried around. The version above probably woks better.

[Johan Commelin]

Ok, I now took some time to actually look at the definition.
@Kevin Wilson what are the results here? If you have a polynomial over $\Z$, what does that say about the Mahler measure? In which ring will it live?

[Kevin Wilson]

Basically all of the results proven for the Mahler measure so far hold for polynomials over Z (multiplicativity, bounds, etc).

The value itself is always a real number; and I can’t think of any results off the top of my head that rely on it being in a smaller ring.

[Kevin Wilson]

There’s sort of two cases: Z, Q, R, and C where the norms all line up and the results are basically mutatis mutandi; or some other number ring where you have to specify the norm you’re using / which embedding into C.

Z, Q, R, and C are the big use cases, so from a notation standpoint it would be nice to unify them. The others probably do require carrying around the embedding/norm.

[Johan Commelin]

I think @Fabrizio Barroero's first version of mahlerMeasure' a few posts up, using algebraMap looks good. If you would also like to get Real-valued output, then we would need to be more careful.
Is the output real-valued as soon as the coefficients of the polynomial live in (a subring of) the real numbers?

[Fabrizio Barroero]

It is always a real number.

[Johan Commelin]

I should learn how to read a type signature :see_no_evil: :man_facepalming:

[Fabrizio Barroero]

Technically, it's value lies in the splitting field of the polynomial

[Fabrizio Barroero]

I mean... in informal maths...

[Johan Commelin]

Cool. Is that already a theorem in Mathlib? Seems completely non-obvious to me, with all the integrals appearing in the definition.

[Fabrizio Barroero]

It is a consequence of this

theorem Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots (p : Polynomial ℂ) :
p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun (a : ℂ) => max 1 ‖a‖) p.roots).prod

[Johan Commelin]

Would it make sense to take that as the definition?

[Johan Commelin]

It sounds like we could take a polynomial over R, and an algebra A over R, and a proof that p splits in A. And then define the Mahler measure as a term of A.

And then prove that this is invariant under algebra homomorphisms. And if you map to A = Complex then you end up with some integral that also computes this value.

[Johan Commelin]

But maybe I'm glossing over a detail.

[Damiano Testa]

In informal maths, I do consider the second one to be the definition of Maehler measure. Probably even without the p.leadingCoeff factor!

EDIT: the leadingCoeff seems to be due to the fact that I always use it for monic polynomials... https://en.wikipedia.org/wiki/Mahler_measure

[Fabrizio Barroero]

Johan Commelin said:

Would it make sense to take that as the definition?

It sounds reasonable. Let me try to write down some definitions and lemmas...

[Fabrizio Barroero]

Damiano Testa said:

In informal maths, I do consider the second one to be the definition of Maehler measure. Probably even without the p.leadingCoeff factor!

EDIT: the leadingCoeff seems to be due to the fact that I always use it for monic polynomials... https://en.wikipedia.org/wiki/Mahler_measure

For me too, actually. But many books adopt the definition with the integral and then use Jensen's formula to prove the formula above...
This is the reason why I chose that approach.

[Michael Stoll]

It shouldn't matter which one is the definition (that's an implementation detail), as long as we have both equalities at our disposal.

[Michael Stoll]

Johan Commelin said:

It sounds like we could take a polynomial over R, and an algebra A over R, and a proof that p splits in A. And then define the Mahler measure as a term of A.

Not quite, because there is a norm and a max involved. The statement that the Mahler measure lies in the splitting field is also not completely true because of this when the coefficients are not real, e.g., the Mahler measure of X - (2 + i) is √5, which is not in ℚ(i).

[Fabrizio Barroero]

True, one needs a norm on A of course.
And the values are in the image of the splitting field via the norm I guess...

[Michael Stoll]

For real coefficients, the result is actually in the maximal real subfield of the splitting field (because non-real roots occur in pairs, and the product of their norms is the product of the roots).

[Johan Commelin]

Michael Stoll said:

It shouldn't matter which one is the definition (that's an implementation detail), as long as we have both equalities at our disposal.

Well, I agree, unless it influences the type signature. Atm, the type is Real. If we want that to be a smaller ring, then one definition might be a lot more practical than another.

[Johan Commelin]

Michael Stoll said:

Johan Commelin said:

It sounds like we could take a polynomial over R, and an algebra A over R, and a proof that p splits in A. And then define the Mahler measure as a term of A.

Not quite, because there is a norm and a max involved.

Point taken.

[Fabrizio Barroero]

I am not sure we gain anything from this

import Mathlib

namespace Polynomial

variable {R A : Type*} [CommRing R] [CommRing A] [IsDomain A] (p : R[X]) [Algebra R A] [Norm A]

variable (A) in
noncomputable def mahlerMeasure' := ‖(algebraMap R A) p.leadingCoeff‖ * (Multiset.map (fun (a : A) => max 1 ‖a‖) (p.aroots A)).prod

example : (X : ℤ[X]).mahlerMeasure' ℂ = 1 := by simp [mahlerMeasure']

example (p : ℤ[X]) : p.mahlerMeasure' ℂ = (p.map (Int.castRingHom ℂ)).mahlerMeasure := by
  simp [mahlerMeasure', mahlerMeasure_eq_leadingCoeff_mul_prod_roots, aroots_def,
    leadingCoeff_map_of_injective <| RingHom.injective_int (Int.castRingHom ℂ)]

end Polynomial