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
49 cic:/CoRN/ftc/WeakIVT/Lemma1/a.var
53 cic:/CoRN/ftc/WeakIVT/Lemma1/b.var
57 cic:/CoRN/ftc/WeakIVT/Lemma1/Hab.var
62 inline procedural "cic:/CoRN/ftc/WeakIVT/Lemma1/I.con" "Lemma1__" as definition.
67 cic:/CoRN/ftc/WeakIVT/Lemma1/F.var
71 cic:/CoRN/ftc/WeakIVT/Lemma1/contF.var
76 %\begin{convention}% Let [a, b : IR] and [Hab : a [<=] b] and denote by [I]
77 the interval [[a,b]]. Let [F] be a continuous function on [I].
80 We begin by proving that, if [f(a) [<] f(b)], then for every [y] in
81 [[f(a),f(b)]] there is an $x\in[a,b]$#x∈[a,b]# such that [f(x)] is close
85 inline procedural "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_lft.con" as lemma.
96 cic:/CoRN/ftc/WeakIVT/Lemma2/a.var
100 cic:/CoRN/ftc/WeakIVT/Lemma2/b.var
104 cic:/CoRN/ftc/WeakIVT/Lemma2/Hab.var
109 inline procedural "cic:/CoRN/ftc/WeakIVT/Lemma2/I.con" "Lemma2__" as definition.
114 cic:/CoRN/ftc/WeakIVT/Lemma2/F.var
118 cic:/CoRN/ftc/WeakIVT/Lemma2/contF.var
122 If [f(b) [<] f(a)], a similar result holds:
125 inline procedural "cic:/CoRN/ftc/WeakIVT/Weak_IVT_ap_rht.con" as lemma.
137 We will now assume that [a [<] b] and that [F] is not only
138 continuous, but also strictly increasing in [I]. Under
139 these assumptions, we can build two sequences of values which
140 converge to [x0] such that [f(x0) [=] z].
144 cic:/CoRN/ftc/WeakIVT/IVT/a.var
148 cic:/CoRN/ftc/WeakIVT/IVT/b.var
152 cic:/CoRN/ftc/WeakIVT/IVT/Hab'.var
156 cic:/CoRN/ftc/WeakIVT/IVT/Hab.var
161 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/I.con" "IVT__" as definition.
166 cic:/CoRN/ftc/WeakIVT/IVT/F.var
170 cic:/CoRN/ftc/WeakIVT/IVT/contF.var
175 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/incF.con" "IVT__" as definition.
182 cic:/CoRN/ftc/WeakIVT/IVT/incrF.var
189 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/Ha.con" "IVT__" as definition.
191 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/Hb.con" "IVT__" as definition.
193 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/HFab'.con" "IVT__" as definition.
200 cic:/CoRN/ftc/WeakIVT/IVT/z.var
204 cic:/CoRN/ftc/WeakIVT/IVT/Haz.var
208 cic:/CoRN/ftc/WeakIVT/IVT/Hzb.var
213 (*#* Given any two points [x [<] y] in [[a,b]] such that [x [<=] z [<=] y],
214 we can find [x' [<] y'] such that $|x'-y'|=\frac23|x-y|$#|x'-y'|=2/3|x-y|#
215 and [x' [<=] z [<=] y'].
218 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_seq_lemma.con" as lemma.
223 We now iterate this construction.
226 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_aux_seq_type.ind".
228 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_iter.con" as definition.
230 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_seq.con" as definition.
233 We now define the sequences built from this iteration, starting with [a] and [b].
236 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq.con" as definition.
238 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq.con" as definition.
240 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_I.con" as definition.
242 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_I.con" as definition.
244 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_less_b_seq.con" as lemma.
246 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_leEq_z.con" as lemma.
248 inline procedural "cic:/CoRN/ftc/WeakIVT/z_leEq_b_seq.con" as lemma.
250 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_mon.con" as lemma.
252 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_mon.con" as lemma.
254 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist_n.con" as lemma.
256 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_dist.con" as lemma.
258 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_Cauchy.con" as lemma.
260 inline procedural "cic:/CoRN/ftc/WeakIVT/b_seq_Cauchy.con" as lemma.
262 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/xa.con" "IVT__" as definition.
264 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT/xb.con" "IVT__" as definition.
266 inline procedural "cic:/CoRN/ftc/WeakIVT/a_seq_b_seq_lim.con" as lemma.
268 inline procedural "cic:/CoRN/ftc/WeakIVT/xa_in_interval.con" as lemma.
270 inline procedural "cic:/CoRN/ftc/WeakIVT/IVT_I.con" as lemma.