helm/software/matita/contribs/procedural/CoRN/reals/NRootIR.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: NRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
  20
  21 (*#* printing NRoot %\ensuremath{\sqrt[n]{\cdot}}% *)
  22
  23 (*#* printing sqrt %\ensuremath{\sqrt{\cdot}}% *)
  24
  25 include "reals/OddPolyRootIR.ma".
  26
  27 (*#* * Roots of Real Numbers *)
  28
  29 (* UNEXPORTED
  30 Section NRoot
  31 *)
  32
  33 (*#* ** Existence of roots
  34
  35 %\begin{convention}% Let [n] be a natural number and [c] a nonnegative real.
  36 [p] is the auxiliary polynomial [_X_[^]n[-] (_C_ c)].
  37 %\end{convention}%
  38 *)
  39
  40 (* UNEXPORTED
  41 cic:/CoRN/reals/NRootIR/NRoot/n.var
  42 *)
  43
  44 (* UNEXPORTED
  45 cic:/CoRN/reals/NRootIR/NRoot/n_pos.var
  46 *)
  47
  48 (* UNEXPORTED
  49 cic:/CoRN/reals/NRootIR/NRoot/c.var
  50 *)
  51
  52 (* UNEXPORTED
  53 cic:/CoRN/reals/NRootIR/NRoot/c_nonneg.var
  54 *)
  55
  56 (* begin hide *)
  57
  58 inline procedural "cic:/CoRN/reals/NRootIR/NRoot/p.con" "NRoot__" as definition.
  59
  60 (* end hide *)
  61
  62 inline procedural "cic:/CoRN/reals/NRootIR/CnrootIR.con" as lemma.
  63
  64 (* UNEXPORTED
  65 End NRoot
  66 *)
  67
  68 (*#* We define the root of order [n] for any nonnegative real number and
  69 prove its main properties:
  70  - $\left(\sqrt[n]x\right)^n=x$#(sqrt(n) x)^n =x#;
  71  - $0\leq\sqrt[n]x$#0&le;sqrt(n)x#;
  72  - if [Zero [<] x] then $0<\sqrt[n]x$#0&lt;sqrt(n)x#;
  73  - $\sqrt[n]{x^n}=x$#sqrt(n) x^n =x#;
  74  - the nth root is monotonous;
  75  - in particular, if [x [<] One] then $\sqrt[n]x<1$#sqrt(n) x&lt;1#.
  76
  77 [(nroot ??)] will be written as [NRoot].
  78 *)
  79
  80 (* UNEXPORTED
  81 Section Nth_Root
  82 *)
  83
  84 inline procedural "cic:/CoRN/reals/NRootIR/nroot.con" as lemma.
  85
  86 inline procedural "cic:/CoRN/reals/NRootIR/NRoot.con" as definition.
  87
  88 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_power.con" as lemma.
  89
  90 (* UNEXPORTED
  91 Hint Resolve NRoot_power: algebra.
  92 *)
  93
  94 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_nonneg.con" as lemma.
  95
  96 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_pos.con" as lemma.
  97
  98 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_power'.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_pres_less.con" as lemma.
 101
 102 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_less_one.con" as lemma.
 103
 104 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_cancel.con" as lemma.
 105
 106 (*#* %\begin{convention}% Let [x,y] be nonnegative real numbers.
 107 %\end{convention}% *)
 108
 109 (* UNEXPORTED
 110 cic:/CoRN/reals/NRootIR/Nth_Root/x.var
 111 *)
 112
 113 (* UNEXPORTED
 114 cic:/CoRN/reals/NRootIR/Nth_Root/y.var
 115 *)
 116
 117 (* UNEXPORTED
 118 cic:/CoRN/reals/NRootIR/Nth_Root/Hx.var
 119 *)
 120
 121 (* UNEXPORTED
 122 cic:/CoRN/reals/NRootIR/Nth_Root/Hy.var
 123 *)
 124
 125 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_wd.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_unique.con" as lemma.
 128
 129 (* UNEXPORTED
 130 End Nth_Root
 131 *)
 132
 133 (* UNEXPORTED
 134 Implicit Arguments NRoot [x n].
 135 *)
 136
 137 (* UNEXPORTED
 138 Hint Resolve NRoot_power NRoot_power': algebra.
 139 *)
 140
 141 inline procedural "cic:/CoRN/reals/NRootIR/NRoot_resp_leEq.con" as lemma.
 142
 143 (*#**********************************)
 144
 145 (* UNEXPORTED
 146 Section Square_root
 147 *)
 148
 149 (*#**********************************)
 150
 151 (*#* ** Square root *)
 152
 153 inline procedural "cic:/CoRN/reals/NRootIR/sqrt.con" as definition.
 154
 155 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_sqr.con" as lemma.
 156
 157 (* UNEXPORTED
 158 Hint Resolve sqrt_sqr: algebra.
 159 *)
 160
 161 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_nonneg.con" as lemma.
 162
 163 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_wd.con" as lemma.
 164
 165 (* UNEXPORTED
 166 Hint Resolve sqrt_wd: algebra_c.
 167 *)
 168
 169 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_to_nonneg.con" as lemma.
 170
 171 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_to_nonpos.con" as lemma.
 172
 173 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_mult.con" as lemma.
 174
 175 (* UNEXPORTED
 176 Hint Resolve sqrt_mult: algebra.
 177 *)
 178
 179 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_mult_wd.con" as lemma.
 180
 181 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_less.con" as lemma.
 182
 183 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_less'.con" as lemma.
 184
 185 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_resp_leEq.con" as lemma.
 186
 187 inline procedural "cic:/CoRN/reals/NRootIR/sqrt_resp_less.con" as lemma.
 188
 189 (* UNEXPORTED
 190 End Square_root
 191 *)
 192
 193 (* UNEXPORTED
 194 Hint Resolve sqrt_wd: algebra_c.
 195 *)
 196
 197 (* UNEXPORTED
 198 Hint Resolve sqrt_sqr sqrt_mult: algebra.
 199 *)
 200
 201 (* UNEXPORTED
 202 Section Absolute_Props
 203 *)
 204
 205 (*#* ** More on absolute value
 206
 207 With the help of square roots, we can prove some more properties of absolute
 208 values in [IR].
 209 *)
 210
 211 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_sqrt_sqr.con" as lemma.
 212
 213 (* UNEXPORTED
 214 Hint Resolve AbsIR_sqrt_sqr: algebra.
 215 *)
 216
 217 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_resp_mult.con" as lemma.
 218
 219 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos.con" as lemma.
 220
 221 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_mult_pos'.con" as lemma.
 222
 223 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_nexp.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_nexp_op.con" as lemma.
 226
 227 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_less_square.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_leEq_square.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_division.con" as lemma.
 232
 233 (*#* Some special cases. *)
 234
 235 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_recip.con" as lemma.
 236
 237 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_div_two.con" as lemma.
 238
 239 (*#* Cauchy-Schwartz for IR and variants on that subject. *)
 240
 241 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR.con" as lemma.
 242
 243 inline procedural "cic:/CoRN/reals/NRootIR/triangle_SumIR.con" as lemma.
 244
 245 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR_minus.con" as lemma.
 246
 247 inline procedural "cic:/CoRN/reals/NRootIR/weird_triangleIR.con" as lemma.
 248
 249 inline procedural "cic:/CoRN/reals/NRootIR/triangle_IR_minus'.con" as lemma.
 250
 251 inline procedural "cic:/CoRN/reals/NRootIR/triangle_SumxIR.con" as lemma.
 252
 253 inline procedural "cic:/CoRN/reals/NRootIR/triangle_Sum2IR.con" as lemma.
 254
 255 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_str_bnd_AbsIR.con" as lemma.
 256
 257 inline procedural "cic:/CoRN/reals/NRootIR/AbsIR_bnd_AbsIR.con" as lemma.
 258
 259 (* UNEXPORTED
 260 End Absolute_Props
 261 *)
 262
 263 (* UNEXPORTED
 264 Section Consequences
 265 *)
 266
 267 (*#* **Cauchy sequences
 268
 269 With these results, we can also prove that the sequence of reciprocals of a
 270 Cauchy sequence that is never zero and whose Limit is not zero is also a
 271 Cauchy sequence.
 272 *)
 273
 274 inline procedural "cic:/CoRN/reals/NRootIR/Cauchy_Lim_recip.con" as lemma.
 275
 276 inline procedural "cic:/CoRN/reals/NRootIR/Cauchy_recip.con" as lemma.
 277
 278 inline procedural "cic:/CoRN/reals/NRootIR/Lim_recip.con" as lemma.
 279
 280 (* UNEXPORTED
 281 End Consequences
 282 *)
 283