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