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