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: RealFuncts.v,v 1.4 2004/04/07 15:08:10 lcf Exp $ *)
21 include "reals/CReals1.ma".
23 (*#* * Continuity of Functions on Reals
29 Set Implicit Arguments.
33 Unset Strict Implicit.
42 alias id "f" = "cic:/CoRN/reals/RealFuncts/Continuity/f.var".
44 alias id "f2" = "cic:/CoRN/reals/RealFuncts/Continuity/f2.var".
47 Let [f] be a unary setoid operation on [IR] and
48 let [f2] be a binary setoid operation on [IR].
50 We use the following notations for intervals. [Intclr a b] for the
51 closed interval [[a,b]], [Intolr a b] for the
52 open interval [(a,b)], [Intcl a] for the
53 left-closed interval $[a,\infty)$#[a,∞)#, [Intol a] for the
54 left-open interval $(a,\infty)$#(a,∞)#, [Intcr b] for the
55 right-closed interval $(-\infty,b]$#(-∞,b]#.
57 Intervals like $[a,b]$#[a,b]# are defined for arbitrary reals [a,b] (being
58 $\emptyset$#∅# for [a [>] b]).
61 inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con" as definition.
63 inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con" as definition.
65 inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con" as definition.
67 inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con" as definition.
69 inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con" as definition.
71 (*#* The limit of [f(x)] as [x] goes to [p = l], for both unary and binary
74 The limit of [f] in [p] is [l] if
76 forall e [>] Zero, exists d [>] Zero, forall (x : IR)
77 ( [--]d [<] p[-]x [<] d) -> ( [--]e [<] [--]f(x) [<] e)
81 inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con" as definition.
83 (*#* The definition of limit of [f] in [p] using Cauchy sequences. *)
85 inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con" as definition.
87 (*#* The first definition implies the second one. *)
90 Ax_iom funLim_prop1 :(p,l:IR)(funLim p l)->(funLim_Cauchy p l).
91 Intros. Unfold funLim_Cauchy. Unfold funLim in H. Intros.
92 Elim (H e H1). Intros.
93 Elim s. Intros s_seq s_proof.
95 Cut (Zero [<] x[/]TwoNZ).
97 Elim (s_proof (x[/]TwoNZ) Hx2).
101 Apply AbsSmall_minus.
103 Generalize (HN m H3).
107 (*#* The limit of [f] in [(p,p')] is [l] if
109 forall e [>] Zero, exists d [>] Zero, forall (x : IR)
110 ( [--]d [<] p[-]x [<] d) -> ( [--]d' [<] p'[-]y [<] d') -> ( [--]e [<] l[-]f(x,y) [<] e
114 inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con" as definition.
116 (*#* The function [f] is continuous at [p] if the limit of [f(x)] as
117 [x] goes to [p] is [f(p)]. This is the [eps [/] delta] definition.
118 We also give the definition with limits of Cauchy sequences.
121 inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con" as definition.
123 inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con" as definition.
125 inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con" as definition.
128 Ax_iom continAt_prop1 :(p:IR)(continAt p)->(continAtCauchy p).
131 inline procedural "cic:/CoRN/reals/RealFuncts/contin.con" as definition.
133 inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con" as definition.
135 inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con" as definition.
138 Continuous on a closed, resp.%\% open, resp.%\% left open, resp.%\% left closed
141 inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con" as definition.
143 inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con" as definition.
145 inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con" as definition.
147 inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con" as definition.
150 Section Sequence_and_function_limits.
153 If $\lim_{x->p} (f x) = l$, then for every sequence $p_n$ whose
154 limit is $p$, $\lim_{n->\infty} f (p_n) =l$.
157 Lemma funLim_SeqLimit:
158 (p,l:IR)(fl:(funLim p l))
159 (pn:nat->IR)(sl:(SeqLimit pn p)) (SeqLimit ( [n:nat] (f (pn n))) l).
161 Intros; Unfold seqLimit.
163 Elim (fl ? epos); Intros del dh; Elim dh; Intros H0 H1.
164 Elim (sl ? H0); Intros N Nh.
165 Exists N. Intros m leNm.
166 Apply AbsSmall_minus.
168 Apply AbsSmall_minus.
172 _**** Is the converse constructively provable? **
173 Lemma SeqLimit_funLim:
174 (p,l:IR)((pn:nat->IR)(sl:(SeqLimit pn p)) (SeqLimit ( [n:nat] (f (pn n))) l))->
179 Now the same Lemma in terms of Cauchy sequences: if $\lim_{x->p} (f x) = l$,
180 then for every Cauchy sequence $s_n$ whose
181 limit is $p$, $\lim_{n->\infty} f (s_n) =l$.
184 Ax_iom funLim_isCauchy:
185 (p,l:IR)(funLim p l)->(s:CauchySeqR)((Lim s) [=] p)->
186 (e:IR)(Zero [<] e)->(Ex [N:nat] (m:nat)(le N m)
187 ->(AbsSmall e ((s m) [-] (s N)))).
189 End Sequence_and_function_limits.
191 Section Monotonic_functions.
193 Definition str_monot := (x,y:IR)(x [<] y)->((f x) [<] (f y)).
195 Definition str_monotOnc := [a,b:IR]
196 (x,y:IR)(Intclr a b x)->(Intclr a b y)
197 ->(x [<] y)->((f x) [<] (f y)).
199 Definition str_monotOncl := [a:IR]
200 (x,y:IR)(Intcl a x)->(Intcl a y)
201 ->(x [<] y)->((f x) [<] (f y)).
203 Definition str_monotOnol := [a:IR]
204 (x,y:IR)(Intol a x)->(Intol a y)
205 ->(x [<] y)->((f x) [<] (f y)).
207 _** Following probably not needed for the FTA proof;
208 it stated that strong monotonicity on a closed interval implies that the
209 intermediate value theorem holds on this interval. For FTA we need IVT on
213 Ax_iom strmonc_imp_ivt :(a,b:IR)(str_monotOnc a b)
214 ->(x,y:IR)(x [<] y)->(Intclr a b x)->(Intclr a b y)
215 ->((f x) [<] Zero)->(Zero [<] (f y))
216 ->(EX z:IR | (Intclr x y z)/\((f z) [=] Zero)).
218 $\forall c\in\RR (f\mbox{ strongly monotonic on }[c,\infty>)
219 \rightarrow \forall a,b\in\RR(c <a)\rightarrow( c< b)\rightarrow\ (f (a)<0)
220 \rightarrow\ (0:<f(b))
221 \rightarrow \forall x,y\in\RR (a\leq x\leq b)\rightarrow
222 (a\leq y\leq b)\rightarrow (x<y)
223 \rightarrow \exists z\in\RR(x\leq z\leq y)\wedge(f(z)\noto 0))$
226 Ax_iom strmon_ivt_prem : (c:IR)(str_monotOncl c)->
227 (a,b:IR)(Intcl c a)->(Intcl c b)->((f a) [<] Zero)->(Zero [<] (f b))
228 ->(x,y:IR)(Intclr a b x)->(Intclr a b y)->(x [<] y)
229 ->(EX z:IR | (Intclr x y z)/\((f z) [#] Zero)).
231 _** The following is lemma 5.8 from the skeleton
233 $\forall c\in\RR (f\mbox{ strongly monotonic on }[c,\infty>)
234 \rightarrow \forall a,b\in\RR(a<b) \rightarrow(c <a)\rightarrow( c< b)
235 \rightarrow(f (a)<0)\rightarrow (0:<f(b))
236 \rightarrow \exists z\in\RR(a\leq z\leq b)\wedge(f(z)= 0))$
239 Ax_iom strmoncl_imp_ivt : (c:IR)(str_monotOncl c)
240 ->(a,b:IR)(a [<] b)->(Intcl c a)->(Intcl c b)
241 ->((f a) [<] Zero)->(Zero [<] (f b))
242 ->(EX z:IR | (Intclr a b z)/\ ((f z) [=] Zero)).
243 End Monotonic_functions.
258 Unset Implicit Arguments.