matita/matita/contribs/CoRN-Decl/ftc/FunctSums.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/FunctSums".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: FunctSums.v,v 1.5 2004/04/23 10:00:59 lcf Exp $ *)
  22
  23 (*#* printing FSum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
  24
  25 (*#* printing FSum %\ensuremath{\sum}% #&sum;# *)
  26
  27 (*#* printing FSumx %\ensuremath{\sum'}% #&sum;'&*)
  28
  29 include "reals/CSumsReals.ma".
  30
  31 include "ftc/PartFunEquality.ma".
  32
  33 (*#* *Sums of Functions
  34
  35 In this file we define sums are defined of arbitrary families of
  36 partial functions.
  37
  38 Given a countable family of functions, their sum is defined on the
  39 intersection of all the domains.  As is the case for groups, we will
  40 define three different kinds of sums.
  41
  42 We will first consider the case of a family
  43 $\{f_i\}_{i\in\NN}$#{f<sub>i</sub>}# of functions; we can both define
  44 $\sum_{i=0}^{n-1}f_i$#the sum of the first n functions# ( [FSum0]) or
  45 $\sum_{i=m}^nf_i$#the sum of f<sub>m</sub> through f<sub>n</sub>#
  46 ( [FSum]).
  47 *)
  48
  49 inline "cic:/CoRN/ftc/FunctSums/FSum0.con".
  50
  51 inline "cic:/CoRN/ftc/FunctSums/FSum.con".
  52
  53 (*#*
  54 Although [FSum] is here defined directly, it has the same relationship
  55 to the [FSum0] operator as [Sum] has to [Sum0].  Also, all the results
  56 for [Sum] and [Sum0] hold when these operators are replaced by their
  57 functional equivalents.  This is an immediate consequence of the fact
  58 that the partial functions form a group; however, as we already
  59 mentioned, their forming too big a type makes it impossible to use
  60 those results.
  61 *)
  62
  63 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0.con".
  64
  65 inline "cic:/CoRN/ftc/FunctSums/FSum0_wd.con".
  66
  67 inline "cic:/CoRN/ftc/FunctSums/FSum_one.con".
  68
  69 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum.con".
  70
  71 inline "cic:/CoRN/ftc/FunctSums/FSum_first.con".
  72
  73 inline "cic:/CoRN/ftc/FunctSums/FSum_last.con".
  74
  75 inline "cic:/CoRN/ftc/FunctSums/FSum_last'.con".
  76
  77 inline "cic:/CoRN/ftc/FunctSums/FSum_wd.con".
  78
  79 inline "cic:/CoRN/ftc/FunctSums/FSum_plus_FSum.con".
  80
  81 inline "cic:/CoRN/ftc/FunctSums/inv_FSum.con".
  82
  83 inline "cic:/CoRN/ftc/FunctSums/FSum_minus_FSum.con".
  84
  85 inline "cic:/CoRN/ftc/FunctSums/FSum_wd'.con".
  86
  87 inline "cic:/CoRN/ftc/FunctSums/FSum_resp_less.con".
  88
  89 inline "cic:/CoRN/ftc/FunctSums/FSum_resp_leEq.con".
  90
  91 inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal.con".
  92
  93 inline "cic:/CoRN/ftc/FunctSums/FSum_comm_scal'.con".
  94
  95 (*#*
  96 Also important is the case when we have a finite family
  97 $\{f_i\}_{i=0}^{n-1}$ of #exactly n# functions; in this case we need
  98 to use the [FSumx] operator.
  99 *)
 100
 101 inline "cic:/CoRN/ftc/FunctSums/FSumx.con".
 102
 103 (*#*
 104 This operator is well defined, as expected.
 105 *)
 106
 107 inline "cic:/CoRN/ftc/FunctSums/FSumx_wd.con".
 108
 109 inline "cic:/CoRN/ftc/FunctSums/FSumx_wd'.con".
 110
 111 (*#*
 112 As was already the case for [Sumx], in many cases we will need to
 113 explicitly assume that $f_i$#f<sub>1</sub># is independent of the proof that
 114 [i [<] n].  This holds both for the value and the domain of the partial
 115 function $f_i$#f<sub>i</sub>#.
 116 *)
 117
 118 inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq.con".
 119
 120 inline "cic:/CoRN/ftc/FunctSums/ext_fun_seq'.con".
 121
 122 (* UNEXPORTED
 123 Implicit Arguments ext_fun_seq [n].
 124 *)
 125
 126 (* UNEXPORTED
 127 Implicit Arguments ext_fun_seq' [n].
 128 *)
 129
 130 (*#*
 131 Under these assumptions, we can characterize the domain and the value of the sum function from the domains and values of the summands:
 132 *)
 133
 134 inline "cic:/CoRN/ftc/FunctSums/FSumx_pred.con".
 135
 136 inline "cic:/CoRN/ftc/FunctSums/FSumx_pred'.con".
 137
 138 inline "cic:/CoRN/ftc/FunctSums/FSumx_char.con".
 139
 140 (*#*
 141 As we did for arbitrary groups, it is often useful to rewrite this sums as ordinary sums.
 142 *)
 143
 144 inline "cic:/CoRN/ftc/FunctSums/FSumx_to_FSum.con".
 145
 146 inline "cic:/CoRN/ftc/FunctSums/FSumx_lt.con".
 147
 148 inline "cic:/CoRN/ftc/FunctSums/FSumx_le.con".
 149
 150 inline "cic:/CoRN/ftc/FunctSums/FSum_FSumx_to_FSum.con".
 151
 152 (*#*
 153 Some useful lemmas follow.
 154 *)
 155
 156 inline "cic:/CoRN/ftc/FunctSums/FSum0_0.con".
 157
 158 inline "cic:/CoRN/ftc/FunctSums/FSum0_S.con".
 159
 160 inline "cic:/CoRN/ftc/FunctSums/FSum_0.con".
 161
 162 inline "cic:/CoRN/ftc/FunctSums/FSum_S.con".
 163
 164 inline "cic:/CoRN/ftc/FunctSums/FSum_FSum0'.con".
 165