helm/software/matita/contribs/CoRN-Procedural/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 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/a.var".
  50
  51 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/b.var".
  52
  53 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Lemmas/Hab.var".
  54
  55 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_lft.con".
  56
  57 inline procedural "cic:/CoRN/ftc/MoreIntegrals/compact_inc_Min_rht.con".
  58
  59 (* UNEXPORTED
  60 End Lemmas
  61 *)
  62
  63 (* UNEXPORTED
  64 Section Definitions
  65 *)
  66
  67 (*#*
  68 The integral is defined by the formula
  69 $\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#,
  70 inspired by the domain union rule; obviously it coincides with the
  71 classical definition, and it collapses to the old one in the case [a
  72  [<=]  b].
  73 *)
  74
  75 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/a.var".
  76
  77 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/b.var".
  78
  79 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/Hab.var".
  80
  81 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/F.var".
  82
  83 alias id "HF" = "cic:/CoRN/ftc/MoreIntegrals/Definitions/HF.var".
  84
  85 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc1.con".
  86
  87 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inc2.con".
  88
  89 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral.con".
  90
  91 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_integral.con".
  92
  93 (* UNEXPORTED
  94 End Definitions
  95 *)
  96
  97 (* UNEXPORTED
  98 Implicit Arguments Integral [a b Hab F].
  99 *)
 100
 101 (* UNEXPORTED
 102 Section Properties_of_Integral
 103 *)
 104
 105 (*#* **Properties of the Integral
 106
 107 All our old properties carry over to this new definition---and some
 108 new ones, too.  We begin with (strong) extensionality.
 109 *)
 110
 111 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/a.var".
 112
 113 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/b.var".
 114
 115 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/Hab.var".
 116
 117 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/F.var".
 118
 119 alias id "G" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/G.var".
 120
 121 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contF.var".
 122
 123 alias id "contG" = "cic:/CoRN/ftc/MoreIntegrals/Properties_of_Integral/contG.var".
 124
 125 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext.con".
 126
 127 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_strext'.con".
 128
 129 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd.con".
 130
 131 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_wd'.con".
 132
 133 (*#*
 134 The integral is a linear operator.
 135 *)
 136
 137 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_const.con".
 138
 139 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_comm_scal.con".
 140
 141 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus.con".
 142
 143 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_inv.con".
 144
 145 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_minus.con".
 146
 147 inline procedural "cic:/CoRN/ftc/MoreIntegrals/linear_Integral.con".
 148
 149 (*#*
 150 If the endpoints are equal then the integral vanishes.
 151 *)
 152
 153 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_empty.con".
 154
 155 (*#*
 156 And the norm provides an upper bound for the absolute value of the integral.
 157 *)
 158
 159 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_leEq_norm.con".
 160
 161 (* UNEXPORTED
 162 End Properties_of_Integral
 163 *)
 164
 165 (* UNEXPORTED
 166 Section More_Properties
 167 *)
 168
 169 (*#*
 170 Two other ways of stating the addition law for domains.
 171 *)
 172
 173 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_Integral.con".
 174
 175 inline procedural "cic:/CoRN/ftc/MoreIntegrals/integral_plus_integral'.con".
 176
 177 (*#*
 178 And now we can prove the addition law for domains with our general operator.
 179
 180 %\begin{convention}% Assume [c : IR].
 181 %\end{convention}%
 182 *)
 183
 184 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/a.var".
 185
 186 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/b.var".
 187
 188 alias id "c" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/c.var".
 189
 190 (* begin show *)
 191
 192 alias id "Hab'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab'.var".
 193
 194 alias id "Hac'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac'.var".
 195
 196 alias id "Hcb'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb'.var".
 197
 198 alias id "Habc'" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc'.var".
 199
 200 (* end show *)
 201
 202 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/F.var".
 203
 204 (* begin show *)
 205
 206 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hab.var".
 207
 208 alias id "Hac" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hac.var".
 209
 210 alias id "Hcb" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Hcb.var".
 211
 212 alias id "Habc" = "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc.var".
 213
 214 (* end show *)
 215
 216 (* begin hide *)
 217
 218 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ab.con" "More_Properties__".
 219
 220 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_ac.con" "More_Properties__".
 221
 222 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_cb.con" "More_Properties__".
 223
 224 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_a.con" "More_Properties__".
 225
 226 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_b.con" "More_Properties__".
 227
 228 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_abc_c.con" "More_Properties__".
 229
 230 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_a.con" "More_Properties__".
 231
 232 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_c.con" "More_Properties__".
 233
 234 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_a.con" "More_Properties__".
 235
 236 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ab_b.con" "More_Properties__".
 237
 238 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_cb_b.con" "More_Properties__".
 239
 240 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/le_ac_c.con" "More_Properties__".
 241
 242 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_abc.con" "More_Properties__".
 243
 244 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ab.con" "More_Properties__".
 245
 246 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_ac.con" "More_Properties__".
 247
 248 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_cb.con" "More_Properties__".
 249
 250 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_a.con" "More_Properties__".
 251
 252 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_b.con" "More_Properties__".
 253
 254 inline procedural "cic:/CoRN/ftc/MoreIntegrals/More_Properties/Habc_c.con" "More_Properties__".
 255
 256 (* end hide *)
 257
 258 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_plus_Integral.con".
 259
 260 (*#*
 261 Notice that, unlike in the classical case, an extra hypothesis (the
 262 continuity of [F] in the interval [[Min(a,b,c),Max(a,b,c)]]) must be assumed.
 263 *)
 264
 265 (* UNEXPORTED
 266 End More_Properties
 267 *)
 268
 269 (* UNEXPORTED
 270 Section Corollaries
 271 *)
 272
 273 alias id "a" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/a.var".
 274
 275 alias id "b" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/b.var".
 276
 277 alias id "Hab" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/Hab.var".
 278
 279 alias id "F" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/F.var".
 280
 281 alias id "contF" = "cic:/CoRN/ftc/MoreIntegrals/Corollaries/contF.var".
 282
 283 (*#* As a corollary, we get the following rule: *)
 284
 285 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_op.con".
 286
 287 (*#* Finally, some miscellaneous results: *)
 288
 289 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_less_norm.con".
 290
 291 inline procedural "cic:/CoRN/ftc/MoreIntegrals/ub_Integral.con".
 292
 293 (* UNEXPORTED
 294 End Corollaries
 295 *)
 296
 297 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_ap_zero.con".
 298
 299 inline procedural "cic:/CoRN/ftc/MoreIntegrals/Integral_eq_zero.con".
 300