Zulip Chat Archive

Stream: Brownian motion

Topic: Mathlib PRs

Rémy Degenne (Jul 04 2025 at 09:07):

The goal of this topic is to keep track of the Mathlib PRs opened with code from the Brownian motion project.

#26351: covers and covering numbers. On hold for now because there actually was an older PR by Yaël with similar definitions.

Rémy Degenne (Jul 04 2025 at 09:12):

#26243: the pair reduction lemma

David Ledvinka (Jul 07 2025 at 22:00):

#26882: Asymptotic lemmas (for proving constL_lt_top)

Rémy Degenne (Jul 10 2025 at 08:20):

#26954: use edist instead of dist in TendstoInMeasure.

Rémy Degenne (Jul 11 2025 at 11:05):

#26991: ENNReal rpow lemmas

Rémy Degenne (Jul 11 2025 at 11:34):

#26998: covariance of sums and maps

Rémy Degenne (Jul 12 2025 at 06:58):

A few PRs by Peter Pfaffelhuber, that lead to Kolmogorov's extension theorem, which we use in this project:
#25899: compact systems

Rémy Degenne (Jul 12 2025 at 06:58):

#25900: Set system of finite unions of sets in a compact system is again a compact system

Rémy Degenne (Jul 12 2025 at 06:58):

#25906: Closed and compact square cylinders form a compact system

Rémy Degenne (Jul 12 2025 at 07:00):

#25902: The finite product of semi-rings (in terms of measure theory) is a semi-ring

Rémy Degenne (Jul 12 2025 at 07:01):

#25903: finite unions of sets in a semi-ring (in terms of measure theory) form a ring

Rémy Degenne (Jul 12 2025 at 07:05):

#25883: Gram matrices

Rémy Degenne (Jul 12 2025 at 12:50):

I have started to break my big Fernique theorem PR (1000 lines) into several pieces. We use it in the project to know that moments of Gaussian distributions are finite (it's one of the sorry in the project, but it is sorry-free in that big WIP PR).
#27027: two lemmas about subtraction of norms

Rémy Degenne (Jul 12 2025 at 12:50):

#27029: two lemmas about Lp functions and product spaces

Rémy Degenne (Jul 14 2025 at 12:33):

#27127: 2 processes have the same law iff they have the same finite dimensional laws

Rémy Degenne (Jul 16 2025 at 07:27):

#27192: covarianceBilin lemmas

Rémy Degenne (Jul 16 2025 at 07:40):

#27193: ContinuousLinearMap.flip/bilinearComp of zero

Rémy Degenne (Jul 16 2025 at 10:37):

#27201: Nat.log2 <= Real.logb 2

Rémy Degenne (Jul 16 2025 at 11:31):

#27202: define IsKolmogorovProcess
Note that I changed the definition slightly with respect to the one in the project: I added the two conditions 0 < p and 0 < q to the definition, which avoids having them as hypotheses everywhere.
Also I changed the names: IsKolmogorovProcess is the measurable version, and the property of being a modification of such a process is IsAEKolmogorovProcess.

Rémy Degenne (Jul 18 2025 at 11:31):

#27247: measure_inter_eq_of_ae

Rémy Degenne (Jul 18 2025 at 12:14):

#27251: generalize tendstoInMeasure_of_ne_top

Etienne Marion (Jul 23 2025 at 08:58):

#26238: linear isometry between orthonormal bases

Etienne Marion (Jul 23 2025 at 08:59):

#26274: API for symmetric bilinear forms

Etienne Marion (Jul 23 2025 at 08:59):

#26315: continuous bilinear forms

Etienne Marion (Jul 23 2025 at 08:59):

#26378: inner product against basisFun

Etienne Marion (Jul 29 2025 at 07:43):

#27626: turn covarianceBilin into a ContinuousBilinForm

Etienne Marion (Jul 29 2025 at 09:07):

#27628: HasLaw predicate

Etienne Marion (Jul 30 2025 at 09:32):

#27674: Integrability in a product space

Etienne Marion (Jul 30 2025 at 10:18):

#27675: Introduce covInnerBilin

Rémy Degenne (Aug 30 2025 at 12:07):

#28343: Fernique's theorem for distributions that are invariant by rotation.
This is not a PR from the project itself but is a prerequisite: one of the sorry in the Brownian motion project is the fact that Gaussians have finite moments. I had already proved it for Gaussians in a Banach space through Fernique's theorem in #26291 (a big PR that I am cutting into pieces). That latter PR now also contains the definition of the Cameron-Martin space and the Cameron-Martin theorem, minus a few sorry about the total variation distance that are proved in #27579 (another big PR I'm slowly cutting into reviewable pieces).

Etienne Marion (Oct 06 2025 at 21:13):

#28162: define positive semidefinite (sesqui/bi)linear forms

Etienne Marion (Oct 06 2025 at 21:13):

#30108: define the matrix associated to a sesquilinear form

Etienne Marion (Oct 06 2025 at 21:13):

#30277: move a file

Etienne Marion (Oct 06 2025 at 21:14):

#30276: lemmas about the matrix associated with a sesquilinear form

Etienne Marion (Oct 06 2025 at 21:15):

#30274: properties of sesquilinear forms over a star ring

Etienne Marion (Oct 09 2025 at 13:32):

#30324: introduce covInnerBilin

Etienne Marion (Oct 09 2025 at 13:33):

#30371: covInnerBilin of the push-forward measure

Rémy Degenne (Oct 15 2025 at 10:55):

#30543: Borel space on WithTop, which is a prerequisite for the PR below

Rémy Degenne (Oct 15 2025 at 10:56):

#29430: change stopping times to take values in WithTop. This is needed to start the next phase of the project about stochastic integrals, as the current definition of stopping times does not allow us to work correctly with localization.

Etienne Marion (Oct 26 2025 at 14:07):

#30921: Gaussian measures and characteristic functions

Kexing Ying (Oct 28 2025 at 10:21):

#30997: Predictable process

Previously, in the case of discrete processes, we spelt predictability using Adapted. This works well as martingale requires strong measurability. For general processes, predictability means (non-strong) measurability wrt the predictable sigma algebra. These two definitions coincide if measurable => strong measurable, e.g. compare the assumptions on E in Submartingale.zero_le_of_predictable and Submartingale.zero_le_of_predictable' in the PR. I'm not sure if we should replace the previous spelling in the discrete case with the more general spelling as this will require more assumptions. Do you have any opinions on this?

Kexing Ying (Nov 01 2025 at 13:00):

#31148: Defines local and stable properties

Rémy Degenne (Nov 05 2025 at 13:03):

Rémy Degenne said:

#26351: covers and covering numbers. On hold for now because there actually was an older PR by Yaël with similar definitions.

Yaël's PR chain has finally been sent to bors and we will soon be able to PR the Kolmogorov-Chentsov side of the project.

Rémy Degenne (Nov 12 2025 at 10:40):

#31541: Monotonicity of hitting times

Kexing Ying (Nov 12 2025 at 16:32):

#31557: Some lemmas about stopped value/process

Etienne Marion (Nov 12 2025 at 17:41):

#31553: the comap of nhds by the coercion of a dense subset is NeBot

Etienne Marion (Nov 12 2025 at 17:41):

#31555: bounded distance implies bounded space

Etienne Marion (Nov 12 2025 at 17:41):

#31561: monotonicity of Holderianity

Rémy Degenne (Nov 20 2025 at 10:56):

Since we have several new people I'd like to bring attention to this topic: everything in the project should eventually be in Mathlib, and sooner is better than later.
When we introduce a new definition, we should wait a bit before making a PR to Mathlib, until we know that we can actually work with it and prove interesting lemmas about it. But for lemmas about Mathlib definitions, there is no reason to wait.

If you add things to the repository that don't depend on new definitions, please also PR them to Mathlib and list the PRs here (one PR per message, to benefit from the bot reactions).