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

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

从而匹配积分对称性定理的表示形式, 完成证明. 继而, 定理 3 成功验证了公式 (8) 和 (9) 化简过程的正确性.
定理 3. 复合概率密度函数对称化简定理.
val it : thm =
⊢ !h sigma1 sigma2.
reallim (atreal (&0) within {x | &0 <= x})
(\a. reallim at_posinfinity (\b. real_integral (real_interval [a, b]) (\h1. &1 / abs h1 * h / (power2 sigma1 * power2
sigma2) *exp (--power2 h1 / (&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))))
+ reallim (atreal (&0) within {x | x <= &0})
(\a. reallim at_neginfinity (\b. real_integral (real_interval [b, a]) (\h1. &1 / abs h1 * h / (power2 sigma1 * power2
sigma2) * exp (--power2 h1 / (&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))))
= &2 * reallim (atreal (&0) within {x | &0 <= x})
(\a. reallim at_posinfinity (\b. real_integral (real_interval [a, b]) (\h1. &1 / h1 * h / (power2 sigma1 * power2
sigma2) * exp (--power2 h1 / (&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))))
接下来在公式 (9) 的基础上对被积函数进行了换元, 该步骤的化简结果如公式 (10) 所示.

h 2 h ∫ +∞ 1 −v− h 2
1 2 dv
令v = 1 , p(h) = lim e 4σ 2 σ 2 v (10)
2
σ 2 σ σ x→0 + x v
2
1 1 2
在形式化证明中, 由于定理的使用需要严格满足数学逻辑的要求, 在换元时必须确保被积函数的可积性和连
续性. 这不仅是换元操作的充分条件, 也是复合信道的重要数学性质. 故本文在验证换元这一步骤前, 先证明了复
合信道概率密度函数中被积函数的连续性与可积性, 分别如定理 4 和定理 5 所示.
定理 4. 复合概率密度函数连续性.
val it : thm =
⊢ !h sigma1 sigma2 a b. &0 < a
==> (\h1. &1 / h1 * h / (power2 sigma1 * power2 sigma2)
* exp (--power2 h1 / (&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))
real_continuous_on real_interval [a, b]
定理 5. 复合概率密度函数可积性.
val it : thm =
⊢ !h sigma1 sigma2 a b. &0 < a
==> (\h1. &1 / h1 * h / (power2 sigma1 * power2 sigma2)
* exp (--power2 h1 / (&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))
real_integrable_on real_interval [a, b]
定理 4 的证明主要依赖于一系列倒数函数、指数函数、函数乘法等相关实数函数连续定理. 定理 5 的证明则
依赖于定理 4 和函数可积性形式化定理, 该定理描述了连续函数在有限闭区间上可积这一性质. 定理 4 和定理 5
为换元定理的证明提供了充分条件, 该换元定理对公式 (10) 进行了形式化建模, 如定理 6 所示.
定理 6. 换元定理.
val it : thm =
⊢ !h sigma1 sigma2. sigma1 > &0 /\ sigma2 > &0
==> &2 * reallim (atreal (&0) within {x | &0 <= x})
(\a. reallim at_posinfinity (\b. real_integral (real_interval [a, b])
(\h1. &1 / h1 * h / (power2 sigma1 * power2 sigma2) * exp (--power2 h1 /
(&2 * power2 sigma1) + --power2 h / (&2 * power2 sigma2 * power2 h1)))))
= h / (power2 sigma1 * power2 sigma2) *