We first define what we mean by the derivative of order [n] of a function.
*)
-alias id "a" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Nth_Derivative/a.var
+*)
-alias id "b" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Nth_Derivative/b.var
+*)
-alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab'.var
+*)
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/Hab.con" "Nth_Derivative__" as definition.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Nth_Derivative/I.con" "Nth_Derivative__" as definition.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n.con" as definition.
(*#*
Unlike first order differentiability, for our definition to be
[Derivative_I_n] relation.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n.con" as definition.
(* UNEXPORTED
End Nth_Derivative
These are the expected extensionality and uniqueness results.
*)
-alias id "a" = "cic:/CoRN/ftc/NthDerivative/Trivia/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Trivia/a.var
+*)
-alias id "b" = "cic:/CoRN/ftc/NthDerivative/Trivia/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Trivia/b.var
+*)
-alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Trivia/Hab'.var
+*)
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/Hab.con" "Trivia__" as definition.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Trivia/I.con" "Trivia__" as definition.
(* end hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_wd.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdr.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_wdl.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_unique.con" as lemma.
(* UNEXPORTED
End Trivia
definition of [Diffble_I_n].
*)
-alias id "a" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/a.var
+*)
-alias id "b" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/b.var
+*)
-alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab'.var
+*)
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/Hab.con" "Basic_Results__" as definition.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Basic_Results/I.con" "Basic_Results__" as definition.
(* end hide *)
We begin by showing that having a higher order derivative implies being differentiable.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_diffble.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_diffble.con" as lemma.
(*#*
If a function is [n] times differentiable then it is also [m] times differentiable for every [m] less or equal than [n].
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/le_imp_Diffble_I.con" as lemma.
(*#*
The next result consolidates our intuition that a function is [n]
derivatives.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_imp_le.con" as lemma.
(*#*
As expected, an [n] times differentiable in [[a,b]] function must be
defined in that interval.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_inc.con" as lemma.
(*#*
Also, the notions of derivative and differentiability are related as expected.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Diffble_I_n_imp_deriv_n.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_n_imp_Diffble_I_n.con" as lemma.
(*#*
From this we can prove that if [F] has an nth order derivative in
[[a,b]] then both [F] and its derivative are defined in that interval.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_imp_inc'.con" as lemma.
(* UNEXPORTED
Section aux
(* begin show *)
-alias id "F" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/F.var
+*)
-alias id "diffF" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffF.var
+*)
-alias id "diffFn" = "cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/Basic_Results/aux/diffFn.var
+*)
(* end show *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/deriv_1_deriv'.con" as lemma.
(* UNEXPORTED
End aux
As usual, nth order derivability is preserved by shrinking the interval.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_deriv_n.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/included_imp_diffble_n.con" as lemma.
(*#*
And finally we have an addition rule for the order of the derivative.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/Derivative_I_n_plus.con" as lemma.
(* UNEXPORTED
End Basic_Results
Section More_Results
*)
-alias id "a" = "cic:/CoRN/ftc/NthDerivative/More_Results/a.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/More_Results/a.var
+*)
-alias id "b" = "cic:/CoRN/ftc/NthDerivative/More_Results/b.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/More_Results/b.var
+*)
-alias id "Hab'" = "cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var".
+(* UNEXPORTED
+cic:/CoRN/ftc/NthDerivative/More_Results/Hab'.var
+*)
(* begin hide *)
-inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/Hab.con" "More_Results__" as definition.
-inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__".
+inline procedural "cic:/CoRN/ftc/NthDerivative/More_Results/I.con" "More_Results__" as definition.
(* end hide *)
as an existential quantification of the nth derivative relation.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I.con" as definition.
(*#*
This operator is well defined and works as expected.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_lemma.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_inc'.con" as lemma.
(*#*
Some basic properties of this operation.
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_Sn_deriv.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_plus.con" as lemma.
(* UNEXPORTED
End More_Results
Some not so basic properties of this operation (needed in rather specific situations).
*)
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd'.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_wd''.con" as lemma.
-inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con".
+inline procedural "cic:/CoRN/ftc/NthDerivative/n_deriv_I_strext'.con" as lemma.
(* UNEXPORTED
End More_on_n_deriv