Fixed point

Stream: new members

[Alistair Tucker]

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?

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Alistair Tucker]

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

[Patrick Massot]

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

[Patrick Massot]

and probably extract more lemmas out of the big proofs

[Patrick Massot]

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

[Alistair Tucker]

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

[Sebastien Gouezel]

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.

[Patrick Massot]

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

[Patrick Massot]

Refactoring the big proof is much more difficult

[Kevin Buzzard]

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