Formalization Of Series Theory In Mathematical Analysis Based On Coq

With the development of computer technology,the mechanization of mathematics has received more and more attention.Formal mathematics is a important branch of the mathematical mechanism.Specifically,it is to describe the definitions and theorems in mathematics,and complete the corresponding proofs in a formal way,so that the proven of the theoretics can easily use the computer to verify.Recently,with the emergence of proof aids such as Coq and Isabelle,the research of formal mathematics has also made considerable progress.Domestic and foreign scholars have also initiated many formal proof projects,which has further enriched related results.The formalization of basic theories is particularly important to the study of formal mathematics.Series theory is an important content in mathematical analysis and the foundation of other mathematical theories.It has played an important role in the development of physics,astronomy and other disciplines.This article is to use the interactive theorem proving tool Coq to realize the formal proof of the series theory.The main content of the work is as follows:(1)The formal description of concepts such as set,function,and sequence are given,and the formal proofs of the theorems of limit uniqueness,monotonic bounded theorem,Cauchy convergence criterion,power function,etc.are completed.These prepare for the proof of series theory.(2)The number series is described through the sequence,and the formal proofs of the related theorems such as the Cauchy criterion of series,geometric series,the discrimination method of positive series,the Leibniz discrimination method,the nature of absolute convergence series are completed.(3)The function series is described through the function sequence,and the formal definition of the uniform convergence of the function sequence and the function series are given.The formal proofs of the related theorems such as the "discrimination and nature of uniform convergence"and the Cauchy criterion are completed.Finally,the theorems related to power series,such as Abel's theorem,continuity of functions,Taylor formula,expansion of power series,etc.are formalized.All the codes in this article have been verified in Coq,and the proof process fully reflects the standard,rigorous and reliable characteristics of Coq.