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