Gauge积分在HOL4中的形式化

积分是许多数学理论的基础,如实数分析、信号与系统中微分方程的求解等等。Gauge积分是黎曼积分在闭区间上的推广,应用更加方便。将Gauge积分的运算性质在HOL4(Higher-Order Logic 4)中形式化,包括积分的线性运算性质、积分不等式、分部积分、积分分裂定理、子区间的可积性、对特殊函数的积分的形式化及积分极限定理、柯西可积准则,并根据相关性质对反相积分器进行了验证。

关于Gauge积分的注记

在[1]中Armstrong和Lamoreaux定义了一种新型的积分,即Gauge积分和参导数 本文则证明了[1]中一些未证明的结论,并首次提出了Gauge积分的一些性质,对[1]作了一些补充;进一步,本文还系统讨论了Riemann,Lebesgue,Gauge三种积分之间的关系.