Missing theorems

Stream: maths

[Patrick Massot]

We already have a web page listing missing undergrad stuff but it's not so easy to read quickly. I just created a wiki page which I think is easier to read. First I'd be happy to learn that some items are actually already done. Then I think it would be really good to spend some time and energy to work on this list this year. It would be really awesome to clean it before next summer's ICM. I think some of the energy that currently goes in either much more advanced stuff or much more exotic things could go there.

[Yury G. Kudryashov]

I can work on Cauchy–Lipschitz (a.k.a. Picard–Lindelöf) theorem after integrals.

[Yaël Dillies]

I don't think I'll be able to contribute to anything on that list. However, I have some plans myself:

• Finishing Sperner's lemma. Maybe doing Brouwer's fixed point theorem or Monsky's theorem afterwards.
• Equivalence of regular expressions and DFA (probably feat Fox Thomson)
• Working towards Szemerédi's theorem. That probably includes moving Kyle's paths branch towards master.
• More maintenance stuff in order theory/convex analysis

Feel free to tell me what would be the most fashionable.

[Yury G. Kudryashov]

Please ping me before you start working on Brouwer's fixed point theorem. I'd like to discuss which proof should be formalized (but not tonight).

[Yaël Dillies]

Noted!

[Patrick Massot]

Yaël, why do you write "I don't think I'll be able to contribute"? Do you mean you won't have time or you don't know enough math? I'm pretty sure you know enough or could learn easily. For instance the group representation stuff is really elementary.

[Yaël Dillies]

I meant the conjunction of "I don't know enough maths" and "I don't know how to do those maths with mathlib". I basically never heard of group representations, but if you say that's elementary I can take that on!

[Patrick Massot]

It would really nice to have people claiming items on that list. Clearly Yury is working on complex analysis and he wrote that he can also work on ODEs after that. @Rémy Degenne do you think you can handle the law of large number and central limit theorem? @Anne Baanen do you intend to work on the classification of modules of PIDs? @Frédéric Dupuis can you do diagonalization of normal endomorphisms?

[Patrick Massot]

@Heather Macbeth do you have plans for the Fourier analysis items?

[Patrick Massot]

Yaël, finite group representation theory is a really wonderful elementary topics. There are many books where you can learn this stuff and people like @Scott Morrison already thought about how to do it in Lean.

[Rémy Degenne]

Sure, I can handle the probability theorems. I was looking at various proofs of the central limit theorem yesterday.

@Jason KY. has started proving things about real distributions, we have a definition of independence, and facts about moments could come very soon. Some version of the law of large numbers should be feasible soon.

The CLT is another beast and the usual proof uses complex analysis but there is a proof using the moment method, which should be tedious but doable: https://terrytao.wordpress.com/2010/01/05/254a-notes-2-the-central-limit-theorem/

[Eric Rodriguez]

It's not on that list but I'm working on some basic galois stuff at the moment (Gal(K(zeta)/K)) but the pace is glacial as my focus is on alectryon - when that frees up, should be done a lot quicker :)

[Anne Baanen]

Patrick Massot said:

Anne Baanen do you intend to work on the classification of modules of PIDs?

There were a few people (I recall specifically @James Arthur, @Alexey S. Vasilev, @Simon Andreys) who were interested in finishing the full classification. So I have been awaiting their contributions, unless it turns out I need the classification for my own (ideal class group) purposes.

[Sebastien Gouezel]

For the strong law, the nicest proof I know is that of Etemadi https://link.springer.com/article/10.1007%2FBF01013465, which only assumes pairwise independence.

[Patrick Massot]

About CLT, I don't think we should aim for an elementary proof, unless it gives motivation to develop probability tools that will be useful anyway. It would be really nice to precisely state what you need from complex analysis. The real test for a complex analysis library should be to prove the prime number theorem and CLT, and Dirichlet arithmetic progressions theorem

[Patrick Massot]

Note that most of the theorems I listed are real theorems, not lemmas as they do in algebra. There's a reason why the algebra part of mathlib is so much bigger than analysis.

[Patrick Massot]

I'm teaching a third year algebra course with only one theorem in a full semester (the classification of finite abelian groups). An analysis course at the same level would have existence of Lebesgue measure, Fubini, change of variables...

[Rémy Degenne]

The proof of the CLT I have in mind uses some tools that are more widely useful, like facts about convergences of random variables based on the convergence of the moments or lemmas about a reduction to the case of bounded random variables. It's also more widely generalizable than the usual (Fourier based) method.
But i agree that we should aim at being able to write that Fourier proof as well. I will check what is needed.

[Patrick Massot]

Note that I don't claim anything specific to probability theory here. I know nothing about this area of math. I wouldn't be able to state any of those probability theorems I put in the list.

[Rémy Degenne]

I think that I get your point: the proof of the CLT based on Fourier transforms is valuable as a test of another part of the library. I agree.
I also want the tools from the other proof, but we can have both :)

I must admit that I have a bias against proofs using the Fourier method and I am more familiar with moment-based techniques because my usual work focuses on applications for which moments are the only approach that works. But I can overcome that bias.

[Sebastien Gouezel]

I agree with Rémy that the Fourier proof is too specific, and that we should go for another one. What about the Stein method? :-) Joke aside, moments arguments and truncation are tools of a very general use, so this would definitely be a nice proof to have.

[Frédéric Dupuis]

Yes, I could take the diagonalization of normal endomorphisms.

[Kalle Kytölä]

For probability in general and CLT in particular, I think the proposed approaches sound good! The most standard CLT proof based on complex analysis and Fourier analysis of measures should also hopefully become doable. I apologize that PRing my proof of the Portmanteau theorem has stalled a bit (funding applications and semester got in the way of my Leaning), but I definitely plan to go ahead, so that it wouldn't be blocking one natural approach to the CLT. Not all of Portmanteau is needed for the standard CLT proof anyway, and on the other hand I have not included the $\R$-specific characterizations such as the one with the Fourier transform in what I plan to PR for now. In any case, besides the Portmanteau characterizations of convergence in distribution, for the standard proof of CLT one needs some compactness argument (Helly's selection theorem or the much more general Prokhorov's theorem). I hope to work on Prokhorov at some point in the future unless someone gets to it first (but Helly is a lot cheaper approach sufficient for the CLT).

(Btw, I think Sébastien's joke about the Stein's method for the CLT is interesting (I considered this in the past), except that the version of Stein's method I have seen does not give a proof of CLT with the optimal assumptions. It does give convergence rates, though, unlike the standard proof! Ok, this is becoming too CLT-specific, apologies! [Feel free to move to another topic.])

Anyway, I like the "Missing theorems" wiki page! :heart:

[Yaël Dillies]

I am now learning representation theory and looking into proofs of Maschke's theorem.

[Yaël Dillies]

Note however that term is starting soon and I have done ⊥ : with_bot αof the uni work I had.

[Simon Andreys]

I made some progresses on the classification of modules on PIDs last winter, but I was new to lean and I got sidetracked. I won't probably have time to work on it for the next few months, but if the theorem stays missing I may take it up again at some point.

[Julian Külshammer]

@Yaël Dillies Note that one formulatation of Maschke is already in mathlib. What is missing is rather a reformulation that one could consider part of the theory of semisimple modules, namely that a module is semisimple if and only if every submodule has a complement. This reformulation is totally independent of group algebras and holds for every algebra.

[Scott Morrison]

It seems mathlib currently just defines is_semisimple_module as a is_complemented, which is a bit lame, but in any case orthogonal to anything about Maschke's theorem and/or finite groups, so I removed Maschke from the wiki page and added it to undergrad.yaml.

[Scott Morrison]

I think a good thing to do would be to show that an isomorphism between sums of simple modules gives a bijection between summands, with each pair in bijection isomorphic. There's nothing even about modules or algebra here; it holds in any preadditive category.

[Yaël Dillies]

Oh okay. I guess I got tricked into doing category theory :rofl:
Do you have any reference for this result, Scott?

[Patrick Massot]

Yaël, you also work on orthogonality of characters which is the next step in the story.

[Patrick Massot]

Unless this is also reduced to some category theoretic statement.

[Yaël Dillies]

Naive question, why are we interested in vector spaces in particular? Is it because they are "well understood"? Or did Scott just say that actually this question is legitimate and what you need is more generally a preadditive category?

[Johan Commelin]

I think that orthogonality of characters will use at some point that we are working over an alg. closed field.

[Johan Commelin]

But please don't launch into this before wrapping up your current refactor :sweat_smile:

[Yaël Dillies]

I don't think this will slow down the convexity refactor. It is mostly in need of reviewing :upside_down:

[Scott Morrison]

Scott Morrison said:

I think a good thing to do would be to show that an isomorphism between sums of simple modules gives a bijection between summands, with each pair in bijection isomorphic. There's nothing even about modules or algebra here; it holds in any preadditive category.

@Yaël Dillies, I don't actually know a reference that does this for any preadditive category. It's easy though: the work is handling an induction. The inductive step goes as follows.

If you have a nonempty sum of simple objects isomorphic to some sum of simple objects, then must be a pair of isomorphic objects: otherwise an entire column of the isomorphism is zero, which is impossible by src#category_theory.biprod.column_nonzero_of_iso. Once you have a pair of isomorphic objects, the complements must be isomorphic by src#category_theory.biprod.iso_elim, and you can appeal to your inductive hypothesis.

[Scott Morrison]

But the Jordan-Hölder theorem also gives this result for modules, and we want that as well.

[Scott Morrison]

Oh -- and #8976 does Jordan-Holder!

[Yaël Dillies]

Wait wait wait, is there even anything left to do? :sweat_smile:

[Scott Morrison]

We haven't touched character theory at all. There is lots of good juicy stuff there!

[James Arthur]

Anne Baanen said:

Patrick Massot said:

Anne Baanen do you intend to work on the classification of modules of PIDs?

There were a few people (I recall specifically James Arthur, Alexey S. Vasilev, Simon Andreys) who were interested in finishing the full classification. So I have been awaiting their contributions, unless it turns out I need the classification for my own (ideal class group) purposes.

I am working on this, albeit slowly. My current next step is cyclic modules and proving that said decomposition is a load of cyclic modules.

[Apurva Nakade]

I don't see any complex inner product stuff and spectral theorem in the list. Has this already been done? Can't seem to find these in mathlib docs.
(I remember there being a debate about how to formalize complex inner products, but life got busy and I lost track of the discussion.)

[Heather Macbeth]

Yes, this is in progress, see #9272

[Patrick Massot]

It's in the list, part of the bilinear algebra item

[Frédéric Dupuis]

Apurva Nakade said:

I don't see any complex inner product stuff and spectral theorem in the list. Has this already been done? Can't seem to find these in mathlib docs.
(I remember there being a debate about how to formalize complex inner products, but life got busy and I lost track of the discussion.)

Complex inner products have been in mathlib for about a year now, in the form [inner_product_space ℂ E]. We just added semilinear maps a few days ago, so we should be defining the adjoint properly very soon and the spectral theorem shouldn't be too far behind.

[Apurva Nakade]

Thanks! This is exciting!! Spectral theorem will open up the door to so much cool math.

[Tony Wang]

@Rémy Degenne How is the progress on the the CLT and the LLN? Those are two theorems I find very cool and I would love to help with their formalization.

[Kalle Kytölä]

Before Rémy answers, let me already point out a few things...

There has been some discussion about LLN. At least a proof following Terry Tao's blog has been considered, but it might be that a martingale proof is in some people's mind; note that martingales have been defined already. I don't know if anyone has started either of these LLN proofs, though.

For the CLT, we don't yet have even convergence in distribution, but that is hopefully on its way in #9430 and #9943. With that and a definition of Gaussian measures, at least stating the CLT properly should become possible. After these PRs, I would be trying to follow up with the portmanteau theorem, but the characterization by characteristic functions is not included in my draft. It seems to me more Fourier analysis would be needed for that (at least Lévy's inversion theorem). You probably already saw the main proposals in this thread, which were not the standard Fourier-based proofs. Also proving CLT by Stein's method would not require Fourier analysis (but I don't think that option was entertained seriously). Again, I don't really know if anyone has started except that I'm slowly trying to bring in the basics of convergence in distribution.