中心极限定理的形式化验证证明
数学软件
2017-02-02 v4 计算机科学中的逻辑
概率论
摘要
我们描述了一个在Isabelle证明助手中经过形式化验证的中心极限定理证明。我们的形式化构建并扩展了Isabelle用于分析和测度论概率的库。该定理的证明使用特征函数（一种傅里叶变换）来证明，在适当假设下，随机变量之和弱收敛于标准正态分布。我们还讨论了支持形式化的库和基础设施，并反思了从这项工作中汲取的一些经验教训。
引用
@article{arxiv.1405.7012,
title = {A formally verified proof of the Central Limit Theorem},
author = {Jeremy Avigad and Johannes Hölzl and Luke Serafin},
journal= {arXiv preprint arXiv:1405.7012},
year = {2017}
}