src/HOL/Lim.thy
 changeset 31349 2261c8781f73 parent 31338 d41a8ba25b67 child 31353 14a58e2ca374
```     1.1 --- a/src/HOL/Lim.thy	Sun May 31 11:27:19 2009 -0700
1.2 +++ b/src/HOL/Lim.thy	Sun May 31 21:59:33 2009 -0700
1.3 @@ -13,6 +13,10 @@
1.4  text{*Standard Definitions*}
1.5
1.6  definition
1.7 +  at :: "'a::metric_space \<Rightarrow> 'a filter" where
1.8 +  "at a = Abs_filter (\<lambda>P. \<exists>r>0. \<forall>x. x \<noteq> a \<and> dist x a < r \<longrightarrow> P x)"
1.9 +
1.10 +definition
1.11    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
1.12          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
1.13    [code del]: "f -- a --> L =
1.14 @@ -27,6 +31,20 @@
1.15    isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
1.16    [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
1.17
1.18 +subsection {* Neighborhood Filter *}
1.19 +
1.20 +lemma eventually_at:
1.21 +  "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
1.22 +unfolding at_def
1.23 +apply (rule eventually_Abs_filter)
1.24 +apply (rule_tac x=1 in exI, simp)
1.25 +apply (clarify, rule_tac x=r in exI, simp)
1.26 +apply (clarify, rename_tac r s)
1.27 +apply (rule_tac x="min r s" in exI, simp)
1.28 +done
1.29 +
1.30 +lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> tendsto f L (at a)"
1.31 +unfolding LIM_def tendsto_def eventually_at ..
1.32
1.33  subsection {* Limits of Functions *}
1.34
1.35 @@ -86,33 +104,7 @@
1.36    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.37    assumes f: "f -- a --> L" and g: "g -- a --> M"
1.38    shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
1.39 -proof (rule metric_LIM_I)
1.40 -  fix r :: real
1.41 -  assume r: "0 < r"
1.42 -  from metric_LIM_D [OF f half_gt_zero [OF r]]
1.43 -  obtain fs
1.44 -    where fs:    "0 < fs"
1.45 -      and fs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < fs \<longrightarrow> dist (f x) L < r/2"
1.46 -  by blast
1.47 -  from metric_LIM_D [OF g half_gt_zero [OF r]]
1.48 -  obtain gs
1.49 -    where gs:    "0 < gs"
1.50 -      and gs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < gs \<longrightarrow> dist (g x) M < r/2"
1.51 -  by blast
1.52 -  show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x + g x) (L + M) < r"
1.53 -  proof (intro exI conjI strip)
1.54 -    show "0 < min fs gs"  by (simp add: fs gs)
1.55 -    fix x :: 'a
1.56 -    assume "x \<noteq> a \<and> dist x a < min fs gs"
1.57 -    hence "x \<noteq> a \<and> dist x a < fs \<and> dist x a < gs" by simp
1.58 -    with fs_lt gs_lt
1.59 -    have "dist (f x) L < r/2" and "dist (g x) M < r/2" by blast+
1.60 -    hence "dist (f x) L + dist (g x) M < r" by arith
1.61 -    thus "dist (f x + g x) (L + M) < r"
1.62 -      unfolding dist_norm
1.63 -      by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
1.64 -  qed
1.65 -qed
1.66 +using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
1.67
1.69    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.70 @@ -127,7 +119,7 @@
1.71  lemma LIM_minus:
1.72    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.73    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
1.74 -by (simp only: LIM_def dist_norm minus_diff_minus norm_minus_cancel)
1.75 +unfolding LIM_conv_tendsto by (rule tendsto_minus)
1.76
1.77  (* TODO: delete *)
1.79 @@ -138,7 +130,7 @@
1.80  lemma LIM_diff:
1.81    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.82    shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
1.83 -by (simp only: diff_minus LIM_add LIM_minus)
1.84 +unfolding LIM_conv_tendsto by (rule tendsto_diff)
1.85
1.86  lemma LIM_zero:
1.87    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.88 @@ -178,7 +170,7 @@
1.89  lemma LIM_norm:
1.90    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.91    shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
1.92 -by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3)
1.93 +unfolding LIM_conv_tendsto by (rule tendsto_norm)
1.94
1.95  lemma LIM_norm_zero:
1.96    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.97 @@ -369,26 +361,12 @@
1.98
1.99  text {* Bounded Linear Operators *}
1.100
1.101 -lemma (in bounded_linear) cont: "f -- a --> f a"
1.102 -proof (rule LIM_I)
1.103 -  fix r::real assume r: "0 < r"
1.104 -  obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
1.105 -    using pos_bounded by fast
1.106 -  show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - f a) < r"
1.107 -  proof (rule exI, safe)
1.108 -    from r K show "0 < r / K" by (rule divide_pos_pos)
1.109 -  next
1.110 -    fix x assume x: "norm (x - a) < r / K"
1.111 -    have "norm (f x - f a) = norm (f (x - a))" by (simp only: diff)
1.112 -    also have "\<dots> \<le> norm (x - a) * K" by (rule norm_le)
1.113 -    also from K x have "\<dots> < r" by (simp only: pos_less_divide_eq)
1.114 -    finally show "norm (f x - f a) < r" .
1.115 -  qed
1.116 -qed
1.117 -
1.118  lemma (in bounded_linear) LIM:
1.119    "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
1.120 -by (rule LIM_compose [OF cont])
1.121 +unfolding LIM_conv_tendsto by (rule tendsto)
1.122 +
1.123 +lemma (in bounded_linear) cont: "f -- a --> f a"
1.124 +by (rule LIM [OF LIM_ident])
1.125
1.126  lemma (in bounded_linear) LIM_zero:
1.127    "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
1.128 @@ -396,40 +374,16 @@
1.129
1.130  text {* Bounded Bilinear Operators *}
1.131
1.132 +lemma (in bounded_bilinear) LIM:
1.133 +  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
1.134 +unfolding LIM_conv_tendsto by (rule tendsto)
1.135 +
1.136  lemma (in bounded_bilinear) LIM_prod_zero:
1.137    fixes a :: "'d::metric_space"
1.138    assumes f: "f -- a --> 0"
1.139    assumes g: "g -- a --> 0"
1.140    shows "(\<lambda>x. f x ** g x) -- a --> 0"
1.141 -proof (rule metric_LIM_I, unfold dist_norm)
1.142 -  fix r::real assume r: "0 < r"
1.143 -  obtain K where K: "0 < K"
1.144 -    and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
1.145 -    using pos_bounded by fast
1.146 -  from K have K': "0 < inverse K"
1.147 -    by (rule positive_imp_inverse_positive)
1.148 -  obtain s where s: "0 < s"
1.149 -    and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
1.150 -    using metric_LIM_D [OF f r, unfolded dist_norm] by auto
1.151 -  obtain t where t: "0 < t"
1.152 -    and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
1.153 -    using metric_LIM_D [OF g K', unfolded dist_norm] by auto
1.154 -  show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> norm (f x ** g x - 0) < r"
1.155 -  proof (rule exI, safe)
1.156 -    from s t show "0 < min s t" by simp
1.157 -  next
1.158 -    fix x assume x: "x \<noteq> a"
1.159 -    assume "dist x a < min s t"
1.160 -    hence xs: "dist x a < s" and xt: "dist x a < t" by simp_all
1.161 -    from x xs have 1: "norm (f x) < r" by (rule norm_f)
1.162 -    from x xt have 2: "norm (g x) < inverse K" by (rule norm_g)
1.163 -    have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le)
1.164 -    also from 1 2 K have "\<dots> < r * inverse K * K"
1.165 -      by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero)
1.166 -    also from K have "r * inverse K * K = r" by simp
1.167 -    finally show "norm (f x ** g x - 0) < r" by simp
1.168 -  qed
1.169 -qed
1.170 +using LIM [OF f g] by (simp add: zero_left)
1.171
1.172  lemma (in bounded_bilinear) LIM_left_zero:
1.173    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. f x ** c) -- a --> 0"
1.174 @@ -439,19 +393,6 @@
1.175    "f -- a --> 0 \<Longrightarrow> (\<lambda>x. c ** f x) -- a --> 0"
1.176  by (rule bounded_linear.LIM_zero [OF bounded_linear_right])
1.177
1.178 -lemma (in bounded_bilinear) LIM:
1.179 -  "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
1.180 -apply (drule LIM_zero)
1.181 -apply (drule LIM_zero)
1.182 -apply (rule LIM_zero_cancel)
1.183 -apply (subst prod_diff_prod)
1.184 -apply (rule LIM_add_zero)
1.185 -apply (rule LIM_add_zero)
1.186 -apply (erule (1) LIM_prod_zero)
1.187 -apply (erule LIM_left_zero)
1.188 -apply (erule LIM_right_zero)
1.189 -done
1.190 -
1.191  lemmas LIM_mult = mult.LIM
1.192
1.193  lemmas LIM_mult_zero = mult.LIM_prod_zero
```