Zulip Chat Archive

Stream: maths

Topic: notation for nnnorm


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Ruben Van de Velde (Mar 10 2021 at 18:31):

I guess not if lean-liquid uses it already

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

Please don't do that :-)

view this post on Zulip 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?

Please don't do that :-)

view this post on Zulip Johan Commelin (Mar 10 2021 at 18:52):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 10 2021 at 18:53):

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

view this post on Zulip 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.

view this post on Zulip 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