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