Generalization of Banach Steinhaus Theorem

Stream: new members

[Szymon Kubica]

Hello,
I'm Simon and I've recently started working with lean as a part of an undergraduate course at Imperial College London ran by @Kevin Buzzard. I've been trying to formalise the generalised Banach-Steinhaus theorem for barrelled spaces which was mentioned in the TODO next to the regular statement of the theorem. Up to this point I've managed to prove the regular version of the theorem to get some experience working with the concepts required to prove things in functional analysis. When it comes to the generalisation, I found a proof of it in this book:
Bourbaki, Nicolas (1987) [1981]. Topological Vector Spaces: Chapters 1–5. Éléments de mathématique. Translated by Eggleston, H.G.; Madan, S. Berlin New York: Springer-Verlag. ISBN 3-540-13627-4. OCLC 17499190.
It was the theorem 1 in the second part of the chapter 3 to be precise.
I wanted to ask about the current state of the library with respect to barrelled spaces and notions used in the proof. In the attached file you can find a statement of the theorem, its proof and a list of things that are needed to prove it together with the parts that I've been able to find in mathilb.
Is there some theory already in place in mathilb regarding barrelled spaces which I wasn't able to find? When it comes to the recommended way of contributing to mathilb, I found this guide which was helpful: https://leanprover-community.github.io/contribute/index.html . Would you be able to recommend some specific approach and possibly indicate the most common mistakes when contributing so that I can avoid those?

Thank you,
Simon GeneralisedBanachSteinhaus.pdf

[Moritz Doll]

I think @Anatole Dedecker worked on this.

[Anatole Dedecker]

Thanks for pinging me Moritz.
Szymon, indeed I was working on this precise theorem a few months ago. Unfortunately I have not had a lot of time to finish and PR it (but I will have in precisely three weeks), but I have everything either ready of precisely planned, so I don’t think it makes much sense for someone else to start working on a proof in parallel (in particular because I will deviate a bit from Bourbaki to allow vector spaces over other fields).
I realize that it’s probably a bit annoying for you to realize that someone else is already working on this without leaving any clue about it, and I’m sorry for that.
I’m not quite sure what to do in this situation @Kevin Buzzard. Do you want suggestions of other targets in this area? Maybe I could also try to clean my PRs and leave enough instructions for Szymon to finish the work?

[Kevin Buzzard]

Szymon: For barrelled spaces the easiest way to search is to go to the mathlib API docs, type barrelled into the search bar, and hit "google site search". You'll see that there's nothing there -- the only mention is in the TODO which you already know about.

@Anatole Dedecker , Szymon will be handing in his final project in 3 days, my personal main concern is that they get that finished; but for that project it doesn't matter at all if there is overlap with your work. If Szymon wants to continue doing Lean after that time then this would be great.

[Anatole Dedecker]

Looking at the PDF, it seems that your target is not exactly the one that I had, and that in your setting you actually only need the Banach-Steinhaus theorem for complete normed spaces, which we already have (and which you have proved too IIUC), so there may actually not be that much overlap if you only want to prove the theorem in this file (I think you won’t even need barelled spaces in this case), so I guess that’s fine in the end. I will answer some of your other questions later, right now I’m on mobile so it’s a bit painful…

[Szymon Kubica]

@Anatole Dedecker Thank you for your replies and thorough explanation of the situation. First of all I wanted to indicate that it isn't a problem at all that you've been working on that theorem in the past. That's why I asked my question to see if there is any work in progress. I understand that there is no point in duplicating the work, however from the perspective of the project that I'm working on (the one Kevin mentioned) it is not a problem if the theorems that I prove are already implemented in the library or if someone more experienced is currently working on them. My objective is to gain experience using lean and try to get to a point where I could contribute to the library. In this case, the project that I'm working on right now is more of an exploration and I didn't expect to get it to a state where it could be merged into the library (given the time constraint that I have). However, in the future I plan to continue working on this and possibly contribute to mathlib repo.

[Jireh Loreaux]

@Szymon Kubica to answer some of your library questions in your pdf:

1. vector space generated by a set is listed as docs#submodule.span (this takes a subset of a vector space and returns the smallest subspace containing that set).
2. A Hausdorff space is a docs#t2_space
3. LCTVS is docs#locally_convex_space and you can build one by providing a suitable family of seminorms using docs#with_seminorms.to_locally_convex_space
4. That the guage is a seminorm is given by docs#guage_seminorm.
5. I'm not exactly sure what you mean by "complete bounded disk". Do you mean a Banach disk? If so, I don't think we have those, but they shouldn't be too hard to create from the pieces above. Importantly, you will need a type synonym so that you can put a different (semi)norm on the docs#submodule.span than the one it naturally inherits as a subspace.

[Jireh Loreaux]

and I just realized that you already knew some of these. :face_palm:

[Szymon Kubica]

Hi Jireh,
Thank you for taking your time to answer my questions. I really appreciate it. Thank your for the t2_space in particular, I had quite a lot of trouble looking for Hausdorff spaces in mathlib, the only things that I could find were Is_Hausdorff and Gromov_Hausdorff.GH_space and neither of those looked like the thing I was looking for. I should be able to pick up from here. Thanks

[Kevin Buzzard]

@Szymon Kubica for future information: the way to find Hausdorff spaces in mathlib is to go to the API docs, type "Hausdorff" into the search bar and then click on "Google site search" and ponder over the options. It's about seven hits down but you'll see "t2_space : A T₂/Hausdorff space is a space where, for every two points x ≠ y , there is two disjoint open sets, one containing x , and the other y ..."

[Eric Wieser]

Searching the docs for "as a hausdorff space" (not the site search) also finds a result, not that you would expect to search for that