]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/ftc/Taylor.mma
ground_2 released and permanently renamed as ground
[helm.git] / helm / software / matita / contribs / procedural / CoRN / ftc / Taylor.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: Taylor.v,v 1.10 2004/04/23 10:01:01 lcf Exp $ *)
20
21 include "ftc/TaylorLemma.ma".
22
23 (* UNEXPORTED
24 Opaque Min Max N_Deriv.
25 *)
26
27 (* UNEXPORTED
28 Section More_Taylor_Defs
29 *)
30
31 (*#* **General case
32
33 The generalization to arbitrary intervals just needs a few more definitions.
34
35 %\begin{convention}% Let [I] be a proper interval, [F:PartIR] and
36 [a,b:IR] be points of [I].
37 %\end{convention}%
38 *)
39
40 (* UNEXPORTED
41 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/I.var
42 *)
43
44 (* UNEXPORTED
45 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/pI.var
46 *)
47
48 (* UNEXPORTED
49 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/F.var
50 *)
51
52 (* begin show *)
53
54 inline procedural "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/deriv_Sn.con" "More_Taylor_Defs__" as definition.
55
56 (* end show *)
57
58 (* UNEXPORTED
59 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/a.var
60 *)
61
62 (* UNEXPORTED
63 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/b.var
64 *)
65
66 (* UNEXPORTED
67 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/Ha.var
68 *)
69
70 (* UNEXPORTED
71 cic:/CoRN/ftc/Taylor/More_Taylor_Defs/Hb.var
72 *)
73
74 (* begin show *)
75
76 inline procedural "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/fi.con" "More_Taylor_Defs__" as definition.
77
78 inline procedural "cic:/CoRN/ftc/Taylor/More_Taylor_Defs/funct_i.con" "More_Taylor_Defs__" as definition.
79
80 (* end show *)
81
82 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Seq'.con" as definition.
83
84 (* begin hide *)
85
86 inline procedural "cic:/CoRN/ftc/Taylor/TaylorB.con" as lemma.
87
88 (* end hide *)
89
90 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Rem.con" as definition.
91
92 (* begin hide *)
93
94 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Sumx_lemma.con" as lemma.
95
96 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_lemma_ap.con" as lemma.
97
98 (* end hide *)
99
100 inline procedural "cic:/CoRN/ftc/Taylor/Taylor'.con" as theorem.
101
102 (* UNEXPORTED
103 End More_Taylor_Defs
104 *)
105
106 (* UNEXPORTED
107 Section Taylor_Theorem
108 *)
109
110 (*#*
111 And finally the ``nice'' version, when we know the expression of the
112 derivatives of [F].
113
114 %\begin{convention}% Let [f] be the sequence of derivatives of [F] of
115 order up to [n] and [F'] be the nth-derivative of [F].
116 %\end{convention}%
117 *)
118
119 (* UNEXPORTED
120 cic:/CoRN/ftc/Taylor/Taylor_Theorem/I.var
121 *)
122
123 (* UNEXPORTED
124 cic:/CoRN/ftc/Taylor/Taylor_Theorem/pI.var
125 *)
126
127 (* UNEXPORTED
128 cic:/CoRN/ftc/Taylor/Taylor_Theorem/F.var
129 *)
130
131 (* UNEXPORTED
132 cic:/CoRN/ftc/Taylor/Taylor_Theorem/n.var
133 *)
134
135 (* UNEXPORTED
136 cic:/CoRN/ftc/Taylor/Taylor_Theorem/f.var
137 *)
138
139 (* UNEXPORTED
140 cic:/CoRN/ftc/Taylor/Taylor_Theorem/goodF.var
141 *)
142
143 (* UNEXPORTED
144 cic:/CoRN/ftc/Taylor/Taylor_Theorem/goodF'.var
145 *)
146
147 (* UNEXPORTED
148 cic:/CoRN/ftc/Taylor/Taylor_Theorem/derF.var
149 *)
150
151 (* UNEXPORTED
152 cic:/CoRN/ftc/Taylor/Taylor_Theorem/F'.var
153 *)
154
155 (* UNEXPORTED
156 cic:/CoRN/ftc/Taylor/Taylor_Theorem/derF'.var
157 *)
158
159 (* UNEXPORTED
160 cic:/CoRN/ftc/Taylor/Taylor_Theorem/a.var
161 *)
162
163 (* UNEXPORTED
164 cic:/CoRN/ftc/Taylor/Taylor_Theorem/b.var
165 *)
166
167 (* UNEXPORTED
168 cic:/CoRN/ftc/Taylor/Taylor_Theorem/Ha.var
169 *)
170
171 (* UNEXPORTED
172 cic:/CoRN/ftc/Taylor/Taylor_Theorem/Hb.var
173 *)
174
175 (* begin show *)
176
177 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Theorem/funct_i.con" "Taylor_Theorem__" as definition.
178
179 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Seq.con" as definition.
180
181 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_Theorem/deriv_Sn.con" "Taylor_Theorem__" as definition.
182
183 (* end show *)
184
185 inline procedural "cic:/CoRN/ftc/Taylor/Taylor_aux.con" as lemma.
186
187 (* UNEXPORTED
188 Transparent N_Deriv.
189 *)
190
191 inline procedural "cic:/CoRN/ftc/Taylor/Taylor.con" as theorem.
192
193 (* UNEXPORTED
194 End Taylor_Theorem
195 *)
196