Formalization of Gauge Integration Theory in HOL4
Weiqing Gu, Zhiping Shi, Yong Guan, Jie Zhang, Zhao Chunna, Shiwei Ye · 2013
Integral is one of the most important foundations in many subjects,such as real analysis,the differential equations in signals and systems and so on.Gauge integral is a generalization of the Riemann integral in which some situations are more useful than the Lebesgue integral.This paper formalized the operational properties which contain the linearity,ordering properties,integration by parts,the integral split theorem,integrability on a subinterval,integrability of special functions and limit theorem,cauchy-type integrability criterion of gauge integral in higher-order-logic 4(HOL4),and then used them to verify an inverting integrator.