Formal verification of mathematical theory has received widespread concern and grown rapidly. The formalization of the fundamental theory will contribute to the development of large projects. In this paper, we present the formalization in Coq of calculus without limit theory. The theory aims to found a new form of calculus more easily but rigorously. This theory as an innovation differs from traditional calculus but is equivalent and more comprehensible. First, the definition of the difference-quotient control function is given intuitively from the physical facts. Further, conditions are added to it to get the derivative, and define the integral by the axiomatization. Then some important conclusions in calculus such as the Newton–Leibniz formula and the Taylor formula can be formally verified. This shows that this theory can be independent of limit theory, and any proof does not involve real number completeness. This work can help learners to study calculus and lay the foundation for many applications.
Keywords: calculus; difference-quotient control function; Coq; formalization; limit theory
As proof assistants Coq [[
As one of the milestone accomplishments in mathematics history, calculus was founded more than 300 years ago. It greatly promoted the development of mathematics and other scientific fields, and solved many problems in practical engineering. Newton and Leibniz first created calculus, which settled many historical mathematical problems at that time and made a profound influence. Due to the concept of vague infinitesimal, however, it was questioned and this caused the second mathematical crisis.
Lagrange endeavored to establish the whole calculus theory on Taylor formula to avoid dealing with Newton's "fluxion", and Leibniz's "infinitesimal", but the convergence of infinite series still could not avoid the concept of limit. Until the 19th century, the progress of analysis led mathematicians to establish a rigorous limit theory [[
In order to enable learners to study calculus theory with less time and energy, several scholars [[
The calculus without limit theory can be founded rigorously and comprehensibly. Moreover, most propositions whose proof needs to involve completeness, continuity and limit in traditional calculus can be proved directly in this theory. This does not mean, however, that limit theory should never be learned [[
Our formalization draws lessons from all the former works and sorts out a more complete and systematic version. This work is based on the formal system of Landau's "Foundations of Analysis" [[
In this work, the concept of difference-quotient control function is first introduced from motion law. Next, the elementary definitions of uniform derivative and strong derivative can be naturally obtained. Then, the integral system and definite integral are given by axiomatization. At the same time, we discuss the relationship between them. Furthermore, we present the related concept of higher order derivative. At last, some important theorems in calculus can be directly proved, and this suggests that this theory does not rely on real number completeness and limit theory. On the one hand, every proof is verified by Coq to show rigor and correctness. On the other hand, we make up for missing proof details to make it more complete. In addition, there are some innovations of formal methods in the proof process. The proofs are checked formally using the Coq proof assistant, and the machine proving progress is rigorous and reliable.
The paper is organized in the following way. Section 2 is dedicated to related work. Section 3 briefly states the necessary background needed for understanding this work. Section 4 introduces some definitions and consequences concerning them needed in establishing the theory. Section 5 presents the formalization of calculus without limit theory. Section 6 describes the definition of higher order derivative and related properties. Section 7 discusses the proof of critical theorems in calculus. Finally, we draw our conclusions and discuss some potential further work in Section 8.
In the 1960s, Ljusternik et al. [[
There already exist some formalizations of Landau's "Foundations of Analysis" [[
Our previous paper [[
The Coq system uses a very expressive variation on typed
Axiom classicT : ∀ P, {P} + {~P}. Axiom prop_ext : ∀ P Q, P <-> Q -> P = Q. Axiom fun_ext : ∀ {T1 T2 : Type } (P Q :T1 -> T2), (∀ m, P m = Q m) -> P = Q.
The first one can be used to build the piecewise function according to the correctness of the proposition, and the definition of real addition uses it first. The second one states that equivalent propositions can be replaced by each other, and further, we can derive proof irrelevance which is necessary to substitute equivalent types in proofs. The last one [[
∀ {A : Type } {P :A -> Prop }, (∀ a, P a ↔ Q a) → P = Q.
In addition, more details are discussed in Section 3.2 of our paper [[
In the formalization of calculus without limit theory, another axiom needs to be introduced to instantiate an existing variable that cannot be constructed. This axiom called "cid" is short for "constructive_indefinite_description" in the standard library, and we can define the function to get an element satisfying a specific property by it. This function appears only in definitions or theorem statements because in propositional proofs we "elim" the existential to get an existential witness. The formal descriptions are as follows: Axiom cid : ∀ {A : Type } {P :A -> Prop }, (∃ x, P x) -> { x :A | P x }. Definition Getele {A : Type } {P :A -> Prop } (Q :∃ x, P x) ≔ proj1_sig (cid Q).
Landau's "Foundations of Analysis" [[
This system formalizes the set of strictly positive natural numbers, i.e., natural numbers without zero. For readability, "1" means One, and "x"' means the successor of x. The formalization of the set of strictly positive natural numbers is as follows:
Inductive Nat : Type ≔ | One | Successor : Nat -> Nat. Notation "1" ≔ One. Notation " x ' " ≔ (Successor x)(at level 0).
Then the whole formalization strictly follows Landau's "Foundations of Analysis", and we do not discuss it in detail. If you are interested, the complete source is available online
https://github.com/coderfys/Analysis/tree/main/Foundations%5fof%5fAnalysis/, accessed on 10 June 2021
The definitions of some operations are different from the traditional ones. For example, natural number subtraction is a partial function; the definition of subtraction needs three input parameters: Two natural numbers and a proof that the second one is less than the first one. For example, "
The formal definition of the real valued function is as follows:
Definition RFun ≔ Real -> Real.
We define a conversion from a univariate function to a bivariate function like this:
Definition input2Mi (F :Rfun) ≔ λ u v, F(v) - F(u). Notation "F #" ≔ (input2Mi F)(at level 5).
The identical function and constant function are represented by
Definition Δ :Rfun ≔ λ x, x. Definition ϕ :Real -> Rfun ≔ λ C, (λ _, C).
Here are the formalizations of function operations (
Definition mult_fun c (f :Rfun) ≔ λ x, c · f(x). Definition multfun_ (f :Rfun) c ≔ λ x, f(c · x). Definition multfun_pl (f :Rfun) c d ≔ λ x, f(c · x + d). Definition minus_fun (f :Rfun) ≔ λ x, - f(x). Definition Plus_Fun (f g :Rfun) ≔ λ x, f(x) + g(x). Definition Minus_Fun (f g :Rfun) ≔ λ x, f(x) - g(x). Definition Mult_Fun (f g :Rfun) ≔ λ x, f(x) · g(x). Definition maxfun (f g :Rfun) ≔ λ x, match (Rcase (f x)(g x)) with | left _ => g x | right _ => f x end.
The formalizations of increasing (strictly) function and decreasing (strictly) function are as follows:
Definition fun_inc f I ≔ ∀ x y, x ∈ I -> y ∈ I -> x < y -> f x ≤ f y. Definition fun_sinc f I ≔ ∀ x y, x ∈ I -> y ∈ I -> x < y -> f x < f y. Definition fun_dec f I ≔ ∀ x y, x ∈ I -> y ∈ I -> x < y -> f y ≤ f x. Definition fun_sdec f I ≔ ∀ x y, x ∈ I -> y ∈ I -> x < y -> f x > f y. Definition convexdown f I ≔ ∀ x1 x2, x1 ∈ I -> x2 ∈ I -> ∀ c, c > O -> c < 1 -> f(c·x1+(1-c)·x2) ≤ c·f(x1) + (1-c)·f(x2). Definition convexup f I ≔ ∀ x1 x2, x1 ∈ I -> x2 ∈ I -> ∀ c, c > O -> c < 1 -> c·f(x1) + (1-c)·f(x2) ≤ f(c·x1+(1-c)·x2).
Here are the formalizations of positive value increasing function, unbounded reciprocal function and bounded function as follows.
Definition fun_pinc f I ≔ (∀ z, z ∈ I -> f z > O) /\ fun_inc f I. Definition unbRecF (f :Rfun) I ≔ ∀ M, ∃ z l, z ∈ I /\ M < |(1/(f z)) l|. Definition bound_ran f a b ≔ ∃ A, A > O /\ ∀ x, x ∈ [a|b] -> |f x| < A.
We can get some propositions from the above definitions. The identical mapping is a positive value increasing function and an unbounded reciprocal function. If both
Fact fpcp1 : ∀ a b, fun_pinc Δ (O|b-a]. Fact fpcp2 : ∀ {d1 d2 R}, fun_pinc d1 R -> fun_pinc d2 R -> fun_pinc (maxfun d1 d2) R. Fact ubrp1 : ∀ {a b}, a~< b -> unbRecF Δ (O|b-a]. Fact ubrp2 : ∀ {d1 d2 R}, fun_pinc d1 R -> fun_pinc d2 R -> unbRecF d1 R -> unbRecF d2 R -> unbRecF (maxfun d1 d2) R. Fact brp1 : ∀ {f d a b}, fun_pinc d (O|b-a] -> (∀ x h, x ∈ [a|b] -> (x+h) ∈ [a|b] -> |f(x+h) - f(x)| ≤ d(|h|)) -> bound_ran f a b.
Moreover, we define a uniformly continuous function by two definitions above. It is defined in Coq as follows:
Definition uniform_continuous f a b ≔ ∃ d, fun_pinc d (O|b-a] /\ unbRecF d (O|b-a] /\ ∀ x h, x ∈ [a|b] -> (x+h) ∈ [a|b] -> |f(x+h) - f(x)| ≤ d(|h|).
Furthermore, we can get that if f is uniformly continuous on
Fact uclt : ∀ {f a b}, uniform_continuous f a b -> a < b. Fact ucbound : ∀ {f a b}, uniform_continuous f a b -> bound_ran f a b.
Here is the formalization of a Lipschitz function as follows.
Definition Lipschitz f a b ≔ ∃ M, M > O /\ ∀ x h, x ∈ [a|b] -> (x+h) ∈ [a|b] -> |f(x+h) - f(x)| ≤ M·|h|.
Further, we can prove that a function is bounded.
Fact lipbound : ∀ {f a b}, Lipschitz f a b -> bound_ran f a b.
"Calculus without limit theory is founded upon two physical facts: (
Let functions F and f be defined on
then the function f is called the difference-quotient control function (DCF) of F on
Its formalization is as follows (as shown in Table 1, "uneqOP l" is the proof of "
Definition diff_quo_median F f a b ≔ ∀ u v l, u ∈ [a|b] -> v ∈ [a|b] -> ∃ p q, p ∈ [u|v] /\ q ∈ [u|v] /\ f p ≤ ((F v - F u)/(v-u))(uneqOP l) /\ ((F v - F u)/(v-u))(uneqOP l) ≤ f q.
Let f be the DCF of F on
Their formalizations are as follows:
Fact medC : ∀ a b C, diff_quo_median (ϕ(C)) (ϕ(O)) a b. Fact medCx : ∀ a b C, diff_quo_median (λ x, C·x) (ϕ(C)) a b. Fact medfMu : ∀ {a b F f} c, diff_quo_median F f a b -> diff_quo_median (mult_fun c F) (mult_fun c f) a b. Fact medf_mi : ∀ {F f a b}, diff_quo_median F f a b -> diff_quo_median (λ x, F(-x)) (λ x, -f(-x)) (-b) (-a). Fact medf_cd : ∀ {F f a b} c d l, diff_quo_median F f a b -> diff_quo_median (multfun_pl F c d) (mult_fun c (multfun_pl f c d))(((a-d)/c) (uneqOP l))(((b-d)/c) (uneqOP l)).
Next, we can get the relation between DCF and monotonicity, concavity.
- If
- If
- If f is increasing(decreasing) in I, then F is convex down(convex up) in I.
Their formalizations are as follows:
Fact medpos_inc : ∀ F f a b, diff_quo_median F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≥ O) -> fun_inc F [a|b]. Fact medneg_dec : ∀ F f a b, diff_quo_median F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≤ O) -> fun_dec F [a|b]. Fact medpos_sinc : ∀ F f a b, diff_quo_median F f a b -> (∀ x, x ∈ [a|b] -> f(x) > O) -> fun_sinc F [a|b]. Fact medneg_sdec : ∀ F f a b, diff_quo_median F f a b -> (∀ x, x ∈ [a|b] -> f(x) < O) -> fun_sdec F [a|b]. Fact medconc : ∀ {F f a b}, diff_quo_median F f a b -> fun_inc f [a|b] -> convexdown F [a|b]. Fact medconv : ∀ {F f a b}, diff_quo_median F f a b -> fun_dec f [a|b] -> convexup F [a|b].
The proof of the first four propositions can be easily obtained, and we discuss the proof of the last two propositions in detail. Let f be the DCF of F on
Supposing f is increasing on
Lemma medccpre : ∀ {F f a b}, diff_quo_median F f a b -> fun_inc f [a|b] -> ∀ {x1 x2}, x1 < x2 -> x1 ∈ [a|b] -> x2 ∈ [a|b] -> ∀ c, c > O -> c < 1 -> F(c·x1+(1-c)·x2) ≤ c·F(x1) + (1-c)·F(x2).
Let "y" be equal to "
We multiply the two sides of the inequalities by
We can obtain
If
Supposing f is decreasing on
We multiply the two sides of the inequalities by
Let functions F and f be defined on
then f is called the uniform derivative function (UnD) of F on
Definition uni_derivative F f a b ≔ ∃ d, pos_inc d (O|b-a] /\ unbRecF d (O|b-a] /\ ∃ M, O < M /\ ∀ x h, x ∈ [a|b] -> (x+h) ∈ [a|b] -> |F(x+h) - F(x) - f(x)·h| ≤ M·|h|·d(|h|). Definition uni_derivability F a b ≔ ∃ f, uni_derivative F f a b.
From the definition of UnD, we can prove that f is a UnD of F on
Fact der_lt : ∀ {F f a b}, uni_derivative F f a b -> a < b.
According to the definition, there exist d with unbounded reciprocals on
Moreover, f is a UnD of F on
Fact dersub : ∀ {F f u v a b}, u ∈ [a|b] -> v ∈ [a|b] -> v-u > O -> uni_derivative F f a b -> uni_derivative F f u v.
Furthermore, if f is a UnD of F on
Fact ucderf : ∀ {F f a b}, uni_derivative F f a b -> uniform_continuous f a b. Fact boundderf : ∀ {F f a b}, uni_derivative F f a b -> bound_ran f a b. Fact lipderF : ∀ {F f a b}, uni_derivative F f a b -> Lipschitz F a b. Fact boundderF : ∀ {F f a b}, uni_derivative F f a b -> bound_ran F a b.
On the other hand, we can prove the uniqueness of the UnD. Let both
Fact unider : ∀ {F f1 f2 a b}, uni_derivative F f1 a b -> uni_derivative F f2 a b -> ∀ x, x ∈ [a|b] -> f1 x = f2 x.
Both
Let M be max(
Assume to the contrary that it is. There exist
Besides the properties of DCF, there are some conclusions of UnD about binary operations. Let
Their formalizations are as follows:
Fact derC : ∀ {a b} C, a~< b -> uni_derivative (ϕ(C)) (ϕ(O)) a b. Fact derCx : ∀ {a b} C, a~< b -> uni_derivative (λ x, C·x) (ϕ(C)) a b. Fact derfMu : ∀ {a b F f} c, uni_derivative F f a b -> uni_derivative (mult_fun c F) (mult_fun c f) a b. Fact derf_mi : ∀ {F f a b}, uni_derivative F f a b -> uni_derivative (λ x, F(-x)) (λ x, -f(-x)) (-b) (-a). Fact derf_cd : ∀ {F f a b} c d l, uni_derivative F f a b -> uni_derivative (multfun_pl F c d) (mult_fun c (multfun_pl f c d))(((a-d)/c) (uneqOP l))(((b-d)/c) (uneqOP l)). Fact derFPl : ∀ {F G f g a b}, uni_derivative F f a b -> uni_derivative G g a b -> uni_derivative (Plus_Fun F G) (Plus_Fun f g) a b. Fact derFMi : ∀ {F G f g a b}, uni_derivative F f a b -> uni_derivative G g a b -> uni_derivative (Minus_Fun F G) (Minus_Fun f g) a b. Fact derFMu : ∀ {F G f g a b}, uni_derivative F f a b -> uni_derivative G g a b -> uni_derivative (Mult_Fun F G) (λ x, (f x)·(G x) + (F x)·(g x)) a b.
Next, we present the proof details of how to get the UnD of function multiplication.
Let
By the lemma boundderF, there exist the positive numbers
By the definition of UnD, there exist the positive increasing functions
Let d be max
It is easy to prove when
By the conversion, we can get
Thus the proposition is proved. □
In addition, we can prove the relation between UnD and monotonicity.
Fact derpos_inc : ∀ {F f a b}, uni_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≥ O) -> fun_inc F [a|b]. Fact derneg_dec : ∀ {F f a b}, uni_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≤ O) -> fun_dec F [a|b] Fact derpos_sinc : ∀ {F f a b}, uni_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) > O) -> fun_sinc F [a|b]. Fact derneg_sdec : ∀ {F f a b}, uni_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) < O) -> fun_sdec F [a|b].
The second and fourth propositions can be derived from the first and third propositions by the inverse function, so we present the proof of the first and third propositions.
Let f be a UnD of F and nonnegative on
On the other hand, we can get
Let f be a UnD of F and positive on
Hence
Consequently, we can obtain three corollaries:
- If
- If f is a UnD of
- Let
Their formalizations are as follows:
Corollary derFC : ∀ {F a b}, uni_derivative F (ϕ(O)) a b -> ∀ {x y}, x ∈ [a|b] -> y ∈ [a|b] -> F x = F y. Corollary derF2MiC : ∀ {F1 F2 f a b}, uni_derivative F1 f a b -> uni_derivative F2 f a b -> ∀ {x y}, x ∈ [a|b] -> y ∈ [a|b] -> F1# x y = F2# x y. Corollary derVle : ∀ {F G f g a b}, uni_derivative F f a b -> uni_derivative G g a b -> F a = G a -> (∀ x, x ∈ [a|b] -> f x ≤ g x) -> ∀ x, x ∈ [a|b] -> F x ≤ G x.
Furthermore, we deduce a crucial conclusion. Valuation theorem: If f is a UnD of F, there must exist
Theorem derValT :∀ {F f a b}, uni_derivative F f a b -> ∃ u v, u ∈ [a|b] /\ v ∈ [a|b] /\ f(u)·(b-a) ≤ F(b) - F(a) /\ F(b) - F(a) ≤ f(v)·(b-a).
Assume to the contrary that it is. We have
Finally, we can prove that f is a UnD of F on
Theorem Med_der : ∀ {F f a b}, uni_derivative F f a b <-> diff_quo_median F f a b /\ uniform_continuous f a b.
Sufficiency: According to the definition of UnD, there exists the positive increasing function d with unbounded reciprocals on
It is not difficult to prove that D is positive increasing with unbounded reciprocals on
Necessity: By uniform continuity, there exists the positive increasing function d with unbounded reciprocals on
By the DCF, there exists
We can prove that
Furthermore, we prove
Let functions F and f be defined on
then f is called a strong derivative function (StD) of F on
Definition str_derivative F f a b ≔ ∃ M, O < M /\ ∀ x h, x ∈ [a|b] -> (x+h) ∈ [a|b] -> |F(x+h) - F(x) - f(x)·h| ≤ M·h^2. Definition str_derivability F a b ≔ ∃ f, str_derivative F f a b.
From the definition of StD, we can prove the proposition: Every function f is the StD of F on
Fact std_le : ∀ F a b, b ≤ a -> ∀ f, str_derivative F f a b. Fact std_lt : ∀ {F f a b}, (a < b -> str_derivative F f a b) -> str_derivative F f a b.
Moreover, we can get the relation between StD and UnD. If f is an StD of F on
Fact std_imply_der : ∀ {F f a b}, a < b -> str_derivative F f a b -> uni_derivative F f a b.
Furthermore, we can deduce that if f is an StD of F on
Fact lipstdf : ∀ {F f a b}, str_derivative F f a b -> Lipschitz f a b. Fact boundstdf : ∀ {F f a b}, str_derivative F f a b -> bound_ran f a b. Fact lipstdF : ∀ {F f a b}, str_derivative F f a b -> Lipschitz F a b. Fact boundstdF : ∀ {F f a b}, str_derivative F f a b -> bound_ran F a b.
As for UnD, there are several properties of StD we would state. Since most of these properties are similar, we only show the formal descriptions to avoid redundancy. While some proposition cannot be obtained directly, it can refer to the proof methods of UnD's related proposition.
Fact stdC : ∀ {a b} C, str_derivative (ϕ(C)) (ϕ(O)) a b. Fact stdCx : ∀ {a b} C, str_derivative (λ x, C·x) (ϕ(C)) a b. Fact stdfMu : ∀ {a b F f} c, str_derivative F f a b -> str_derivative (mult_fun c F) (mult_fun c f) a b. Fact stdf_mi : ∀ {F f a b}, str_derivative F f a b -> str_derivative (λ x, F(-x)) (λ x, -f(-x)) (-b) (-a). Fact stdf_cd : ∀ {F f a b} c d l, str_derivative F f a b -> str_derivative (multfun_pl F c d) (mult_fun c (multfun_pl f c d))(((a-d)/c) (uneqOP l))(((b-d)/c) (uneqOP l)). Fact stdFPl : ∀ {F G f g a b}, str_derivative F f a b -> str_derivative G g a b -> str_derivative (Plus_Fun F G) (Plus_Fun f g) a b. Fact stdFMi : ∀ {F G f g a b}, str_derivative F f a b -> str_derivative G g a b -> str_derivative (Minus_Fun F G) (Minus_Fun f g) a b. Fact stdFMu : ∀ {F G f g a b}, str_derivative F f a b -> str_derivative G g a b -> str_derivative (Mult_Fun F G) (λ x, (f x)·(G x) + (F x)·(g x)) a b.
Some propositions for StD can be proved directly by the conclusions of UnD's related propositions, such as uniqueness, monotonicity, concavity.
Corollary unistd : ∀ {F f1 f2 a b}, a~< b -> str_derivative F f1 a b -> str_derivative F f2 a b -> ∀ x, x ∈ [a|b] -> f1 x = f2 x. Corollary stdpos_inc : ∀ {F f a b}, str_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≥ O) -> fun_inc F [a|b]. Corollary stdneg_dec : ∀ {F f a b}, str_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) ≤ O) -> fun_dec F [a|b]. Corollary stdpos_sinc : ∀ {F f a b}, str_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) > O) -> fun_sinc F [a|b]. Corollary stdneg_sdec : ∀ {F f a b}, str_derivative F f a b -> (∀ x, x ∈ [a|b] -> f(x) < O) -> fun_sdec F [a|b]. Corollary stdconc : ∀ {F f a b}, str_derivative F f a b -> fun_inc f [a|b] -> convexdown F [a|b]. Corollary stdconv : ∀ {F f a b}, str_derivative F f a b -> fun_dec f [a|b] -> convexup F [a|b].
Further, we can prove that f is an StD of F on
Theorem Med_std : ∀ {F f a b}, str_derivative F f a b <-> diff_quo_median F f a b /\ Lipschitz f a b.
Sufficiency: Let f be an StD of F on
By adding the two inequalities, we can get that
Necessity: Let f be a DCF of F and a Lipschitz function on
According to the definition of DCF, there exists
We can get that
Furthermore, we prove
The last theorem in this section and the previous one show the close relationship between DCF, UnD and StD.
Let I be an interval and S be a binary function. If the following properties hold:
Additivity:
Intermediate Value Property:
then S is called an integral system of f on I. If f has a unique integral system S on I, then f is said to be integrable on I, and the value of
Here are the formal descriptions:
Definition additivity S a b≔ ∀ u v w, u ∈ [a|b] -> v ∈ [a|b] -> w ∈ [a|b] -> S u v + S v w = S u w. Definition intermed S f a b ≔ ∀ u v, u ∈ [a|b] -> v ∈ [a|b] -> v > u -> ∃ p q, p ∈ [u|v] /\ q ∈ [u|v] /\ f(p)·(v-u) ≤ S u v /\ S u v ≤ f(q)·(v-u). Definition integralsystem S f a b ≔ additivity S a b /\ intermed S f a
Next, we can prove two propositions to show the relation between DCF and the integral system.
1. If S is the integral system of f on
Suppose
2. If f is the DCF of F on
On the one hand, it is easy to prove that
The formalizations are as follows:
Theorem Int_med : ∀ {S f a b}, integralsystem S f a b -> ∀ c, c ∈ [a|b] -> diff_quo_median (S c) f a b. Theorem Med_Int : ∀ {F f a b}, diff_quo_median F f a b -> integralsystem F# f a b.
Furthermore, we can get the relation between DCF and definite integral by these propositions.
1. Let S be the definite integral of f on
By the Int_med, we can get that
2. Let f be the DCF of F on
By the Med_Int, we can get that
The formalizations are as follows:
Theorem Int_DefInt : ∀ {S f a b}, S =∫ f a b -> ∀ c, c ∈ [a|b] -> ∀ F, diff_quo_median F f a b -> ∀ u v, u ∈ [a|b] -> v ∈ [a|b] -> (S c)# u v = F# u v. Theorem DefInt_Int : ∀ {F f a b} , diff_quo_median F f a b -> (∀ F', diff_quo_median F' f a b -> ∀ u v, u ∈ [a|b] -> v ∈ [a|b] -> F# u v = F'# u v) -> F# =∫ f a b.
In view of the importance and independent meaning of higher order derivative in calculus, we will focus on it in this section. Specifically, we only consider the higher order form of UnD because it is more applicable than StD. Moreover, some essential contents about higher order strong derivative are shown in Appendix A.
f is the n order derivative of F on
Fixpoint N_uni_derivative F f a b n ≔ match n with | 1 => uni_derivative F f a b | p' => ∃ f1, uni_derivative F f1 a b /\ N_uni_derivative f1 f a b p end. Definition N_uni_derivability F a b n ≔ ∃ f, N_uni_derivative F f a b n.
We can prove the equivalent definition of higher order derivative.
Fact NderNec : ∀ {F f a b n}, N_uni_derivative F f a b n' -> ∃ f1, N_uni_derivative F f1 a b n /\ uni_derivative f1 f a b. Fact NderSuf : ∀ {F f a b n}, (∃ f1, N_uni_derivative F f1 a b n /\ uni_derivative f1 f a b) -> N_uni_derivative F f a b n'.
Then, we can prove the uniqueness of higher order derivative.
Fact uniNder : ∀ {F f1 f2 a b k}, N_uni_derivative F f1 a b k -> N_uni_derivative F f2 a b k -> ∀ x, x ∈ [a|b] -> f1 x = f2 x.
Further, we can prove the following facts by the uniqueness of higher order derivative.
In particular, when
The formalizations are as follows:
Fact NderOrdPl : ∀ {F f1 f2 a b n k}, N_uni_derivative F f1 a b n -> N_uni_derivative f1 f2 a b k -> N_uni_derivative F f2 a b (Plus_N n k). Fact NderOrdMi : ∀ {F f1 f2 a b n k}, N_uni_derivative F f1 a b n -> N_uni_derivative F f2 a b (Plus_N n k) -> N_uni_derivative f1 f2 a b k. Fact Nderp1 : ∀ {F f1 f2 a b n}, N_uni_derivative F f1 a b n -> N_uni_derivative F f2 a b n' -> uni_derivative f1 f2 a b. Fact Nderp2 : ∀ {F f1 f2 a b n}, N_uni_derivative F f1 a b n -> uni_derivative f1 f2 a b -> N_uni_derivative F f2 a b n'.
Like the UnD, higher order derivative has two properties as follows:
Fact Fact_lt : ∀ {F a b k}, N_uni_derivability F a b k -> a < b. Fact Nderin : ∀ {F f a b c n}, c ∈ [a|b] -> c < b -> N_uni_derivative F f a b n -> N_uni_derivative F f c b n.
Next, we define four functions (
Fact Nderpred : ∀ {F a b n}, N_uni_derivability F a b n' -> N_uni_derivability F a b n. Fact Nderltn : ∀ {F a b n k}, ILT_N k n -> N_uni_derivability F a b n -> N_uni_derivability F a b k. Fact Nderlen : ∀ {F a b n m} l, N_uni_derivability F a b n -> N_uni_derivability F a b (Minus_N n' m (Le_Lt l)). Definition n_th {F a b n} (H :N_uni_derivability F a b n) ≔ Getele H. Definition p_th {F a b n} (H :N_uni_derivability F a b n') ≔ Getele (Nderpred H). Definition k_th {F a b n} k (H :ILT_N k n) (H0 :N_uni_derivability F a b n) ≔ Getele (Nderltn H H0). Definition m_th {F a b n} k (H :ILE_N k n) (H0 :N_uni_derivability F a b n) ≔ Getele (Nderlen H H0).
We can get the conclusion that if F has the n order derivability, then
Fact NderCut : ∀ {F a b n} k l1 (l :N_uni_derivability F a b n), N_uni_derivability (k_th k l1 l) a b (Minus_N n k l1).
There are several propositions about the higher order derivative operation.
Fact NderfMu : ∀ {F f a b c n}, N_uni_derivative F f a b n -> N_uni_derivative (mult_fun c F) (mult_fun c f) a b n. Fact NderFPl : ∀ {F f G g a b n}, N_uni_derivative F f a b n -> N_uni_derivative G g a b n -> N_uni_derivative (Plus_Fun F G) (Plus_Fun f g) a b n. Fact NderFMi : ∀ {F f G g a b n}, N_uni_derivative F f a b n -> N_uni_derivative G g a b n -> N_uni_derivative (Minus_Fun F G) (Minus_Fun f g) a b n. Fact Nderf_mi : ∀ {F f a b n}, N_uni_derivative F f a b n -> N_uni_derivative (λ x, F(-x)) (λ x, (-(
Let f be the UnD of F, then
The formalization is as follows:
Theorem NewtonLeibniz : ∀ {F f a b} , uni_derivative F f a b -> F# =∫ f a b.
Since f is a UnD of F on
As shown in Figure 1, the formal proof process is very simple.
If f is a uniformly continuous function and f has the definite integral on
Theorem UpLimVarInt : ∀ {S f a b}, uniform_continuous f a b -> S =∫ f a b -> uni_derivative (S a) f a b.
Due to the uniform continuity, we can get
As shown in Figure 2, the formal proof process is highly readable in Coq.
The Taylor formula is an important conclusion in calculus, and it has a far-reaching meaning. As it involves much content, we will divide it into four parts to present it.
Let H have the n order derivability on
then
The formalization is as follows:
Theorem TaylorLemma : ∀ {H a b n m M} (l :N_uni_derivability H a b n), H a = O -> (∀ k l1, (k_th k l1 l) a = O) -> (∀ x, x ∈ [a|b] -> m ≤ (n_th l) x) -> (∀ x, x ∈ [a|b] -> (n_th l) x ≤ M) -> ∀ x, x ∈ [a|b] -> m·(Rdifa ((x-a)^n) n) ≤ H x /\ H x ≤ M·(Rdifa ((x-a)^n) n).
First, we need to prove a lemma:
The formalization is as follows:
Fact tlp : ∀ {m n} l, ILE_N (Minus_N n' m (Le_Lt l)) n. Lemma TLpre : ∀ {H a b n m M} (l :N_uni_derivability H a b n), (∀ k l1, (k_th k l1 l) a = O) -> (∀ x, x ∈ [a|b] -> m ≤ (n_th l) x) -> (∀ x, x ∈ [a|b] -> (n_th l) x ≤ M) -> ∀ k l1 l2, let j≔(Minus_N k 1 l2) in let i≔ (Minus_N n' k (Le_Lt l1)) in ∀ x, x ∈ [a|b] -> m·(Rdifa ((x-a)^j) j) ≤ (m_th i (tlp l1) l) x /\ (m_th i (tlp l1) l) x ≤ M·(Rdifa ((x-a)^j) j).
Using the incomplete mathematical induction for k.
When
Let
Suppose case
we prove the
Let
Next we prove the Taylor Lemma.
When
When
Let
Supposing F has the n order derivability on
represents the main term of the n order Taylor formula about F on c, that is, the Taylor formula without remainder.
It is defined in Coq as follows:
Fixpoint TaylorFormula_main F a b c n :N_uni_derivability F a b n -> Rfun ≔ match n with | 1 => λ _ _, F c | p' => λ l x, (p_th l c)·(Rdifa ((x-c)^p) p) + TaylorFormula_main F a b c p (Nderpred l) x end.
These two properties can be obtained directly from the expression:
Here are the formalizations.
Fact tayp1 : ∀ F a b c n l, TaylorFormula_main F a b c n l c = F c. Fact tayp2 : ∀ {F a b c n} l, c ∈ [a|b] -> N_uni_derivative (TaylorFormula_main F a b c n l) (ϕ(O)) a b n.
Supposing F has the n order derivability on
represents the k-th derivative of the main term of the n order Taylor formula about F on c.
It is defined in Coq as follows:
Fact Ndec : ∀ n m, {ILT_N n m} + {ILE_N m n}. Definition TFmain_kthd F a b c n k (l :N_uni_derivability F a b n) :Rfun ≔ match Ndec k n with | left l1 => TaylorFormula_main (k_th k l1 l) a b c (Minus_N n k l1) (NderCut k l1 l) | right _ => ϕ(O) end.
These properties can be obtained directly from the expression:
Here are the formalizations.
Fact taykdp1 : ∀ {F a b c k n l} l0, c ∈ [a|b] -> let m≔Minus_N n k l0 in (TFmain_kthd F a b c n' k l) = Plus_Fun (λ x, p_th l c · Rdifa ((x-c)^m) m) (TFmain_kthd F a b c n k (Nderpred l)). Fact taykdp2 : ∀ F a b c n l, TaylorFormula_kder F a b c n' n l = ϕ(n_th (Nderpred l) c). Fact taykdp3 : ∀ F a b c n l k l1, c ∈ [a|b] -> TaylorFormula_kder F a b c n k l c = k_th k l1 l c.
At last, we can verify the correctness of the definition, i.e.,
Fact tayder : ∀ {F a b n} k l c, c ∈ [a|b] -> N_uni_derivative (TaylorFormula_main F a b c n l) (TFmain_kthd F a b c n k l) a b k.
Let F have the n order derivability on
The formalization of this theorem is as follows:
Theorem TaylorThoerem : ∀ {F a b n l}, ∀ M, (∀ x, x ∈ [a|b] -> |(n_th l) x|≤M) -> ∀ c x, c ∈ [a|b] -> x ∈ [a|b] -> |F(x)-(TaylorFormula_main F a b c n l x)|≤ M·(Rdifa (|x-c|^n) n).
First, we prove the lemma: If
Lemma TTpre : ∀ {F a b n M l}, (∀ x, x ∈ [a|b] -> |(n_th l) x| ≤ M) -> ∀ c x, c ∈ [a|b] -> x ∈ [c|b] -> |F(x)-(TaylorFormula_main F a b c n l x)|≤ M·(Rdifa (|x-c|^n) n).
When
When
Next we prove: If
If
As long as
So the proposition is proved. We can deduce that the Taylor formula for strong derivative also holds; the details can be found in the appendix. □
The calculus without limit theory starts from the physical facts. Then, the concept of the difference-quotient control function is introduced, which corresponds to but is not equivalent to the mean value theorem in traditional calculus. The conclusions drawn from it are amazing, but it is not necessarily the derivative. On the one hand, it can become a strong derivative with a Lipschitz function, which is enough for practical application in the field of science and engineering. On the other hand, it can become a uniform derivative with a uniformly continuous function to relax the too restrictive condition of a Lipschitz function. Both of them have all the properties of a difference-quotient control function and have uniqueness and can carry out binary operations. Furthermore, the integral system and definite integral are naturally defined by axiomatization and are closely related to the difference-quotient control function. With these basic concepts, some important theorems in calculus can be proved. Compared with derivative in the generic sense, the strong derivative also satisfies that the derivative is a Lipschitz function and the uniform derivative also satisfies that the derivative is continuous. In summary, the condition of the derivative in this theory is indeed stronger than that of the traditional derivative, but there is no difference in practical application.
We are formalizing the calculus without limit theory on the basis of a system without real number completeness. It is feasible and rigorous to verify this theory by the proof assistant Coq. Moreover, we obtain some facts which are not pointed out in previously developed paper proofs. Uniform derivability only holds on a strict interval. To prove the strong derivability, we only need to consider whether it holds on a strict interval. So strong derivability implies uniform derivability only on a strict interval. The complete source files containing the Coq formalization and proofs are accessible at:
https://github.com/coderfys/Analysis/tree/main/Calculus%5fwithout%5flimt, accessed on 10 June 2021
In the future, we will complete the formalization of deeper contents of this theory. At the same time, this theory can also be applied to calculus teaching. Furthermore, we can supplement the real number completeness to enrich the theory and unify it with traditional calculus in a formal way.
Graph: Figure 1 The formalization of Newton Leibniz formula.
Graph: Figure 2 The formalization of differentiability of upper limit-variable integral.
Table 1 The meaning of the code in real number theory system.
Code Meanning Minus_N absolute value of factorial , , RdiN , Rdifa , , maxfun
Conceptualization, Y.F. and W.Y.; methodology, Y.F. and W.Y.; software, Y.F.; validation, Y.F. and W.Y.; formal analysis, Y.F. and W.Y.; investigation, Y.F. and W.Y.; resources, Y.F.; data curation, Y.F.; writing—original draft preparation, Y.F.; writing—review and editing, Y.F.; supervision, W.Y.; project administration, Y.F. and W.Y.; funding acquisition, W.Y. All authors have read and agreed to the published version of the manuscript.
This research was funded by National Natural Science Foundation (NNSF) of China under Grant 61936008, 61571064.
The authors declare no conflict of interest.
We are grateful to the anonymous reviewers, whose comments greatly helped to improve the presentation of our research in this article.
As shown in Figure A1, the upper half contains the definition of higher order form of strong derivative and its properties, and the lower half shows the formal proof of Taylor Formula for strong derivative.
Graph: Figure A1 Higher order strong derivative.
By Yaoshun Fu and Wensheng Yu
Reported by Author; Author