Zulip Chat Archive

Stream: new members

Topic: Fixed point


view this post on Zulip Alistair Tucker (Nov 21 2018 at 14:00):

I'd like to define a function E from ℝ^n to ℝ^n as the fixed point of a contraction mapping (or equivalently I think as the solution to a variational inequality). Is this easy to do? What files should I be looking at?

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 14:16):

One of my students proved the contraction mapping theorem for metric spaces... @Luca Gerolla did you ever PR this?

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:16):

It's currently not easy. There is a pending PR on contraction mapping, but I don't remember what is proved there exactly

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:16):

https://github.com/leanprover/mathlib/pull/428

view this post on Zulip Alistair Tucker (Nov 21 2018 at 14:19):

Thanks! I'll have a look at that but if it's not easy I might just declare it as a constant :)

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:20):

That PR needs to be reworked to use https://github.com/leanprover/mathlib/commit/4a013fb04d6e504be8582ad610016d8dcce3e5f3

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:20):

and probably extract more lemmas out of the big proofs

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

compare https://github.com/leanprover/mathlib/pull/428/files#diff-6f3fee1c28d757f0199c3512ffc8e5e9R83 and https://github.com/leanprover/mathlib/commit/4a013fb04d6e504be8582ad610016d8dcce3e5f3#diff-5edb379056f11c116887dcff6e8bed0dR366 for instance

view this post on Zulip Alistair Tucker (Nov 21 2018 at 14:22):

If I think I can help with that I will but I suspect it'll be beyond me.

view this post on Zulip Sebastien Gouezel (Nov 21 2018 at 14:22):

Yes, I think everything in the file analysis/topology/metric_sequences.lean of the PR is now already in the library. But the result on the Banach contraction is not.

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:23):

Alistair, updating that PR in order to replace stuff that came to mathlib in the meantime should be a nice exercise

view this post on Zulip Patrick Massot (Nov 21 2018 at 14:24):

Refactoring the big proof is much more difficult

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 17:54):

Luca reminds me that it was in fact @Rohan Mitta who was doing the contraction mapping theorem.


Last updated: May 06 2021 at 21:09 UTC