Zulip Chat Archive

Stream: maths

Topic: Lipschitz stuff


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

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

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

view this post on Zulip Sebastien Gouezel (Mar 04 2019 at 15:14):

Done.

view this post on Zulip Patrick Massot (Mar 04 2019 at 15:27):

I love it

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

view this post on Zulip Johannes Hölzl (Mar 05 2019 at 08:19):

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

view this post on Zulip Patrick Massot (Mar 05 2019 at 08:29):

Let's merge it then!


Last updated: May 12 2021 at 08:14 UTC