Lean概率论库[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

Lean概率论库是Lean定理证明器中用于形式化概率论和随机过程的数学库。它基于测度论构建，提供了概率空间、随机变量、期望、方差等核心概念的形式化定义，并与Lean的数学库（如分析、测度论）深度集成。该库适用于从基础概率论到高级随机分析的形式化验证，尤其适合机器学习、统计学和金融数学等领域的应用验证。

核心概念[编辑 | 编辑源代码]

概率空间[编辑 | 编辑源代码]

概率空间是三元组 $(Ω, ℱ, P)$ ，其中：

$Ω$ 是样本空间
$ℱ$ 是事件σ-代数
$P$ 是概率测度

在Lean中，概率空间通过测度论库定义：

  
import probability.probability_measure  

-- 定义概率空间  
variables {Ω : Type*} [measurable_space Ω] (μ : measure Ω) [probability_measure μ]

随机变量[编辑 | 编辑源代码]

随机变量是从样本空间到可测空间的映射。Lean中通过可测函数定义：

  
variables {E : Type*} [measurable_space E]  

def random_variable (X : Ω → E) : Prop := measurable X

期望与方差[编辑 | 编辑源代码]

期望是随机变量关于概率测度的积分： $𝔼 [X] = \int_{Ω} X d P$

Lean中计算期望的示例：

  
import probability.integration  

variables (X : Ω → ℝ) (hX : measurable X) (hint : integrable X μ)  

#check μ[X]  -- 期望的Lean表示

实际案例[编辑 | 编辑源代码]

硬币抛掷实验[编辑 | 编辑源代码]

形式化描述公平硬币的概率空间：

  
import probability.distributions  

def coin_space : measure bool := bernoulli 0.5  
lemma coin_is_fair : coin_space {tt} = 0.5 := by simp

大数定律验证[编辑 | 编辑源代码]

弱大数定律的形式化陈述：

  
import probability.law_large_numbers  

theorem WLLN {X : ℕ → Ω → ℝ} (h_indep : pairwise (λ i j, indep_fun (X i) (X j)))  
  (h_ident : ∀ i, ident_distrib (X i) (X 0)) (hint : integrable (X 0)) :  
  ∀ ε > 0, tendsto (λ n, μ {ω | |(∑ i in finset.range n, X i ω) / n - μ[X 0]| ≥ ε})  
    at_top (𝓝 0) :=  
weak_law_of_large_numbers h_indep h_ident hint

可视化[编辑 | 编辑源代码]

概率分布关系[编辑 | 编辑源代码]

进阶主题[编辑 | 编辑源代码]

随机过程[编辑 | 编辑源代码]

布朗运动的形式化定义片段：

  
import probability.process  

def brownian_motion :=  
  is_gaussian_process (λ t, 0) (λ t s, min t s)

条件期望[编辑 | 编辑源代码]

基于σ-代数的条件期望构造：

  
import probability.conditional_expectation  

variables {G : measurable_space Ω} (hG : G ≤ ⊤)  

def cond_exp (X : Ω → ℝ) : Ω → ℝ :=  
  conditional_expectation hG (μ.restrict {ω | X ω ≠ 0}) X

常见问题[编辑 | 编辑源代码]

Q: 如何处理非可测集？ A: 通过Carathéodory扩展定理构造完备测度空间，或使用外层测度技术。

Q: 如何验证概率算法的正确性？ A: 结合程序逻辑（如Hoare逻辑）与概率测度，例如验证随机快速排序的期望复杂度。

参见[编辑 | 编辑源代码]

该内容持续更新于2023年12月，对应Lean 4版本。