Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> (Def. 2) There exists r such that for every y such that y ∈ dom f holds r < f (y). Let us consider s1. Let us observe that s1 is upper bounded if and only if: (Def. 3) There exists r such that for every n holds s1(n) < r. Let us observe that s1 is lower bounded if and only if: 1 The propositions (1) and (2) have been removed. 2 The proposition (5) has been removed. 3 The proposition (8) has been removed. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> The articles [6], [8], [1], [7], [4], [9], [2], [5], [10], and [3] provide the notation and terminology for this paper. For simplicity, we adopt the following convention: f is a function, n is a natural number, r, p are real numbers, and x is a set. A sequence of real numbers is a function from N into R. In the sequel s1, s2, s3, s4, s1, s ′ 2 denote sequences of real numbers. We now state two propositions: <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> Summary. Definitions of functional sequences and basic operations on functional sequences from a domain to a domain, point and uniform convergent, limit of functional sequence from a domain to the set of real numbers and facts about properties of the limit of functional sequences are proved. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers. <s> BIB005 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> This paper reports on a construction of the real numbers in the ProofPower implementation of the HOL logic. Since the original construction was implemented, some major improvements to the ideas have been discovered. The improvements involve some entertaining mathematics: it turns out that the Dedekind cuts provide many routes one can travel to get from the ring of integers, Z, to the field of real numbers, R. The traditional stop-over on the way is the field of rational numbers, Q. This paper shows that going via certain rings of algebraic numbers can provide a pleasant alternative to the more well-trodden track. <s> BIB006 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as √2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis. <s> BIB007 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Sequences and Series <s> The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, ℂ and ℝn. Isabelle's new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps. <s> BIB008
Almost all the formalizations define real sequences as functions from natural numbers to real numbers. Only Mizar has a slightly different definition, due to its set theoretical approach to functions. Convergence definitions, however, differ. 4.1.1. Real sequences In the Coq standard library  , C-CoRN/MathClasses, Mizar BIB001 , PVS BIB005 , and ProofPower BIB006 , convergence of a real sequence (u n ) toward ∈ R is defined with the usual property: where R + is the set of positive reals. Note that the definition for C-CoRN/MathClasses works in any ordered field and not just real numbers; also it names this property Cauchy prop while it is not equivalent to Cauchy property in non-complete spaces. Definition (1) is dedicated to real sequences. But some properties can be formalized in a weaker scope, and thus be used later for convergence of real functions. For instance, in Isabelle/HOL, convergence of sequences is defined using convergence in topological spaces BIB008 : where F is a proper filter, i.e. For sequences, the chosen filter is F = {A ⊂ N | ∃N ∈ N, ∀n ∈ N, n ≥ N ⇒ n ∈ A}. Definition (2) will also be used for convergence of real functions, by choosing a different filter (Section 4.2.2). In HOL4 and HOL Light, the definition of convergence in a topological space is formalized using nets: where is a partial order. For sequences, N is a neighborhood for the topology generated by the metric space (R, (x, y) → |y − x|) and is the order on natural numbers. Moreover, function lim gives the limit if it exists using Hilbert's epsilon. Finally, in ACL2(r), a sequence (u n ) converges to ∈ R if u N ≈ (i.e. u N and are infinitesimally close) for all non-standard natural numbers N (Gamboa and Kaufmann 2001). The limit is the standard part of u N for a specific N . These definitions of convergence and limit show the point of choosing non-standard analysis for ACL2(r). Indeed, they make it possible to avoid quantifiers almost entirely. For all these formalizations, compatibility of limit with arithmetic operations (+, −, ×, and /) and relations (=, ≤) is proved. They also provide the usual convergence theorems, e.g. the convergence of Cauchy sequences. While the notion of sub-sequences is useful to prove non-convergence of a sequence in practice, only C-CoRN and Mizar BIB002 include it. 4.1.2. Real series Power series are the usual tool for defining transcendental functions such as exponential and trigonometric functions. So it does not come as a surprise that most formalizations provide an implementation of partial sums, series, and power series. Only Mizar, HOL Light, and C-CoRN/MathClasses, provide more theorems than what is strictly needed for defining elementary functions. PVS provides a development of about 300 lemmas about series and power series too, but they are not used in the main development about real analysis. For instance, there are two definitions of the real exponential function, which are not proved to be equivalent. Series are defined, with few variations, with the usual definition: The Coq standard library and C-CoRN/MathClasses first define the partial sums starting from 0 and use them to define other partial sums. In the standard library, the partial sum m k=n u k is defined as m−n k=0 u k+n . Notice that, when m < n, the natural difference m − n is 0, so the sum between n and m is u n , rather than 0 or the opposite of another sum. Convergent series use an ad-hoc predicate rather than being defined as the convergence of the sequence of partial sums. This unfortunate choice prevents the reuse of theorems on sequences. In C-CoRN, k=0 u k where (u n ) takes value in an abelian group. This time, the definition for the case m < n is a bit more sensible. The convergence of series is given by Definition (4). In HOL4  , Isabelle/HOL, and PVS  , which formalizations are based on Harrison's, With this definition, having a partial sum m k=n u k with m < n is no longer possible, but the way bounds are handled is a bit less natural, since the partial sum is now sum(u, n, m − n + 1). The convergence of partial sums is the convergence of sequences described in Section 4.1.1. In these formalizations, the d'Alembert criterion and convergence of alternated series are proved. In HOL4 and Isabelle/HOL, a function that returns the limit of partial sums is defined using Hilbert's epsilon. In HOL Light, sums have been generalized to having indexes in arbitrary finite sets and there are combinatorial theorems to manipulate them, thus avoiding the above inconvenience. Mizar (Raczkowski and Nedzusiak 1991b) and ProofPower (Arthan 2012) define series using explicitly Definition (4). Various convergence theorems are proved, from the d'Alembert criterion to comparison theorems. The Cauchy product is provided by these formalizations as it is used to prove the usual property on exponential ∀x, y ∈ R, e x+y = e x · e y : n∈N a n n∈N ACL2(r) does not formalize partial sums and series BIB007 ; it uses only sequences to define exponential and trigonometric functions. 4.1.3. Power series and series of functions Power series are defined as functions f : x → n∈N a n x n where the sequence (a n ) takes value in real numbers or in an abelian group. These functions are defined for x such that n∈N a n x n is convergent. HOL Light provides an advanced formalization of complex analysis, e.g. equivalence between holomorphic and analytic functions. As such, this prover comes with a fullyfeatured library when it comes to power series and series of functions. Other systems are much less comprehensive. Indeed, in order to define exponential and trigonometric functions, one does not need many theorems about sequences and series of functions. As a consequence, most provers provide just the definition of power series and some theorems about them. This is the case for HOL4 BIB003 and PVS  . They provide some convergence criteria for power series, e.g. d'Alembert's. They also have a notion of convergence circle. HOL4 provides a theorem about the differentiability of power series. Another way to represent power series is as series of functions, as is done in Coq, C-CoRN, Isabelle/HOL, Mizar BIB004 , and ProofPower (Arthan 2012) For instance, usual theorems about continuity and differentiability for limits of sequences and series are proved and used to study exponential and trigonometric functions. Coq provides a definition of power series and the d'Alembert criterion.