src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 51478 270b21f3ae0a parent 51475 ebf9d4fd00ba child 51479 33db4b7189af
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -1273,18 +1273,6 @@
1.4
1.5  subsection {* Limits *}
1.6
1.7 -text{* Notation Lim to avoid collition with lim defined in analysis *}
1.8 -
1.9 -definition Lim :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b"
1.10 -  where "Lim A f = (THE l. (f ---> l) A)"
1.11 -
1.12 -text{* Uniqueness of the limit, when nontrivial. *}
1.13 -
1.14 -lemma tendsto_Lim:
1.15 -  fixes f :: "'a \<Rightarrow> 'b::t2_space"
1.16 -  shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
1.17 -  unfolding Lim_def using tendsto_unique[of net f] by auto
1.18 -
1.19  lemma Lim:
1.20   "(f ---> l) net \<longleftrightarrow>
1.21          trivial_limit net \<or>
1.22 @@ -3769,35 +3757,6 @@
1.23
1.24  subsection {* Continuity *}
1.25
1.26 -text {* Define continuity over a net to take in restrictions of the set. *}
1.27 -
1.28 -definition
1.29 -  continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
1.30 -  where "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
1.31 -
1.32 -lemma continuous_trivial_limit:
1.33 - "trivial_limit net ==> continuous net f"
1.34 -  unfolding continuous_def tendsto_def trivial_limit_eq by auto
1.35 -
1.36 -lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
1.37 -  unfolding continuous_def
1.38 -  unfolding tendsto_def
1.39 -  using netlimit_within[of x s]
1.40 -  by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
1.41 -
1.42 -lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
1.43 -  using continuous_within [of x UNIV f] by simp
1.44 -
1.45 -lemma continuous_isCont: "isCont f x = continuous (at x) f"
1.46 -  unfolding isCont_def LIM_def
1.47 -  unfolding continuous_at Lim_at unfolding dist_nz by auto
1.48 -
1.49 -lemma continuous_at_within:
1.50 -  assumes "continuous (at x) f"  shows "continuous (at x within s) f"
1.51 -  using assms unfolding continuous_at continuous_within
1.52 -  by (rule Lim_at_within)
1.53 -
1.54 -
1.55  text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
1.56
1.57  lemma continuous_within_eps_delta:
1.58 @@ -3843,20 +3802,6 @@
1.59
1.60  text{* Define setwise continuity in terms of limits within the set. *}
1.61
1.62 -definition
1.63 -  continuous_on ::
1.64 -    "'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
1.65 -where
1.66 -  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
1.67 -
1.68 -lemma continuous_on_topological:
1.69 -  "continuous_on s f \<longleftrightarrow>
1.70 -    (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
1.71 -      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
1.72 -unfolding continuous_on_def tendsto_def
1.73 -unfolding Limits.eventually_within eventually_at_topological
1.74 -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
1.75 -
1.76  lemma continuous_on_iff:
1.77    "continuous_on s f \<longleftrightarrow>
1.78      (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
1.79 @@ -3884,38 +3829,7 @@
1.80    unfolding continuous_within continuous_at using Lim_at_within by auto
1.81
1.82  lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
1.83 -unfolding tendsto_def by (simp add: trivial_limit_eq)
1.84 -
1.85 -lemma continuous_at_imp_continuous_on:
1.86 -  assumes "\<forall>x\<in>s. continuous (at x) f"
1.87 -  shows "continuous_on s f"
1.88 -unfolding continuous_on_def
1.89 -proof
1.90 -  fix x assume "x \<in> s"
1.91 -  with assms have *: "(f ---> f (netlimit (at x))) (at x)"
1.92 -    unfolding continuous_def by simp
1.93 -  have "(f ---> f x) (at x)"
1.94 -  proof (cases "trivial_limit (at x)")
1.95 -    case True thus ?thesis
1.96 -      by (rule Lim_trivial_limit)
1.97 -  next
1.98 -    case False
1.99 -    hence 1: "netlimit (at x) = x"
1.100 -      using netlimit_within [of x UNIV] by simp
1.101 -    with * show ?thesis by simp
1.102 -  qed
1.103 -  thus "(f ---> f x) (at x within s)"
1.104 -    by (rule Lim_at_within)
1.105 -qed
1.106 -
1.107 -lemma continuous_on_eq_continuous_within:
1.108 -  "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
1.109 -unfolding continuous_on_def continuous_def
1.110 -apply (rule ball_cong [OF refl])
1.111 -apply (case_tac "trivial_limit (at x within s)")
1.112 -apply (simp add: Lim_trivial_limit)
1.113 -apply (simp add: netlimit_within)
1.114 -done
1.115 +  by simp
1.116
1.117  lemmas continuous_on = continuous_on_def -- "legacy theorem name"
1.118
1.119 @@ -4056,169 +3970,32 @@
1.120
1.121  subsubsection {* Structural rules for pointwise continuity *}
1.122
1.123 -ML {*
1.124 -
1.125 -structure Continuous_Intros = Named_Thms
1.126 -(
1.127 -  val name = @{binding continuous_intros}
1.128 -  val description = "Structural introduction rules for pointwise continuity"
1.129 -)
1.130 -
1.131 -*}
1.132 -
1.133 -setup Continuous_Intros.setup
1.134 -
1.135 -lemma continuous_within_id[continuous_intros]: "continuous (at a within s) (\<lambda>x. x)"
1.136 -  unfolding continuous_within by (rule tendsto_ident_at_within)
1.137 -
1.138 -lemma continuous_at_id[continuous_intros]: "continuous (at a) (\<lambda>x. x)"
1.139 -  unfolding continuous_at by (rule tendsto_ident_at)
1.140 -
1.141 -lemma continuous_const[continuous_intros]: "continuous F (\<lambda>x. c)"
1.142 -  unfolding continuous_def by (rule tendsto_const)
1.143 -
1.144 -lemma continuous_fst[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
1.145 -  unfolding continuous_def by (rule tendsto_fst)
1.146 -
1.147 -lemma continuous_snd[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
1.148 -  unfolding continuous_def by (rule tendsto_snd)
1.149 -
1.150 -lemma continuous_Pair[continuous_intros]: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
1.151 -  unfolding continuous_def by (rule tendsto_Pair)
1.152 -
1.153 -lemma continuous_dist[continuous_intros]:
1.154 -  assumes "continuous F f" and "continuous F g"
1.155 -  shows "continuous F (\<lambda>x. dist (f x) (g x))"
1.156 -  using assms unfolding continuous_def by (rule tendsto_dist)
1.157 +lemmas continuous_within_id = continuous_ident
1.158 +
1.159 +lemmas continuous_at_id = isCont_ident
1.160
1.161  lemma continuous_infdist[continuous_intros]:
1.162    assumes "continuous F f"
1.163    shows "continuous F (\<lambda>x. infdist (f x) A)"
1.164    using assms unfolding continuous_def by (rule tendsto_infdist)
1.165
1.166 -lemma continuous_norm[continuous_intros]:
1.167 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
1.168 -  unfolding continuous_def by (rule tendsto_norm)
1.169 -
1.170  lemma continuous_infnorm[continuous_intros]:
1.171    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. infnorm (f x))"
1.172    unfolding continuous_def by (rule tendsto_infnorm)
1.173
1.174 -lemma continuous_add[continuous_intros]:
1.175 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.176 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x + g x)"
1.177 -  unfolding continuous_def by (rule tendsto_add)
1.178 -
1.179 -lemma continuous_minus[continuous_intros]:
1.180 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.181 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. - f x)"
1.182 -  unfolding continuous_def by (rule tendsto_minus)
1.183 -
1.184 -lemma continuous_diff[continuous_intros]:
1.185 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.186 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x - g x)"
1.187 -  unfolding continuous_def by (rule tendsto_diff)
1.188 -
1.189 -lemma continuous_scaleR[continuous_intros]:
1.190 -  fixes g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
1.191 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x *\<^sub>R g x)"
1.192 -  unfolding continuous_def by (rule tendsto_scaleR)
1.193 -
1.194 -lemma continuous_mult[continuous_intros]:
1.195 -  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
1.196 -  shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
1.197 -  unfolding continuous_def by (rule tendsto_mult)
1.198 -
1.199  lemma continuous_inner[continuous_intros]:
1.200    assumes "continuous F f" and "continuous F g"
1.201    shows "continuous F (\<lambda>x. inner (f x) (g x))"
1.202    using assms unfolding continuous_def by (rule tendsto_inner)
1.203
1.204 -lemma continuous_inverse[continuous_intros]:
1.205 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.206 -  assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
1.207 -  shows "continuous F (\<lambda>x. inverse (f x))"
1.208 -  using assms unfolding continuous_def by (rule tendsto_inverse)
1.209 -
1.210 -lemma continuous_at_within_inverse[continuous_intros]:
1.211 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.212 -  assumes "continuous (at a within s) f" and "f a \<noteq> 0"
1.213 -  shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
1.214 -  using assms unfolding continuous_within by (rule tendsto_inverse)
1.215 -
1.216 -lemma continuous_at_inverse[continuous_intros]:
1.217 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.218 -  assumes "continuous (at a) f" and "f a \<noteq> 0"
1.219 -  shows "continuous (at a) (\<lambda>x. inverse (f x))"
1.220 -  using assms unfolding continuous_at by (rule tendsto_inverse)
1.221 +lemmas continuous_at_inverse = isCont_inverse
1.222
1.223  subsubsection {* Structural rules for setwise continuity *}
1.224
1.225 -ML {*
1.226 -
1.227 -structure Continuous_On_Intros = Named_Thms
1.228 -(
1.229 -  val name = @{binding continuous_on_intros}
1.230 -  val description = "Structural introduction rules for setwise continuity"
1.231 -)
1.232 -
1.233 -*}
1.234 -
1.235 -setup Continuous_On_Intros.setup
1.236 -
1.237 -lemma continuous_on_id[continuous_on_intros]: "continuous_on s (\<lambda>x. x)"
1.238 -  unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
1.239 -
1.240 -lemma continuous_on_const[continuous_on_intros]: "continuous_on s (\<lambda>x. c)"
1.241 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
1.242 -
1.243 -lemma continuous_on_norm[continuous_on_intros]:
1.244 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. norm (f x))"
1.245 -  unfolding continuous_on_def by (fast intro: tendsto_norm)
1.246 -
1.247  lemma continuous_on_infnorm[continuous_on_intros]:
1.248    shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. infnorm (f x))"
1.249    unfolding continuous_on by (fast intro: tendsto_infnorm)
1.250
1.251 -lemma continuous_on_minus[continuous_on_intros]:
1.252 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.253 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
1.254 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
1.255 -
1.256 -lemma continuous_on_add[continuous_on_intros]:
1.257 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.258 -  shows "continuous_on s f \<Longrightarrow> continuous_on s g
1.259 -           \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
1.260 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
1.261 -
1.262 -lemma continuous_on_diff[continuous_on_intros]:
1.263 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.264 -  shows "continuous_on s f \<Longrightarrow> continuous_on s g
1.265 -           \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
1.266 -  unfolding continuous_on_def by (auto intro: tendsto_intros)
1.267 -
1.268 -lemma (in bounded_linear) continuous_on[continuous_on_intros]:
1.269 -  "continuous_on s g \<Longrightarrow> continuous_on s (\<lambda>x. f (g x))"
1.270 -  unfolding continuous_on_def by (fast intro: tendsto)
1.271 -
1.272 -lemma (in bounded_bilinear) continuous_on[continuous_on_intros]:
1.273 -  "\<lbrakk>continuous_on s f; continuous_on s g\<rbrakk> \<Longrightarrow> continuous_on s (\<lambda>x. f x ** g x)"
1.274 -  unfolding continuous_on_def by (fast intro: tendsto)
1.275 -
1.276 -lemma continuous_on_scaleR[continuous_on_intros]:
1.277 -  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
1.278 -  assumes "continuous_on s f" and "continuous_on s g"
1.279 -  shows "continuous_on s (\<lambda>x. f x *\<^sub>R g x)"
1.280 -  using bounded_bilinear_scaleR assms
1.281 -  by (rule bounded_bilinear.continuous_on)
1.282 -
1.283 -lemma continuous_on_mult[continuous_on_intros]:
1.284 -  fixes g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
1.285 -  assumes "continuous_on s f" and "continuous_on s g"
1.286 -  shows "continuous_on s (\<lambda>x. f x * g x)"
1.287 -  using bounded_bilinear_mult assms
1.288 -  by (rule bounded_bilinear.continuous_on)
1.289 -
1.290  lemma continuous_on_inner[continuous_on_intros]:
1.291    fixes g :: "'a::topological_space \<Rightarrow> 'b::real_inner"
1.292    assumes "continuous_on s f" and "continuous_on s g"
1.293 @@ -4226,12 +4003,6 @@
1.294    using bounded_bilinear_inner assms
1.295    by (rule bounded_bilinear.continuous_on)
1.296
1.297 -lemma continuous_on_inverse[continuous_on_intros]:
1.298 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
1.299 -  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
1.300 -  shows "continuous_on s (\<lambda>x. inverse (f x))"
1.301 -  using assms unfolding continuous_on by (fast intro: tendsto_inverse)
1.302 -
1.303  subsubsection {* Structural rules for uniform continuity *}
1.304
1.305  lemma uniformly_continuous_on_id[continuous_on_intros]:
1.306 @@ -4312,33 +4083,7 @@
1.307
1.308  text{* Continuity of all kinds is preserved under composition. *}
1.309
1.310 -lemma continuous_within_topological:
1.311 -  "continuous (at x within s) f \<longleftrightarrow>
1.312 -    (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
1.313 -      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
1.314 -unfolding continuous_within
1.315 -unfolding tendsto_def Limits.eventually_within eventually_at_topological
1.316 -by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
1.317 -
1.318 -lemma continuous_within_compose[continuous_intros]:
1.319 -  assumes "continuous (at x within s) f"
1.320 -  assumes "continuous (at (f x) within f ` s) g"
1.321 -  shows "continuous (at x within s) (g o f)"
1.322 -using assms unfolding continuous_within_topological by simp metis
1.323 -
1.324 -lemma continuous_at_compose[continuous_intros]:
1.325 -  assumes "continuous (at x) f" and "continuous (at (f x)) g"
1.326 -  shows "continuous (at x) (g o f)"
1.327 -proof-
1.328 -  have "continuous (at (f x) within range f) g" using assms(2)
1.329 -    using continuous_within_subset[of "f x" UNIV g "range f"] by simp
1.330 -  thus ?thesis using assms(1)
1.331 -    using continuous_within_compose[of x UNIV f g] by simp
1.332 -qed
1.333 -
1.334 -lemma continuous_on_compose[continuous_on_intros]:
1.335 -  "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
1.336 -  unfolding continuous_on_topological by simp metis
1.337 +lemmas continuous_at_compose = isCont_o
1.338
1.339  lemma uniformly_continuous_on_compose[continuous_on_intros]:
1.340    assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
1.341 @@ -5182,8 +4927,7 @@
1.342    have "compact (s \<times> s)" using `compact s` by (intro compact_Times)
1.343    moreover have "s \<times> s \<noteq> {}" using `s \<noteq> {}` by auto
1.344    moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
1.345 -    by (intro continuous_at_imp_continuous_on ballI continuous_dist
1.346 -      continuous_isCont[THEN iffD1] isCont_fst isCont_snd isCont_ident)
1.347 +    by (intro continuous_at_imp_continuous_on ballI continuous_intros)
1.348    ultimately show ?thesis
1.349      using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
1.350  qed
1.351 @@ -5873,7 +5617,7 @@
1.352    by (rule isCont_open_vimage)
1.353
1.354  lemma open_Collect_less:
1.355 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
1.356 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
1.357    assumes f: "\<And>x. isCont f x"
1.358    assumes g: "\<And>x. isCont g x"
1.359    shows "open {x. f x < g x}"
1.360 @@ -5887,7 +5631,7 @@
1.361  qed
1.362
1.363  lemma closed_Collect_le:
1.364 -  fixes f g :: "'a::topological_space \<Rightarrow> real"
1.365 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
1.366    assumes f: "\<And>x. isCont f x"
1.367    assumes g: "\<And>x. isCont g x"
1.368    shows "closed {x. f x \<le> g x}"
1.369 @@ -5901,7 +5645,7 @@
1.370  qed
1.371
1.372  lemma closed_Collect_eq:
1.373 -  fixes f g :: "'a::topological_space \<Rightarrow> 'b::t2_space"
1.374 +  fixes f g :: "'a::t2_space \<Rightarrow> 'b::t2_space"
1.375    assumes f: "\<And>x. isCont f x"
1.376    assumes g: "\<And>x. isCont g x"
1.377    shows "closed {x. f x = g x}"
```