Nonarchimedean norm typeclass

Stream: Is there code for X?

[Yakov Pechersky]

Is there anything that specifies that the norm of a NormedAddCommGroup is nonarchimedean? Perhaps something akin to this?

import Mathlib.Analysis.Normed.Group.Basic
import Mathlib.Topology.Algebra.Nonarchimedean.Basic

variable {M : Type*} [NormedAddCommGroup M] [NonarchimedeanAddGroup M]

lemma IsNonarchimedean_norm : IsNonarchimedean (fun x : M ↦ ‖x‖) := by sorry

[Yakov Pechersky]

@Mitchell Lee

[Mitchell Lee]

I don't think so

[Yakov Pechersky]

It seems that one implies the other (IsNonarchimedean norm -> NonarchimedeanAddGroup), but not the other way around (?). I'm not great at rigid analysis. What is the right generalization / typeclass constraint to make the following make sense?

import Mathlib

variable {M : Type*} [NormedAddCommGroup M] [NonarchimedeanAddGroup M] [ContinuousAdd M]

lemma Finset.norm_sum_le_norm_sup_nonarchimedean {ι : Type*} (f : ι → M) (s : Finset ι)
    (hs : s.Nonempty) :
    ‖∑ i ∈ s, f i‖ ≤ s.sup' hs (‖f ·‖) := by sorry

[Mitchell Lee]

It's equivalent to the hypothesis that the norm is nonarchimedean, but you probably have to define that yourself

[Yakov Pechersky]

Right, I'm asking whether there is a typeclass of nonarchimedean normed addgroup that doesn't rely on Fact (IsNonarchimedean ...) or something

[Yakov Pechersky]

I thought that NonarchimedeanAddGroup would be it, but I think it's too weak, even in conjunction with NormedAddCommGroup.

[Kevin Buzzard]

NB the claim is also true if s is empty, if you regard the codomain of the norm map as being $\R_{\geq0}$, because the supremum of the empty set in this ordering is $0$.

[Mitchell Lee]

To rephrase: I don't think that the concept of a nonarchimedean normed additive group is in mathlib and it should be added

[Yakov Pechersky]

Bikeshed time -- what should the name of this be?

[Mitchell Lee]

NonarchimedeanNormedAddCommGroup

[Mitchell Lee]

Oh

[Mitchell Lee]

Sorry, this actually is in mathlib already; it's called NonarchAddGroupNorm

[Mitchell Lee]

Well, there's that, but there doesn't appear to be a typeclass for it

[Yakov Pechersky]

It's a structure that has a "class" typeclass for functions of this shape, but not one that say "for the distinguished norm on this NormedAddGroup, that norm is NonarchFoo"

[Yakov Pechersky]

Basically, if I wanted this lemma about sums (and in the future, tsums) to hold over Z_p, Q_p, and extensions thereof, what would we want the typeclass argument to look like?

[Mitchell Lee]

Yes, you still need to add a typeclass NonarchimedeanNormedAddCommGroup that extends NormedAddCommGroup.

[Yakov Pechersky]

Another option is to make a Prop typeclass saying the metric is an ultrametric

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib4/pull/14433