Lean projects in probability
This is a list of results that are currently missing from
Mathlib, the mathematics library of Lean. I put them here with the hope that someone feels tempted to formalize them and add them to Mathlib.
The selection is purely subjective: I chose results that interest me or that I will need for other developments.
- Jensen's inequality for the conditional expectation - Proposition 2.6.29 in [2]. The Mathlib definition of the conditional expectation is here: MeasureTheory.condexp.
In the proof of Proposition 2.6.29, we need to write a convex function as a supremum over linear functions: this is the main step missing in Mathlib.
- Randomization of Markov kernels and measures - Lemma 4.22 in [1]. In standard Borel spaces, we can isolate the randomness and have it be only over \(\mathbb{R}\): we can write a Markov kernel \(\kappa : \mathcal X \rightsquigarrow \mathcal Y\) as the map by a deterministic function \(f : \mathcal X \times [0,1] \to \mathcal Y\) of a uniform measure on [0,1].
- Sub-Gaussian random variables - define random variables with cumulant generating function bounded by a given function. Define sub-Gaussian random variables as a special case.
It might be better to define a sub-Gaussian measure instead of a sub-Gaussian random variable.
A generalization of both conditional sub-Gaussian and sub-Gaussian could then be the following: a kernel \(P : \mathcal X \rightsquigarrow \mathcal Y\) is \(\sigma^2\)-sub-Gaussian with respect to a measure \(\mu\) on \(\mathcal X\) if for \(\mu\)-almost all \(x\), for all \(\lambda \in \mathbb{R}\),
$$\log P(x)[y \mapsto e^{\lambda y}] \le \frac{\sigma^2}{2}\lambda^2 \: .$$
This definition gives in particular a definition of a sub-Gaussian measure if we apply it to a constant kernel.
- Integration by parts for Stieltjes functions - If \(f\) and \(g\) are Stieltjes functions (monotone right continuous functions) then they define measures \(\gamma_f, \gamma_g\) and under some integrability conditions (find out what are the weakest hypotheses),
$$\int_a^b f(x) \partial \gamma_g(x) + \int_a^b g(x) \partial \gamma_f(x) = f(b)g(b) - f(a)g(a) \: .$$
- Monoidal composition for kernels - measurable spaces and s-finite Markov kernels are a symmetric monoidal category.
We could hope to adapt the tactics from those categories to use them with kernels: see MonoidalComp.
