Markov kernels in Mathlib's probability library

TL;DR

This work develops a kernel-centered formalization of probability in Mathlib, positioning Markov kernels as the core objects and enabling a compositional calculus over measurable spaces. It formalizes the disintegration theorem for finite kernels and uses it to define conditional distributions and the posterior kernel, establishing a foundation for kernel-based independence and Bayesian updates. The paper then extends the kernel framework to sub-Gaussian random variables and to information-theoretic notions such as entropy $H$ and the Kullback–Leibler divergence $KL$, with attention to their composition and data-processing properties. Together, these contributions yield a flexible, modular toolkit for probability in Lean and point toward future work on sequential kernel models and broader divergences.

Abstract

The probability folder of Mathlib, Lean's mathematical library, makes a heavy use of Markov kernels. We present their definition and properties and describe the formalization of the disintegration theorem for Markov kernels. That theorem is used to define conditional probability distributions of random variables as well as posterior distributions. We then explain how Markov kernels are used in a more unusual way to get a common definition of independence and conditional independence and, following the same principles, to define sub-Gaussian random variables. Finally, we also discuss the role of kernels in our formalization of entropy and Kullback-Leibler divergence.