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