]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/Derivative.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / Derivative.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: Derivative.v,v 1.7 2004/04/23 10:00:58 lcf Exp $ *)
20
21 include "ftc/Continuity.ma".
22
23 (* UNEXPORTED
24 Section Definitions
25 *)
26
27 (*#* *Derivatives
28
29 We will now proceed toward the development of differential calculus.
30 To begin with, the main notion is that of derivative.
31
32 At this stage we will not define a notion of differentiable function,
33 mainly because the natural definition (that of being a function which
34 has some derivative) poses some technical problems; thus, we will
35 postpone that part of our work to a subsequent stage.
36
37 Derivative is a binary relation in the type of partial functions,
38 dependent (once again) on a compact interval with distinct
39 endpoints#. #%\footnote{%As before, we do not define pointwise
40 differentiability, mainly for coherence reasons.  See Bishop [1967]
41 for a discussion on the relative little interest of that concept.%}.%
42 The reason for requiring the endpoints to be apart is mainly to be
43 able to derive the usual properties of the derivative
44 relation---namely, that any two derivatives of the same function must
45 coincide.
46
47 %\begin{convention}% Let [a,b:IR] with [a [<] b] and denote by [I] the
48 interval [[a,b]].  Throughout this chapter, [F, F', G, G'] and [H]
49 will be partial functions with domains respectively [P, P', Q, Q'] and
50 [R].
51 %\end{convention}%
52 *)
53
54 (* UNEXPORTED
55 cic:/CoRN/ftc/Derivative/Definitions/a.var
56 *)
57
58 (* UNEXPORTED
59 cic:/CoRN/ftc/Derivative/Definitions/b.var
60 *)
61
62 (* UNEXPORTED
63 cic:/CoRN/ftc/Derivative/Definitions/Hab'.var
64 *)
65
66 (* begin hide *)
67
68 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/Hab.con" "Definitions__" as definition.
69
70 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/I.con" "Definitions__" as definition.
71
72 (* end hide *)
73
74 (* UNEXPORTED
75 cic:/CoRN/ftc/Derivative/Definitions/F.var
76 *)
77
78 (* begin hide *)
79
80 inline procedural "cic:/CoRN/ftc/Derivative/Definitions/P.con" "Definitions__" as definition.
81
82 (* end hide *)
83
84 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I.con" as definition.
85
86 (* UNEXPORTED
87 End Definitions
88 *)
89
90 (* UNEXPORTED
91 Implicit Arguments Derivative_I [a b].
92 *)
93
94 (* UNEXPORTED
95 Section Basic_Properties
96 *)
97
98 (*#* **Basic Properties
99 *)
100
101 (* UNEXPORTED
102 cic:/CoRN/ftc/Derivative/Basic_Properties/a.var
103 *)
104
105 (* UNEXPORTED
106 cic:/CoRN/ftc/Derivative/Basic_Properties/b.var
107 *)
108
109 (* UNEXPORTED
110 cic:/CoRN/ftc/Derivative/Basic_Properties/Hab'.var
111 *)
112
113 (* begin hide *)
114
115 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Hab.con" "Basic_Properties__" as definition.
116
117 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/I.con" "Basic_Properties__" as definition.
118
119 (* end hide *)
120
121 (*#*
122 Like we did for equality, we begin by stating a lemma that makes proofs of derivation easier in practice.
123 *)
124
125 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_char.con" as lemma.
126
127 (* end hide *)
128
129 (*#*
130 Derivative is a well defined relation; we will make this explicit for both arguments:
131 *)
132
133 (* UNEXPORTED
134 cic:/CoRN/ftc/Derivative/Basic_Properties/F.var
135 *)
136
137 (* UNEXPORTED
138 cic:/CoRN/ftc/Derivative/Basic_Properties/G.var
139 *)
140
141 (* UNEXPORTED
142 cic:/CoRN/ftc/Derivative/Basic_Properties/H.var
143 *)
144
145 (* begin hide *)
146
147 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/P.con" "Basic_Properties__" as definition.
148
149 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Q.con" "Basic_Properties__" as definition.
150
151 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/R.con" "Basic_Properties__" as definition.
152
153 (* end hide *)
154
155 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdl.con" as lemma.
156
157 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_wdr.con" as lemma.
158
159 (* begin hide *)
160
161 inline procedural "cic:/CoRN/ftc/Derivative/Basic_Properties/Derivative_I_unique_lemma.con" "Basic_Properties__" as definition.
162
163 (* end hide *)
164
165 (*#*
166 Derivative is unique.
167 *)
168
169 inline procedural "cic:/CoRN/ftc/Derivative/Derivative_I_unique.con" as lemma.
170
171 (*#*
172 Finally, the set where we are considering the relation is included in the domain of both functions.
173 *)
174
175 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc.con" as lemma.
176
177 inline procedural "cic:/CoRN/ftc/Derivative/derivative_imp_inc'.con" as lemma.
178
179 (*#*
180 Any function that is or has a derivative is continuous.
181 *)
182
183 (* UNEXPORTED
184 cic:/CoRN/ftc/Derivative/Basic_Properties/Hab''.var
185 *)
186
187 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin'_I.con" as lemma.
188
189 inline procedural "cic:/CoRN/ftc/Derivative/deriv_imp_contin_I.con" as lemma.
190
191 (* UNEXPORTED
192 End Basic_Properties
193 *)
194
195 (*#*
196 If [G] is the derivative of [F] in a given interval, then [G] is also the derivative of [F] in any smaller interval.
197 *)
198
199 inline procedural "cic:/CoRN/ftc/Derivative/included_imp_deriv.con" as lemma.
200