analysis refactor

Stream: maths

[Patrick Massot]

@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]

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

[Johannes Hölzl]

Another idea is to use Galois connections as cheap categorical constructions

[Patrick Massot]

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

[Patrick Massot]

Where do you want to add Galois connections?

[Johannes Hölzl]

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]

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]

For nnreal I need to look at Sebastians argument again.

[Patrick Massot]

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

[Patrick Massot]

(and I think I like the answer)

[Johannes Hölzl]

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]

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

[Patrick Massot]

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

[Reid Barton]

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]

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]

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]

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]

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]

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]

Or an affine space / vector space

[Mario Carneiro]

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

[Mario Carneiro]

same for nnreal and real

[Mario Carneiro]

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

[Sebastien Gouezel]

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?

[Reid Barton]

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]

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.