src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 36667 21404f7dec59
parent 36660 1cc4ab4b7ff7
child 36668 941ba2da372e
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 17:37:31 2010 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue May 04 18:55:18 2010 -0700
     1.3 @@ -1200,7 +1200,7 @@
     1.4  text{* Another limit point characterization. *}
     1.5  
     1.6  lemma islimpt_sequential:
     1.7 -  fixes x :: "'a::metric_space" (* FIXME: generalize to topological_space *)
     1.8 +  fixes x :: "'a::metric_space"
     1.9    shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S -{x}) \<and> (f ---> x) sequentially)"
    1.10      (is "?lhs = ?rhs")
    1.11  proof
    1.12 @@ -1537,40 +1537,41 @@
    1.13  qed
    1.14  
    1.15  lemma Lim_transform_eventually:
    1.16 -  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
    1.17 +  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net \<Longrightarrow> (g ---> l) net"
    1.18    apply (rule topological_tendstoI)
    1.19    apply (drule (2) topological_tendstoD)
    1.20    apply (erule (1) eventually_elim2, simp)
    1.21    done
    1.22  
    1.23  lemma Lim_transform_within:
    1.24 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
    1.25 -  assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
    1.26 -          "(f ---> l) (at x within S)"
    1.27 -  shows   "(g ---> l) (at x within S)"
    1.28 -  using assms(1,3) unfolding Lim_within
    1.29 -  apply -
    1.30 -  apply (clarify, rename_tac e)
    1.31 -  apply (drule_tac x=e in spec, clarsimp, rename_tac r)
    1.32 -  apply (rule_tac x="min d r" in exI, clarsimp, rename_tac y)
    1.33 -  apply (drule_tac x=y in bspec, assumption, clarsimp)
    1.34 -  apply (simp add: assms(2))
    1.35 -  done
    1.36 +  assumes "0 < d" and "\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    1.37 +  and "(f ---> l) (at x within S)"
    1.38 +  shows "(g ---> l) (at x within S)"
    1.39 +proof (rule Lim_transform_eventually)
    1.40 +  show "eventually (\<lambda>x. f x = g x) (at x within S)"
    1.41 +    unfolding eventually_within
    1.42 +    using assms(1,2) by auto
    1.43 +  show "(f ---> l) (at x within S)" by fact
    1.44 +qed
    1.45  
    1.46  lemma Lim_transform_at:
    1.47 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
    1.48 -  shows "0 < d \<Longrightarrow> (\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x') \<Longrightarrow>
    1.49 -  (f ---> l) (at x) ==> (g ---> l) (at x)"
    1.50 -  apply (subst within_UNIV[symmetric])
    1.51 -  using Lim_transform_within[of d UNIV x f g l]
    1.52 -  by (auto simp add: within_UNIV)
    1.53 +  assumes "0 < d" and "\<forall>x'. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
    1.54 +  and "(f ---> l) (at x)"
    1.55 +  shows "(g ---> l) (at x)"
    1.56 +proof (rule Lim_transform_eventually)
    1.57 +  show "eventually (\<lambda>x. f x = g x) (at x)"
    1.58 +    unfolding eventually_at
    1.59 +    using assms(1,2) by auto
    1.60 +  show "(f ---> l) (at x)" by fact
    1.61 +qed
    1.62  
    1.63  text{* Common case assuming being away from some crucial point like 0. *}
    1.64  
    1.65 +text {* TODO: generalize the next few lemmas to T1 spaces. *}
    1.66 +
    1.67  lemma Lim_transform_away_within:
    1.68    fixes a b :: "'a::metric_space"
    1.69 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
    1.70 -  assumes "a\<noteq>b" "\<forall>x\<in> S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
    1.71 +  assumes "a \<noteq> b" and "\<forall>x\<in>S. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
    1.72    and "(f ---> l) (at a within S)"
    1.73    shows "(g ---> l) (at a within S)"
    1.74  proof-
    1.75 @@ -1581,7 +1582,6 @@
    1.76  
    1.77  lemma Lim_transform_away_at:
    1.78    fixes a b :: "'a::metric_space"
    1.79 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
    1.80    assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
    1.81    and fl: "(f ---> l) (at a)"
    1.82    shows "(g ---> l) (at a)"
    1.83 @@ -1591,15 +1591,14 @@
    1.84  text{* Alternatively, within an open set. *}
    1.85  
    1.86  lemma Lim_transform_within_open:
    1.87 -  fixes a :: "'a::metric_space"
    1.88 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
    1.89 -  assumes "open S"  "a \<in> S"  "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"  "(f ---> l) (at a)"
    1.90 +  assumes "open S" and "a \<in> S" and "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> f x = g x"
    1.91 +  and "(f ---> l) (at a)"
    1.92    shows "(g ---> l) (at a)"
    1.93 -proof-
    1.94 -  from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
    1.95 -  hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)
    1.96 -    unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute)
    1.97 -  thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto
    1.98 +proof (rule Lim_transform_eventually)
    1.99 +  show "eventually (\<lambda>x. f x = g x) (at a)"
   1.100 +    unfolding eventually_at_topological
   1.101 +    using assms(1,2,3) by auto
   1.102 +  show "(f ---> l) (at a)" by fact
   1.103  qed
   1.104  
   1.105  text{* A congruence rule allowing us to transform limits assuming not at point. *}
   1.106 @@ -1607,21 +1606,21 @@
   1.107  (* FIXME: Only one congruence rule for tendsto can be used at a time! *)
   1.108  
   1.109  lemma Lim_cong_within(*[cong add]*):
   1.110 -  fixes a :: "'a::metric_space"
   1.111 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.112 -  shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
   1.113 -  by (simp add: Lim_within dist_nz[symmetric])
   1.114 -
   1.115 -lemma Lim_cong_at[cong add]:
   1.116 -  fixes a :: "'a::metric_space"
   1.117 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
   1.118 -  shows "(\<And>x. x \<noteq> a ==> f x = g x) ==> (((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a)))"
   1.119 -  by (simp add: Lim_at dist_nz[symmetric])
   1.120 +  assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
   1.121 +  shows "((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
   1.122 +  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   1.123 +  using assms by simp
   1.124 +
   1.125 +lemma Lim_cong_at(*[cong add]*):
   1.126 +  assumes "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
   1.127 +  shows "((\<lambda>x. f x) ---> l) (at a) \<longleftrightarrow> ((g ---> l) (at a))"
   1.128 +  unfolding tendsto_def eventually_at_topological
   1.129 +  using assms by simp
   1.130  
   1.131  text{* Useful lemmas on closure and set of possible sequential limits.*}
   1.132  
   1.133  lemma closure_sequential:
   1.134 -  fixes l :: "'a::metric_space" (* TODO: generalize *)
   1.135 +  fixes l :: "'a::metric_space"
   1.136    shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially)" (is "?lhs = ?rhs")
   1.137  proof
   1.138    assume "?lhs" moreover
   1.139 @@ -2911,7 +2910,7 @@
   1.140  qed
   1.141  
   1.142  lemma closed_sing [simp]:
   1.143 -  fixes a :: "'a::metric_space"
   1.144 +  fixes a :: "'a::metric_space" (* TODO: generalize to t1_space *)
   1.145    shows "closed {a}"
   1.146    apply (clarsimp simp add: closed_def open_dist)
   1.147    apply (rule ccontr)
   1.148 @@ -3252,7 +3251,7 @@
   1.149        by (rule Lim_trivial_limit)
   1.150    next
   1.151      case False
   1.152 -    hence "netlimit (at x) = x"
   1.153 +    hence 1: "netlimit (at x) = x"
   1.154        using netlimit_within [of x UNIV]
   1.155        by (simp add: within_UNIV)
   1.156      with * show ?thesis by simp
   1.157 @@ -3411,38 +3410,28 @@
   1.158  text{* The usual transformation theorems. *}
   1.159  
   1.160  lemma continuous_transform_within:
   1.161 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   1.162 +  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   1.163    assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
   1.164            "continuous (at x within s) f"
   1.165    shows "continuous (at x within s) g"
   1.166 -proof-
   1.167 -  { fix e::real assume "e>0"
   1.168 -    then obtain d' where d':"d'>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(4) unfolding continuous_within Lim_within by auto
   1.169 -    { fix x' assume "x'\<in>s" "0 < dist x' x" "dist x' x < (min d d')"
   1.170 -      hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) using d' by auto  }
   1.171 -    hence "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
   1.172 -    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto  }
   1.173 -  hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
   1.174 -  thus ?thesis unfolding continuous_within using Lim_transform_within[of d s x f g "g x"] using assms by blast
   1.175 +unfolding continuous_within
   1.176 +proof (rule Lim_transform_within)
   1.177 +  show "0 < d" by fact
   1.178 +  show "\<forall>x'\<in>s. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x'"
   1.179 +    using assms(3) by auto
   1.180 +  have "f x = g x"
   1.181 +    using assms(1,2,3) by auto
   1.182 +  thus "(f ---> g x) (at x within s)"
   1.183 +    using assms(4) unfolding continuous_within by simp
   1.184  qed
   1.185  
   1.186  lemma continuous_transform_at:
   1.187 -  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   1.188 +  fixes f g :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   1.189    assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
   1.190            "continuous (at x) f"
   1.191    shows "continuous (at x) g"
   1.192 -proof-
   1.193 -  { fix e::real assume "e>0"
   1.194 -    then obtain d' where d':"d'>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(3) unfolding continuous_at Lim_at by auto
   1.195 -    { fix x' assume "0 < dist x' x" "dist x' x < (min d d')"
   1.196 -      hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) using d' by auto
   1.197 -    }
   1.198 -    hence "\<forall>xa. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
   1.199 -    hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto
   1.200 -  }
   1.201 -  hence "(f ---> g x) (at x)" unfolding Lim_at using assms(1) by auto
   1.202 -  thus ?thesis unfolding continuous_at using Lim_transform_at[of d x f g "g x"] using assms by blast
   1.203 -qed
   1.204 +  using continuous_transform_within [of d x UNIV f g] assms
   1.205 +  by (simp add: within_UNIV)
   1.206  
   1.207  text{* Combination results for pointwise continuity. *}
   1.208