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