Banach Space Fixed Point Theorem

Stream: Is there code for X?

[Sehun Kim]

Is there a code for Banach Fixed Point Theorem?

When I look for the Picard-Lindelof theorem, it definitely uses Banach fixed point theorem, but I don't see an independent section for the Banach space and Banach fixed point theorem.

If there is no code for it, could I add this contents to Mathlib?

Also, I want to ask whether there exists a definition for a function spaces like $C^n$ space.
I mean I know that there are already codes like ContDiff but can I make it as NormedAddCommGroup or Banach space directly?

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/fd294295c0630b58caa4d261c1d2713d084d2478/docs/100.yaml#L151

[Kenny Lau]

looks like it isn't in mathlib

[Etienne Marion]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/MetricSpace/Contracting.html#ContractingWith.fixedPoint

[Aaron Liu]

it is in mathlib I was looking at it before

[Lua Viana Reis]

Kenny Lau said:

https://github.com/leanprover-community/mathlib4/blob/fd294295c0630b58caa4d261c1d2713d084d2478/docs/100.yaml#L151

you linked Brower, but does it mean the Schauder is also not?

[Aaron Liu]

Etienne Marion said:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/MetricSpace/Contracting.html#ContractingWith.fixedPoint

yeah that

[Aaron Liu]

Lua Viana Reis said:

Kenny Lau said:

https://github.com/leanprover-community/mathlib4/blob/fd294295c0630b58caa4d261c1d2713d084d2478/docs/100.yaml#L151

you linked Brower, but does it mean the Schauder is also not?

probably there's nothing that lets you immediately conclude brouwer either

[Aaron Liu]

docs#ContractingWith.fixedPoint_isFixedPt and docs#ContractingWith.fixedPoint_unique is the fixed point and the uniqueness

[Lua Viana Reis]

I thought Schauder had a simple proof, I could not be more mistaken

[Sehun Kim]

Oh, Thanks. That was what I wanted to find. docs#ContractingWith.fixedPoint_isFixedPt But is there a notion for
C^n(B) space as Banach space? I think it would be useful to prove other things

[Sehun Kim]

where B is compact in Euclidean space

[Aaron Liu]

I see docs#ContMDiffMap

[Aaron Liu]

The M is for Manifold

[Sehun Kim]

Thanks. Where should I find was Differential Geometry part.