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