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.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.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.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.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
```