Zulip Chat Archive

Stream: maths

Topic: analysis refactor


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

view this post on Zulip Johannes Hölzl (Aug 21 2018 at 21:06):

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

view this post on Zulip Johannes Hölzl (Aug 21 2018 at 21:06):

Another idea is to use Galois connections as cheap categorical constructions

view this post on Zulip Patrick Massot (Aug 21 2018 at 21:07):

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

view this post on Zulip Patrick Massot (Aug 21 2018 at 21:07):

Where do you want to add Galois connections?

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

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

view this post on Zulip Johannes Hölzl (Aug 21 2018 at 21:10):

For nnreal I need to look at Sebastians argument again.

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

view this post on Zulip Patrick Massot (Aug 21 2018 at 21:12):

(and I think I like the answer)

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

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

view this post on Zulip Patrick Massot (Aug 21 2018 at 21:21):

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

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

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

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

view this post on Zulip Reid Barton (Aug 21 2018 at 21:36):

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

view this post on Zulip Mario Carneiro (Aug 21 2018 at 22:00):

It's also not uncommon to see d:X×X[0,)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

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

view this post on Zulip Reid Barton (Aug 21 2018 at 22:16):

Or an affine space / vector space

view this post on Zulip Mario Carneiro (Aug 21 2018 at 22:16):

You can always write (a - b : int) where a b : nat

view this post on Zulip Mario Carneiro (Aug 21 2018 at 22:17):

same for nnreal and real

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

view this post on Zulip Sebastien Gouezel (Aug 22 2018 at 07:46):

The most basic object in hyperbolic spaces is the Gromov product of two points xand 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?

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

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