notation for nnnorm

Stream: maths

[Johan Commelin]

In the liquid project we make a lot of use of nnreal, and hence it's convenient to also use nnnorm. But it looks ugly.
What do people think of making

notation `∥`x`∥₊` := nnnorm x

[Johan Commelin]

We can already do this in the liquid project, but for code that is supposed to move to mathlib, I would rather not do this. Unless we also add the notation to mathlib

[Johan Commelin]

Another option (quite radical, I admit) would be to refactor mathlib so that norm takes values in nnreal.

[Eric Wieser]

How bad an idea would a has_some_norm typeclass be that instead of specifiy real or nnreal supports an arbitrary output type?

[Eric Wieser]

Then the notation could just be the same everywhere, although you'd need to give lean a few more hints about what type you're talking about

[Eric Wieser]

As an aside, your proposed notation is actually better behaved than the one for norm, as it has different opening and closing markers!

[Ruben Van de Velde]

Won't lean mind that the starting marker is already in use for plain norm?

[Ruben Van de Velde]

I guess not if lean-liquid uses it already

[Johan Commelin]

Eric Wieser said:

How bad an idea would a has_some_norm typeclass be that instead of specifiy real or nnreal supports an arbitrary output type?
Then the notation could just be the same everywhere, although you'd need to give lean a few more hints about what type you're talking about

I think you would need a lot of hints in mathlib

[Sebastien Gouezel]

Johan Commelin said:

In the liquid project we make a lot of use of nnreal, and hence it's convenient to also use nnnorm. But it looks ugly.
What do people think of making

notation `∥`x`∥₊` := nnnorm x

I think that's a very good idea!

[Sebastien Gouezel]

Johan Commelin said:

Another option (quite radical, I admit) would be to refactor mathlib so that norm takes values in nnreal.

Please don't do that :-)

[Sebastien Gouezel]

Eric Wieser said:

How bad an idea would a has_some_norm typeclass be that instead of specifiy real or nnreal supports an arbitrary output type?

Please don't do that :-)

[Johan Commelin]

@Sebastien Gouezel What do you think of decoupling the definition of nnnorm from norm?

[Johan Commelin]

Currently you can only get nnnorm if you have a normed_group. But in LTE we have gadgets that are not normed groups, but still carry a norm.

[Johan Commelin]

So I would like to have has_nnnorm, which is automatically filled in by normed_group

[Sebastien Gouezel]

We have the syntactic class has_norm. You could register a norm_nonneg class extending has_norm (which would be instantiated by all usual classes), and define nnnorm on all norm_nonneg classes.

[Sebastien Gouezel]

Or you could definitely have a has_nnnorm class if that's more convenient for you!