Absolute values on polynomials

Stream: Is there code for X?

[Fabrizio Barroero]

Hi, I started formalising some of the content of this file because it is useful for heights in number theory.

Here is how I defined what’s called “Gauss Norm” in this notes:

import Mathlib

namespace Polynomial

variable {R α : Type*} [Semiring R] [Semiring α] [LinearOrder α]
 (f : AbsoluteValue R α) (hna : IsNonarchimedean f)

def GaussNorm : R[X] → α := fun p ↦ if h : p.support.Nonempty then p.support.sup' h fun I ↦
    (f (p.coeff i)) else 0

include hna in
theorem isNonarchimedean_GaussNorm [AddLeftMono α] : IsNonarchimedean (GaussNorm f) := sorry

end Polynomial

I have some API’s and plan to prove Theorem 7 in the notes.

I just would like to have some feedback on the definition and make sure that this is not already done somewhere else before I continue working on this and start making PRs.

[Chris Birkbeck]

So @William Coram has been working on defining this for restricted power series, so maybe talking with him would be useful.

[Michael Stoll]

I would perhaps not use f to denote an absolute value (maybe v instead), but otherwise this looks basically OK to me.

I think Mathlib style would prefer

def GaussNorm (p : R[X]) : α := if ...

[Kevin Buzzard]

For Theorem 7 you should prove the result for A a Dedekind domain with field of fractions K, rather than A = integers and K = rationals. (it will then apply to rings of integers of number fields, for example)

[Ruben Van de Velde]

Presumably def gaussNorm

[Antoine Chambert-Loir]

I'd want all Gauss norms, at any real scale ($\sup | c_n | r^n$).

[William Coram]

As mentioned by Chris, I was working with defining this for restricted power series. I had

variable (c : ℝ) (R : Type*) [NormedRing R] [IsUltrametricDist R]

noncomputable
def gaussNormC : PowerSeries R → ℝ :=
  fun f => sSup {‖coeff R i f‖ * c^i | (i : ℕ)}

I have shown this is a non-arch norm on restricted power series and (mostly shown) an absolute value on polynomials (for c nneg).

This work is a while form being properly PR'd as it is dependent on restricted power series being merged (and other commitments).

I had not planned on formalising any of the results in that file though, so we just need to agree on a definition that works.

[Fabrizio Barroero]

Thanks everyone for the feedback.

[Fabrizio Barroero]

William Coram said:

As mentioned by Chris, I was working with defining this for restricted power series. I had

variable (c : ℝ) (R : Type*) [NormedRing R] [IsUltrametricDist R]

noncomputable
def gaussNormC : PowerSeries R → ℝ :=
  fun f => sSup {‖coeff R i f‖ * c^i | (i : ℕ)}

I have shown this is a non-arch norm on restricted power series and (mostly shown) an absolute value on polynomials (for c nneg).

This work is a while form being properly PR'd as it is dependent on restricted power series being merged (and other commitments).

I had not planned on formalising any of the results in that file though, so we just need to agree on a definition that works.

I see.. That's interesting!
We certainly should agree on a common definition.

[Filippo A. E. Nuccio]

Pinging @María Inés de Frutos Fernández who has worked a lot on related stuff.