Page 273 - 《软件学报》2026年第7期

2958 软件学报 2026 年第 37 卷第 7 期

定义 5. Lebesgue-Borel 测度.
⊢ lborel = space_s real_borel, subsets real_borel, measure_ext lebesgue

定义 5 中, “space_s”表示空间; “subsets”表示子集; “real_borel”表示 Borel-σ 代数, 其数学含义为指定空间上所
σ 代数.
有开集的最小
3.2 基于扩展实数的积分形式化
扩展实数的引入进一步扩展了积分的适用范围, 它允许积分结果取无穷值. 扩展实数可以精确地表达积分过
程中极限运算的结果, 这在单调收敛性定理的证明中尤为关键. Lebesgue 积分将积分运算扩展至任意测度空间, 其
通过对函数值进行分段处理, 避免了传统黎曼积分对函数连续性的要求, 能够更灵活地处理不可积函数和复杂的
测度空间. 本研究重点形式化了 Lebesgue 积分相关定义, 作为后续高铁复合通信信道建模的基础. Lebesgue 积分
的核心思想是将函数值域划分为若干区间, 并对这些子区间的测度与函数值进行加权求和. 公式 (2) 表示 Lebesgue
积分的数学定义.

∫ ∫ ∫
+
−
f(x)dx = f (x)dx− f (x)dx (2)
E E E
其中, f (x) 和 f (x) 分别称为函数 f(x) 在 E 上的正部和负部, 二者皆是非负可测函数, 且存在 Lebesgue 积分. 当二
+
−
者的 Lebesgue 积分都是有限值时, 称函数 f(x) 在 E 上 Lebesgue 可积.
本研究结合 Lebesgue 积分数学定义与 Mhamdi 等人 [8,9] 在 HOL4 中的对其构建的形式化定义, 在 HOL Light
中构建 Lebesgue 积分的高阶逻辑模型. 具体而言, 需先形式化正简单函数的 Lebesgue 积分, 再形式化非负可测函
数的 Lebesgue 积分, 最后推广至一般形式的 Lebesgue 积分. 定义 6 表示一般形式 Lebesgue 积分的形式化模型.
定义 6. Lebesgue 积分.
⊢ L_integral m f = extreal_sub (pos_fn_integral m (fn_plus f)) (pos_fn_integral m (fn_minus f))

定义 6 的作用域均为扩展实数, “extreal_sub”表示扩展实数的“ − ”运算符; “pos_simple_fn_integral”定义了正
∫
∑ ∑
简单函数的 Lebesgue 积分, 即 x i I A i (x) = µ(A i )· x i ; “pos_fn_integral”定义了非负可测函数的 Lebesgue 积
i i
∫ {∫ s }

分, 即 fdµ = sup gdµg ⩽ f , 其中 g 为正简单函数.
3.3 基于扩展实数的概率形式化
本文基于尹晓娜等人 [20] 的概率形式化工作, 将概率相关定义进行了扩展实数域的推广, 重点形式化了随机变
量和概率分布等核心概念. 随机变量本质上是一个可测函数. 扩展随机变量的定义域, 能够使其更广泛地适用于不
同类型的随机过程和更复杂的概率空间, 以适用于复杂信道的建模. 定义 7 表示扩展实数上的随机变量 X 定义在

概率空间 p 上, 取值范围为 p 中的可测集合.
定义 7. 随机变量.
⊢ !X p s. random_variable_ext X p s <=>
prob_space_ext p /\ X IN gen_measurable (p_space_ext p, events_ext p) s
定义７中, “prob_space_ext”“p_space_ext”“events_ext”分别表示扩展实数上的概率空间、样本空间和事件集.
概率分布通常定义为函数, 表示随机变量取某个特定值或落入某个区间的概率. 定义 8 描述了随机变量 X 在
−1
测度空间上的概率分布, 其数学含义为 distribution(X, p) = λs.P(X (s)∩Ω).
定义 8. 概率分布.
⊢ !X p. distribution_ext p X = (\s. prob_ext p (PREIMAGE X s INTER p_space_ext p))
除了通用定义外, 本研究还形式化了一些信道中常用的概率相关定义, 包括概率密度函数和正态随机变量. 连

续型随机变量在区域 P 上的取值为概率密度函数在 P 上的积分. 因此在形式化概率密度函数时, 可采用求导的思
路. 本文参考 Mhamdi 等人 [8,9] 的形式化建模思路, 使用 Radon-Nikodym (RN) 导数来定义概率密度函数. 而 Radon-
Nikodym 定理是证明该导数存在性的重要定理, 该定理反映了概率测度可由其 Lebesgue 测度 λ 的 RN 导数的积