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

[Kevin Wilson]

So I didn't get around to figuring out the best way to set this up yet, but I did setup a PR for the height of a polynomial in #33240

I also have a complete proof of the asymptotics of reducible polynomials which I'll break up into a few PRs :-)

[Kevin Wilson]

Also, out of curiosity, I have a mostly AI generated proof (read, really long and verbose and first principles) of the fact that

theorem mahlerMeasure_le_sqrt_natDegree_mul_height (p : ℂ[X]) : p.mahlerMeasure ≤ √(p.natDegree + 1) * p.height

The current implementation has

theorem mahlerMeasure_le_sum_norm_coeff (p : ℂ[X]) : p.mahlerMeasure ≤ p.sum fun _ a ↦ ‖a‖ := by

I'm not expert enough in things like how Fourier theory works in Lean to improve the proof of the sqrt bound, but I can make a PR of it if it would be useful.

[Fabrizio Barroero]

Something similar to your Polynomial.height is already in Mathlib under the name of Polynomial.gaussNorm.

[Fabrizio Barroero]

I am very curious to see your proof of the asymptotics!

[Kevin Wilson]

Oh nice! I guess height is just gaussNorm with v = id and c = 1. That’s probably the best definition then and then there can be a lemma with the simpler definition suggested by Violeta

[Violeta Hernández]

This is entirely tangential, but why does the MahlerMeasure file define notation for BoxPoly rather than just making it into a def?

[Violeta Hernández]

Fabrizio Barroero said:

Something similar to your Polynomial.height is already in Mathlib under the name of Polynomial.gaussNorm.

As for this, it might be worth mentioning the words "height" and "length" somewhere in the docstring so that future mathematicians know where to look :slight_smile:

[Fabrizio Barroero]

Violeta Hernández said:

Fabrizio Barroero said:

Something similar to your Polynomial.height is already in Mathlib under the name of Polynomial.gaussNorm.

As for this, it might be worth mentioning the words "height" and "length" somewhere in the docstring so that future mathematicians know where to look :)

Good idea! See #33338

[Fabrizio Barroero]

Violeta Hernández said:

This is entirely tangential, but why does the MahlerMeasure file define notation for BoxPoly rather than just making it into a def?

What is the advantage of making it into a def?

[Violeta Hernández]

A notation basically means that you're inserting that whole string of symbols as is into your theorem. A def gives you some degree of encapsulation, and is generally just more idiomatic.

[Kevin Wilson]

Apologies for the delays. Christmas holidays :-)

The asymptotics I was building rely on an identical notion to BoxPoly I called PolyBox. It will definitely be a common notion if arithmetic statistics get added to Mathlib, so worth giving it a name.

As for the l^p norms, I was starting to define the height as the gaussNorm and I was having some problems figuring out how to get norm packaged into a FunLike F A ℝ along with an instance of NonnegHomClass F A ℝ needed by things like gaussNorm_eq_zero_iff. I'd appreciate any pointers on that front

As for renaming height to something else, I figure that Polynomial.supNorm works? If that's still confusing with the polynomial as a function, then Polynomial.coeffSupNorm is more explicit. (The other l^p norms would have similar names.)

[Aaron Liu]

is docs#Polynomial.gaussNorm another one of those bad definitions (because it takes an argument which is a generic FunLike)

[Violeta Hernández]

Is that a known antipattern? Why if so?

[Aaron Liu]

see #mathlib4 > Mathlib's morphism hierarchy

[Fabrizio Barroero]

In #33326 you can see that the Gauss Norm works well with an AbsoluteValue. Tomorrow I’m gonna have a look at the norm issue.

[Kevin Wilson]

I think the underlying issue is that the norm on a SeminormedRing isn’t a Seminorm.

[Fabrizio Barroero]

This works

import Mathlib

open Polynomial

variable {A : Type*} [NormedField A]

#check gaussNorm (NormedField.toAbsoluteValue A) 1

lemma gaussNorm_eq (p : A[X]) :
  p.gaussNorm (NormedField.toAbsoluteValue A) 1 =
  if h : p.support.Nonempty then p.support.sup' h fun i ↦ ‖p.coeff i‖ else 0 := by
  simp [gaussNorm, NormedField.toAbsoluteValue]

[Kevin Wilson]

That works, @Fabrizio Barroero . Thanks much!

I also needed to import Mathlib.Algebra.Order.Hom.Basic to get some of the nonnegative instances. I don't know if there's any documentation on the morphism hierarchy anywhere and how to work with it, but it would be super helpful to newbies like me :-)

[Kevin Wilson]

Back to the mahlerMeasure' definition :-) Now that I understand a bit more about the morphism hierarchy, perhaps this is the right definition of mahlerMeasure' ?

variable {A F : Type*} [Semiring A] [FunLike F A ℂ] [RingHomClass F A ℂ] (p : A[X]) (v : F)

noncomputable def mahlerMeasure' := (p.map v).mahlerMeasure

This gist has some lemmas built on it. In particular, note the typeclasses on Line 28:

variable {A F : Type*} [NormedRing A] [FunLike F A ℂ] [RingHomClass F A ℂ]
  [IsometryClass F A ℂ] (p : A[X]) (v : F)

lemma leadingCoeff_le_mahlerMeasure' :
    ‖p.leadingCoeff‖ ≤ p.mahlerMeasure' v := by

This would cover the major use cases (integer, rational, and real coefficients), but if there's a desire to cover number field coefficients specifically, then I could unbundle the norm

[Artie Khovanov]

I think the funlike in the first definition is an anti-pattern. RingHom.map should (and eventually will) be changed to take a concrete RingHom, so definitions using it should too.

[Kevin Wilson]

So to check my understanding, the definition proposed is:

variable {A F : Type*} [Semiring A] (p : A[X]) (v : RingHom A ℂ)

noncomputable def mahlerMeasure' := (p.map v).mahlerMeasure

[Kevin Wilson]

And for the _second_ definition, the suggestion is to keep the FunLike since here we're layering together two FunLike classes?

[Aaron Liu]

for definitions you shouldn't use FunLike

[Aaron Liu]

for theorems it's fine probably

[Kevin Wilson]

Gotcha! In that case, I can put together a PR

[Kevin Wilson]

Here is the promised PR: https://github.com/leanprover-community/mathlib4/pull/33463

Not sure I'm correctly utilizing the morphism hierarchy here, but I defer to @Aaron Liu and others on that front.

[Violeta Hernández]

I think we generally like to avoid primed names, and more so for defs. Also, is there no way to unify both of these definitions? Perhaps by requiring an Algebra R ℂ instance or something similar?

[Violeta Hernández]

In fact, why can't we take docs#Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots as the definition of the Mahler measure? That should merge your two definitions.

[Kevin Wilson]

In docs#Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots the norm of the leading coefficient depends on the choice of embedding

AFAICT, you can:

• Require the user supply a map from the base ring to Complex and carry it around in the notation (essentially, make mahlerMeasure' the main definition). This leads to a syntactic annoyance for users, but perhaps a docstring is sufficient to elucidate? (E.g., "This notion is most commonly used for polynomials over Complex or Int. In those cases, ...") OR
• Have the current setup which makes it relatively easy for users but requires a ' definition.

[Artie Khovanov]

Often auxillary definitions are named ...Aux and made private declarations

[Violeta Hernández]

Making mahlerMeasure' the main definition seems reasonable to me. To recover the complex case you just write .id for the map field.

[Fabrizio Barroero]

If p is a polynomial with integer coefficients, what is the point of replacing (p.map (Int.castRingHom ℂ)).mahlerMeasure by p.mahlerMeasure (Int.castRingHom ℂ)?

[Kevin Wilson]

Maybe it's a mild irritant, but lemmas like this one that package up casts I personally found useful in trying to put together the asymptotics on integer polynomials.

(p.map (Int.castRingHom ℂ)).mahlerMeasure (I think) means you need to figure out the casts; p.mahlerMeasure (Int.castRingHom ℂ) can package them up for the user.

[Fabrizio Barroero]

I see, but then isn't it possible to make this independent of v?
@Violeta Hernández was suggesting an Algebra A ℂ instance above...

[Violeta Hernández]

Algebra might be too weak, I don't think that would preserve the norm in the general case

[Fabrizio Barroero]

You are right. There is docs#NormedAlgebra but it seems to require the base ring to be a field, unfortunately.

[Kevin Wilson]

I did look into that possibility earlier and there were two potential problems:

1. As you note NormedAlgebra and its ilk require the base ring to be a field. I didn’t try to figure out why, but even if it’s not necessary changing that to require only a ring structure would be a big surgery.

2. If you wanted to work with polynomials over a number ring, you’d need to specify which embedding into C you’re taking. I only have worked with the Mahler measure over Z so I don’t know if this would be a big inconvenience for future formalization

[Fabrizio Barroero]

I see the point now and I agree. Thanks.
I still think it would be nice to keep the original definition and an alternative one for general rings that embed into C.