what's the status of random matrix theory?

Stream: maths

[Yuxi Liu]

I want to formalize some basic results from RMT to lean after getting burnt from errors. What's the status of RMT in lean mathlib4? Can I just take a standard textbook like Terence Tao's topics in matrix theory and start formalizing them?

[Yaël Dillies]

(this would better be in #maths or #general)

[Notification Bot]

This topic was moved here from #lean4 > what's the status of random matrix theory? by Kim Morrison.

[Kim Morrison]

Yes, mostly we are ready to do this. You'll run into the fact that the CLT is not quite done yet, c.f. https://remydegenne.github.io/CLT/index.html and check in with @Rémy Degenne to see where things are at / if contributions are wanted there.

[Rémy Degenne]

I'd say that Mathlib is mostly ready: you can start formalizing things from that book and should not lack any significant prerequisite.

About the CLT

There are various people working on parts of what's needed for the CLT proof sketched in the repository https://github.com/RemyDegenne/CLT right now. It's quite decentralized, and most of them don't do it in the repository I created, and probably do their work for other reasons. That repository does not reflect at all the current progress, don't refer too much to it.

• Defining characteristic functions and proving properties of separating algebras is done in a series of Mathlib PRs by Jakob Stiefel (see that link for their PRs: https://github.com/leanprover-community/mathlib4/pulls/JakobStiefel)
• Thomas Zhu pushed a bunch of things to my repo, mostly about proving the CLT itself once other theorems are done, and not all of them are reflected in the blueprint.
• There are Mathlib PRs for the Riesz-Markov-Kakutani theorem, by Yoh Tanimoto. See for example https://github.com/leanprover-community/mathlib4/pull/12290
• Josha Dekker has an old PR to Mathlib about tight measures
• One piece that is still missing is Prokhorov's theorem about tightness of measures and relative compactness. The idea was to prove it from RMK.
  I was asked about the progress of the CLT by @Arav Bhattacharyya a month ago and I suggested that Prokhorov's theorem could be a cool project. I don't know if they are working on that in the end or not.

After those various PRs land in Mathlib and after proving Prokhorov's theorem, most (all?) of the pieces of the puzzle should be there for the CLT.

About other related topics

I looked briefly at Tao's book on random matrix theory. The preliminaries mention many non-asymptotic techniques for proving concentration of measures that don't need the CLT.

• We should have all the tools needed for the moment methods, even if we might not have the results themselves.
• You can see an example of the truncation technique in our proof of the strong law (by Sébastien Gouëzel), https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/StrongLaw.html
• I recently added some results about moment generating functions and I am currently preparing PRs for concentration of sub-Gaussian random variables (#21387), and Kei TSUKAMOTO has an open PR for Hoeffding's lemma showing that bounded random variables are sub-Gaussian.

[Rémy Degenne]

I also quite like Vershynin's book High Dimensional Probability for concentration of random vectors and matrices. You could also formalize things from that one.

[Yaël Dillies]

Am I right in saying that we want Prokhorov to generalise and upstream the result from PFR that probability measures on a compact space are compact?

[Edward van de Meent]

I'm personally working on proving the Free Probability version of CLT, which iiuc is somewhat related?

[Edward van de Meent]

(i'm not an expert in this topic, i'm doing this because it seemed like a feasible project)

[Rémy Degenne]

Yaël Dillies said:

Am I right in saying that we want Prokhorov to generalise and upstream the result from PFR that probability measures on a compact space are compact?

If I recall correctly the proof of that result in the general case needs the RMK theorem but not necessarily Prokhorov (and can be a step towards the proof of Prokhorov's theorem).

[Arav Bhattacharyya]

I am indeed working on Prokhorov!

[Josha Dekker]

As Rémy said, I have an old PR defining (among others) tightness of measures, mainly following definitions from Weak Convergence and Empirical Processes by van der Vaart and Wellner. I'm currently caught up in work for my PhD, so I don't have time to return to this one. I'm very sorry for letting this grow (so) stale...

I've labelled it please-adopt for now as I'm happy to let someone take over, but please also feel free to skim through it and extract what you need; if I have time in the future (which won't be in the foreseeable future), I'll check what has been used and try to add the remainder! The PR is #12394. It went up to Ulam's tightness theorem and defines pre-tight measures and tight measures.

[Rémy Degenne]

I extracted the definition of a tight measure from your PR and opened #21955. I also added a definition of a tight set of measures in there.

[Thomas Zhu]

Rémy Degenne said:

• Thomas Zhu pushed a bunch of things to my repo, mostly about proving the CLT itself once other theorems are done, and not all of them are reflected in the blueprint.

I would really like to update the CLT blueprint to reflect the current theorems proved, as well as these dependencies listed on other projects / Mathlib PRs, so more people can more easily see the status or potentially get involved. However, I am not familiar with how the blueprint should be set up, and I ran into a problem that I haven't found time to look into.

[Thomas Zhu]

For RMT, I guess it would be safe to use sorry for the CLT statement for now.

[Thomas Zhu]

Rémy Degenne said:

After those various PRs land in Mathlib and after proving Prokhorov's theorem, most (all?) of the pieces of the puzzle should be there for the CLT.

Another small piece needed is Taylor's theorem on ℝ → ℝ in Peano form. This is recently done in #19796 by @Tian Chen .

[Yaël Dillies]

@Thomas Zhu, when you find time, I am happy to hop on a call to explain blueprints to you

[Rémy Degenne]

An issue is that the blueprint setup of my CLT repository is ancient. The blueprint did not build for me either when I tested it on a new computer with an updated leanblueprint a few weeks ago. I am currently updating it (and bumping mathlib and other dependencies as well).