Extending Functional Analysis Coverage

Stream: mathlib4

[Michal Swietek]

Hello everyone,

My name is Michał Świętek. Several years ago, I worked in the geometry of Banach spaces before transitioning to a business career. I am now looking to shift back closer to the theoretical side and contribute to the Lean community.

I'm deeply impressed by the state of mathlib, but I feel that Functional Analysis and the Geometry of Banach spaces are currently underrepresented compared to areas like Algebra or Classical Analysis. I would like to express my strong interest in focusing my contributions on this branch of the library. I am currently seeking guidance on the best way to start, but here are my proposed initial contributions:

• Formalize Missing Core Theorems: I want to start by tackling foundational theorems from the 1000+ Theorems list. My top priorities are:

  1. Basic properties and charactrizations of reflexive Banach spaces including Goldstine's Theorem.
  2. Eberlein–Šmulian Theorem: Relating different kinds of weak compactness.
  3. Fixed Point Theorems: Generalizing results like Brouwer's theorem to Banach spaces.

• Work on Open Issues: I plan to review Functional Analysis-related issues and documentation TODOs on GitHub. I've seen several TODOs in the API Documentation.

• Review PRs: I'd be happy to offer my mathematical expertise to review PRs related to functional analysis concepts, though I recognize this may be a better activity once I am more familiar with mathlib's conventions.

I'm new to the process of contributing to a large repository like mathlib. I would greatly appreciate any guidance from core contributors, especially those familiar with the functional analysis library's current structure and priorities.

[Ruben Van de Velde]

Welcome! How much experience do you have with lean?

[Michael Rothgang]

Everybody is welcome to review pull requests, no matter your experience. This page https://leanprover-community.github.io/contribute/pr-review.html gives some hints as to why: don't worry if you don't know about all of this; even partial reviews are helpful.

[Michael Rothgang]

@Filippo A. E. Nuccio is working on Goldstine's theorem, if I remember correctly.

[Michal Swietek]

Ruben Van de Velde said:

Welcome! How much experience do you have with lean?

Just finished working through tutorials: Mathematics in Lean and Theorem Proving in Lean.

[Filippo A. E. Nuccio]

Hi @Michal Swietek ! Indeed, I' m working on proving Millman-Pettis in #28693 (it contains a proof of Goldstine actually, but I need to polish it a bit to finalise MP). Perhaps 2. is more interesting/urgent than 1. which I hope to close soon.

[Michal Swietek]

Great to hear that! Would you consider pushing Goldstine Theorem in separate PR as it's of independent interest and could be used in basic theory of reflexive spaces? I'd be happy to review such a PR :)

[Filippo A. E. Nuccio]

Sure (it was not actually done by me, as you can see in the PR): I will try to push it next week, I'm at a conference today+tomorrow.

[Michal Swietek]

Ok, so plan for me is then:

• go through the list of open PRs and see if I can review some,
• wait for Goldstine Theorem PR by @Filippo A. E. Nuccio,
• start pondering the structure for Eberlain-Smulyan contribution.

Thank you all for swift responses :)

[Kevin Buzzard]

Are we at the point where we can state the Eberlein–Šmulian Theorem? That would be an interesting start; stating theorems idiomatically is surprisingly hard and people here would I'm sure be happy to help.

[Michal Swietek]

I don't know exactly but after briefly familiarizing myself with the state of the theory already formlized my guess is that some preparatory work is needed to just state the theorem.

[Michal Swietek]

Let me delve then in the topic and I'll come back with some plan and questions.

[Kevin Buzzard]

You should start by reading a bunch of docstrings (the text at the top of the files in the documentation, like the stuff at the top of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Operator/Completeness.html) and please let us know (or even better make a pull request) if anything is unclear!

[Michal Swietek]

I sure do, thanks for the link!

[Kevin Buzzard]

actually that is a pretty poor docstring, apologies, I just chose a random file about Banach spaces; you can click around on the files on the left to see if you can find anything more interesting! Also perhaps of use to you are semantic search tools such as https://leandex.projectnumina.ai/ -- here you just literally type in natural language what you're looking for and it will attempt to find relevant theorems and definitions.

[Moritz Doll]

Also improving docstrings would be greatly appreciated. If it is related to functional analysis/PDEs I am very happy to review documentation PRs.

[Michal Swietek]

No worries @Kevin Buzzard, I understood the link as "go there and hop around to familirize with current state" :)

[Michal Swietek]

I didn't know about the tool from numina project, looks quite handy, thanks!

[Jireh Loreaux]

I don't think we need any special tools to state Eberlein–Šmulian. We already have docs#WeakSpace.

[Jireh Loreaux]

and we have all the tools to follow the elementary proof

[Michal Swietek]

That seems right. But there are two more options:

1. Introduce some theory of basic sequences and use them to prove the Eberlein-Šmulian Theorem following Pełczyński proof as described in Albiac–Kalton, Topics in Banach Space Theory (GTM 233), Corollary 1.6.4, page 24. Basic sequences are a very popular tool in the Geometry of Banach spaces so are of independent interest.
2. Prove the more general Eberlein-Šmulian-Grothendieck Theorem in the setting of point-wise continous functions on a compact topological space. See Fabian at al. Banach Space: Theory The Basis for Linear and Nonlinear Analysis, Theorem 3.58, page 107.

[Michal Swietek]

The first require more preliminary work but then proof is nicer and as a side effect we have basic sequences formalized to some extent. The second, is more general but I'm not sure how much of underlying theory is already formalized, haven't dug there yet.

[Michal Swietek]

The question is then what do you believe is the best approach :)

[Jireh Loreaux]

(aside: I've always disliked the "basic sequence" terminology, and personally I would prefer if we could go with something like SchauderBasis or SchauderBasisOn.)

[Jireh Loreaux]

Unless you have a something that needs Eberlein-Šmulian now, then I think it would be better to wait and develop the general tools for Banach spaces.

On the other hand, proving a theorem (as opposed to developing definitions and API) is often a much better way to get your feet wet with formalization.

[Michal Swietek]

My personal preference would be to develop the theory of Schauder bases as I used it in my own work back in the day and later prove Eberlein-Smulian theorem unless there is a strong need for the generalized version.