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数学库）的概率文件夹大量使用了马尔可夫核。我们介绍了它们的定义和性质，并描述了马尔可夫核分解定理的形式化。该定理用于定义随机变量的条件概率分布以及后验分布。随后，我们解释了如何以一种更不寻常的方式使用马尔可夫核来获得独立性和条件独立性的统一定义，并遵循相同原则来定义次高斯随机变量。最后，我们还讨论了核在熵和KL散度形式化中的作用。