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 from Mathlib.
The result should be close to this:
import Mathlib
open ProbabilityTheory MeasureTheory
example {α X : Type*} {m mα : MeasurableSpace α} [NormedAddCommGroup X] [NormedSpace ℝ X]
[CompleteSpace X]
(hm : m ≤ mα) {μ : Measure α} [SigmaFinite (μ.trim hm)]
{f : α → X} {φ : X → ℝ} (hφ_cvx : ConvexOn ℝ Set.univ φ) (hφ_cont : LowerSemicontinuous φ)
(hf_int : Integrable f μ) (hφ_int : Integrable (φ ∘ f) μ) :
∀ᵐ x ∂μ, φ (μ[f | m] x) ≤ μ[φ ∘ f | m] x := by
sorry
- 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].
- 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.
