src/HOL/Lim.thy
author hoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51478 270b21f3ae0a
parent 51473 1210309fddab
permissions -rw-r--r--
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
     1 (*  Title       : Lim.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{* Limits and Continuity *}
     8 
     9 theory Lim
    10 imports SEQ
    11 begin
    12 
    13 subsection {* Limits of Functions *}
    14 
    15 lemma LIM_eq:
    16   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    17   shows "f -- a --> L =
    18      (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    19 by (simp add: LIM_def dist_norm)
    20 
    21 lemma LIM_I:
    22   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    23   shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    24       ==> f -- a --> L"
    25 by (simp add: LIM_eq)
    26 
    27 lemma LIM_D:
    28   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    29   shows "[| f -- a --> L; 0<r |]
    30       ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    31 by (simp add: LIM_eq)
    32 
    33 lemma LIM_offset:
    34   fixes a :: "'a::real_normed_vector"
    35   shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    36 apply (rule topological_tendstoI)
    37 apply (drule (2) topological_tendstoD)
    38 apply (simp only: eventually_at dist_norm)
    39 apply (clarify, rule_tac x=d in exI, safe)
    40 apply (drule_tac x="x + k" in spec)
    41 apply (simp add: algebra_simps)
    42 done
    43 
    44 lemma LIM_offset_zero:
    45   fixes a :: "'a::real_normed_vector"
    46   shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    47 by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    48 
    49 lemma LIM_offset_zero_cancel:
    50   fixes a :: "'a::real_normed_vector"
    51   shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    52 by (drule_tac k="- a" in LIM_offset, simp)
    53 
    54 lemma LIM_zero:
    55   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    56   shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
    57 unfolding tendsto_iff dist_norm by simp
    58 
    59 lemma LIM_zero_cancel:
    60   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    61   shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
    62 unfolding tendsto_iff dist_norm by simp
    63 
    64 lemma LIM_zero_iff:
    65   fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    66   shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
    67 unfolding tendsto_iff dist_norm by simp
    68 
    69 lemma LIM_imp_LIM:
    70   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    71   fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
    72   assumes f: "f -- a --> l"
    73   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
    74   shows "g -- a --> m"
    75   by (rule metric_LIM_imp_LIM [OF f],
    76     simp add: dist_norm le)
    77 
    78 lemma LIM_equal2:
    79   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    80   assumes 1: "0 < R"
    81   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
    82   shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    83 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
    84 
    85 lemma LIM_compose2:
    86   fixes a :: "'a::real_normed_vector"
    87   assumes f: "f -- a --> b"
    88   assumes g: "g -- b --> c"
    89   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
    90   shows "(\<lambda>x. g (f x)) -- a --> c"
    91 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
    92 
    93 lemma real_LIM_sandwich_zero:
    94   fixes f g :: "'a::topological_space \<Rightarrow> real"
    95   assumes f: "f -- a --> 0"
    96   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
    97   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
    98   shows "g -- a --> 0"
    99 proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
   100   fix x assume x: "x \<noteq> a"
   101   have "norm (g x - 0) = g x" by (simp add: 1 x)
   102   also have "g x \<le> f x" by (rule 2 [OF x])
   103   also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   104   also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   105   finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   106 qed
   107 
   108 
   109 subsection {* Continuity *}
   110 
   111 lemma LIM_isCont_iff:
   112   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   113   shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   114 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   115 
   116 lemma isCont_iff:
   117   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   118   shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   119 by (simp add: isCont_def LIM_isCont_iff)
   120 
   121 lemma isCont_LIM_compose2:
   122   fixes a :: "'a::real_normed_vector"
   123   assumes f [unfolded isCont_def]: "isCont f a"
   124   assumes g: "g -- f a --> l"
   125   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   126   shows "(\<lambda>x. g (f x)) -- a --> l"
   127 by (rule LIM_compose2 [OF f g inj])
   128 
   129 
   130 lemma isCont_norm [simp]:
   131   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   132   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   133   by (fact continuous_norm)
   134 
   135 lemma isCont_rabs [simp]:
   136   fixes f :: "'a::t2_space \<Rightarrow> real"
   137   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   138   by (fact continuous_rabs)
   139 
   140 lemma isCont_add [simp]:
   141   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   142   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   143   by (fact continuous_add)
   144 
   145 lemma isCont_minus [simp]:
   146   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   147   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   148   by (fact continuous_minus)
   149 
   150 lemma isCont_diff [simp]:
   151   fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   152   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   153   by (fact continuous_diff)
   154 
   155 lemma isCont_mult [simp]:
   156   fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
   157   shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   158   by (fact continuous_mult)
   159 
   160 lemma (in bounded_linear) isCont:
   161   "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   162   by (fact continuous)
   163 
   164 lemma (in bounded_bilinear) isCont:
   165   "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   166   by (fact continuous)
   167 
   168 lemmas isCont_scaleR [simp] = 
   169   bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   170 
   171 lemmas isCont_of_real [simp] =
   172   bounded_linear.isCont [OF bounded_linear_of_real]
   173 
   174 lemma isCont_power [simp]:
   175   fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   176   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   177   by (fact continuous_power)
   178 
   179 lemma isCont_setsum [simp]:
   180   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   181   shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   182   by (auto intro: continuous_setsum)
   183 
   184 lemmas isCont_intros =
   185   isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   186   isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   187   isCont_of_real isCont_power isCont_sgn isCont_setsum
   188 
   189 subsection {* Uniform Continuity *}
   190 
   191 lemma (in bounded_linear) isUCont: "isUCont f"
   192 unfolding isUCont_def dist_norm
   193 proof (intro allI impI)
   194   fix r::real assume r: "0 < r"
   195   obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   196     using pos_bounded by fast
   197   show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   198   proof (rule exI, safe)
   199     from r K show "0 < r / K" by (rule divide_pos_pos)
   200   next
   201     fix x y :: 'a
   202     assume xy: "norm (x - y) < r / K"
   203     have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   204     also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   205     also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   206     finally show "norm (f x - f y) < r" .
   207   qed
   208 qed
   209 
   210 lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   211 by (rule isUCont [THEN isUCont_Cauchy])
   212 
   213 
   214 lemma LIM_less_bound: 
   215   fixes f :: "real \<Rightarrow> real"
   216   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   217   shows "0 \<le> f x"
   218 proof (rule tendsto_le_const)
   219   show "(f ---> f x) (at_left x)"
   220     using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   221   show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   222     using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
   223 qed simp
   224 
   225 end