helm/software/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 (* $Id: FTAreg.v,v 1.4 2004/04/23 10:00:57 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 KneserLemma
  23 *)
  24
  25 (* INCLUDE
  26 CPoly_Shift
  27 *)
  28
  29 (* INCLUDE
  30 CPoly_Contin1
  31 *)
  32
  33 (*#* * FTA for regular polynomials
  34 ** The Kneser sequence
  35 %\begin{convention}% Let [n] be a positive natural number.
  36 %\end{convention}%
  37 *)
  38
  39 (* UNEXPORTED
  40 Section Seq_Exists.
  41 *)
  42
  43 inline cic:/CoRN/fta/FTAreg/n.var.
  44
  45 inline cic:/CoRN/fta/FTAreg/lt0n.var.
  46
  47 (*#*
  48 %\begin{convention}% Let [qK] be a real between 0 and 1, with
  49 [[
  50 forall (p : CCX), (monic n p) -> forall (c : IR), ((AbsCC (p!Zero)) [<] c) ->
  51  {z:CC | ((AbsCC z) [^]n [<] c) | ((AbsCC (p!z)) [<] qK[*]c)}.
  52 ]]
  53 Let [p] be a monic polynomial over the complex numbers with degree
  54 [n], and let [c0] be such that [(AbsCC (p!Zero)) [<] c0].
  55 %\end{convention}%
  56 *)
  57
  58 (* UNEXPORTED
  59 Section Kneser_Sequence.
  60 *)
  61
  62 inline cic:/CoRN/fta/FTAreg/qK.var.
  63
  64 inline cic:/CoRN/fta/FTAreg/zltq.var.
  65
  66 inline cic:/CoRN/fta/FTAreg/qlt1.var.
  67
  68 inline cic:/CoRN/fta/FTAreg/q_prop.var.
  69
  70 inline cic:/CoRN/fta/FTAreg/p.var.
  71
  72 inline cic:/CoRN/fta/FTAreg/mp.var.
  73
  74 inline cic:/CoRN/fta/FTAreg/c0.var.
  75
  76 inline cic:/CoRN/fta/FTAreg/p0ltc0.var.
  77
  78 inline cic:/CoRN/fta/FTAreg/Knes_tup.ind.
  79
  80 inline cic:/CoRN/fta/FTAreg/Knes_tupp.ind.
  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 inline cic:/CoRN/fta/FTAreg/n.var.
 124
 125 inline cic:/CoRN/fta/FTAreg/lt0n.var.
 126
 127 inline cic:/CoRN/fta/FTAreg/q.var.
 128
 129 inline cic:/CoRN/fta/FTAreg/zleq.var.
 130
 131 inline cic:/CoRN/fta/FTAreg/qlt1.var.
 132
 133 inline cic:/CoRN/fta/FTAreg/c.var.
 134
 135 inline cic:/CoRN/fta/FTAreg/zltc.var.
 136
 137 (* begin hide *)
 138
 139 inline cic:/CoRN/fta/FTAreg/q_.con.
 140
 141 (* end hide *)
 142
 143 inline cic:/CoRN/fta/FTAreg/e.var.
 144
 145 inline cic:/CoRN/fta/FTAreg/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 inline cic:/CoRN/fta/FTAreg/n.var.
 160
 161 inline cic:/CoRN/fta/FTAreg/lt0n.var.
 162
 163 inline cic:/CoRN/fta/FTAreg/q.var.
 164
 165 inline cic:/CoRN/fta/FTAreg/zleq.var.
 166
 167 inline cic:/CoRN/fta/FTAreg/qlt1.var.
 168
 169 inline cic:/CoRN/fta/FTAreg/c.var.
 170
 171 inline cic:/CoRN/fta/FTAreg/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/q_.con.
 185
 186 inline cic:/CoRN/fta/FTAreg/nrtq.con.
 187
 188 inline cic:/CoRN/fta/FTAreg/nrtc.con.
 189
 190 inline cic:/CoRN/fta/FTAreg/nrtqlt1.con.
 191
 192 inline cic:/CoRN/fta/FTAreg/nrtq_.con.
 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