author | immler |

Fri May 20 22:01:42 2016 +0200 (2016-05-20 ago) | |

changeset 63105 | c445b0924e3a |

parent 63104 | 9505a883403c |

child 63107 | 932cf444f2fe |

uniformly continuous function extended continuously on closure

1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 20 21:21:28 2016 +0200 1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri May 20 22:01:42 2016 +0200 1.3 @@ -6086,6 +6086,158 @@ 1.4 qed 1.5 qed 1.6 1.7 +lemma uniformly_continuous_on_extension_at_closure: 1.8 + fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space" 1.9 + assumes uc: "uniformly_continuous_on X f" 1.10 + assumes "x \<in> closure X" 1.11 + obtains l where "(f \<longlongrightarrow> l) (at x within X)" 1.12 +proof - 1.13 + from assms obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" 1.14 + by (auto simp: closure_sequential) 1.15 + 1.16 + from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs] 1.17 + obtain l where l: "(\<lambda>n. f (xs n)) \<longlonglongrightarrow> l" 1.18 + by atomize_elim (simp only: convergent_eq_cauchy) 1.19 + 1.20 + have "(f \<longlongrightarrow> l) (at x within X)" 1.21 + proof (safe intro!: Lim_within_LIMSEQ) 1.22 + fix xs' 1.23 + assume "\<forall>n. xs' n \<noteq> x \<and> xs' n \<in> X" 1.24 + and xs': "xs' \<longlonglongrightarrow> x" 1.25 + then have "xs' n \<noteq> x" "xs' n \<in> X" for n by auto 1.26 + 1.27 + from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \<open>xs' \<longlonglongrightarrow> x\<close> \<open>xs' _ \<in> X\<close>] 1.28 + obtain l' where l': "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l'" 1.29 + by atomize_elim (simp only: convergent_eq_cauchy) 1.30 + 1.31 + show "(\<lambda>n. f (xs' n)) \<longlonglongrightarrow> l" 1.32 + proof (rule tendstoI) 1.33 + fix e::real assume "e > 0" 1.34 + define e' where "e' \<equiv> e / 2" 1.35 + have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def) 1.36 + 1.37 + have "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) l < e'" 1.38 + by (simp add: \<open>0 < e'\<close> l tendstoD) 1.39 + moreover 1.40 + from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>e' > 0\<close>] 1.41 + obtain d where d: "d > 0" "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x x' < d \<Longrightarrow> dist (f x) (f x') < e'" 1.42 + by auto 1.43 + have "\<forall>\<^sub>F n in sequentially. dist (xs n) (xs' n) < d" 1.44 + by (auto intro!: \<open>0 < d\<close> order_tendstoD tendsto_eq_intros xs xs') 1.45 + ultimately 1.46 + show "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) l < e" 1.47 + proof eventually_elim 1.48 + case (elim n) 1.49 + have "dist (f (xs' n)) l \<le> dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l" 1.50 + by (metis dist_triangle dist_commute) 1.51 + also have "dist (f (xs n)) (f (xs' n)) < e'" 1.52 + by (auto intro!: d xs \<open>xs' _ \<in> _\<close> elim) 1.53 + also note \<open>dist (f (xs n)) l < e'\<close> 1.54 + also have "e' + e' = e" by (simp add: e'_def) 1.55 + finally show ?case by simp 1.56 + qed 1.57 + qed 1.58 + qed 1.59 + thus ?thesis .. 1.60 +qed 1.61 + 1.62 +lemma uniformly_continuous_on_extension_on_closure: 1.63 + fixes f::"'a::metric_space \<Rightarrow> 'b::complete_space" 1.64 + assumes uc: "uniformly_continuous_on X f" 1.65 + obtains g where "uniformly_continuous_on (closure X) g" "\<And>x. x \<in> X \<Longrightarrow> f x = g x" 1.66 + "\<And>Y h x. X \<subseteq> Y \<Longrightarrow> Y \<subseteq> closure X \<Longrightarrow> continuous_on Y h \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> f x = h x) \<Longrightarrow> x \<in> Y \<Longrightarrow> h x = g x" 1.67 +proof - 1.68 + from uc have cont_f: "continuous_on X f" 1.69 + by (simp add: uniformly_continuous_imp_continuous) 1.70 + obtain y where y: "(f \<longlongrightarrow> y x) (at x within X)" if "x \<in> closure X" for x 1.71 + apply atomize_elim 1.72 + apply (rule choice) 1.73 + using uniformly_continuous_on_extension_at_closure[OF assms] 1.74 + by metis 1.75 + let ?g = "\<lambda>x. if x \<in> X then f x else y x" 1.76 + 1.77 + have "uniformly_continuous_on (closure X) ?g" 1.78 + unfolding uniformly_continuous_on_def 1.79 + proof safe 1.80 + fix e::real assume "e > 0" 1.81 + define e' where "e' \<equiv> e / 3" 1.82 + have "e' > 0" using \<open>e > 0\<close> by (simp add: e'_def) 1.83 + from uc[unfolded uniformly_continuous_on_def, rule_format, OF \<open>0 < e'\<close>] 1.84 + obtain d where "d > 0" and d: "\<And>x x'. x \<in> X \<Longrightarrow> x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> dist (f x') (f x) < e'" 1.85 + by auto 1.86 + define d' where "d' = d / 3" 1.87 + have "d' > 0" using \<open>d > 0\<close> by (simp add: d'_def) 1.88 + show "\<exists>d>0. \<forall>x\<in>closure X. \<forall>x'\<in>closure X. dist x' x < d \<longrightarrow> dist (?g x') (?g x) < e" 1.89 + proof (safe intro!: exI[where x=d'] \<open>d' > 0\<close>) 1.90 + fix x x' assume x: "x \<in> closure X" and x': "x' \<in> closure X" and dist: "dist x' x < d'" 1.91 + then obtain xs xs' where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" 1.92 + and xs': "xs' \<longlonglongrightarrow> x'" "\<And>n. xs' n \<in> X" 1.93 + by (auto simp: closure_sequential) 1.94 + have "\<forall>\<^sub>F n in sequentially. dist (xs' n) x' < d'" 1.95 + and "\<forall>\<^sub>F n in sequentially. dist (xs n) x < d'" 1.96 + by (auto intro!: \<open>0 < d'\<close> order_tendstoD tendsto_eq_intros xs xs') 1.97 + moreover 1.98 + have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" if "x \<in> closure X" "x \<notin> X" "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" for xs x 1.99 + using that not_eventuallyD 1.100 + by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at) 1.101 + then have "(\<lambda>x. f (xs' x)) \<longlonglongrightarrow> ?g x'" "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> ?g x" 1.102 + using x x' 1.103 + by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs) 1.104 + then have "\<forall>\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'" 1.105 + "\<forall>\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'" 1.106 + by (auto intro!: \<open>0 < e'\<close> order_tendstoD tendsto_eq_intros) 1.107 + ultimately 1.108 + have "\<forall>\<^sub>F n in sequentially. dist (?g x') (?g x) < e" 1.109 + proof eventually_elim 1.110 + case (elim n) 1.111 + have "dist (?g x') (?g x) \<le> 1.112 + dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)" 1.113 + by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le) 1.114 + also 1.115 + { 1.116 + have "dist (xs' n) (xs n) \<le> dist (xs' n) x' + dist x' x + dist (xs n) x" 1.117 + by (metis add.commute add_le_cancel_left dist_triangle dist_triangle_le) 1.118 + also note \<open>dist (xs' n) x' < d'\<close> 1.119 + also note \<open>dist x' x < d'\<close> 1.120 + also note \<open>dist (xs n) x < d'\<close> 1.121 + finally have "dist (xs' n) (xs n) < d" by (simp add: d'_def) 1.122 + } 1.123 + with \<open>xs _ \<in> X\<close> \<open>xs' _ \<in> X\<close> have "dist (f (xs' n)) (f (xs n)) < e'" 1.124 + by (rule d) 1.125 + also note \<open>dist (f (xs' n)) (?g x') < e'\<close> 1.126 + also note \<open>dist (f (xs n)) (?g x) < e'\<close> 1.127 + finally show ?case by (simp add: e'_def) 1.128 + qed 1.129 + then show "dist (?g x') (?g x) < e" by simp 1.130 + qed 1.131 + qed 1.132 + moreover have "f x = ?g x" if "x \<in> X" for x using that by simp 1.133 + moreover 1.134 + { 1.135 + fix Y h x 1.136 + assume Y: "x \<in> Y" "X \<subseteq> Y" "Y \<subseteq> closure X" and cont_h: "continuous_on Y h" 1.137 + and extension: "(\<And>x. x \<in> X \<Longrightarrow> f x = h x)" 1.138 + { 1.139 + assume "x \<notin> X" 1.140 + have "x \<in> closure X" using Y by auto 1.141 + then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X" 1.142 + by (auto simp: closure_sequential) 1.143 + from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y 1.144 + have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x" 1.145 + by (auto simp: set_mp extension) 1.146 + moreover 1.147 + then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x" 1.148 + using \<open>x \<notin> X\<close> not_eventuallyD xs(2) 1.149 + by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs) 1.150 + ultimately have "h x = y x" by (rule LIMSEQ_unique) 1.151 + } then 1.152 + have "h x = ?g x" 1.153 + using extension by auto 1.154 + } 1.155 + ultimately show ?thesis .. 1.156 +qed 1.157 + 1.158 + 1.159 subsection\<open>Quotient maps\<close> 1.160 1.161 lemma quotient_map_imp_continuous_open: