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.

[Rémy Degenne]

Hi everyone. As you have surely noted, there has not been much activity on the project in the last month. I'd like to change that soon.
The main issue right now is that there are no available tasks: everything has been claimed and mostly done, and several PRs have been awaiting review for a while. The project needs blueprint work to create new tasks.

I will work on the blueprint next week, with the first goal being to write an overview of where we are, what we could do next, and what tasks could be created. That will happen next week and not before, because this week I am co-organizing Lean Together 2026, and I encourage you all to join and watch the talks! Today David Ledvinka will present the formalization of Brownian motion, and on Thursday Etienne Marion will give another probability talk on his nice work on the Ionescu-Tulcea theorem.

I would also like to start weekly zoom meetings for the project, starting next week. The goal of these meetings would be to discuss the broad picture of the project and how we organize our work, to raise any question about formalization choices that could impact several PRs, and to discuss any other issue that could require coordination. I'll make a poll later about possible times.

[Yongxi Lin (Aaron)]

Can't wait to formalize probability again :grinning_face_with_smiling_eyes:

[Ryan McCorvie]

The talk was great, and inspired me to want to join this project

[Rémy Degenne]

For the first meeting, what about 2026-01-30T17:00:00+01:00 ?
It's 5pm on a Friday for Europeans, so not ideal, but we have contributors from the US west coast so anything earlier would be really early for them.

[Yongxi Lin (Aaron)]

/poll Time to meet
2026-01-30T11:00:00-05:00

[Yongxi Lin (Aaron)]

Ok it seems like that one cannot use the global time feature in the poll

[Etienne Marion]

This works for me

[Ryan McCorvie]

Is the time set for tomorrow then? How does one join the meeting?

[Rémy Degenne]

Yes let's meet at that time. I'll post a zoom link in this topic tomorrow, a few hours before the start.

[Rémy Degenne]

We'll meet here at 2026-01-30T17:00:00+01:00 : https://univ-lille-fr.zoom.us/j/98302757855?pwd=iDb9aLqb3K2LCy5Z1s5OFxht9y6hQt.1

[David Ledvinka]

Sorry I didn't realize I double booked myself with London Learning Lean so had to leave after the first 30 minutes. Would love a summary of the conclusions after the meeting is done!

[Rémy Degenne]

Slides: Brownian.pdf (but without me talking over them you don't know if the thing on the slide is something we have, or don't have yet)

[Rémy Degenne]

Some things we said:

• n°1 priority is to find good references for each of the main parts of the construction, so that we can just follow the book when writing the blueprint. Apart from the ones on the last slide, Peter mentioned this book: https://link.springer.com/book/10.1007/978-3-662-10061-5
• One of the last slides lists potential sub-projects, that are almost independent of each other (or one uses only the end result of another). Ideally we want to work on several of those in parallel.
• In the short term, I'll try to flesh out the Doob-Meyer decomposition proof in the blueprint and produce tasks for that. Etienne will look at improving the blueprint for the existence of cadlag modifications of local submartingales.
• We'll try LeanArchitect. Demo of what that will look like: https://github.com/hanwenzhu/brownian-motion/blob/master/BrownianMotion/StochasticIntegral/ClassD.lean
• In the class D file, it would be nice to figure out which of ProgMeasurable vs jointly measurable we want in the definitions of ClassD, HasIntegrableSup and friends (to have IsStable for them). Right now we have a mix of both and they don't mix very well.

Something we did not talk about much but is important: please PR everything to Mathlib!

[Peter Pfaffelhuber]

What I realised yesterday: One benefit of the project to formalize stochastic integrals is that it will become apparent where the usual conditions (filtrations are right-continuous, all sigma-algebras are complete) are really used in the theory. I think in textbooks, they are mentioned once and then never discussed again. Maybe a selling point for the project...

[Rémy Degenne]

A similar thing: most references use cadlag everywhere, but the vast majority of results we encountered so far don't need left limits, and others need right-continuity only to get progressive measurability. It would be nice to clearly see where cadlag is fully needed. (I think there was already a discussion about this but I don't remember where)

Although a justification for using cadlag everywhere is that it's for free: for right-continuous filtrations, local martingales have cadlag modifications.

[Rémy Degenne]

About references: the current Doob-Meyer proof in the blueprint follows https://www.sciencedirect.com/science/article/pii/S0304414911002973, which looks like a good ref. I'll continue following this proof when detailing the blueprint further for that theorem.

[Peter Pfaffelhuber]

Does this mean we should have cad-functions (conitue à droit) and lag-functions (limite a gauche), and cadlag are the functions in cad ∩ lag?

[Rémy Degenne]

We have a definition for right-continuous already. We don't have one for left limits, but it's just ∀ x, ∃ l, Tendsto f (𝓝[<] x) (𝓝 l) (and I think we don't have a definition because whenever we need that we also have right-continuity, so we use IsCadlag).

[Peter Pfaffelhuber]

Sooner or later (but maybe not in this project) we will need a topology on cadlag-functions. Shouldn't is then be also a Type?

[Rémy Degenne]

The proof that square integrable martingales are a Hilbert space in these lecture notes uses convergence in the space of cadlag functions. So if we follow a similar proof we'll need that type and its topology.

[Peter Pfaffelhuber]

Ah, ok. Here, they use the topology of uniform convergence, which is very strong. (For limits of stochastic processes, you either have the Skorohod J1 or M1 topology.)

[Peter Pfaffelhuber]

I asked my colleague David Criens, who also pointed me to the paper we took for Kolmogorov-Chentsov, which general references he can recommend for the purpose of formalizing stochastic integrals. Here is his detailed (and deepl-translated) answer... I will try to have a look at all of the references...

Classic references are certainly Jacod 79 (1D only), Jacod-Shiryaev, and He-Wan-Yan (https://zbmath.org/0781.60002).

The “predictable characterizations” for integration in JS III.6d are particularly interesting; I only know them from there.

Metivier-Pellaumail (https://zbmath.org/0463.60004) is also very general (jumps + Hilbert space); but the approach is somewhat less classical (they have a concept of “dominating process” to define integration; it may be that it is not entirely general). There is also a “newer” version by Metivier (https://zbmath.org/0503.60054); a few things are done differently, but the treatment of integration should be similar (caution: lots of typos).

A more modern book (well written; notation+theory are classic) is Cohen-Elliott (https://zbmath.org/?q=ia%3Acohen.samuel-n+dt%3Ab); a revised version of Elliott's Classic (in which, for example, the proof of the Debut Theorem was allegedly incorrect).

Another book I consider to be very good is Medvegyev (https://zbmath.org/?q=ia%3Amedvegyev.peter+dt%3Ab); very precise and detailed (also many examples/counterexamples).

Of course, Bichteler (https://zbmath.org/1189.60004) should not go unmentioned; however, the notation and concept are very unusual, and the approach is also non-standard.

One book I don't like very much is the one by Protter (https://zbmath.org/1041.60005); he derives integration via the Bichteler-Dellacherie theorem; the class of integrable processes is initially limited to \mathbb L (left-continuous and adapted); this is generally insufficient (consider SDEs with irregular coefficients); he then develops a more general theory, but this is again classical (as far as I remember).

There is another book by Dellacherie-Meyer that deals with stochastic integration (it is probably also very general, although I am not familiar with it; I usually only use the first parts of their books).

Kallenberg also has a chapter on this, of course, but it is very brief and perhaps not so suitable.

Best regards,

David

P.S. In my opinion, the most effective way to approach Ito is to calculate integration by parts, which leads directly (by induction) to polynomials and then to a density argument (i.e., nothing to do with Taylor, etc.). In Hilbert space, this is of course much more delicate.

[Peter Pfaffelhuber]

Here is an addendum to the mail by David Criens. There seems to be theory if the integrator takes values in Banach spaces:

Developing the theory on Banach spaces is also very exciting to me; however, as far as I understand it, the case is much more delicate than Hilbert spaces and mostly depends on the geometry. I only know theory for UMD spaces (https://zbmath.org/1366.46001), because martingale equations apply there, or 2-smooth spaces (https://zbmath.org/1053.60071), which satisfy a kind of polarization inequality.

I would be very interested to know if there is a good book on this.

[Joris van Winden]

Peter Pfaffelhuber said:

Here is an addendum to the mail by David Criens. There seems to be theory if the integrator takes values in Banach spaces:

Developing the theory on Banach spaces is also very exciting to me; however, as far as I understand it, the case is much more delicate than Hilbert spaces and mostly depends on the geometry. I only know theory for UMD spaces (https://zbmath.org/1366.46001), because martingale equations apply there, or 2-smooth spaces (https://zbmath.org/1053.60071), which satisfy a kind of polarization inequality.

I would be very interested to know if there is a good book on this.

There is the book series 'Analysis in Banach Spaces' by Hytonen, van Neerven, Veraar, and Weis. The upcoming volume 4 will deal specifically with stochastic integration. Although it will take at least a few years until it will come out.

[Joris van Winden]

(I did my PhD in the Analysis group in Delft with Mark Veraar as my promotor)

[Etienne Marion]

I won't be able to attend the meeting tomorrow (holidays)

[Rémy Degenne]

About that meeting:
time: 2026-02-06T17:00:00+01:00
link: https://univ-lille-fr.zoom.us/j/95328461252?pwd=ek1k8octGc4oZbwbUiJC9VxFDAXsuB.1

[Peter Pfaffelhuber]

Sorry, today our school holidays start, so I cannot attend the toom meeting today.

I promised to look at the book by Cohen and Elliott. Actually, the case of Hilbert-space-valued stochastic integration is not covered there. All is built upon the real-valued case, unfortunately. I saw that some books on SPDEs introduce the stochastic integral in Hilbert spaces, but I dod not find any which also covers jumps...

[Rémy Degenne]

Same link, same time as last week.

[Rémy Degenne]

(it started 5 minutes ago)

[Peter Pfaffelhuber]

Will there be a zoom today at the usual time?

[Rémy Degenne]

Yes, same time. 2026-02-20T17:00:00+01:00
link: https://univ-lille-fr.zoom.us/j/95328461252?pwd=ek1k8octGc4oZbwbUiJC9VxFDAXsuB.1

[Rémy Degenne]

Something came up and I can't make it to the meeting today. Also I won't be available next week either, so the next one will be on March 13.