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