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.68  lemma LIM_add_zero:
    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.78  lemma LIM_add_minus:
    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