helm/software/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