helm/software/matita/contribs/procedural/CoRN/ftc/MoreIntegrals.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: MoreIntegrals.v,v 1.6 2004/04/23 10:00:59 lcf Exp $ *)
  20
  21 include "ftc/Integral.ma".
  22
  23 include "ftc/MoreFunctions.ma".
  24
  25 (* UNEXPORTED
  26 Section Lemmas
  27 *)
  28
  29 (*#* printing Integral %\ensuremath{\int}% #&int;# *)
  30
  31 (*#* printing integral' %\ensuremath{\int}% #&int;# *)
  32
  33 (*#* *The generalized integral
  34
  35 In this file we extend the definition of integral to allow for
  36 arbitrary integration domains (that is, not requiring that the lower
  37 endpoint of integration be less or equal than the upper endpoint) and
  38 we prove the fundamental properties of the new operator.
  39
  40 %\begin{convention}% Let [a, b : IR] and assume that [F] and [G] are two
  41 partial functions continuous in [[Min(a,b),Max(a,b)]].
  42 %\end{convention}%
  43
  44 ** Definitions
  45
  46 Before we define the new integral we need to some trivial interval inclusions.
  47 *)
  48
  49 (* UNEXPORTED
  50 cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var
  51 *)
  52
  53 (* UNEXPORTED
  54 cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var
  55 *)
  56
  57 (* UNEXPORTED
  58 cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var
  59 *)
  60
  61 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con" as lemma.
  62
  63 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con" as lemma.
  64
  65 (* UNEXPORTED
  66 End Lemmas
  67 *)
  68
  69 (* UNEXPORTED
  70 Section Definitions
  71 *)
  72
  73 (*#*
  74 The integral is defined by the formula
  75 $\int_a^bf=\int_{\min(a,b)}^bf-\int_{\min(a,b)}^af$#&int;<sub>a</sub><sup>b</sup>f=&int;<sub>min(a,b)</sub><sup>b</sup>f-&int;<sub>min(a,b)</sub><sup>a</sup>f#,
  76 inspired by the domain union rule; obviously it coincides with the
  77 classical definition, and it collapses to the old one in the case [a
  78  [<=]  b].
  79 *)
  80
  81 (* UNEXPORTED
  82 cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var
  83 *)
  84
  85 (* UNEXPORTED
  86 cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var
  87 *)
  88
  89 (* UNEXPORTED
  90 cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var
  91 *)
  92
  93 (* UNEXPORTED
  94 cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var
  95 *)
  96
  97 (* UNEXPORTED
  98 cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var
  99 *)
 100
 101 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con" as lemma.
 102
 103 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con" as lemma.
 104
 105 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral.con" as definition.
 106
 107 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con" as lemma.
 108
 109 (* UNEXPORTED
 110 End Definitions
 111 *)
 112
 113 (* UNEXPORTED
 114 Implicit Arguments Integral [a b Hab F].
 115 *)
 116
 117 (* UNEXPORTED
 118 Section Properties_of_Integral
 119 *)
 120
 121 (*#* **Properties of the Integral
 122
 123 All our old properties carry over to this new definition---and some
 124 new ones, too.  We begin with (strong) extensionality.
 125 *)
 126
 127 (* UNEXPORTED
 128 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var
 129 *)
 130
 131 (* UNEXPORTED
 132 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var
 133 *)
 134
 135 (* UNEXPORTED
 136 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var
 137 *)
 138
 139 (* UNEXPORTED
 140 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var
 141 *)
 142
 143 (* UNEXPORTED
 144 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var
 145 *)
 146
 147 (* UNEXPORTED
 148 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var
 149 *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var
 153 *)
 154
 155 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con" as lemma.
 156
 157 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con" as lemma.
 158
 159 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con" as lemma.
 160
 161 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con" as lemma.
 162
 163 (*#*
 164 The integral is a linear operator.
 165 *)
 166
 167 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con" as lemma.
 168
 169 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con" as lemma.
 170
 171 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con" as lemma.
 172
 173 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con" as lemma.
 174
 175 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con" as lemma.
 178
 179 (*#*
 180 If the endpoints are equal then the integral vanishes.
 181 *)
 182
 183 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con" as lemma.
 184
 185 (*#*
 186 And the norm provides an upper bound for the absolute value of the integral.
 187 *)
 188
 189 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con" as lemma.
 190
 191 (* UNEXPORTED
 192 End Properties_of_Integral
 193 *)
 194
 195 (* UNEXPORTED
 196 Section More_Properties
 197 *)
 198
 199 (*#*
 200 Two other ways of stating the addition law for domains.
 201 *)
 202
 203 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con" as lemma.
 204
 205 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con" as lemma.
 206
 207 (*#*
 208 And now we can prove the addition law for domains with our general operator.
 209
 210 %\begin{convention}% Assume [c : IR].
 211 %\end{convention}%
 212 *)
 213
 214 (* UNEXPORTED
 215 cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var
 216 *)
 217
 218 (* UNEXPORTED
 219 cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var
 220 *)
 221
 222 (* UNEXPORTED
 223 cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var
 224 *)
 225
 226 (* begin show *)
 227
 228 (* UNEXPORTED
 229 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var
 230 *)
 231
 232 (* UNEXPORTED
 233 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var
 234 *)
 235
 236 (* UNEXPORTED
 237 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var
 238 *)
 239
 240 (* UNEXPORTED
 241 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var
 242 *)
 243
 244 (* end show *)
 245
 246 (* UNEXPORTED
 247 cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var
 248 *)
 249
 250 (* begin show *)
 251
 252 (* UNEXPORTED
 253 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var
 254 *)
 255
 256 (* UNEXPORTED
 257 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var
 258 *)
 259
 260 (* UNEXPORTED
 261 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var
 262 *)
 263
 264 (* UNEXPORTED
 265 cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var
 266 *)
 267
 268 (* end show *)
 269
 270 (* begin hide *)
 271
 272 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__" as definition.
 273
 274 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__" as definition.
 275
 276 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__" as definition.
 277
 278 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__" as definition.
 279
 280 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__" as definition.
 281
 282 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__" as definition.
 283
 284 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__" as definition.
 285
 286 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__" as definition.
 287
 288 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__" as definition.
 289
 290 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__" as definition.
 291
 292 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__" as definition.
 293
 294 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__" as definition.
 295
 296 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__" as definition.
 297
 298 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__" as definition.
 299
 300 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__" as definition.
 301
 302 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__" as definition.
 303
 304 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__" as definition.
 305
 306 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__" as definition.
 307
 308 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__" as definition.
 309
 310 (* end hide *)
 311
 312 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con" as lemma.
 313
 314 (*#*
 315 Notice that, unlike in the classical case, an extra hypothesis (the
 316 continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed.
 317 *)
 318
 319 (* UNEXPORTED
 320 End More_Properties
 321 *)
 322
 323 (* UNEXPORTED
 324 Section Corollaries
 325 *)
 326
 327 (* UNEXPORTED
 328 cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var
 329 *)
 330
 331 (* UNEXPORTED
 332 cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var
 333 *)
 334
 335 (* UNEXPORTED
 336 cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var
 337 *)
 338
 339 (* UNEXPORTED
 340 cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var
 341 *)
 342
 343 (* UNEXPORTED
 344 cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var
 345 *)
 346
 347 (*#* As a corollary, we get the following rule: *)
 348
 349 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con" as lemma.
 350
 351 (*#* Finally, some miscellaneous results: *)
 352
 353 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con" as lemma.
 354
 355 inline procedural "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con" as lemma.
 356
 357 (* UNEXPORTED
 358 End Corollaries
 359 *)
 360
 361 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con" as lemma.
 362
 363 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con" as lemma.
 364