helm/software/matita/contribs/CoRN-Decl/ftc/WeakIVT.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/WeakIVT".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
  22
  23 (*#* printing ** %\ensuremath\times% #&times;# *)
  24
  25 (* begin hide *)
  26
  27 (* end hide *)
  28
  29 include "ftc/Continuity.ma".
  30
  31 (*#* *IVT for Partial Functions
  32
  33 In general, we cannot prove the classically valid Intermediate Value
  34 Theorem for arbitrary partial functions, which states that in any
  35 interval [[a,b]], for any value [z] between [f(a)] and [f(b)]
  36 there exists $x\in[a,b]$#x&isin;[a,b]# such that [f(x) [=] z].
  37
  38 However, as is usually the case, there are some good aproximation results.  We
  39 will prove them here.
  40 *)
  41
  42 (* UNEXPORTED
  43 Section Lemma1.
  44 *)
  45
  46 inline "cic:/CoRN/ftc/WeakIVT/a.var".
  47
  48 inline "cic:/CoRN/ftc/WeakIVT/b.var".
  49
  50 inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
  51
  52 (* begin hide *)
  53
  54 inline "cic:/CoRN/ftc/WeakIVT/I.con".
  55
  56 (* end hide *)
  57
  58 inline "cic:/CoRN/ftc/WeakIVT/F.var".
  59
  60 inline "cic:/CoRN/ftc/WeakIVT/contF.var".
  61
  62 (*#* **First Lemmas
  63
  64 %\begin{convention}% Let [a, b : IR] and [Hab : a [<=] b] and denote by [I]
  65 the interval [[a,b]].  Let [F] be a continuous function on [I].
  66 %\end{convention}%
  67
  68 We begin by proving that, if [f(a) [<] f(b)], then for every [y] in
  69 [[f(a),f(b)]] there is an $x\in[a,b]$#x&isin;[a,b]# such that [f(x)] is close
  70 enough to [z].
  71 *)
  72
  73 inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con".
  74
  75 (* UNEXPORTED
  76 End Lemma1.
  77 *)
  78
  79 (* UNEXPORTED
  80 Section Lemma2.
  81 *)
  82
  83 inline "cic:/CoRN/ftc/WeakIVT/a.var".
  84
  85 inline "cic:/CoRN/ftc/WeakIVT/b.var".
  86
  87 inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
  88
  89 (* begin hide *)
  90
  91 inline "cic:/CoRN/ftc/WeakIVT/I.con".
  92
  93 (* end hide *)
  94
  95 inline "cic:/CoRN/ftc/WeakIVT/F.var".
  96
  97 inline "cic:/CoRN/ftc/WeakIVT/contF.var".
  98
  99 (*#*
 100 If [f(b) [<] f(a)], a similar result holds:
 101 *)
 102
 103 inline "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con".
 104
 105 (* UNEXPORTED
 106 End Lemma2.
 107 *)
 108
 109 (* UNEXPORTED
 110 Section IVT.
 111 *)
 112
 113 (*#* **The IVT
 114
 115 We will now assume that [a [<] b] and that [F] is not only
 116 continuous, but also strictly increasing in [I].  Under
 117 these assumptions, we can build two sequences of values which
 118 converge to [x0] such that [f(x0) [=] z].
 119 *)
 120
 121 inline "cic:/CoRN/ftc/WeakIVT/a.var".
 122
 123 inline "cic:/CoRN/ftc/WeakIVT/b.var".
 124
 125 inline "cic:/CoRN/ftc/WeakIVT/Hab'.var".
 126
 127 inline "cic:/CoRN/ftc/WeakIVT/Hab.var".
 128
 129 (* begin hide *)
 130
 131 inline "cic:/CoRN/ftc/WeakIVT/I.con".
 132
 133 (* end hide *)
 134
 135 inline "cic:/CoRN/ftc/WeakIVT/F.var".
 136
 137 inline "cic:/CoRN/ftc/WeakIVT/contF.var".
 138
 139 (* begin hide *)
 140
 141 inline "cic:/CoRN/ftc/WeakIVT/incF.con".
 142
 143 (* end hide *)
 144
 145 (* begin show *)
 146
 147 inline "cic:/CoRN/ftc/WeakIVT/incrF.var".
 148
 149 (* end show *)
 150
 151 (* begin hide *)
 152
 153 inline "cic:/CoRN/ftc/WeakIVT/Ha.con".
 154
 155 inline "cic:/CoRN/ftc/WeakIVT/Hb.con".
 156
 157 inline "cic:/CoRN/ftc/WeakIVT/HFab'.con".
 158
 159 (* end hide *)
 160
 161 (* begin show *)
 162
 163 inline "cic:/CoRN/ftc/WeakIVT/z.var".
 164
 165 inline "cic:/CoRN/ftc/WeakIVT/Haz.var".
 166
 167 inline "cic:/CoRN/ftc/WeakIVT/Hzb.var".
 168
 169 (* end show *)
 170
 171 (*#* Given any two points [x [<] y] in [[a,b]] such that [x [<=] z [<=] y],
 172 we can find [x' [<] y'] such that $|x'-y'|=\frac23|x-y|$#|x'-y'|=2/3|x-y|#
 173 and [x' [<=] z [<=] y'].
 174 *)
 175
 176 inline "cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con".
 177
 178 (* end hide *)
 179
 180 (*#*
 181 We now iterate this construction.
 182 *)
 183
 184 inline "cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind".
 185
 186 inline "cic:/CoRN/ftc/WeakIVT/IVT_iter.con".
 187
 188 inline "cic:/CoRN/ftc/WeakIVT/IVT_seq.con".
 189
 190 (*#*
 191 We now define the sequences built from this iteration, starting with [a] and [b].
 192 *)
 193
 194 inline "cic:/CoRN/ftc/WeakIVT/a_seq.con".
 195
 196 inline "cic:/CoRN/ftc/WeakIVT/b_seq.con".
 197
 198 inline "cic:/CoRN/ftc/WeakIVT/a_seq_I.con".
 199
 200 inline "cic:/CoRN/ftc/WeakIVT/b_seq_I.con".
 201
 202 inline "cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con".
 203
 204 inline "cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con".
 205
 206 inline "cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con".
 207
 208 inline "cic:/CoRN/ftc/WeakIVT/a_seq_mon.con".
 209
 210 inline "cic:/CoRN/ftc/WeakIVT/b_seq_mon.con".
 211
 212 inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con".
 213
 214 inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con".
 215
 216 inline "cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con".
 217
 218 inline "cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con".
 219
 220 inline "cic:/CoRN/ftc/WeakIVT/xa.con".
 221
 222 inline "cic:/CoRN/ftc/WeakIVT/xb.con".
 223
 224 inline "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con".
 225
 226 inline "cic:/CoRN/ftc/WeakIVT/xa_in_interval.con".
 227
 228 inline "cic:/CoRN/ftc/WeakIVT/IVT_I.con".
 229
 230 (* UNEXPORTED
 231 End IVT.
 232 *)
 233