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}"