src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51641 cd05e9fcc63d
parent 51530 609914f0934a
child 51773 9328c6681f3c
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 08 21:01:59 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 09 14:04:41 2013 +0200
     1.3 @@ -39,9 +39,6 @@
     1.4    shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
     1.5    by (fact tendsto_within_open)
     1.6  
     1.7 -lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
     1.8 -  by (fact tendsto_within_subset)
     1.9 -
    1.10  lemma continuous_on_union:
    1.11    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    1.12    by (fact continuous_on_closed_Un)
    1.13 @@ -1205,7 +1202,7 @@
    1.14  definition
    1.15    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
    1.16      (infixr "indirection" 70) where
    1.17 -  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    1.18 +  "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    1.19  
    1.20  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
    1.21  
    1.22 @@ -1215,7 +1212,7 @@
    1.23    assume "trivial_limit (at a within S)"
    1.24    thus "\<not> a islimpt S"
    1.25      unfolding trivial_limit_def
    1.26 -    unfolding eventually_within eventually_at_topological
    1.27 +    unfolding eventually_at_topological
    1.28      unfolding islimpt_def
    1.29      apply (clarsimp simp add: set_eq_iff)
    1.30      apply (rename_tac T, rule_tac x=T in exI)
    1.31 @@ -1225,7 +1222,7 @@
    1.32    assume "\<not> a islimpt S"
    1.33    thus "trivial_limit (at a within S)"
    1.34      unfolding trivial_limit_def
    1.35 -    unfolding eventually_within eventually_at_topological
    1.36 +    unfolding eventually_at_topological
    1.37      unfolding islimpt_def
    1.38      apply clarsimp
    1.39      apply (rule_tac x=T in exI)
    1.40 @@ -1292,11 +1289,11 @@
    1.41  
    1.42  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
    1.43             (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a  \<and> dist x a  <= d \<longrightarrow> dist (f x) l < e)"
    1.44 -  by (auto simp add: tendsto_iff eventually_within_le)
    1.45 +  by (auto simp add: tendsto_iff eventually_at_le dist_nz)
    1.46  
    1.47  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
    1.48          (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    1.49 -  by (auto simp add: tendsto_iff eventually_within_less)
    1.50 +  by (auto simp add: tendsto_iff eventually_at dist_nz)
    1.51  
    1.52  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
    1.53          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    1.54 @@ -1311,12 +1308,12 @@
    1.55  
    1.56  text{* The expected monotonicity property. *}
    1.57  
    1.58 -lemma Lim_within_empty: "(f ---> l) (net within {})"
    1.59 -  unfolding tendsto_def Limits.eventually_within by simp
    1.60 -
    1.61 -lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
    1.62 -  shows "(f ---> l) (net within (S \<union> T))"
    1.63 -  using assms unfolding tendsto_def Limits.eventually_within
    1.64 +lemma Lim_within_empty: "(f ---> l) (at x within {})"
    1.65 +  unfolding tendsto_def eventually_at_filter by simp
    1.66 +
    1.67 +lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
    1.68 +  shows "(f ---> l) (at x within (S \<union> T))"
    1.69 +  using assms unfolding tendsto_def eventually_at_filter
    1.70    apply clarify
    1.71    apply (drule spec, drule (1) mp, drule (1) mp)
    1.72    apply (drule spec, drule (1) mp, drule (1) mp)
    1.73 @@ -1324,17 +1321,16 @@
    1.74    done
    1.75  
    1.76  lemma Lim_Un_univ:
    1.77 - "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow>  S \<union> T = UNIV
    1.78 -        ==> (f ---> l) net"
    1.79 -  by (metis Lim_Un within_UNIV)
    1.80 + "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
    1.81 +        ==> (f ---> l) (at x)"
    1.82 +  by (metis Lim_Un)
    1.83  
    1.84  text{* Interrelations between restricted and unrestricted limits. *}
    1.85  
    1.86 -lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
    1.87 -  (* FIXME: rename *)
    1.88 -  unfolding tendsto_def Limits.eventually_within
    1.89 -  apply (clarify, drule spec, drule (1) mp, drule (1) mp)
    1.90 -  by (auto elim!: eventually_elim1)
    1.91 +
    1.92 +lemma Lim_at_within: (* FIXME: rename *)
    1.93 +  "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
    1.94 +  by (metis order_refl filterlim_mono subset_UNIV at_le)
    1.95  
    1.96  lemma eventually_within_interior:
    1.97    assumes "x \<in> interior S"
    1.98 @@ -1343,7 +1339,7 @@
    1.99    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   1.100    { assume "?lhs"
   1.101      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   1.102 -      unfolding Limits.eventually_within eventually_at_topological
   1.103 +      unfolding eventually_at_topological
   1.104        by auto
   1.105      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
   1.106        by auto
   1.107 @@ -1351,15 +1347,14 @@
   1.108        unfolding eventually_at_topological by auto
   1.109    } moreover
   1.110    { assume "?rhs" hence "?lhs"
   1.111 -      unfolding Limits.eventually_within
   1.112 -      by (auto elim: eventually_elim1)
   1.113 +      by (auto elim: eventually_elim1 simp: eventually_at_filter)
   1.114    } ultimately
   1.115    show "?thesis" ..
   1.116  qed
   1.117  
   1.118  lemma at_within_interior:
   1.119    "x \<in> interior S \<Longrightarrow> at x within S = at x"
   1.120 -  by (simp add: filter_eq_iff eventually_within_interior)
   1.121 +  unfolding filter_eq_iff by (intro allI eventually_within_interior)
   1.122  
   1.123  lemma Lim_within_LIMSEQ:
   1.124    fixes a :: "'a::metric_space"
   1.125 @@ -1386,17 +1381,14 @@
   1.126          by (auto intro: cInf_lower)
   1.127        with a have "a < f y" by (blast intro: less_le_trans) }
   1.128      then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
   1.129 -      by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
   1.130 +      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
   1.131    next
   1.132      fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
   1.133      from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
   1.134 -    show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
   1.135 -      unfolding within_within_eq[symmetric]
   1.136 -        Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
   1.137 -    proof (safe intro!: exI[of _ y] y)
   1.138 -      fix z assume "x < z" "z \<in> I" "z < y"
   1.139 -      with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
   1.140 -    qed
   1.141 +    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
   1.142 +      unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
   1.143 +    then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
   1.144 +      unfolding eventually_at_filter by eventually_elim simp
   1.145    qed
   1.146  qed
   1.147  
   1.148 @@ -1540,7 +1532,7 @@
   1.149  text{* These are special for limits out of the same vector space. *}
   1.150  
   1.151  lemma Lim_within_id: "(id ---> a) (at a within s)"
   1.152 -  unfolding id_def by (rule tendsto_ident_at_within)
   1.153 +  unfolding id_def by (rule tendsto_ident_at)
   1.154  
   1.155  lemma Lim_at_id: "(id ---> a) (at a)"
   1.156    unfolding id_def by (rule tendsto_ident_at)
   1.157 @@ -1567,13 +1559,13 @@
   1.158  
   1.159  lemma lim_within_interior:
   1.160    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   1.161 -  by (simp add: at_within_interior)
   1.162 +  by (metis at_within_interior)
   1.163  
   1.164  lemma netlimit_within_interior:
   1.165    fixes x :: "'a::{t2_space,perfect_space}"
   1.166    assumes "x \<in> interior S"
   1.167    shows "netlimit (at x within S) = x"
   1.168 -using assms by (simp add: at_within_interior netlimit_at)
   1.169 +using assms by (metis at_within_interior netlimit_at)
   1.170  
   1.171  text{* Transformation of limit. *}
   1.172  
   1.173 @@ -1596,8 +1588,7 @@
   1.174    shows "(g ---> l) (at x within S)"
   1.175  proof (rule Lim_transform_eventually)
   1.176    show "eventually (\<lambda>x. f x = g x) (at x within S)"
   1.177 -    unfolding eventually_within_less
   1.178 -    using assms(1,2) by auto
   1.179 +    using assms(1,2) by (auto simp: dist_nz eventually_at)
   1.180    show "(f ---> l) (at x within S)" by fact
   1.181  qed
   1.182  
   1.183 @@ -1622,7 +1613,7 @@
   1.184  proof (rule Lim_transform_eventually)
   1.185    show "(f ---> l) (at a within S)" by fact
   1.186    show "eventually (\<lambda>x. f x = g x) (at a within S)"
   1.187 -    unfolding Limits.eventually_within eventually_at_topological
   1.188 +    unfolding eventually_at_topological
   1.189      by (rule exI [where x="- {b}"], simp add: open_Compl assms)
   1.190  qed
   1.191  
   1.192 @@ -1655,7 +1646,7 @@
   1.193    assumes "a = b" "x = y" "S = T"
   1.194    assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
   1.195    shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
   1.196 -  unfolding tendsto_def Limits.eventually_within eventually_at_topological
   1.197 +  unfolding tendsto_def eventually_at_topological
   1.198    using assms by simp
   1.199  
   1.200  lemma Lim_cong_at(*[cong add]*):
   1.201 @@ -3759,7 +3750,7 @@
   1.202  lemma continuous_within_subset:
   1.203   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
   1.204               ==> continuous (at x within t) f"
   1.205 -  unfolding continuous_within by(metis Lim_within_subset)
   1.206 +  unfolding continuous_within by(metis tendsto_within_subset)
   1.207  
   1.208  lemma continuous_on_interior:
   1.209    shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
   1.210 @@ -3768,7 +3759,7 @@
   1.211  
   1.212  lemma continuous_on_eq:
   1.213    "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
   1.214 -  unfolding continuous_on_def tendsto_def Limits.eventually_within
   1.215 +  unfolding continuous_on_def tendsto_def eventually_at_topological
   1.216    by simp
   1.217  
   1.218  text {* Characterization of various kinds of continuity in terms of sequences. *}
   1.219 @@ -3783,7 +3774,7 @@
   1.220    { fix x::"nat \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
   1.221      fix T::"'b set" assume "open T" and "f a \<in> T"
   1.222      with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
   1.223 -      unfolding continuous_within tendsto_def eventually_within_less by auto
   1.224 +      unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
   1.225      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
   1.226        using x(2) `d>0` by simp
   1.227      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
   1.228 @@ -4015,7 +4006,7 @@
   1.229  
   1.230  lemma continuous_at_open:
   1.231    shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
   1.232 -unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
   1.233 +unfolding continuous_within_topological [of x UNIV f]
   1.234  unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
   1.235  
   1.236  lemma continuous_imp_tendsto:
   1.237 @@ -4181,7 +4172,7 @@
   1.238    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
   1.239      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
   1.240    thus ?thesis
   1.241 -    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
   1.242 +    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_at)
   1.243  qed
   1.244  
   1.245  lemma continuous_at_avoid:
   1.246 @@ -4514,7 +4505,7 @@
   1.247  proof (rule continuous_attains_sup [OF assms])
   1.248    { fix x assume "x\<in>s"
   1.249      have "(dist a ---> dist a x) (at x within s)"
   1.250 -      by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
   1.251 +      by (intro tendsto_dist tendsto_const tendsto_ident_at)
   1.252    }
   1.253    thus "continuous_on s (dist a)"
   1.254      unfolding continuous_on ..
   1.255 @@ -5350,7 +5341,7 @@
   1.256    assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
   1.257  proof -
   1.258    from assms(1) have "continuous_on UNIV f"
   1.259 -    unfolding isCont_def continuous_on_def within_UNIV by simp
   1.260 +    unfolding isCont_def continuous_on_def by simp
   1.261    hence "open {x \<in> UNIV. f x \<in> s}"
   1.262      using open_UNIV `open s` by (rule continuous_open_preimage)
   1.263    thus "open (f -` s)"
   1.264 @@ -5508,14 +5499,13 @@
   1.265  text{* Limits relative to a union.                                               *}
   1.266  
   1.267  lemma eventually_within_Un:
   1.268 -  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
   1.269 -    eventually P (net within s) \<and> eventually P (net within t)"
   1.270 -  unfolding Limits.eventually_within
   1.271 +  "eventually P (at x within (s \<union> t)) \<longleftrightarrow> eventually P (at x within s) \<and> eventually P (at x within t)"
   1.272 +  unfolding eventually_at_filter
   1.273    by (auto elim!: eventually_rev_mp)
   1.274  
   1.275  lemma Lim_within_union:
   1.276 - "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
   1.277 -  (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
   1.278 + "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
   1.279 +  (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
   1.280    unfolding tendsto_def
   1.281    by (auto simp add: eventually_within_Un)
   1.282