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 (* $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
  32 FTC
  33 *)
  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 inline cic:/CoRN/transc/PowerSeries/J.var.
  54
  55 inline cic:/CoRN/transc/PowerSeries/x0.var.
  56
  57 inline cic:/CoRN/transc/PowerSeries/Hx0.var.
  58
  59 inline cic:/CoRN/transc/PowerSeries/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 inline cic:/CoRN/transc/PowerSeries/Ha.var.
  71
  72 inline cic:/CoRN/transc/PowerSeries/r.con.
  73
  74 inline cic:/CoRN/transc/PowerSeries/Hr.con.
  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 inline cic:/CoRN/transc/PowerSeries/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 inline cic:/CoRN/transc/PowerSeries/x0.var.
 123
 124 inline cic:/CoRN/transc/PowerSeries/a.var.
 125
 126 (* begin hide *)
 127
 128 inline cic:/CoRN/transc/PowerSeries/F.con.
 129
 130 inline cic:/CoRN/transc/PowerSeries/G.con.
 131
 132 (* end hide *)
 133
 134 (* begin show *)
 135
 136 inline cic:/CoRN/transc/PowerSeries/Hf.var.
 137
 138 inline cic:/CoRN/transc/PowerSeries/Hf'.var.
 139
 140 inline cic:/CoRN/transc/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