src/HOL/Lim.thy
changeset 51526 155263089e7b
parent 51525 d3d170a2887f
child 51527 bd62e7ff103b
     1.1 --- a/src/HOL/Lim.thy	Tue Mar 26 12:20:58 2013 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,225 +0,0 @@
     1.4 -(*  Title       : Lim.thy
     1.5 -    Author      : Jacques D. Fleuriot
     1.6 -    Copyright   : 1998  University of Cambridge
     1.7 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.8 -*)
     1.9 -
    1.10 -header{* Limits and Continuity *}
    1.11 -
    1.12 -theory Lim
    1.13 -imports SEQ
    1.14 -begin
    1.15 -
    1.16 -subsection {* Limits of Functions *}
    1.17 -
    1.18 -lemma LIM_eq:
    1.19 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    1.20 -  shows "f -- a --> L =
    1.21 -     (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    1.22 -by (simp add: LIM_def dist_norm)
    1.23 -
    1.24 -lemma LIM_I:
    1.25 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    1.26 -  shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    1.27 -      ==> f -- a --> L"
    1.28 -by (simp add: LIM_eq)
    1.29 -
    1.30 -lemma LIM_D:
    1.31 -  fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    1.32 -  shows "[| f -- a --> L; 0<r |]
    1.33 -      ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    1.34 -by (simp add: LIM_eq)
    1.35 -
    1.36 -lemma LIM_offset:
    1.37 -  fixes a :: "'a::real_normed_vector"
    1.38 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    1.39 -apply (rule topological_tendstoI)
    1.40 -apply (drule (2) topological_tendstoD)
    1.41 -apply (simp only: eventually_at dist_norm)
    1.42 -apply (clarify, rule_tac x=d in exI, safe)
    1.43 -apply (drule_tac x="x + k" in spec)
    1.44 -apply (simp add: algebra_simps)
    1.45 -done
    1.46 -
    1.47 -lemma LIM_offset_zero:
    1.48 -  fixes a :: "'a::real_normed_vector"
    1.49 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    1.50 -by (drule_tac k="a" in LIM_offset, simp add: add_commute)
    1.51 -
    1.52 -lemma LIM_offset_zero_cancel:
    1.53 -  fixes a :: "'a::real_normed_vector"
    1.54 -  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    1.55 -by (drule_tac k="- a" in LIM_offset, simp)
    1.56 -
    1.57 -lemma LIM_zero:
    1.58 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.59 -  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
    1.60 -unfolding tendsto_iff dist_norm by simp
    1.61 -
    1.62 -lemma LIM_zero_cancel:
    1.63 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.64 -  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
    1.65 -unfolding tendsto_iff dist_norm by simp
    1.66 -
    1.67 -lemma LIM_zero_iff:
    1.68 -  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
    1.69 -  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
    1.70 -unfolding tendsto_iff dist_norm by simp
    1.71 -
    1.72 -lemma LIM_imp_LIM:
    1.73 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    1.74 -  fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
    1.75 -  assumes f: "f -- a --> l"
    1.76 -  assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
    1.77 -  shows "g -- a --> m"
    1.78 -  by (rule metric_LIM_imp_LIM [OF f],
    1.79 -    simp add: dist_norm le)
    1.80 -
    1.81 -lemma LIM_equal2:
    1.82 -  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    1.83 -  assumes 1: "0 < R"
    1.84 -  assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
    1.85 -  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    1.86 -by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
    1.87 -
    1.88 -lemma LIM_compose2:
    1.89 -  fixes a :: "'a::real_normed_vector"
    1.90 -  assumes f: "f -- a --> b"
    1.91 -  assumes g: "g -- b --> c"
    1.92 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
    1.93 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    1.94 -by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
    1.95 -
    1.96 -lemma real_LIM_sandwich_zero:
    1.97 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
    1.98 -  assumes f: "f -- a --> 0"
    1.99 -  assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   1.100 -  assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
   1.101 -  shows "g -- a --> 0"
   1.102 -proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
   1.103 -  fix x assume x: "x \<noteq> a"
   1.104 -  have "norm (g x - 0) = g x" by (simp add: 1 x)
   1.105 -  also have "g x \<le> f x" by (rule 2 [OF x])
   1.106 -  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
   1.107 -  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
   1.108 -  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
   1.109 -qed
   1.110 -
   1.111 -
   1.112 -subsection {* Continuity *}
   1.113 -
   1.114 -lemma LIM_isCont_iff:
   1.115 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   1.116 -  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
   1.117 -by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   1.118 -
   1.119 -lemma isCont_iff:
   1.120 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   1.121 -  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   1.122 -by (simp add: isCont_def LIM_isCont_iff)
   1.123 -
   1.124 -lemma isCont_LIM_compose2:
   1.125 -  fixes a :: "'a::real_normed_vector"
   1.126 -  assumes f [unfolded isCont_def]: "isCont f a"
   1.127 -  assumes g: "g -- f a --> l"
   1.128 -  assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   1.129 -  shows "(\<lambda>x. g (f x)) -- a --> l"
   1.130 -by (rule LIM_compose2 [OF f g inj])
   1.131 -
   1.132 -
   1.133 -lemma isCont_norm [simp]:
   1.134 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.135 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
   1.136 -  by (fact continuous_norm)
   1.137 -
   1.138 -lemma isCont_rabs [simp]:
   1.139 -  fixes f :: "'a::t2_space \<Rightarrow> real"
   1.140 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
   1.141 -  by (fact continuous_rabs)
   1.142 -
   1.143 -lemma isCont_add [simp]:
   1.144 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.145 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
   1.146 -  by (fact continuous_add)
   1.147 -
   1.148 -lemma isCont_minus [simp]:
   1.149 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.150 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
   1.151 -  by (fact continuous_minus)
   1.152 -
   1.153 -lemma isCont_diff [simp]:
   1.154 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
   1.155 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
   1.156 -  by (fact continuous_diff)
   1.157 -
   1.158 -lemma isCont_mult [simp]:
   1.159 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
   1.160 -  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
   1.161 -  by (fact continuous_mult)
   1.162 -
   1.163 -lemma (in bounded_linear) isCont:
   1.164 -  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
   1.165 -  by (fact continuous)
   1.166 -
   1.167 -lemma (in bounded_bilinear) isCont:
   1.168 -  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   1.169 -  by (fact continuous)
   1.170 -
   1.171 -lemmas isCont_scaleR [simp] = 
   1.172 -  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   1.173 -
   1.174 -lemmas isCont_of_real [simp] =
   1.175 -  bounded_linear.isCont [OF bounded_linear_of_real]
   1.176 -
   1.177 -lemma isCont_power [simp]:
   1.178 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
   1.179 -  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   1.180 -  by (fact continuous_power)
   1.181 -
   1.182 -lemma isCont_setsum [simp]:
   1.183 -  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
   1.184 -  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   1.185 -  by (auto intro: continuous_setsum)
   1.186 -
   1.187 -lemmas isCont_intros =
   1.188 -  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   1.189 -  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   1.190 -  isCont_of_real isCont_power isCont_sgn isCont_setsum
   1.191 -
   1.192 -subsection {* Uniform Continuity *}
   1.193 -
   1.194 -lemma (in bounded_linear) isUCont: "isUCont f"
   1.195 -unfolding isUCont_def dist_norm
   1.196 -proof (intro allI impI)
   1.197 -  fix r::real assume r: "0 < r"
   1.198 -  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
   1.199 -    using pos_bounded by fast
   1.200 -  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
   1.201 -  proof (rule exI, safe)
   1.202 -    from r K show "0 < r / K" by (rule divide_pos_pos)
   1.203 -  next
   1.204 -    fix x y :: 'a
   1.205 -    assume xy: "norm (x - y) < r / K"
   1.206 -    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
   1.207 -    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
   1.208 -    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
   1.209 -    finally show "norm (f x - f y) < r" .
   1.210 -  qed
   1.211 -qed
   1.212 -
   1.213 -lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   1.214 -by (rule isUCont [THEN isUCont_Cauchy])
   1.215 -
   1.216 -
   1.217 -lemma LIM_less_bound: 
   1.218 -  fixes f :: "real \<Rightarrow> real"
   1.219 -  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   1.220 -  shows "0 \<le> f x"
   1.221 -proof (rule tendsto_le_const)
   1.222 -  show "(f ---> f x) (at_left x)"
   1.223 -    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
   1.224 -  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
   1.225 -    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
   1.226 -qed simp
   1.227 -
   1.228 -end