# Zulip Chat Archive

## Stream: maths

### Topic: analysis refactor

#### Patrick Massot (Aug 21 2018 at 21:04):

@Johannes Hölzl If you have some time, I'd be interested to know what is the big plan underlying your recent mathilb commits

#### Johannes Hölzl (Aug 21 2018 at 21:06):

Cleanup ennreal, and enhance nnreal. Change metrics and norms to nnreal.

#### Johannes Hölzl (Aug 21 2018 at 21:06):

Another idea is to use Galois connections as cheap categorical constructions

#### Patrick Massot (Aug 21 2018 at 21:07):

Didn't @Sebastien Gouezel make a convincing point of not doing that?

#### Patrick Massot (Aug 21 2018 at 21:07):

Where do you want to add Galois connections?

#### Johannes Hölzl (Aug 21 2018 at 21:09):

Galois connections are already there. I "lift" along the `generate`

/ `sets`

Galois connection (`generate g`

produces the smallest filter/topology/measurable sets containing `g`

, `sets`

is the forgetful functor).

#### Johannes Hölzl (Aug 21 2018 at 21:10):

This allows me to lift the complete lattice structure on `set`

to topologies, filters, and measurable spaces. They were there before, but now we have a nicer construction.

#### Johannes Hölzl (Aug 21 2018 at 21:10):

For `nnreal`

I need to look at Sebastians argument again.

#### Patrick Massot (Aug 21 2018 at 21:11):

I know Galois connections are already there, I used filters quite a lot. I as asking about new uses.

#### Patrick Massot (Aug 21 2018 at 21:12):

(and I think I like the answer)

#### Johannes Hölzl (Aug 21 2018 at 21:18):

I need to look at Sebastians argument more concretely. `dist`

and `norm`

will always return nonnegative numbers. So the difference is only that we pack this proof into the result type. Subtracting on `nnreal`

and `ennreal`

is very ugly, but I don't see how this appears in a concrete case.

#### Patrick Massot (Aug 21 2018 at 21:20):

From https://github.com/leanprover/mathlib/pull/208#issuecomment-406893134 it's not hard to see where Sébastien encountered that

#### Patrick Massot (Aug 21 2018 at 21:21):

https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html

#### Reid Barton (Aug 21 2018 at 21:27):

`abs(dist e a - dist e b)`

But surely `nnreal`

is a metric space too? Why not just write `dist (dist e a) (dist e b)`

?

#### Reid Barton (Aug 21 2018 at 21:29):

More generally, faced with a problem of the form "I have to do X a lot", maybe it's better to write a small convenience function to do X rather than distorting the underlying theory to avoid needing to do X.

#### Patrick Massot (Aug 21 2018 at 21:34):

Maybe "distorting the underlying theory" is a bit exaggerated here. But really I have no idea about what should be done. I can only see that Sébastien did quite a lot of Gromov hyperbolic spaces in Isabelle, so this is a really concrete and battle tested opinion.

#### Reid Barton (Aug 21 2018 at 21:36):

Fair enough. In this case, it's not uncommon to see $d(x, y) \ge 0$ stated as an axiom of a metric space

#### Mario Carneiro (Aug 21 2018 at 22:00):

It's also not uncommon to see $d:X\times X\to[0,\infty)$. Honestly I don't think mathematicians have a mental structure that allows them to even distinguish these approaches, so I don't consider this good evidence in either direction

#### Reid Barton (Aug 21 2018 at 22:16):

I wonder whether it would help to have `has_sub a b`

with `sub : a -> a -> b`

with instances like `nat int`

and `nnreal real`

#### Reid Barton (Aug 21 2018 at 22:16):

Or an affine space / vector space

#### Mario Carneiro (Aug 21 2018 at 22:16):

You can always write `(a - b : int)`

where `a b : nat`

#### Mario Carneiro (Aug 21 2018 at 22:17):

same for `nnreal`

and `real`

#### Mario Carneiro (Aug 21 2018 at 22:17):

indeed this is what I recommend if you want proper subtraction on one of these partial subtraction domains

#### Sebastien Gouezel (Aug 22 2018 at 07:46):

The most basic object in hyperbolic spaces is the Gromov product of two points `x`

and `y`

with basepoint `e`

, defined as `(d(e, x) + d(e, y) - d(x,y))/2`

. And one keeps computing with such objects, adding, subtracting or comparing them. All these computations are really much more convenient in reals than nnreals, although I guess they could most of the time be done in nnreals, at the price of making the proofs much more painful (for instance, in the definition of the Gromov product, the triangular inequality shows that `d(x, y) ≤ d(e,x) + d(e,y)`

, so that the definition in reals or nnreals gives the same result, at least if one parenthesises the expression correctly).

In fact, at the beginning I defined the Gromov product to be in `nnreal`

, but later on I had to refactor everything as it made things uselessly complicated.

For the general issue, making distances and norms take values in `nnreal`

would mathematically be the right thing to do. But I am not convinced that the benefits outweigh the difficulties in applications. As a middle ground, one could have two functions `nndist`

and `dist`

. Another related question is to have distances even taking values in `ennreal`

. I think this is important to have, for instance to define the graph distance on a non-connected graph, or the `L^2`

norm of a function which is not square-integrable (these are two real-life problems that I met in Isabelle and where I was stuck with the current hierarchy). Maybe a class `emetric_space`

with distances taking values in `ennreal`

(this is enough to define for instance a uniform structure, a topology, and so on), and a subclass `metric_space`

in which the distance only takes finite values?

#### Reid Barton (Aug 22 2018 at 14:32):

Thanks for the more detailed example. Having both `nndist`

and `dist`

is a good option, in which case it may not even matter which of `dist`

or `nndist`

is taken to be part of the defining structure of a metric space. The potential cost is wanting two versions of all the lemmas about `nndist`

/`dist`

, but this kind of problem I feel could be solvable in the long run with better tools.

#### Reid Barton (Aug 22 2018 at 14:33):

Also totally agree with your second paragraph. An even more basic example is the extended metric space of (not necessarily bounded) functions from a given set to a given metric space, with the sup/uniform metric.

Last updated: May 19 2021 at 02:10 UTC