Probability theory in formal mathematics requires careful handling of Markov kernels for conditional distributions, independence, and related constructions. Prior to this work, the Mathlib probability library lacked a unified kernel-based framework for these concepts.

The authors describe the formalization of Markov kernels in Mathlib, Lean's mathematical library. They present the definition and composition operations for kernels, formalize the disintegration theorem (which enables defining conditional probability distributions and posterior distributions), and show how kernels provide a common definition for both independence and conditional independence. The same kernel-based approach is used to define sub-Gaussian random variables.

The disintegration theorem for Markov kernels is fully formalized in Lean and integrated into Mathlib. The kernel framework unifies the definitions of independence and conditional independence under a single abstraction and enables the definition of conditional probability distributions of random variables and posterior distributions.