uniformly continuous function extended continuously on closure
authorimmler
Fri May 20 22:01:42 2016 +0200 (2016-05-20 ago)
changeset 63105c445b0924e3a
parent 63104 9505a883403c
child 63107 932cf444f2fe
uniformly continuous function extended continuously on closure
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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: