1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: WeakIVT.v,v 1.9 2004/04/23 10:01:01 lcf Exp $ *)
21 (*#* printing ** %\ensuremath\times% #×# *)
26 Infix "**" := prodT (at level 20).
31 include "ftc/Continuity.ma".
33 (*#* *IVT for Partial Functions
35 In general, we cannot prove the classically valid Intermediate Value
36 Theorem for arbitrary partial functions, which states that in any
37 interval [[a,b]], for any value [z] between [f(a)] and [f(b)]
38 there exists $x\in[a,b]$#x∈[a,b]# such that [f(x) [=] z].
40 However, as is usually the case, there are some good aproximation results. We
48 alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma1/a.var".
50 alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma1/b.var".
52 alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var".
56 inline procedural "cic:/CoRN/ftc/WeakIVT/Lemma1/I.con" "Lemma1__".
60 alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma1/F.var".
62 alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var".
66 %\begin{convention}% Let [a, b : IR] and [Hab : a [<=] b] and denote by [I]
67 the interval [[a,b]]. Let [F] be a continuous function on [I].
70 We begin by proving that, if [f(a) [<] f(b)], then for every [y] in
71 [[f(a),f(b)]] there is an $x\in[a,b]$#x∈[a,b]# such that [f(x)] is close
75 inline procedural "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con".
85 alias id "a" = "cic:/CoRN/ftc/WeakIVT/Lemma2/a.var".
87 alias id "b" = "cic:/CoRN/ftc/WeakIVT/Lemma2/b.var".
89 alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var".
93 inline procedural "cic:/CoRN/ftc/WeakIVT/Lemma2/I.con" "Lemma2__".
97 alias id "F" = "cic:/CoRN/ftc/WeakIVT/Lemma2/F.var".
99 alias id "contF" = "cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var".
102 If [f(b) [<] f(a)], a similar result holds:
105 inline procedural "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con".
117 We will now assume that [a [<] b] and that [F] is not only
118 continuous, but also strictly increasing in [I]. Under
119 these assumptions, we can build two sequences of values which
120 converge to [x0] such that [f(x0) [=] z].
123 alias id "a" = "cic:/CoRN/ftc/WeakIVT/IVT/a.var".
125 alias id "b" = "cic:/CoRN/ftc/WeakIVT/IVT/b.var".
127 alias id "Hab'" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var".
129 alias id "Hab" = "cic:/CoRN/ftc/WeakIVT/IVT/Hab.var".
133 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/I.con" "IVT__".
137 alias id "F" = "cic:/CoRN/ftc/WeakIVT/IVT/F.var".
139 alias id "contF" = "cic:/CoRN/ftc/WeakIVT/IVT/contF.var".
143 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/incF.con" "IVT__".
149 alias id "incrF" = "cic:/CoRN/ftc/WeakIVT/IVT/incrF.var".
155 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/Ha.con" "IVT__".
157 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/Hb.con" "IVT__".
159 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/HFab'.con" "IVT__".
165 alias id "z" = "cic:/CoRN/ftc/WeakIVT/IVT/z.var".
167 alias id "Haz" = "cic:/CoRN/ftc/WeakIVT/IVT/Haz.var".
169 alias id "Hzb" = "cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var".
173 (*#* Given any two points [x [<] y] in [[a,b]] such that [x [<=] z [<=] y],
174 we can find [x' [<] y'] such that $|x'-y'|=\frac23|x-y|$#|x'-y'|=2/3|x-y|#
175 and [x' [<=] z [<=] y'].
178 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con".
183 We now iterate this construction.
186 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind".
188 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_iter.con".
190 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_seq.con".
193 We now define the sequences built from this iteration, starting with [a] and [b].
196 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq.con".
198 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq.con".
200 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_I.con".
202 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_I.con".
204 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con".
206 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con".
208 inline procedural "cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con".
210 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_mon.con".
212 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_mon.con".
214 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con".
216 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con".
218 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con".
220 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con".
222 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/xa.con" "IVT__".
224 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/xb.con" "IVT__".
226 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con".
228 inline procedural "cic:/CoRN/ftc/WeakIVT/xa_in_interval.con".
230 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_I.con".