Formalising big results in functional analysis

Stream: maths

[Esteban Martínez Vañó]

Hi everyone.

I'm starting a project with some colleagues about formalasing some big results in functional analysis (we haven't decided yet which ones exactly) so I'd like to know the state of art of this branch in Lean.

I know that basic theorems (Hahn-Banach, Alaoglu-Bourbaki, uniform boundness) are introduced and I've also seen weak topologies are introduced (btw, I've formalized Mazur's theorem about convex closed sets in some generality, so I'll open a new post to discuss it and to try to upload it to mathlib), that ℓp-spaces are also included and that Lp-spaces are, although it is not proven they are complete with the Lp-norm, isn't it?

I'm missing something important?

For example, a first baby step for us is to fomalize completeness characterization in terms of absolutely convergent series and the open map and closed graph theorems. Are these results already in mathlib?

Anyway, thanks for your time.

[Etienne Marion]

Completeness is formalized: docs#MeasureTheory.Lp.instCompleteSpace

[Yaël Dillies]

Open map and closed graph too are done

[Esteban Martínez Vañó]

Okay, thank you!

[Floris van Doorn]

Take a look at the library overview: https://leanprover-community.github.io/mathlib-overview.html
The open mapping theorem is listed there (the closed graph theorem is not).