Status of the project

Stream: Brownian motion

[Rémy Degenne]

Main goal

We want to define a Brownian motion on the positive real line, which is a central object in probability.
The Brownian motion or Wiener process is a stochastic process with specific finite-dimensional distributions (which are Gaussian) and the property that its paths are continuous.

Project overview

The project contains two mostly independent parts, that we then bring together to finish the construction:

• the first part contains results about Gaussian distributions. Mathlib does not have multivariate Gaussians yet, and we need those. Most lemmas in that part are standard properties of Gaussians and should not be hard to prove, but the blueprint is missing several proofs and some lemmas don't have Lean statements yet. At the end of that part, we use the Kolmogorov extension theorem to build a process that we call pre-Brownian with the right distribution but without the property of continuous paths.

• the second part is a Kolmogorov-Chentsov type continuity theorem, which will give us the existence of a modification of the pre-Brownian with continuous paths. The blueprint mostly follows a recent paper [1] that contains a general form of the continuity theorem for metric spaces, instead of a more usual version specialized to R^d. The proof uses Talagrand's chaining techniques.
  That second part is different in nature to the first: this is a long list of lemmas that each depend on the previous ones to advance the proof. The blueprint for that part is much more advanced, and most results have also been stated in Lean and are only waiting for a proof.

Here is a list of notable results to help you explore the dependency graph:

• isGaussian_multivariateGaussian. The measure that we call a multivariate Gaussian is actually a Gaussian.
• isProjectiveMeasureFamily_gaussianProjectiveFamily. A particular family of Gaussian measures is projective, which allows us to use the Kolmogorov extension theorem to build the pre-Brownian process.
• pair_reduction. A statement about finite sets in a metric space that has nothing to do with stochastic processes or probability. It's the result of a self-contained mini-project and is then used as a black-box.
• finite_set_bound, which uses mainly finite_set_bound_of_dist_le. The main technical results on the Kolmogorov-Chentsov side of the project. Every lemma needed for its proof has a formalized statement.
• holder_modification. The existence of a modification with Hölder continuous paths, which is what we want to use to build a Brownian motion.
• brownianMotion. The definition of the Brownian motion. The end of the blueprint near that definition needs more work.
• ContinuousMap.borel_eq_iSup_comap_eval. A statement about the equality of two sigma-algebras on the space of continuous functions. Independent of everything else. It allows us to use the Brownian motion process to get a measure on the Borel space of continuous functions.

We invite anyone interested to have a look at the project, pick something they want to do, announce it in the Tasks and claims topic and open a PR!

Remarks:

• Contributions to both the blueprint and the code are welcome.
• Everything in that project should eventually be in Mathlib. Please make PRs to Mathlib regularly.
• Feel free to remove or add hypotheses from the lemma statements. Perhaps an hypothesis exists only to avoid an edge case that is actually fine because of Lean's default values, perhaps a measurability hypothesis needs to be added... If you're not sure, don't hesitate to talk about it in this channel.
• For distances and integrals, we work in ENNReal as much as possible: use edist, EMetric.diam, the Lebesgue integral and not the Bochner integral, etc.
• I modified the argument of [1] slightly to avoid exponents in Int (to use Nat instead) and I might have introduced a few errors in the computations while doing so. I hope not!

[1] Krätschmer, Volker, and Mikhail Urusov. "A Kolmogorov–Chentsov type theorem on general metric spaces with applications to limit theorems for Banach-valued processes." *Journal of Theoretical Probability* 36.3 (2023): 1454-1486.

[Rémy Degenne]

Another remark: if someone has access to a very smart AI that can formalize the whole thing correctly on its own, please use it ! :)
I'd be happy to review the PR.

[Rémy Degenne]

The progress over the last 3 days has been impressive!

Completed:
:check: 1.10 and 1.12 covInnerBilin_map and covMatrix_map. Etienne Marion
:check: 3.23, integral_id_stdGaussian. Rémy Degenne
:check: 5.12 to 5.15 (edist_chainingSequence lemmas). Markus Himmel
:check: 5.33 and 5.34, Kolmogorov condition distance bounds. Markus Himmel
:check: 5.35 and 5.36, scale_change lemmas. Markus Himmel
:check: 5.37, lintegral_sup_rpow_edist_cover_of_dist_le. Markus Himmel
:check: 5.39, lintegral_sup_rpow_edist_succ. Markus Himmel

Claimed:
:working_on_it: Chapter 2 (stochastic processes, modifications). Jonas Bayer
:working_on_it: 3.3, centralMoment_two_mul_gaussianReal. Jérémy Scanvic
:working_on_it: 3.14 to 3.16, about gaussian characteristic function. Etienne Marion
:working_on_it: 4.9, isProjectiveMeasureFamily_gaussianProjectiveFamily. Peter Pfaffelhuber
:working_on_it: lemmas in LogSizeBallSequence.lean (5.20 to 5.27, everything leading to pair_reduction). David Ledvinka

If you want to contribute, please have look at the blueprint, pick a lemma that's not claimed already, and announce it in the #Brownian motion > Tasks and claims topic.

I'll post some suggestions later today.
On my side, I will work on parts of the blueprint that need more details to unlock more tasks.

[Peter Pfaffelhuber]

Just for the correct setup: In order to get started, I need my own fork of the repository, and PR from there. So, I am going through pressing fork here, then

git clone https://github.com/<MYUSERNAME>/brownian-motion.git
git remote add upstream https://github.com/RemyDegenne/brownian-motion/
git fetch upstream

Finally, I am doing a PR on my fork as usual.
Correct?

[Rémy Degenne]

Yes that's it. On your fork, you should create a new branch and work there, then open a PR from that branch.

[Rémy Degenne]

In your case, you are also collaborator of the main repository so you could also create a new branch there (without a fork) and make a PR from that branch.
But for everybody else, what you describe is the standard way.

[Rémy Degenne]

New update! I'll omit what was already completed last time from the new list. The numbers of the lemmas can be inconsistent with the previous numbers (the blueprint also changes).

:check: 3.3, centralMoment_two_mul_gaussianReal. Jérémy Scanvic
:check: 3.14 to 3.16, about gaussian characteristic function. Etienne Marion
:check: ext lemmas for Gaussians. Etienne Marion
:check: An API for continuous bilinear forms, and refactor of several lemmas to use bilinear forms instead of matrices. Etienne Marion
:check: lemmas in LogSizeBallSequence.lean (everything leading to pair_reduction). David Ledvinka
:check: 5.41 integral_sup_dist_le_sum_rpow. Markus Himmel
:check: 5.45 integral_sup_dist_le_sum_rpow_of_le_one. Markus Himmel

Markus detected an issue with the proof in the blueprint for integral_sup_dist_le_sum_rpow, which was fixed (integral_sup_dist_le_sum_rpow_of_le_one is one of the new lemmas coming from the fix).

Claimed:
:working_on_it: Chapter 2 (stochastic processes, modifications). Jonas Bayer
:working_on_it: 3.19 (integral_eval_pi) to 3.25 ("The covariance matrix of the standard Gaussian measure is the identity matrix."). Etienne Marion
:working_on_it: 3.29 isGaussian_multivariateGaussian. Peter Pfaffelhuber
:working_on_it: 4.9, isProjectiveMeasureFamily_gaussianProjectiveFamily. Peter Pfaffelhuber
:working_on_it: 5.5 internalCoveringNumber_eq_one_of_diam_le. Alessio Rondelli, Lorenzo Luccioli

[Rémy Degenne]

The project launched a week ago, and there is already a lot of green in the dependency graph.
Here is a summary of the two sides of the project:

• on the first side, we are building a projective family of Gaussian measures. The main sub-goal of that side is isProjectiveMeasureFamily_gaussianProjectiveFamily. We now have many generic results about Gaussian measures, as well as properties of a standard Gaussian distribution in $\mathbb{R}^d$. We still need results about the multivariateGaussian definition, that gives a measure $\mathcal{N}(\mu, \Sigma)$. Then only the proof of projectivity will remain.
• On the second side (Kolmogorov-Chentsov theorem), we have all the prerequisites and are about half-way in the list of lemmas that lead to countable_set_bound.

The blueprint still needs work for the last part, that brings the two sides together to actually define the Brownian motion. We will also need a list of properties of the Brownian motion, which we will check in order to be sure that we implemented the right object. Blueprint PRs are also welcome!
I will also extend the blueprint with more facts about covering and packing numbers (following section 4.2 of High Dimensional Probability by Roman Vershynin), which will be useful to be able to apply the Kolmogorov-Chentsov theorem in other contexts.

[Rémy Degenne]

To mark the end of the first week of this project, I propose that Friday becomes the Make a PR to Mathlib day!

Let's all look at our contributions and identify something that we can already PR to Mathlib. Eventually every result in the project should move to Mathlib, and we have to do it soon if we want to avoid ending with a big pile of results that rots once everybody moved on.

[Rémy Degenne]

Goals accomplished! :tada:

As shown in the dependency graph, we now have a full formalization of a Brownian motion on $\mathbb{R}_+$. We know that that process has the right finite dimensional distributions, is locally Hölder continuous and has independent increments (that last point is still in a draft PR by Etienne Marion, but is sorry-free).

The next very important step is to get all of the project into Mathlib! I'll create a new topic to track the current PRs to Mathlib from the project.

[Rémy Degenne]

Congrats to everyone who contributed to the project, and especially to @Etienne Marion , @David Ledvinka and @Markus Himmel who did most of the proving effort!

[Rémy Degenne]

There were two sorry on the path of the Brownian motion in the project that referred to code in Mathlib PRs: Fernique's theorem for Gaussian distributions and Gram matrices. Now both have been merged to Mathlib and the Brownian motion construction is sorry-free!

[Rémy Degenne]

Status of the stochastic integral formalization

Goal

Formalize Ito's lemma for the stochastic integral against a semimartingale.

Quick summary of the project

Before proving Ito's lemma, we need the definition of the integral against a semimartingale. A semimartingale is the sum of a local cadlag martingale and an adapted process with finite variation: we will define an integral for each of those parts separately and sum them. There is some work in Mathlib PRs that will be useful for the integral of the finite variation process, but apart from that we are focusing on the local martingale part for now. We are first defining an elementary stochastic integral on simple processes, and then extending that integral by Ito's isometry (we also need Doob's Lp inequality for some steps there). In order to get there, we need to define the quadratic variation of a local martingale, which is obtained by using the (local) Doob-Meyer decomposition theorem. To apply Doob-Meyer, we want to know that local cadlag submartingales are locally of class D. And finally there is a basic tool that we need in several places: the Debut theorem, stating that hitting times are stopping times.

Other things that would be nice to show, but are not essential to the definition of the stochastic integral: existence of cadlag modifications of (sub)martingales, Bichteler-Dellacherie theorem that states that semimartingales are the class for which it makes sense to define a stochastic integral.

Status of the formalization

For different parts of the formalization, I now list if we are done with the formalization, or if it's in progress with tasks available (see https://github.com/RemyDegenne/brownian-motion/issues), or if it needs blueprint work.

• Right-continuous filtrations and their properties: definition and many properties done.
• Extension of martingale theorems that are available in Mathlib in discrete time to continuous time: in progress, tasks are available.
• Debut theorem: claimed by people in Bologna who work on it together. Not separated in small tasks. In progress. (@Lorenzo Luccioli if at some point you want to change to the task system, tell me)
• Definition of "locally", and its properties: done
• Proving that various classes of processes are stable by the locally operation: tasks are available, in progress.
• Proving that local submartingales are locally of class D: tasks are available, in progress.
• Doob-Meyer theorem: the blueprint needs work to be better suited to formalization. No prerequisite definition missing. We should work on creating tasks. A subpart of that is the Komlos lemma: some tasks are available, and more could be created from the blueprint.
• Elementary stochastic integral and simple processes: definition done, proving their properties in in progress, but there are no detailed tasks. The blueprint looks ok?
• Doob's Lp inequality: tasks are available for parts of it.
• Ito's isometry and square integrable martingales: the blueprint needs work.
• Stochastic integral definition and Ito's formula: the blueprint needs work.