编辑“︁Lean概率论库”︁（章节）

= Lean概率论库 =  

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

== 核心概念 ==  

=== 概率空间 ===  
概率空间是三元组<math>(\Omega, \mathcal{F}, P)</math>，其中：  
* <math>\Omega</math> 是样本空间  
* <math>\mathcal{F}</math> 是事件σ-代数  
* <math>P</math> 是概率测度  

在Lean中，概率空间通过测度论库定义：  
<syntaxhighlight lang="lean">  
import probability.probability_measure  

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

=== 随机变量 ===  
随机变量是从样本空间到可测空间的映射。Lean中通过可测函数定义：  
<syntaxhighlight lang="lean">  
variables {E : Type*} [measurable_space E]  

def random_variable (X : Ω → E) : Prop := measurable X  
</syntaxhighlight>  

=== 期望与方差 ===  
期望是随机变量关于概率测度的积分：  
<math>\mathbb{E}[X] = \int_\Omega X \, dP</math>  

Lean中计算期望的示例：  
<syntaxhighlight lang="lean">  
import probability.integration  

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

#check μ[X]  -- 期望的Lean表示  
</syntaxhighlight>  

== 实际案例 ==  

=== 硬币抛掷实验 ===  
形式化描述公平硬币的概率空间：  
<syntaxhighlight lang="lean">  
import probability.distributions  

def coin_space : measure bool := bernoulli 0.5  
lemma coin_is_fair : coin_space {tt} = 0.5 := by simp  
</syntaxhighlight>  

=== 大数定律验证 ===  
弱大数定律的形式化陈述：  
<syntaxhighlight lang="lean">  
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  
</syntaxhighlight>  

== 可视化 ==  

=== 概率分布关系 ===  
<mermaid>  
graph LR  
    A[概率空间] --> B[离散分布]  
    A --> C[连续分布]  
    B --> D[伯努利分布]  
    B --> E[泊松分布]  
    C --> F[正态分布]  
    C --> G[指数分布]  
</mermaid>  

== 进阶主题 ==  

=== 随机过程 ===  
布朗运动的形式化定义片段：  
<syntaxhighlight lang="lean">  
import probability.process  

def brownian_motion :=  
  is_gaussian_process (λ t, 0) (λ t s, min t s)  
</syntaxhighlight>  

=== 条件期望 ===  
基于σ-代数的条件期望构造：  
<syntaxhighlight lang="lean">  
import probability.conditional_expectation  

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

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

== 常见问题 ==  

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

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

== 参见 ==  
* [[测度论基础]]  
* [[随机过程形式化]]  
* [[概率编程验证]]  

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

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]