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.

[Fabrizio Barroero]

Here is an attempt to unify the definitions.

import Mathlib

variable {R F : Type*} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ)

namespace PowerSeries

noncomputable def gaussNormC (f : PowerSeries R) : ℝ := sSup {v (f.coeff R i) * c ^ i | (i : ℕ)}

@[simp]
lemma gaussNormC_zero [ZeroHomClass F R ℝ] : gaussNormC v c 0 = 0 := by simp [gaussNormC]

end PowerSeries

namespace Polynomial

def gaussNormC (p : R[X]) : ℝ := if h : p.support.Nonempty then p.support.sup' h fun I ↦ (v (p.coeff i) * c ^ i) else 0

@[simp]
lemma gaussNormC_zero : gaussNormC v c 0 = 0 := by simp [gaussNormC]

@[simp]
lemma gaussNormC_C [ZeroHomClass F R ℝ] (r : R) : (C r).gaussNormC v c = v r := by
by_cases hr : r = (0 : R); simp [gaussNormC, hr]
simp [gaussNormC, support_C, hr]

@[simp]
theorem gaussNormC_toPowerSeries [ZeroHomClass F R ℝ] (p : R[X]) : (p.toPowerSeries).gaussNormC v c = p.gaussNormC v c := by sorry

end Polynomial

@[simp]
theorem PowerSeries.gaussNormC_C [ZeroHomClass F R ℝ] (r : R) : (C R r).gaussNormC v c = v r := by
simp [← @Polynomial.coe_C]

section NormedRing

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

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

theorem gaussNormC'_eq (f : PowerSeries R) : gaussNormC' c R f = f.gaussNormC (NormedRing.toRingNorm R) c := by
simp [gaussNormC', PowerSeries.gaussNormC]

end NormedRing

[Fabrizio Barroero]

I kept my original definition Polynomial.gaussNormC because that is not noncomputable and it is easier to work with. It can also be dropped and we can just keep what I called gaussNormC_toPowerSeries.

[William Coram]

I agree that keeping your original definition will be useful.

[Fabrizio Barroero]

see #24940

[Jz Pan]

William Coram said:

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

Do you think iSup is better than sSup? i.e. ⨆ i : ℕ, ‖coeff R i f‖ * c^i

[Jz Pan]

Although iSup is defined using sSup ...

[Yaël Dillies]

Yes, please use iSup here. You will have a much better time

[Yaël Dillies]

Jz Pan said:

Although iSup is defined using sSup ...

This is necessary due to the universe polymorphism in docs#iSup, but really docs#CompleteLattice would like to have an iSup field

[Fabrizio Barroero]

Ok, I am going to change everything to iSup. Thanks for the tip

[Fabrizio Barroero]

I’m done. It’s much better now. Thanks