12 2008 Ab90 the Function F is Continuous on the Closed Interval
Mathematical Software – ICMS 2020. 2020 Jun 6; 12097: 272–280.
A Formalization of Properties of Continuous Functions on Closed Intervals
Guest Editor (s): Anna Maria Bigatti,8 Jacques Carette,9 James H. Davenport,10 Michael Joswig,11 and Timo de Wolff12
8Dipartimento di Matematica, Università degli Studi di Genova, Genova, Genova Italy
9Computing and Software, McMaster University, Hamilton, ON Canada
10Department of Computer Science, University of Bath, Bath, UK
11Institut für Mathematik, MA 6-2, TU Berlin, Berlin, Germany
12Technische Universität Braunschweig, Braunschweig, Germany
Yaoshun Fu
Beijing Key Laboratory of Space-Ground Interconnection and Convergence School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, 100876 China
Wensheng Yu
Beijing Key Laboratory of Space-Ground Interconnection and Convergence School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing, 100876 China
Abstract
Formal mathematics is getting increasing attention in mathematics and computer science. In particular, the formalization of calculus has important applications in engineering design and analysis. In this paper, we present a formal proof of some fundamental theorems of continuous functions on closed intervals based on the Coq proof assistant. In this formalization, we build a real number system referring to Landau's Foundations of Analysis. Then we complete the formalization of the basic definitions of interval, function, and limit and formally prove the theorems including completeness theorem, intermediate value theorem, uniform continuity theorem and others in Coq. The proof process is normalized, rigorous and reliable.
Keywords: Coq, Formalization, Limits, Continuous functions, Closed intervals
Introduction
Analysis is one of the greatest achievements in the history of mathematics. The achievement opens a new era of mathematical progress and plays an important role in development of physics, astronomy, signal processing and other disciplines. Analysis which evolved from calculus is a branch of mathematics that studies limits and related theories [12].
At the end of the 19th century, mathematicians deduced many properties of continuous functions on closed intervals, which undoubtedly promoted the development of analytical theory. There are some important properties of continuous functions on closed intervals including Weierstrass second theorem: Boundedness theorem, Weierstrass first theorem: Extreme value theorem, Bolzano-Cauchy second theorem: Intermediate value theorem, Cantor theorem: Uniform continuity theorem.
Bolzano's Function Theory gives the earliest proofs of the Boundedness theorem and the Extreme value theorem (but published some 100 years later) [15], and Weierstrass proved the Extreme value theorem in Berlin lecture. The Intermediate value theorem was first proved in 1817 by Bolzano, and then Cauchy [7] gave a proof in 1821. The definition of uniform continuity is proposed by Heine, and he published a proof of the Uniform continuity theorem.
With the further research of limits by mathematicians, the establishment of a rigorous and complete system of real numbers theory has become a key issue. In 1872, three major real numbers theories appeared in Germany: Dedekind cut theory, Cantor-Henie-Meray "basic sequence" theory, and Weierstrass "bounded monotone sequence" theory. Among them, the Dedekind cut is particularly recognized, and it is called the creation of human intelligence that does not rely on the intuitiveness of space and time. Then Peano established a natural number theory through a set of axioms, thereby solving the core problems of rational number theory and also the basic problems of real number theory.
In recent years, with the rapid development of computer science, especially the emergence of proof assistant Coq, Isabelle and HOL Light and so on [2, 4, 8, 10, 14, 17], formal proof of mathematical theorems has made great progress. In 2005, the international computer experts Gonthier and Werner provided the formal proof in Coq of the famous "four-color theorem" successfully [5]. After years of hard work, Gonthier again achieved the machine proof in Coq of the "odd order theorem" in 2012 [6]. Those progress make Coq more and more popular in academia. Wiedijk pointed out that relevant research teams around the world have completed or plan to formalize the proof of theorems such as Gödel's first incompleteness theorem, Jordan curve theorem, Prime theorem and Fermat last theorem of a hundred well-known mathematical theorems [17].
Based on "Real number theory" formal system, we formalize the properties of continuous functions on closed intervals. Moreover, we give formal proofs of these theorems, which include the Boundedness theorem, the Extreme value theorem, the Intermediate value theorem, the Uniform continuity theorem. It should be noted that the properties of continuous functions on closed intervals is an important theorem in analysis.
The structure of this article is as follows: In Sect. 2, we introduce the "real number theory" machine proof system. In Sect. 3, we present the formal definition of the function limit and related properties. In Sect. 4, we discuss the machine proof of the properties of continuous functions on closed intervals in detail, which are derived by supremum theorem. In Sect. 5, we draw conclusions and discuss some potential further work.
Real Number Theory System
Before formally proving the properties of continuous functions on closed intervals, we first need to build a formal system of real number theory. van Benthem Jutting [1] completed the formalization in Automath of Landau's "Foundations of Analysis", which was a significant early progress in formal mathematics. Harrison [9] presents formalized real numbers and differential calculus on his HOL Light system. The definition of real numbers in Coq standard library uses the axiomatic way, and based on this, excellent real analysis library Coquelicot [3] has been established. This library accomplishes many achievements, but its definition of real number is non-constructive. Hornung [11] completed the first four chapters of the "Foundations of Analysis" in Coq, which is closed related to our work, however our system is closer to the expression of Landau and more readable. We also completed the complex number part and proved equivalence between eight completeness theorems of real number.
There are several ways to define natural numbers in Coq. Based on Morse-Kelley axiomatic set theory, it is designed to give quickly and naturally a foundation for mathematics, and meanwhile deduce the Peano axioms as theorems [16, 18]. If we start from the more higher type rather than set theory, we can formalize straight Peano axioms as follows:
Based on this, we can use "Parameter" and "Axiom" to define natural number related functions such as addition and multiplication. This way is intuitive but not elegant. The natural numbers defined by "Inductive" can recursively define natural number related functions.
Landau's "Foundations of Analysis" [13] is based on naive set theory and some basic logic. Starting from the Peano axioms, natural numbers (positive integers), fractions (positive), rational numbers/integer (positive) are defined in order. The real number, defined by Dedekind cut, defines complex numbers through real numbers for constructing systematically the whole number system theory. We have completed the Coq formalization of the system, and the complete source is available online:
https://github.com/coderfys/analysis/
In this system, we can prove Dedekind fundamental theorem, and derive Supremum theorem. The proof details are not described, and the formalization is as follows.
Dedekind Fundamental Theorem
Divide all real numbers into two classes, so that the first class and second class are not empty, and each number in the first class is less than each number in the second class. Then there is a unique real number E, so that any number less than E belongs to the first class, and any number greater than E belongs to the second class.
Supremum Theorem
If a non-empty real number set has a upper bound, then there must be a least bound (the Supremum as an example).
Basic Definitions and Properties
The formal definition of functions in this system is as follows:
Related definitions of function continuity:
The function f(x) is continuous at one point implying that
The function f(x) is continuous (left, right) at a point, then the function f(x) is locally bounded at this point (take right continuous for example):
In this real number system, division function requires three parameters, and the third of which is the proof that the second is not 0. Therefore, the "NoO_N" above means " ".
The function f(x) is continuous on [a,b], then is continuous on [a,b]. The function f(x) is continuous on [a,b] and is not everywhere 0, then
is continuous on (take
as an example).
Properties of Continuous Functions on Closed Intervals
Continuous functions have four fundamental properties on closed intervals: Boundedness theorem (Weierstrass second theorem), Extreme value theorem (Weierstrass first theorem), Intermediate value theorem (Bolzano-Cauchy second theorem), Uniform continuity theorem (Cantor theorem). These theorems are the basis of mathematical analysis and the direct expression of real number theory in functions. Our formalizations rely on a logical axiom law of excluded middle.
Theorem 1
Boundedness theorem: A continuous function on a closed interval must be bounded on that interval.
First, we prove a lemma L1: if f(x) is continuous on [a,b], then some neighborhood of z is bounded for any . The notation "
" below represents
in mathematics.
Upper bound: Construct a real number set has an upper bound on
. The formal definition is as follows:
As f(x) is right continuous at the point a, there exists , and f(x) has an upper bound on
, when
proves the proposition. When
, R is not empty. On the other hand, b is an upper bound of R obviously, so R has supremum
, and
.
Case 1( ): According to Lemma L1, there exists
, and f(x) has an upper bound on
. The proposition is proved when
. When
, there is
, which contradicts
is the supremum of R.
Case 2( ): The proposition is proved because of
.
Lower bound: According to the lemma Pr_fun1, it can be deduced that is continuous on [a,b]. From Theorem T1, we know that
has the upper bound "up", then "-up" is the lower bound of f(x) on [a,b].
Theorem 2
Extreme value theorem: The continuous function on the closed interval must achieve the maximum and minimum values in this interval.
Maximum value: Construct a real number set . The formal definition is as follows:
Obviously, R is not empty and we can deduce R has an upper bound by T1, hence R has a supremum M. If there exists and
, the proposition is proved. Otherwise,
for any
. Construct a new function
. Since
for any
[a, b], so g(x) is continuous on [a,b] by Pr_fun2. From T1, g(x) has an supremum K on [a,b], and
. After derivation,
is the upper bound of f(x) on [a,b], which contradicts M is the supremum of R.
Minimum value: According to the lemma Pr_fun1, it can be deduced that is continuous on [a,b]. From Theorem T2, we know that
has a maximum value "max", then "-max" is the minimum value of f(x) on [a,b].
Theorem 3
Intermediate value theorem: If , then for any real number C between f(a), f(b), at least one point c on (a,b) satisfies f (c) = C.
First, we prove a lemma L3: if f(x) is left continuous at point b, and
, then there is z between a,b, satisfies
.
: Construct a real number set
for any x in
. The formal definition is as follows:
: f(x) is right continuous at point a, then there exists
, and
in
, which can be deduced
.
when
and
when
. In summary, R is not empty and b is an upper bound of R, so R has a supremum
, and
. When
, it can deduce contradiction according to Pr_supremum and L3. Therefore
.
Case 1( ): Because f(x) is continuous at point
, by Pr_FunDot there is
, and
for any
, which can be deduced
. Further, we can conclude that
which contradicts
is the supremum of R.
Case 2( ): f(x) is continuous at point
, hence f(x) is left continuous at point
. By L3 there must exist
and
, so z is the upper bound of R, which contradicts
is the supremum of R.
: Refer to T1', T2' proof.
Theorem 4
Uniform continuity theorem: A function is continuous on a closed interval then the function is uniformly continuous on that interval.
Let f(x) be continuous on [a,b], fix any . we construct a real number set
and
when
and
. The formal definition is as follows:
Because f(x) is right continuous at point a, there must exists , and
for any
. Let
, we prove that
. Obviously, b is an upper bound of R, So R has a supremum
and
. As f(x) is continuous at point
, there exists
, and
for any
. Further, we can deduce
for any
. Therefore,
for any
and
.
Case 1( ): When
, the proposition is proved due to the arbitrariness of
. When
, we further prove
, which contradicts
is the supremum of R.
Case 2( ):
, the proposition is proved by the arbitrariness of
.
Conclusion
This paper formalizes limits, continuous functions and related theorems. These theorems include Boundedness theorem, Extreme value theorem, Intermediate value theorem, and Uniform continuity theorem. We have completed their formal proofs based on the real number theory system developed by ourselves. In the future, we will formalize more theorems of continuous functions and make meaningful attempts for formal work in the fields of real analysis and complex analysis. We are grateful to the anonymous reviewers, whose comments much helped to improve the presentation of the research in this article.
Footnotes
This research is supported by National Natural Science Foundation (NNSF) of China under Grant 61936008, 61571064.
Contributor Information
Anna Maria Bigatti, Email: ti.eginu.amid@ittagib.
Jacques Carette, Email: ac.retsamcm@etterac.
James H. Davenport, Email: ku.ca.htab@tropnevad.h.j.
Michael Joswig, Email: ed.nilreb-ut.htam@giwsoj.
Timo de Wolff, Email: ed.giewhcsnuarb-ut@fflow-ed.t.
Yaoshun Fu, Email: nc.ude.tpub@syuf.
Wensheng Yu, Email: nc.ude.tpub@uysw.
References
1. van Benthem Jutting LS. Checking Landau's "Grundlagen" in the AUTOMATH System. Amsterdam: North-Holland; 1994. [Google Scholar]
2. Bertot Y, Castéran P. Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Heidelberg: Spring-Verlag; 2004. [Google Scholar]
3. Boldo S, Lelay C, Melquiond G. Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 2015;9(1):41–62. doi: 10.1007/s11786-014-0181-1. [CrossRef] [Google Scholar]
4. Chlipala A. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. Cambridge: MIT Press; 2013. [Google Scholar]
5. Gonthier G. Formal proof-the four-color theorem. Notices AMS. 2008;55(11):1382–1393. [Google Scholar]
6. Gonthier G, et al. A machine-checked proof of the odd order theorem. In: Blazy S, Paulin-Mohring C, Pichardie D, et al., editors. Interactive Theorem Proving; Heidelberg: Springer; 2013. pp. 163–179. [Google Scholar]
7. Grabiner JV. Who gave you the epsilon? Cauchy and the origins of rigorous calculus. Am. Math. Mon. 1983;90(3):185–194. doi: 10.1080/00029890.1983.11971185. [CrossRef] [Google Scholar]
8. Hales TC. Formal proof. Notices AMS. 2008;55(11):1370–1380. [Google Scholar]
9. Harrison J. Theorem Proving with the Real Numbers. Heidelberg: Springer; 1994. [Google Scholar]
10. Harrison J. Formal proof—theory and practice. Notices AMS. 2008;55(11):1395–1406. [Google Scholar]
11. Hornung, C.: Constructing Number Systems in Coq. Saarland University, Saarbrücken (2011)
12. Katz VJ. A History of Mathematics. Boston: Pearson/Addison-Wesley; 2004. [Google Scholar]
13. Landau E. Foundations of Analysis: The Arithmetic of Whole, Rational, Irrational, and Complex Numbers. New York: Chelsea Publishing Company; 1966. [Google Scholar]
14. Nipkow T, Wenzel M, Paulson LC, editors. Isabelle/HOL; Heidelberg: Springer; 2002. [Google Scholar]
15. Rusnock P, Kerr-Lawson A. Bolzano and uniform continuity. Historia Mathematica. 2005;32(3):303–311. doi: 10.1016/j.hm.2004.11.003. [CrossRef] [Google Scholar]
16. Sun T, Yu W. A formal system of axiomatic set theory in Coq. IEEE Access. 2020;8:21510–21523. doi: 10.1109/ACCESS.2020.2969486. [CrossRef] [Google Scholar]
17. Wiedijk F. Formal proof-getting started. Notices AMS. 2008;55(11):1408–1414. [Google Scholar]
18. Yu W, Sun T, Fu Y. Machine Proof System of Axiomatic Set Theory. Beijing: Science Press; 2020. [Google Scholar]
dawsonwasonerecied.blogspot.com
Source: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7340941/
0 Response to "12 2008 Ab90 the Function F is Continuous on the Closed Interval"
Post a Comment