Zulip Chat Archive

Stream: maths

Topic: Lipschitz stuff

Patrick Massot (Mar 04 2019 at 14:11):

Sébastien, since you are here: did you have a look at https://github.com/leanprover-community/mathlib/blob/master/src/topology/metric_space/lipschitz.lean? Is there anything you could simplify or factor out, using your latest commits?

Sebastien Gouezel (Mar 04 2019 at 14:19):

The end of the argument could be simplified a little bit, yes, just controlling the distance between f^n x and f^(n+1) x to get a simpler statement than dist_bound_of_contraction, and then using a recent commit to mathlib to deduce that it is a Cauchy sequence. This would shave off maybe 15 lines. I'll do it when I have some time...

Patrick Massot (Mar 04 2019 at 14:21):

Ok, this is exactly what I expected, but I guess it will be easier to do for you

Sebastien Gouezel (Mar 04 2019 at 15:14):

Done.

Patrick Massot (Mar 04 2019 at 15:27):

I love it

Patrick Massot (Mar 04 2019 at 15:54):

@Rohan Mitta @Alistair Tucker @Johannes Hölzl maybe I should point out that what Sébastien did was not really changing the proof. He mostly removed duplication of efforts. The complexity that used to be in the lipschitz file is now in https://github.com/leanprover-community/mathlib/commit/108486871aa0a7f0afd221c191766e9bebefde82

Johannes Hölzl (Mar 05 2019 at 08:19):

Yes! I love this kind of de-duplication / reuse / abstraction!

Patrick Massot (Mar 05 2019 at 08:29):

Let's merge it then!

Last updated: Dec 20 2023 at 11:08 UTC