]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/fta/FTAreg.mma
partial update in delayed_updating
[helm.git] / matita / matita / contribs / procedural / CoRN / fta / FTAreg.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: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *)
20
21 include "fta/KneserLemma.ma".
22
23 include "fta/CPoly_Shift.ma".
24
25 include "fta/CPoly_Contin1.ma".
26
27 (*#* * FTA for regular polynomials
28 ** The Kneser sequence
29 %\begin{convention}% Let [n] be a positive natural number.
30 %\end{convention}%
31 *)
32
33 (* UNEXPORTED
34 Section Seq_Exists
35 *)
36
37 (* UNEXPORTED
38 cic:/CoRN/fta/FTAreg/Seq_Exists/n.var
39 *)
40
41 (* UNEXPORTED
42 cic:/CoRN/fta/FTAreg/Seq_Exists/lt0n.var
43 *)
44
45 (*#*
46 %\begin{convention}% Let [qK] be a real between 0 and 1, with
47 [[
48 forall (p : CCX), (monic n p) -> forall (c : IR), ((AbsCC (p!Zero)) [<] c) ->
49  {z:CC | ((AbsCC z) [^]n [<] c) | ((AbsCC (p!z)) [<] qK[*]c)}.
50 ]]
51 Let [p] be a monic polynomial over the complex numbers with degree 
52 [n], and let [c0] be such that [(AbsCC (p!Zero)) [<] c0].
53 %\end{convention}%
54 *)
55
56 (* UNEXPORTED
57 Section Kneser_Sequence
58 *)
59
60 (* UNEXPORTED
61 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qK.var
62 *)
63
64 (* UNEXPORTED
65 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/zltq.var
66 *)
67
68 (* UNEXPORTED
69 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qlt1.var
70 *)
71
72 (* UNEXPORTED
73 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/q_prop.var
74 *)
75
76 (* UNEXPORTED
77 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p.var
78 *)
79
80 (* UNEXPORTED
81 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/mp.var
82 *)
83
84 (* UNEXPORTED
85 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/c0.var
86 *)
87
88 (* UNEXPORTED
89 cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p0ltc0.var
90 *)
91
92 inline procedural "cic:/CoRN/fta/FTAreg/Knes_tup.ind".
93
94 (* COERCION
95 cic:/matita/CoRN-Procedural/fta/FTAreg/z_el.con
96 *)
97
98 inline procedural "cic:/CoRN/fta/FTAreg/Knes_tupp.ind".
99
100 (* COERCION
101 cic:/matita/CoRN-Procedural/fta/FTAreg/Kntup.con
102 *)
103
104 inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con" as definition.
105
106 inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con" as definition.
107
108 inline procedural "cic:/CoRN/fta/FTAreg/sK.con" as definition.
109
110 inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con" as lemma.
111
112 inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con" as lemma.
113
114 inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con" as lemma.
115
116 inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con" as lemma.
117
118 inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con" as lemma.
119
120 (* UNEXPORTED
121 End Kneser_Sequence
122 *)
123
124 (* UNEXPORTED
125 Section Seq_Exists_Main
126 *)
127
128 (*#* **Main results
129 *)
130
131 inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con" as lemma.
132
133 (* UNEXPORTED
134 End Seq_Exists_Main
135 *)
136
137 (* UNEXPORTED
138 End Seq_Exists
139 *)
140
141 (* UNEXPORTED
142 Section N_Exists
143 *)
144
145 (* UNEXPORTED
146 cic:/CoRN/fta/FTAreg/N_Exists/n.var
147 *)
148
149 (* UNEXPORTED
150 cic:/CoRN/fta/FTAreg/N_Exists/lt0n.var
151 *)
152
153 (* UNEXPORTED
154 cic:/CoRN/fta/FTAreg/N_Exists/q.var
155 *)
156
157 (* UNEXPORTED
158 cic:/CoRN/fta/FTAreg/N_Exists/zleq.var
159 *)
160
161 (* UNEXPORTED
162 cic:/CoRN/fta/FTAreg/N_Exists/qlt1.var
163 *)
164
165 (* UNEXPORTED
166 cic:/CoRN/fta/FTAreg/N_Exists/c.var
167 *)
168
169 (* UNEXPORTED
170 cic:/CoRN/fta/FTAreg/N_Exists/zltc.var
171 *)
172
173 (* begin hide *)
174
175 inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__" as definition.
176
177 (* end hide *)
178
179 (* UNEXPORTED
180 cic:/CoRN/fta/FTAreg/N_Exists/e.var
181 *)
182
183 (* UNEXPORTED
184 cic:/CoRN/fta/FTAreg/N_Exists/zlte.var
185 *)
186
187 inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con" as lemma.
188
189 (* UNEXPORTED
190 End N_Exists
191 *)
192
193 (* UNEXPORTED
194 Section Seq_is_CC_CAuchy
195 *)
196
197 (*#* ** The Kneser sequence is Cauchy in [CC] *)
198
199 (* UNEXPORTED
200 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/n.var
201 *)
202
203 (* UNEXPORTED
204 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/lt0n.var
205 *)
206
207 (* UNEXPORTED
208 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q.var
209 *)
210
211 (* UNEXPORTED
212 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zleq.var
213 *)
214
215 (* UNEXPORTED
216 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/qlt1.var
217 *)
218
219 (* UNEXPORTED
220 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/c.var
221 *)
222
223 (* UNEXPORTED
224 cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var
225 *)
226
227 (*#* %\begin{convention}% Let:
228  - [q_] prove [q[-]One [#] Zero]
229  - [nrtq := NRoot q n]
230  - [nrtc := Nroot c n]
231  - [nrtqlt1] prove [nrtq [<] One]
232  - [nrtq_] prove [nrtq[-]One [#] Zero]
233
234 %\end{convention}% *)
235
236 (* begin hide *)
237
238 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__" as definition.
239
240 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__" as definition.
241
242 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__" as definition.
243
244 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__" as definition.
245
246 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__" as definition.
247
248 (* end hide *)
249
250 inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con" as lemma.
251
252 inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con" as lemma.
253
254 inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con" as lemma.
255
256 inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con" as lemma.
257
258 inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con" as lemma.
259
260 inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con" as lemma.
261
262 inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con" as lemma.
263
264 inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con" as lemma.
265
266 (* UNEXPORTED
267 End Seq_is_CC_CAuchy
268 *)
269
270 inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con" as lemma.
271
272 inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con" as lemma.
273