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.

翻译：Mathlib（Lean数学库）的概率文件夹大量使用了马尔可夫核。我们介绍了马尔可夫核的定义与性质，并描述了马尔可夫核分解定理的形式化过程。该定理被用于定义随机变量的条件概率分布以及后验分布。随后，我们阐释了如何以非常规方式运用马尔可夫核来获得独立性与条件独立性的通用定义，并遵循相同原理定义次高斯随机变量。最后，我们还讨论了核在信息熵与Kullback-Leibler散度形式化中所起的作用。