helm/software/matita/contribs/CoRN-Procedural/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 alias id "J" = "cic:/CoRN/transc/PowerSeries/Power_Series/J.var".
  52
  53 alias id "x0" = "cic:/CoRN/transc/PowerSeries/Power_Series/x0.var".
  54
  55 alias id "Hx0" = "cic:/CoRN/transc/PowerSeries/Power_Series/Hx0.var".
  56
  57 alias id "a" = "cic:/CoRN/transc/PowerSeries/Power_Series/a.var".
  58
  59 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries.con".
  60
  61 (*#*
  62 The most important convergence criterium specifically for power series
  63 is the Dirichlet criterium.
  64 *)
  65
  66 (* begin show *)
  67
  68 alias id "Ha" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha.var".
  69
  70 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/r.con" "Power_Series__".
  71
  72 inline procedural "cic:/CoRN/transc/PowerSeries/Power_Series/Hr.con" "Power_Series__".
  73
  74 (* end show *)
  75
  76 inline procedural "cic:/CoRN/transc/PowerSeries/Dirichlet_crit.con".
  77
  78 (*#*
  79 When defining a function using its Taylor series as a motivation, the following operator can be of use.
  80 *)
  81
  82 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'.con".
  83
  84 (*#*
  85 This function is also continuous and has a good convergence ratio.
  86 *)
  87
  88 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_cont.con".
  89
  90 inline procedural "cic:/CoRN/transc/PowerSeries/included_FPowerSeries'.con".
  91
  92 (* begin show *)
  93
  94 alias id "Ha'" = "cic:/CoRN/transc/PowerSeries/Power_Series/Ha'.var".
  95
  96 (* end show *)
  97
  98 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv'.con".
  99
 100 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_conv.con".
 101
 102 (* UNEXPORTED
 103 End Power_Series
 104 *)
 105
 106 (* UNEXPORTED
 107 Hint Resolve FPowerSeries'_cont: continuous.
 108 *)
 109
 110 (* UNEXPORTED
 111 Section More_on_PowerSeries
 112 *)
 113
 114 (*#*
 115 %\begin{convention}% Let [F] and [G] be the power series defined
 116 respectively by [a] and by [fun n => (a (S n))].
 117 %\end{convention}%
 118 *)
 119
 120 alias id "x0" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/x0.var".
 121
 122 alias id "a" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/a.var".
 123
 124 (* begin hide *)
 125
 126 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/F.con" "More_on_PowerSeries__".
 127
 128 inline procedural "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/G.con" "More_on_PowerSeries__".
 129
 130 (* end hide *)
 131
 132 (* begin show *)
 133
 134 alias id "Hf" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf.var".
 135
 136 alias id "Hf'" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hf'.var".
 137
 138 alias id "Hg" = "cic:/CoRN/transc/PowerSeries/More_on_PowerSeries/Hg.var".
 139
 140 (* end show *)
 141
 142 (*#* We get a comparison test for power series. *)
 143
 144 inline procedural "cic:/CoRN/transc/PowerSeries/FPowerSeries'_comp.con".
 145
 146 (*#* And a rule for differentiation. *)
 147
 148 (* UNEXPORTED
 149 Opaque nring fac.
 150 *)
 151
 152 inline procedural "cic:/CoRN/transc/PowerSeries/Derivative_FPowerSeries1'.con".
 153
 154 (* UNEXPORTED
 155 End More_on_PowerSeries
 156 *)
 157
 158 (* UNEXPORTED
 159 Section Definitions
 160 *)
 161
 162 (*#* **Function definitions through power series
 163
 164 We now define the exponential, sine and cosine functions as power
 165 series, and prove their convergence.  Tangent is defined as the
 166 quotient of sine over cosine.
 167 *)
 168
 169 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_ps.con".
 170
 171 inline procedural "cic:/CoRN/transc/PowerSeries/sin_seq.con".
 172
 173 inline procedural "cic:/CoRN/transc/PowerSeries/sin_ps.con".
 174
 175 inline procedural "cic:/CoRN/transc/PowerSeries/cos_seq.con".
 176
 177 inline procedural "cic:/CoRN/transc/PowerSeries/cos_ps.con".
 178
 179 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv'.con".
 180
 181 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_conv.con".
 182
 183 inline procedural "cic:/CoRN/transc/PowerSeries/sin_conv.con".
 184
 185 inline procedural "cic:/CoRN/transc/PowerSeries/cos_conv.con".
 186
 187 inline procedural "cic:/CoRN/transc/PowerSeries/Expon.con".
 188
 189 inline procedural "cic:/CoRN/transc/PowerSeries/Sine.con".
 190
 191 inline procedural "cic:/CoRN/transc/PowerSeries/Cosine.con".
 192
 193 inline procedural "cic:/CoRN/transc/PowerSeries/Tang.con".
 194
 195 (*#*
 196 Some auxiliary domain results.
 197 *)
 198
 199 inline procedural "cic:/CoRN/transc/PowerSeries/Exp_domain.con".
 200
 201 inline procedural "cic:/CoRN/transc/PowerSeries/sin_domain.con".
 202
 203 inline procedural "cic:/CoRN/transc/PowerSeries/cos_domain.con".
 204
 205 inline procedural "cic:/CoRN/transc/PowerSeries/included_Exp.con".
 206
 207 inline procedural "cic:/CoRN/transc/PowerSeries/included_Sin.con".
 208
 209 inline procedural "cic:/CoRN/transc/PowerSeries/included_Cos.con".
 210
 211 (*#*
 212 Definition of the logarithm.
 213 *)
 214
 215 inline procedural "cic:/CoRN/transc/PowerSeries/log_defn_lemma.con".
 216
 217 inline procedural "cic:/CoRN/transc/PowerSeries/Logarithm.con".
 218
 219 (* UNEXPORTED
 220 End Definitions
 221 *)
 222
 223 (* UNEXPORTED
 224 Hint Resolve included_Exp included_Sin included_Cos: included.
 225 *)
 226
 227 (*#*
 228 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.
 229 *)
 230
 231 inline procedural "cic:/CoRN/transc/PowerSeries/Exp.con".
 232
 233 inline procedural "cic:/CoRN/transc/PowerSeries/Sin.con".
 234
 235 inline procedural "cic:/CoRN/transc/PowerSeries/Cos.con".
 236
 237 inline procedural "cic:/CoRN/transc/PowerSeries/Log.con".
 238
 239 inline procedural "cic:/CoRN/transc/PowerSeries/Tan.con".
 240