1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *)
21 include "fta/KneserLemma.ma".
23 include "fta/CPoly_Shift.ma".
25 include "fta/CPoly_Contin1.ma".
27 (*#* * FTA for regular polynomials
28 ** The Kneser sequence
29 %\begin{convention}% Let [n] be a positive natural number.
37 alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/n.var".
39 alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_Exists/lt0n.var".
42 %\begin{convention}% Let [qK] be a real between 0 and 1, with
44 forall (p : CCX), (monic n p) -> forall (c : IR), ((AbsCC (p!Zero)) [<] c) ->
45 {z:CC | ((AbsCC z) [^]n [<] c) | ((AbsCC (p!z)) [<] qK[*]c)}.
47 Let [p] be a monic polynomial over the complex numbers with degree
48 [n], and let [c0] be such that [(AbsCC (p!Zero)) [<] c0].
53 Section Kneser_Sequence
56 alias id "qK" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qK.var".
58 alias id "zltq" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/zltq.var".
60 alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/qlt1.var".
62 alias id "q_prop" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/q_prop.var".
64 alias id "p" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p.var".
66 alias id "mp" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/mp.var".
68 alias id "c0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/c0.var".
70 alias id "p0ltc0" = "cic:/CoRN/fta/FTAreg/Seq_Exists/Kneser_Sequence/p0ltc0.var".
72 inline procedural "cic:/CoRN/fta/FTAreg/Knes_tup.ind".
75 cic:/matita/CoRN-Procedural/fta/FTAreg/z_el.con
78 inline procedural "cic:/CoRN/fta/FTAreg/Knes_tupp.ind".
81 cic:/matita/CoRN-Procedural/fta/FTAreg/Kntup.con
84 inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun.con".
86 inline procedural "cic:/CoRN/fta/FTAreg/Knes_fun_it.con".
88 inline procedural "cic:/CoRN/fta/FTAreg/sK.con".
90 inline procedural "cic:/CoRN/fta/FTAreg/sK_c.con".
92 inline procedural "cic:/CoRN/fta/FTAreg/sK_c0.con".
94 inline procedural "cic:/CoRN/fta/FTAreg/sK_prop1.con".
96 inline procedural "cic:/CoRN/fta/FTAreg/sK_it.con".
98 inline procedural "cic:/CoRN/fta/FTAreg/sK_prop2.con".
105 Section Seq_Exists_Main
111 inline procedural "cic:/CoRN/fta/FTAreg/seq_exists.con".
125 alias id "n" = "cic:/CoRN/fta/FTAreg/N_Exists/n.var".
127 alias id "lt0n" = "cic:/CoRN/fta/FTAreg/N_Exists/lt0n.var".
129 alias id "q" = "cic:/CoRN/fta/FTAreg/N_Exists/q.var".
131 alias id "zleq" = "cic:/CoRN/fta/FTAreg/N_Exists/zleq.var".
133 alias id "qlt1" = "cic:/CoRN/fta/FTAreg/N_Exists/qlt1.var".
135 alias id "c" = "cic:/CoRN/fta/FTAreg/N_Exists/c.var".
137 alias id "zltc" = "cic:/CoRN/fta/FTAreg/N_Exists/zltc.var".
141 inline procedural "cic:/CoRN/fta/FTAreg/N_Exists/q_.con" "N_Exists__".
145 alias id "e" = "cic:/CoRN/fta/FTAreg/N_Exists/e.var".
147 alias id "zlte" = "cic:/CoRN/fta/FTAreg/N_Exists/zlte.var".
149 inline procedural "cic:/CoRN/fta/FTAreg/N_exists.con".
156 Section Seq_is_CC_CAuchy
159 (*#* ** The Kneser sequence is Cauchy in [CC] *)
161 alias id "n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/n.var".
163 alias id "lt0n" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/lt0n.var".
165 alias id "q" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q.var".
167 alias id "zleq" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zleq.var".
169 alias id "qlt1" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/qlt1.var".
171 alias id "c" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/c.var".
173 alias id "zltc" = "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/zltc.var".
175 (*#* %\begin{convention}% Let:
176 - [q_] prove [q[-]One [#] Zero]
177 - [nrtq := NRoot q n]
178 - [nrtc := Nroot c n]
179 - [nrtqlt1] prove [nrtq [<] One]
180 - [nrtq_] prove [nrtq[-]One [#] Zero]
182 %\end{convention}% *)
186 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/q_.con" "Seq_is_CC_CAuchy__".
188 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq.con" "Seq_is_CC_CAuchy__".
190 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtc.con" "Seq_is_CC_CAuchy__".
192 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtqlt1.con" "Seq_is_CC_CAuchy__".
194 inline procedural "cic:/CoRN/fta/FTAreg/Seq_is_CC_CAuchy/nrtq_.con" "Seq_is_CC_CAuchy__".
198 inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtq.con".
200 inline procedural "cic:/CoRN/fta/FTAreg/zlt_nrtc.con".
202 inline procedural "cic:/CoRN/fta/FTAreg/nrt_pow.con".
204 inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltRe.con".
206 inline procedural "cic:/CoRN/fta/FTAreg/abs_pow_ltIm.con".
208 inline procedural "cic:/CoRN/fta/FTAreg/SublemmaRe.con".
210 inline procedural "cic:/CoRN/fta/FTAreg/SublemmaIm.con".
212 inline procedural "cic:/CoRN/fta/FTAreg/seq_is_CC_Cauchy.con".
218 inline procedural "cic:/CoRN/fta/FTAreg/FTA_monic.con".
220 inline procedural "cic:/CoRN/fta/FTAreg/FTA_reg.con".