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