## Stream: maths

### Topic: notation for nnnorm

#### Johan Commelin (Mar 10 2021 at 18:22):

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 (Mar 10 2021 at 18:23):

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 (Mar 10 2021 at 18:23):

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

#### Eric Wieser (Mar 10 2021 at 18:28):

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 (Mar 10 2021 at 18:28):

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 (Mar 10 2021 at 18:28):

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 (Mar 10 2021 at 18:31):

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

#### Ruben Van de Velde (Mar 10 2021 at 18:31):

I guess not if lean-liquid uses it already

#### Johan Commelin (Mar 10 2021 at 18:41):

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 (Mar 10 2021 at 18:48):

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 (Mar 10 2021 at 18:48):

Johan Commelin said:

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

#### Sebastien Gouezel (Mar 10 2021 at 18:49):

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?

#### Johan Commelin (Mar 10 2021 at 18:52):

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

#### Johan Commelin (Mar 10 2021 at 18:52):

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 (Mar 10 2021 at 18:53):

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

#### Sebastien Gouezel (Mar 10 2021 at 19:41):

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 (Mar 10 2021 at 20:03):

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

Last updated: May 19 2021 at 02:10 UTC