src/HOL/Limits.thy
changeset 60141 833adf7db7d8
parent 60017 b785d6d06430
child 60182 e1ea5a6379c9
     1.1 --- a/src/HOL/Limits.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/Limits.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -396,7 +396,7 @@
     1.4  lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\<lambda>x. f x - a) F"
     1.5    by (simp only: tendsto_iff Zfun_def dist_norm)
     1.6  
     1.7 -lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk> 
     1.8 +lemma tendsto_0_le: "\<lbrakk>(f ---> 0) F; eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) F\<rbrakk>
     1.9                       \<Longrightarrow> (g ---> 0) F"
    1.10    by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff)
    1.11  
    1.12 @@ -1134,7 +1134,7 @@
    1.13  
    1.14  *}
    1.15  
    1.16 -lemma filterlim_tendsto_pos_mult_at_top: 
    1.17 +lemma filterlim_tendsto_pos_mult_at_top:
    1.18    assumes f: "(f ---> c) F" and c: "0 < c"
    1.19    assumes g: "LIM x F. g x :> at_top"
    1.20    shows "LIM x F. (f x * g x :: real) :> at_top"
    1.21 @@ -1156,7 +1156,7 @@
    1.22    qed
    1.23  qed
    1.24  
    1.25 -lemma filterlim_at_top_mult_at_top: 
    1.26 +lemma filterlim_at_top_mult_at_top:
    1.27    assumes f: "LIM x F. f x :> at_top"
    1.28    assumes g: "LIM x F. g x :> at_top"
    1.29    shows "LIM x F. (f x * g x :: real) :> at_top"
    1.30 @@ -1202,7 +1202,7 @@
    1.31    shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> odd n \<Longrightarrow> LIM x F. (f x)^n :> at_bot"
    1.32    using filterlim_pow_at_top[of n "\<lambda>x. - f x" F] by (simp add: filterlim_uminus_at_bot)
    1.33  
    1.34 -lemma filterlim_tendsto_add_at_top: 
    1.35 +lemma filterlim_tendsto_add_at_top:
    1.36    assumes f: "(f ---> c) F"
    1.37    assumes g: "LIM x F. g x :> at_top"
    1.38    shows "LIM x F. (f x + g x :: real) :> at_top"
    1.39 @@ -1225,7 +1225,7 @@
    1.40    unfolding divide_inverse
    1.41    by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g])
    1.42  
    1.43 -lemma filterlim_at_top_add_at_top: 
    1.44 +lemma filterlim_at_top_add_at_top:
    1.45    assumes f: "LIM x F. f x :> at_top"
    1.46    assumes g: "LIM x F. g x :> at_top"
    1.47    shows "LIM x F. (f x + g x :: real) :> at_top"
    1.48 @@ -1315,16 +1315,108 @@
    1.49    shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
    1.50    by (rule Bfun_inverse)
    1.51  
    1.52 -lemma LIMSEQ_diff_approach_zero:
    1.53 -  fixes L :: "'a::real_normed_vector"
    1.54 -  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
    1.55 -  by (drule (1) tendsto_add, simp)
    1.56 +text{* Transformation of limit. *}
    1.57 +
    1.58 +lemma eventually_at2:
    1.59 +  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    1.60 +  unfolding eventually_at dist_nz by auto
    1.61 +
    1.62 +lemma Lim_transform:
    1.63 +  fixes a b :: "'a::real_normed_vector"
    1.64 +  shows "\<lbrakk>(g ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (f ---> a) F"
    1.65 +  using tendsto_add [of g a F "\<lambda>x. f x - g x" 0] by simp
    1.66 +
    1.67 +lemma Lim_transform2:
    1.68 +  fixes a b :: "'a::real_normed_vector"
    1.69 +  shows "\<lbrakk>(f ---> a) F; ((\<lambda>x. f x - g x) ---> 0) F\<rbrakk> \<Longrightarrow> (g ---> a) F"
    1.70 +  by (erule Lim_transform) (simp add: tendsto_minus_cancel)
    1.71 +
    1.72 +lemma Lim_transform_eventually:
    1.73 +  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
    1.74 +  apply (rule topological_tendstoI)
    1.75 +  apply (drule (2) topological_tendstoD)
    1.76 +  apply (erule (1) eventually_elim2, simp)
    1.77 +  done
    1.78 +
    1.79 +lemma Lim_transform_within:
    1.80 +  assumes "0 < d"
    1.81 +    and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    1.82 +    and "(f ---> l) (at x within S)"
    1.83 +  shows "(g ---> l) (at x within S)"
    1.84 +proof (rule Lim_transform_eventually)
    1.85 +  show "eventually (\<lambda>x. f x = g x) (at x within S)"
    1.86 +    using assms(1,2) by (auto simp: dist_nz eventually_at)
    1.87 +  show "(f ---> l) (at x within S)" by fact
    1.88 +qed
    1.89 +
    1.90 +lemma Lim_transform_at:
    1.91 +  assumes "0 < d"
    1.92 +    and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    1.93 +    and "(f ---> l) (at x)"
    1.94 +  shows "(g ---> l) (at x)"
    1.95 +  using _ assms(3)
    1.96 +proof (rule Lim_transform_eventually)
    1.97 +  show "eventually (\<lambda>x. f x = g x) (at x)"
    1.98 +    unfolding eventually_at2
    1.99 +    using assms(1,2) by auto
   1.100 +qed
   1.101 +
   1.102 +text{* Common case assuming being away from some crucial point like 0. *}
   1.103  
   1.104 -lemma LIMSEQ_diff_approach_zero2:
   1.105 -  fixes L :: "'a::real_normed_vector"
   1.106 -  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
   1.107 -  by (drule (1) tendsto_diff, simp)
   1.108 +lemma Lim_transform_away_within:
   1.109 +  fixes a b :: "'a::t1_space"
   1.110 +  assumes "a \<noteq> b"
   1.111 +    and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.112 +    and "(f ---> l) (at a within S)"
   1.113 +  shows "(g ---> l) (at a within S)"
   1.114 +proof (rule Lim_transform_eventually)
   1.115 +  show "(f ---> l) (at a within S)" by fact
   1.116 +  show "eventually (\<lambda>x. f x = g x) (at a within S)"
   1.117 +    unfolding eventually_at_topological
   1.118 +    by (rule exI [where x="- {b}"], simp add: open_Compl assms)
   1.119 +qed
   1.120 +
   1.121 +lemma Lim_transform_away_at:
   1.122 +  fixes a b :: "'a::t1_space"
   1.123 +  assumes ab: "a\<noteq>b"
   1.124 +    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.125 +    and fl: "(f ---> l) (at a)"
   1.126 +  shows "(g ---> l) (at a)"
   1.127 +  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
   1.128 +
   1.129 +text{* Alternatively, within an open set. *}
   1.130  
   1.131 +lemma Lim_transform_within_open:
   1.132 +  assumes "open S" and "a \<in> S"
   1.133 +    and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
   1.134 +    and "(f ---> l) (at a)"
   1.135 +  shows "(g ---> l) (at a)"
   1.136 +proof (rule Lim_transform_eventually)
   1.137 +  show "eventually (\<lambda>x. f x = g x) (at a)"
   1.138 +    unfolding eventually_at_topological
   1.139 +    using assms(1,2,3) by auto
   1.140 +  show "(f ---> l) (at a)" by fact
   1.141 +qed
   1.142 +
   1.143 +text{* A congruence rule allowing us to transform limits assuming not at point. *}
   1.144 +
   1.145 +(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   1.146 +
   1.147 +lemma Lim_cong_within(*[cong add]*):
   1.148 +  assumes "a = b"
   1.149 +    and "x = y"
   1.150 +    and "S = T"
   1.151 +    and "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
   1.152 +  shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
   1.153 +  unfolding tendsto_def eventually_at_topological
   1.154 +  using assms by simp
   1.155 +
   1.156 +lemma Lim_cong_at(*[cong add]*):
   1.157 +  assumes "a = b" "x = y"
   1.158 +    and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
   1.159 +  shows "((\<lambda>x. f x) ---> x) (at a) \<longleftrightarrow> ((g ---> y) (at a))"
   1.160 +  unfolding tendsto_def eventually_at_topological
   1.161 +  using assms by simp
   1.162  text{*An unbounded sequence's inverse tends to 0*}
   1.163  
   1.164  lemma LIMSEQ_inverse_zero:
   1.165 @@ -1684,7 +1776,7 @@
   1.166    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
   1.167    by (fact continuous)
   1.168  
   1.169 -lemmas isCont_scaleR [simp] = 
   1.170 +lemmas isCont_scaleR [simp] =
   1.171    bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
   1.172  
   1.173  lemmas isCont_of_real [simp] =
   1.174 @@ -1740,7 +1832,7 @@
   1.175  lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
   1.176  by (rule isUCont [THEN isUCont_Cauchy])
   1.177  
   1.178 -lemma LIM_less_bound: 
   1.179 +lemma LIM_less_bound:
   1.180    fixes f :: "real \<Rightarrow> real"
   1.181    assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   1.182    shows "0 \<le> f x"
   1.183 @@ -1804,7 +1896,7 @@
   1.184  
   1.185    show "P a b"
   1.186    proof (rule ccontr)
   1.187 -    assume "\<not> P a b" 
   1.188 +    assume "\<not> P a b"
   1.189      { fix n have "\<not> P (l n) (u n)"
   1.190        proof (induct n)
   1.191          case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
   1.192 @@ -1911,7 +2003,7 @@
   1.193  lemma isCont_Lb_Ub:
   1.194    fixes f :: "real \<Rightarrow> real"
   1.195    assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   1.196 -  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and> 
   1.197 +  shows "\<exists>L M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> L \<le> f x \<and> f x \<le> M) \<and>
   1.198                 (\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> (f x = y)))"
   1.199  proof -
   1.200    obtain M where M: "a \<le> M" "M \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> f M"
   1.201 @@ -1974,8 +2066,8 @@
   1.202  
   1.203  lemma isCont_inv_fun:
   1.204    fixes f g :: "real \<Rightarrow> real"
   1.205 -  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
   1.206 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
   1.207 +  shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
   1.208 +         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
   1.209        ==> isCont g (f x)"
   1.210  by (rule isCont_inverse_function)
   1.211