helm/software/matita/contribs/procedural/CoRN/transc/PowerSeries.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: PowerSeries.v,v 1.8 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 (*#* printing Exp %\ensuremath{\exp}% *)
  22
  23 (*#* printing Sin %\ensuremath{\sin}% *)
  24
  25 (*#* printing Cos %\ensuremath{\cos}% *)
  26
  27 (*#* printing Log %\ensuremath{\log}% *)
  28
  29 (*#* printing Tan %\ensuremath{\tan}% *)
  30
  31 include "ftc/FTC.ma".
  32
  33 (*#* *More on Power Series
  34
  35 We will now formally define an operator that defines a function as the
  36 sum of some series given a number sequence.  Along with it, we will
  37 prove some important properties of these entities.
  38 *)
  39
  40 (* UNEXPORTED
  41 Section Power_Series
  42 *)
  43
  44 (*#* **General results
  45
  46 %\begin{convention}% Let [J : interval] and [x0 : IR] be a point of [J].
  47 Let [a : nat -> IR].
  48 %\end{convention}%
  49 *)
  50
  51 (* UNEXPORTED
  52 cic:/CoRN/transc/PowerSeries/Power_Series/J.var
  53 *)
  54
  55 (* UNEXPORTED
  56 cic:/CoRN/transc/PowerSeries/Power_Series/x0.var
  57 *)
  58
  59 (* UNEXPORTED
  60 cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var
  61 *)
  62
  63 (* UNEXPORTED
  64 cic:/CoRN/transc/PowerSeries/Power_Series/a.var
  65 *)
  66
  67 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries.con" as definition.
  68
  69 (*#*
  70 The most important convergence criterium specifically for power series
  71 is the Dirichlet criterium.
  72 *)
  73
  74 (* begin show *)
  75
  76 (* UNEXPORTED
  77 cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var
  78 *)
  79
  80 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__" as definition.
  81
  82 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__" as definition.
  83
  84 (* end show *)
  85
  86 inline procedural "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con" as lemma.
  87
  88 (*#*
  89 When defining a function using its Taylor series as a motivation, the following operator can be of use.
  90 *)
  91
  92 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con" as definition.
  93
  94 (*#*
  95 This function is also continuous and has a good convergence ratio.
  96 *)
  97
  98 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con" as lemma.
  99
 100 inline procedural "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con" as lemma.
 101
 102 (* begin show *)
 103
 104 (* UNEXPORTED
 105 cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var
 106 *)
 107
 108 (* end show *)
 109
 110 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con" as lemma.
 111
 112 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con" as lemma.
 113
 114 (* UNEXPORTED
 115 End Power_Series
 116 *)
 117
 118 (* UNEXPORTED
 119 Hint Resolve FPowerSeries'_cont: continuous.
 120 *)
 121
 122 (* UNEXPORTED
 123 Section More_on_PowerSeries
 124 *)
 125
 126 (*#*
 127 %\begin{convention}% Let [F] and [G] be the power series defined
 128 respectively by [a] and by [fun n => (a (S n))].
 129 %\end{convention}%
 130 *)
 131
 132 (* UNEXPORTED
 133 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var
 134 *)
 135
 136 (* UNEXPORTED
 137 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var
 138 *)
 139
 140 (* begin hide *)
 141
 142 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__" as definition.
 143
 144 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__" as definition.
 145
 146 (* end hide *)
 147
 148 (* begin show *)
 149
 150 (* UNEXPORTED
 151 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var
 152 *)
 153
 154 (* UNEXPORTED
 155 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var
 156 *)
 157
 158 (* UNEXPORTED
 159 cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var
 160 *)
 161
 162 (* end show *)
 163
 164 (*#* We get a comparison test for power series. *)
 165
 166 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con" as lemma.
 167
 168 (*#* And a rule for differentiation. *)
 169
 170 (* UNEXPORTED
 171 Opaque nring fac.
 172 *)
 173
 174 inline procedural "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con" as lemma.
 175
 176 (* UNEXPORTED
 177 End More_on_PowerSeries
 178 *)
 179
 180 (* UNEXPORTED
 181 Section Definitions
 182 *)
 183
 184 (*#* **Function definitions through power series
 185
 186 We now define the exponential, sine and cosine functions as power
 187 series, and prove their convergence.  Tangent is defined as the
 188 quotient of sine over cosine.
 189 *)
 190
 191 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_ps.con" as definition.
 192
 193 inline procedural "cic:/CoRN/transc/PowerSeries/sin_seq.con" as definition.
 194
 195 inline procedural "cic:/CoRN/transc/PowerSeries/sin_ps.con" as definition.
 196
 197 inline procedural "cic:/CoRN/transc/PowerSeries/cos_seq.con" as definition.
 198
 199 inline procedural "cic:/CoRN/transc/PowerSeries/cos_ps.con" as definition.
 200
 201 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv'.con" as lemma.
 202
 203 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv.con" as lemma.
 204
 205 inline procedural "cic:/CoRN/transc/PowerSeries/sin_conv.con" as lemma.
 206
 207 inline procedural "cic:/CoRN/transc/PowerSeries/cos_conv.con" as lemma.
 208
 209 inline procedural "cic:/CoRN/transc/PowerSeries/Expon.con" as definition.
 210
 211 inline procedural "cic:/CoRN/transc/PowerSeries/Sine.con" as definition.
 212
 213 inline procedural "cic:/CoRN/transc/PowerSeries/Cosine.con" as definition.
 214
 215 inline procedural "cic:/CoRN/transc/PowerSeries/Tang.con" as definition.
 216
 217 (*#*
 218 Some auxiliary domain results.
 219 *)
 220
 221 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_domain.con" as lemma.
 222
 223 inline procedural "cic:/CoRN/transc/PowerSeries/sin_domain.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/transc/PowerSeries/cos_domain.con" as lemma.
 226
 227 inline procedural "cic:/CoRN/transc/PowerSeries/included_Exp.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/transc/PowerSeries/included_Sin.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/transc/PowerSeries/included_Cos.con" as lemma.
 232
 233 (*#*
 234 Definition of the logarithm.
 235 *)
 236
 237 inline procedural "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con" as lemma.
 238
 239 inline procedural "cic:/CoRN/transc/PowerSeries/Logarithm.con" as definition.
 240
 241 (* UNEXPORTED
 242 End Definitions
 243 *)
 244
 245 (* UNEXPORTED
 246 Hint Resolve included_Exp included_Sin included_Cos: included.
 247 *)
 248
 249 (*#*
 250 As most of these functions are total, it makes sense to treat them as setoid functions on the reals.  In the case of logarithm and tangent, this is not possible; however, we still define some abbreviations for aesthetical reasons.
 251 *)
 252
 253 inline procedural "cic:/CoRN/transc/PowerSeries/Exp.con" as definition.
 254
 255 inline procedural "cic:/CoRN/transc/PowerSeries/Sin.con" as definition.
 256
 257 inline procedural "cic:/CoRN/transc/PowerSeries/Cos.con" as definition.
 258
 259 inline procedural "cic:/CoRN/transc/PowerSeries/Log.con" as definition.
 260
 261 inline procedural "cic:/CoRN/transc/PowerSeries/Tan.con" as definition.
 262