src/HOL/Topological_Spaces.thy
changeset 62101 26c0a70f78a3
parent 62083 7582b39f51ed
child 62102 877463945ce9
     1.1 --- a/src/HOL/Topological_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4  
     1.5  named_theorems continuous_intros "structural introduction rules for continuity"
     1.6  
     1.7 -
     1.8  subsection \<open>Topological space\<close>
     1.9  
    1.10  class "open" =
    1.11 @@ -693,8 +692,6 @@
    1.12    by (rule tendsto_le [OF F tendsto_const x a])
    1.13  
    1.14  
    1.15 -
    1.16 -
    1.17  subsubsection \<open>Rules about @{const Lim}\<close>
    1.18  
    1.19  lemma tendsto_Lim:
    1.20 @@ -2435,4 +2432,173 @@
    1.21    qed
    1.22  qed (intro cSUP_least \<open>antimono f\<close>[THEN antimonoD] cInf_lower S)
    1.23  
    1.24 +subsection \<open>Uniform spaces\<close>
    1.25 +
    1.26 +class uniformity = 
    1.27 +  fixes uniformity :: "('a \<times> 'a) filter"
    1.28 +begin
    1.29 +
    1.30 +abbreviation uniformity_on :: "'a set \<Rightarrow> ('a \<times> 'a) filter" where
    1.31 +  "uniformity_on s \<equiv> inf uniformity (principal (s\<times>s))"
    1.32 +
    1.33  end
    1.34 +
    1.35 +class open_uniformity = "open" + uniformity +
    1.36 +  assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
    1.37 +
    1.38 +class uniform_space = open_uniformity +
    1.39 +  assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
    1.40 +  assumes uniformity_sym: "eventually E uniformity \<Longrightarrow> eventually (\<lambda>(x, y). E (y, x)) uniformity"
    1.41 +  assumes uniformity_trans: "eventually E uniformity \<Longrightarrow> \<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
    1.42 +begin
    1.43 +
    1.44 +subclass topological_space
    1.45 +  proof qed (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
    1.46 +
    1.47 +lemma uniformity_bot: "uniformity \<noteq> bot"
    1.48 +  using uniformity_refl by auto
    1.49 +
    1.50 +lemma uniformity_trans':
    1.51 +  "eventually E uniformity \<Longrightarrow> eventually (\<lambda>((x, y), (y', z)). y = y' \<longrightarrow> E (x, z)) (uniformity \<times>\<^sub>F uniformity)"
    1.52 +  by (drule uniformity_trans) (auto simp add: eventually_prod_same)
    1.53 +
    1.54 +lemma uniformity_transE:
    1.55 +  assumes E: "eventually E uniformity"
    1.56 +  obtains D where "eventually D uniformity" "\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)"
    1.57 +  using uniformity_trans[OF E] by auto
    1.58 +
    1.59 +lemma eventually_nhds_uniformity:
    1.60 +  "eventually P (nhds x) \<longleftrightarrow> eventually (\<lambda>(x', y). x' = x \<longrightarrow> P y) uniformity" (is "_ \<longleftrightarrow> ?N P x")
    1.61 +  unfolding eventually_nhds
    1.62 +proof safe
    1.63 +  assume *: "?N P x"
    1.64 +  { fix x assume "?N P x"
    1.65 +    then guess D by (rule uniformity_transE) note D = this
    1.66 +    from D(1) have "?N (?N P) x"
    1.67 +      by eventually_elim (insert D, force elim: eventually_mono split: prod.split) }
    1.68 +  then have "open {x. ?N P x}"
    1.69 +    by (simp add: open_uniformity)
    1.70 +  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x\<in>S. P x)"
    1.71 +    by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
    1.72 +qed (force simp add: open_uniformity elim: eventually_mono)
    1.73 +
    1.74 +subsubsection \<open>Totally bounded sets\<close>
    1.75 +
    1.76 +definition totally_bounded :: "'a set \<Rightarrow> bool" where
    1.77 +  "totally_bounded S \<longleftrightarrow>
    1.78 +    (\<forall>E. eventually E uniformity \<longrightarrow> (\<exists>X. finite X \<and> (\<forall>s\<in>S. \<exists>x\<in>X. E (x, s))))"
    1.79 +
    1.80 +lemma totally_bounded_empty[iff]: "totally_bounded {}"
    1.81 +  by (auto simp add: totally_bounded_def)
    1.82 +
    1.83 +lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
    1.84 +  by (force simp add: totally_bounded_def)
    1.85 +
    1.86 +lemma totally_bounded_Union[intro]: 
    1.87 +  assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
    1.88 +  unfolding totally_bounded_def
    1.89 +proof safe
    1.90 +  fix E assume "eventually E uniformity"
    1.91 +  with M obtain X where "\<forall>S\<in>M. finite (X S) \<and> (\<forall>s\<in>S. \<exists>x\<in>X S. E (x, s))"
    1.92 +    by (metis totally_bounded_def)
    1.93 +  with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
    1.94 +    by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
    1.95 +qed
    1.96 +
    1.97 +subsubsection \<open>Cauchy filter\<close>
    1.98 +
    1.99 +definition cauchy_filter :: "'a filter \<Rightarrow> bool" where
   1.100 +  "cauchy_filter F \<longleftrightarrow> F \<times>\<^sub>F F \<le> uniformity"
   1.101 +
   1.102 +definition Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.103 +  Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
   1.104 +
   1.105 +lemma Cauchy_uniform_iff:
   1.106 +  "Cauchy X \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)))"
   1.107 +  unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
   1.108 +    eventually_filtermap eventually_sequentially
   1.109 +proof safe
   1.110 +  let ?U = "\<lambda>P. eventually P uniformity"
   1.111 +  { fix P assume "?U P" "\<forall>P. ?U P \<longrightarrow> (\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
   1.112 +    then obtain Q N where "\<And>n. n \<ge> N \<Longrightarrow> Q (X n)" "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> P (x, y)"
   1.113 +      by metis
   1.114 +    then show "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)"
   1.115 +      by blast }
   1.116 +  { fix P assume "?U P" and P: "\<forall>P. ?U P \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m))"
   1.117 +    then obtain Q where "?U Q" and Q: "\<And>x y z. Q (x, y) \<Longrightarrow> Q (y, z) \<Longrightarrow> P (x, z)"
   1.118 +      by (auto elim: uniformity_transE)
   1.119 +    then have "?U (\<lambda>x. Q x \<and> (\<lambda>(x, y). Q (y, x)) x)"
   1.120 +      unfolding eventually_conj_iff by (simp add: uniformity_sym)
   1.121 +    from P[rule_format, OF this]
   1.122 +    obtain N where N: "\<And>n m. n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> Q (X n, X m) \<and> Q (X m, X n)"
   1.123 +      by auto
   1.124 +    show "\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
   1.125 +    proof (safe intro!: exI[of _ "\<lambda>x. \<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)"] exI[of _ N] N)
   1.126 +      fix x y assume "\<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)" "\<forall>n\<ge>N. Q (y, X n) \<and> Q (X n, y)"
   1.127 +      then have "Q (x, X N)" "Q (X N, y)" by auto
   1.128 +      then show "P (x, y)"
   1.129 +        by (rule Q)
   1.130 +    qed }
   1.131 +qed
   1.132 +
   1.133 +lemma nhds_imp_cauchy_filter:
   1.134 +  assumes *: "F \<le> nhds x" shows "cauchy_filter F"
   1.135 +proof -
   1.136 +  have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
   1.137 +    by (intro prod_filter_mono *)
   1.138 +  also have "\<dots> \<le> uniformity"
   1.139 +    unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
   1.140 +  proof safe
   1.141 +    fix P assume "eventually P uniformity"
   1.142 +    then guess Ql by (rule uniformity_transE) note Ql = this
   1.143 +    moreover note Ql(1)[THEN uniformity_sym]
   1.144 +    ultimately show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
   1.145 +      by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
   1.146 +  qed
   1.147 +  finally show ?thesis
   1.148 +    by (simp add: cauchy_filter_def)
   1.149 +qed
   1.150 +
   1.151 +lemma LIMSEQ_imp_Cauchy: "X \<longlonglongrightarrow> x \<Longrightarrow> Cauchy X"
   1.152 +  unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
   1.153 +
   1.154 +lemma Cauchy_subseq_Cauchy: assumes "Cauchy X" "subseq f" shows "Cauchy (X \<circ> f)"
   1.155 +  unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
   1.156 +  by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
   1.157 +     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
   1.158 +
   1.159 +lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
   1.160 +  unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
   1.161 +
   1.162 +definition complete :: "'a set \<Rightarrow> bool" where
   1.163 +  complete_uniform: "complete S \<longleftrightarrow> (\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
   1.164 +
   1.165 +end
   1.166 +
   1.167 +subsubsection \<open>Uniformly continuous functions\<close>
   1.168 +
   1.169 +definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
   1.170 +  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow> 
   1.171 +    (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
   1.172 +
   1.173 +lemma uniformly_continuous_onD:
   1.174 +  "uniformly_continuous_on s f \<Longrightarrow> eventually E uniformity
   1.175 +    \<Longrightarrow> eventually (\<lambda>(x, y). x \<in> s \<longrightarrow> y \<in> s \<longrightarrow> E (f x, f y)) uniformity"
   1.176 +  by (simp add: uniformly_continuous_on_uniformity filterlim_iff eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
   1.177 +
   1.178 +lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. c)"
   1.179 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
   1.180 +
   1.181 +lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
   1.182 +  by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
   1.183 +
   1.184 +lemma uniformly_continuous_on_compose[continuous_intros]:
   1.185 +  "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f (g x))"
   1.186 +  using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity "uniformity_on (g`s)"  "\<lambda>(x, y). (g x, g y)" "uniformity_on s"]
   1.187 +  by (simp add: split_beta' uniformly_continuous_on_uniformity filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
   1.188 +
   1.189 +lemma uniformly_continuous_imp_continuous: assumes f: "uniformly_continuous_on s f" shows "continuous_on s f"
   1.190 +  by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
   1.191 +           elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
   1.192 +
   1.193 +end