helm/software/matita/contribs/procedural/CoRN/reals/RealFuncts.mma

   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 include "CoRN.ma".
  18
  19 (* $Id: RealFuncts.v,v 1.4 2004/04/07 15:08:10 lcf Exp $ *)
  20
  21 include "reals/CReals1.ma".
  22
  23 (*#* * Continuity of Functions on Reals
  24 *)
  25
  26 (* begin hide *)
  27
  28 (* UNEXPORTED
  29 Set Implicit Arguments.
  30 *)
  31
  32 (* UNEXPORTED
  33 Unset Strict Implicit.
  34 *)
  35
  36 (* end hide *)
  37
  38 (* UNEXPORTED
  39 Section Continuity
  40 *)
  41
  42 (* UNEXPORTED
  43 cic:/CoRN/reals/RealFuncts/Continuity/f.var
  44 *)
  45
  46 (* UNEXPORTED
  47 cic:/CoRN/reals/RealFuncts/Continuity/f2.var
  48 *)
  49
  50 (*#*
  51 Let [f] be a unary setoid operation on [IR] and
  52 let [f2] be a binary setoid operation on [IR].
  53
  54 We use the following notations for intervals. [Intclr a b] for the
  55 closed interval [[a,b]], [Intolr a b] for the
  56 open interval [(a,b)], [Intcl a] for the
  57 left-closed interval $[a,\infty)$#[a,&infin;)#, [Intol a] for the
  58 left-open interval $(a,\infty)$#(a,&infin;)#, [Intcr b] for the
  59 right-closed interval $(-\infty,b]$#(-&infin;,b]#.
  60
  61 Intervals like $[a,b]$#[a,b]# are defined for arbitrary reals [a,b] (being
  62 $\emptyset$#&empty;# for [a [>] b]).
  63 *)
  64
  65 inline procedural "cic:/CoRN/reals/RealFuncts/Intclr.con" as definition.
  66
  67 inline procedural "cic:/CoRN/reals/RealFuncts/Intolr.con" as definition.
  68
  69 inline procedural "cic:/CoRN/reals/RealFuncts/Intol.con" as definition.
  70
  71 inline procedural "cic:/CoRN/reals/RealFuncts/Intcl.con" as definition.
  72
  73 inline procedural "cic:/CoRN/reals/RealFuncts/Intcr.con" as definition.
  74
  75 (*#* The limit of [f(x)] as [x] goes to [p = l], for both unary and binary
  76 functions:
  77
  78 The limit of [f] in [p] is [l] if
  79 [[
  80 forall e [>] Zero, exists d [>] Zero, forall (x : IR)
  81 ( [--]d [<] p[-]x [<] d) -> ( [--]e [<] [--]f(x) [<] e)
  82 ]]
  83 *)
  84
  85 inline procedural "cic:/CoRN/reals/RealFuncts/funLim.con" as definition.
  86
  87 (*#* The definition of limit of [f] in [p] using Cauchy sequences. *)
  88
  89 inline procedural "cic:/CoRN/reals/RealFuncts/funLim_Cauchy.con" as definition.
  90
  91 (*#* The first definition implies the second one. *)
  92
  93 (*
  94  Ax_iom funLim_prop1 :(p,l:IR)(funLim p l)->(funLim_Cauchy p l).
  95 Intros. Unfold funLim_Cauchy. Unfold funLim in H. Intros.
  96 Elim (H e H1). Intros.
  97 Elim s. Intros s_seq s_proof.
  98 Decompose [and] H2.
  99 Cut (Zero  [<]   x[/]TwoNZ).
 100 Intro Hx2.
 101 Elim (s_proof (x[/]TwoNZ) Hx2).
 102 Intros N HN.
 103 Exists N.
 104 Intros.
 105 Apply AbsSmall_minus.
 106 Apply H5.
 107 Generalize (HN m H3).
 108 Intro HmN.
 109 *)
 110
 111 (*#* The limit of [f] in [(p,p')] is [l] if
 112 [[
 113 forall e [>] Zero, exists d [>] Zero, forall (x : IR)
 114 ( [--]d [<] p[-]x [<] d) -> ( [--]d' [<] p'[-]y [<] d') -> ( [--]e [<] l[-]f(x,y) [<] e
 115 ]]
 116 *)
 117
 118 inline procedural "cic:/CoRN/reals/RealFuncts/funLim2.con" as definition.
 119
 120 (*#* The function [f] is continuous at [p] if the limit of [f(x)] as
 121 [x] goes to [p] is [f(p)].  This is the [eps [/] delta] definition.
 122 We also give the definition with limits of Cauchy sequences.
 123 *)
 124
 125 inline procedural "cic:/CoRN/reals/RealFuncts/continAt.con" as definition.
 126
 127 inline procedural "cic:/CoRN/reals/RealFuncts/continAtCauchy.con" as definition.
 128
 129 inline procedural "cic:/CoRN/reals/RealFuncts/continAt2.con" as definition.
 130
 131 (*
 132 Ax_iom continAt_prop1 :(p:IR)(continAt p)->(continAtCauchy p).
 133 *)
 134
 135 inline procedural "cic:/CoRN/reals/RealFuncts/contin.con" as definition.
 136
 137 inline procedural "cic:/CoRN/reals/RealFuncts/continCauchy.con" as definition.
 138
 139 inline procedural "cic:/CoRN/reals/RealFuncts/contin2.con" as definition.
 140
 141 (*#*
 142 Continuous on a closed, resp.%\% open, resp.%\% left open, resp.%\% left closed
 143 interval *)
 144
 145 inline procedural "cic:/CoRN/reals/RealFuncts/continOnc.con" as definition.
 146
 147 inline procedural "cic:/CoRN/reals/RealFuncts/continOno.con" as definition.
 148
 149 inline procedural "cic:/CoRN/reals/RealFuncts/continOnol.con" as definition.
 150
 151 inline procedural "cic:/CoRN/reals/RealFuncts/continOncl.con" as definition.
 152
 153 (*
 154 Section Sequence_and_function_limits.
 155
 156 _**
 157 If $\lim_{x->p} (f x) = l$, then for every sequence $p_n$ whose
 158 limit is $p$, $\lim_{n->\infty} f (p_n) =l$.
 159  *_
 160
 161 Lemma funLim_SeqLimit:
 162   (p,l:IR)(fl:(funLim p l))
 163     (pn:nat->IR)(sl:(SeqLimit pn p)) (SeqLimit ( [n:nat] (f (pn n))) l).
 164 Proof.
 165 Intros; Unfold seqLimit.
 166 Intros eps epos.
 167 Elim (fl ? epos); Intros del dh; Elim dh; Intros H0 H1.
 168 Elim (sl ? H0); Intros N Nh.
 169 Exists N. Intros m leNm.
 170 Apply AbsSmall_minus.
 171 Apply H1.
 172 Apply AbsSmall_minus.
 173 Apply (Nh ? leNm).
 174 Qed.
 175
 176 _**** Is the converse constructively provable? **
 177 Lemma SeqLimit_funLim:
 178   (p,l:IR)((pn:nat->IR)(sl:(SeqLimit pn p)) (SeqLimit ( [n:nat] (f (pn n))) l))->
 179     (funLim p l).
 180 ****_
 181
 182 _**
 183 Now the same Lemma in terms of Cauchy sequences: if $\lim_{x->p} (f x) = l$,
 184 then for every Cauchy sequence $s_n$ whose
 185 limit is $p$, $\lim_{n->\infty} f (s_n) =l$.
 186  *_
 187
 188 Ax_iom funLim_isCauchy:
 189   (p,l:IR)(funLim p l)->(s:CauchySeqR)((Lim s)  [=]   p)->
 190         (e:IR)(Zero  [<]  e)->(Ex [N:nat] (m:nat)(le N m)
 191                          ->(AbsSmall e ((s m) [-] (s N)))).
 192
 193 End Sequence_and_function_limits.
 194
 195 Section Monotonic_functions.
 196
 197 Definition str_monot  := (x,y:IR)(x  [<]  y)->((f x)  [<]  (f y)).
 198
 199 Definition str_monotOnc  := [a,b:IR]
 200          (x,y:IR)(Intclr a b x)->(Intclr a b y)
 201                 ->(x  [<]  y)->((f x)  [<]  (f y)).
 202
 203 Definition str_monotOncl  := [a:IR]
 204          (x,y:IR)(Intcl a x)->(Intcl a y)
 205                 ->(x  [<]  y)->((f x)  [<]  (f y)).
 206
 207 Definition str_monotOnol  := [a:IR]
 208          (x,y:IR)(Intol a x)->(Intol a y)
 209                 ->(x  [<]  y)->((f x)  [<]  (f y)).
 210
 211 _** Following probably not needed for the FTA proof;
 212 it stated that strong monotonicity on a closed interval implies that the
 213 intermediate value theorem holds on this interval. For FTA we need IVT on
 214 $[0,\infty>$.
 215 *_
 216
 217 Ax_iom strmonc_imp_ivt :(a,b:IR)(str_monotOnc a b)
 218            ->(x,y:IR)(x  [<]  y)->(Intclr a b x)->(Intclr a b y)
 219                ->((f x)  [<]  Zero)->(Zero  [<]  (f y))
 220                    ->(EX z:IR | (Intclr x y z)/\((f z)  [=]  Zero)).
 221 _**
 222 $\forall c\in\RR (f\mbox{ strongly monotonic on }[c,\infty>)
 223 \rightarrow \forall a,b\in\RR(c <a)\rightarrow( c< b)\rightarrow\ (f (a)<0)
 224 \rightarrow\ (0:<f(b))
 225          \rightarrow \forall x,y\in\RR (a\leq x\leq b)\rightarrow
 226         (a\leq y\leq b)\rightarrow (x<y)
 227                 \rightarrow \exists z\in\RR(x\leq z\leq y)\wedge(f(z)\noto 0))$
 228 *_
 229
 230 Ax_iom strmon_ivt_prem : (c:IR)(str_monotOncl c)->
 231   (a,b:IR)(Intcl c a)->(Intcl c b)->((f a)  [<]   Zero)->(Zero   [<]  (f b))
 232        ->(x,y:IR)(Intclr a b x)->(Intclr a b y)->(x  [<]  y)
 233               ->(EX z:IR | (Intclr x y z)/\((f z)  [#]  Zero)).
 234
 235 _** The following is lemma 5.8 from the skeleton
 236
 237 $\forall c\in\RR (f\mbox{ strongly monotonic on }[c,\infty>)
 238 \rightarrow \forall a,b\in\RR(a<b) \rightarrow(c <a)\rightarrow( c< b)
 239 \rightarrow(f (a)<0)\rightarrow (0:<f(b))
 240          \rightarrow \exists z\in\RR(a\leq z\leq b)\wedge(f(z)= 0))$
 241 *_
 242
 243 Ax_iom strmoncl_imp_ivt : (c:IR)(str_monotOncl c)
 244            ->(a,b:IR)(a  [<]  b)->(Intcl c a)->(Intcl c b)
 245                ->((f a)  [<]  Zero)->(Zero  [<]  (f b))
 246                    ->(EX z:IR | (Intclr a b z)/\ ((f z)  [=]  Zero)).
 247 End Monotonic_functions.
 248
 249 *)
 250
 251 (* UNEXPORTED
 252 End Continuity
 253 *)
 254
 255 (* begin hide *)
 256
 257 (* UNEXPORTED
 258 Set Strict Implicit.
 259 *)
 260
 261 (* UNEXPORTED
 262 Unset Implicit Arguments.
 263 *)
 264
 265 (* end hide *)
 266