src/HOL/Analysis/Topology_Euclidean_Space.thy
 changeset 65204 d23eded35a33 parent 65038 9391ea7daa17 child 65585 a043de9ad41e
```     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Mar 12 19:06:10 2017 +0100
1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Mar 10 23:16:40 2017 +0100
1.3 @@ -3940,6 +3940,9 @@
1.4  lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
1.5    by (simp add: bounded_iff bdd_above_def)
1.6
1.7 +lemma bounded_norm_comp: "bounded ((\<lambda>x. norm (f x)) ` S) = bounded (f ` S)"
1.8 +  by (simp add: bounded_iff)
1.9 +
1.10  lemma boundedI:
1.11    assumes "\<And>x. x \<in> S \<Longrightarrow> norm x \<le> B"
1.12    shows "bounded S"
1.13 @@ -4056,6 +4059,19 @@
1.14      shows "bounded (- S) \<Longrightarrow> ~ (bounded S)"
1.15    using bounded_Un [of S "-S"]  by (simp add: sup_compl_top)
1.16
1.17 +lemma bounded_dist_comp:
1.18 +  assumes "bounded (f ` S)" "bounded (g ` S)"
1.19 +  shows "bounded ((\<lambda>x. dist (f x) (g x)) ` S)"
1.20 +proof -
1.21 +  from assms obtain M1 M2 where *: "dist (f x) undefined \<le> M1" "dist undefined (g x) \<le> M2" if "x \<in> S" for x
1.22 +    by (auto simp: bounded_any_center[of _ undefined] dist_commute)
1.23 +  have "dist (f x) (g x) \<le> M1 + M2" if "x \<in> S" for x
1.24 +    using *[OF that]
1.25 +    by (rule order_trans[OF dist_triangle add_mono])
1.26 +  then show ?thesis
1.27 +    by (auto intro!: boundedI)
1.28 +qed
1.29 +
1.30  lemma bounded_linear_image:
1.31    assumes "bounded S"
1.32      and "bounded_linear f"
1.33 @@ -4090,6 +4106,13 @@
1.34    apply (rule bounded_linear_scaleR_right)
1.35    done
1.36
1.37 +lemma bounded_scaleR_comp:
1.38 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.39 +  assumes "bounded (f ` S)"
1.40 +  shows "bounded ((\<lambda>x. r *\<^sub>R f x) ` S)"
1.41 +  using bounded_scaling[of "f ` S" r] assms
1.42 +  by (auto simp: image_image)
1.43 +
1.44  lemma bounded_translation:
1.45    fixes S :: "'a::real_normed_vector set"
1.46    assumes "bounded S"
1.47 @@ -4119,6 +4142,33 @@
1.48    shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
1.49  by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
1.50
1.51 +lemma uminus_bounded_comp [simp]:
1.52 +  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
1.53 +  shows "bounded ((\<lambda>x. - f x) ` S) \<longleftrightarrow> bounded (f ` S)"
1.54 +  using bounded_uminus[of "f ` S"]
1.55 +  by (auto simp: image_image)
1.56 +
1.57 +lemma bounded_plus_comp:
1.58 +  fixes f g::"'a \<Rightarrow> 'b::real_normed_vector"
1.59 +  assumes "bounded (f ` S)"
1.60 +  assumes "bounded (g ` S)"
1.61 +  shows "bounded ((\<lambda>x. f x + g x) ` S)"
1.62 +proof -
1.63 +  {
1.64 +    fix B C
1.65 +    assume "\<And>x. x\<in>S \<Longrightarrow> norm (f x) \<le> B" "\<And>x. x\<in>S \<Longrightarrow> norm (g x) \<le> C"
1.66 +    then have "\<And>x. x \<in> S \<Longrightarrow> norm (f x + g x) \<le> B + C"
1.67 +      by (auto intro!: norm_triangle_le add_mono)
1.68 +  } then show ?thesis
1.69 +    using assms by (fastforce simp: bounded_iff)
1.70 +qed
1.71 +
1.72 +lemma bounded_minus_comp:
1.73 +  "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
1.74 +  for f g::"'a \<Rightarrow> 'b::real_normed_vector"
1.75 +  using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
1.76 +  by (auto simp: )
1.77 +
1.78
1.79  subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
1.80
1.81 @@ -5915,89 +5965,6 @@
1.82    then show ?thesis ..
1.83  qed
1.84
1.85 -text\<open>Cauchy-type criteria for uniform convergence.\<close>
1.86 -
1.87 -lemma uniformly_convergent_eq_cauchy:
1.88 -  fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::complete_space"
1.89 -  shows
1.90 -    "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e) \<longleftrightarrow>
1.91 -      (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  \<longrightarrow> dist (s m x) (s n x) < e)"
1.92 -  (is "?lhs = ?rhs")
1.93 -proof
1.94 -  assume ?lhs
1.95 -  then obtain l where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e"
1.96 -    by auto
1.97 -  {
1.98 -    fix e :: real
1.99 -    assume "e > 0"
1.100 -    then obtain N :: nat where N: "\<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l x) < e / 2"
1.101 -      using l[THEN spec[where x="e/2"]] by auto
1.102 -    {
1.103 -      fix n m :: nat and x :: "'b"
1.104 -      assume "N \<le> m \<and> N \<le> n \<and> P x"
1.105 -      then have "dist (s m x) (s n x) < e"
1.106 -        using N[THEN spec[where x=m], THEN spec[where x=x]]
1.107 -        using N[THEN spec[where x=n], THEN spec[where x=x]]
1.108 -        using dist_triangle_half_l[of "s m x" "l x" e "s n x"] by auto
1.109 -    }
1.110 -    then have "\<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e"  by auto
1.111 -  }
1.112 -  then show ?rhs by auto
1.113 -next
1.114 -  assume ?rhs
1.115 -  then have "\<forall>x. P x \<longrightarrow> Cauchy (\<lambda>n. s n x)"
1.116 -    unfolding cauchy_def
1.117 -    apply auto
1.118 -    apply (erule_tac x=e in allE)
1.119 -    apply auto
1.120 -    done
1.121 -  then obtain l where l: "\<forall>x. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l x) sequentially"
1.122 -    unfolding convergent_eq_Cauchy[symmetric]
1.123 -    using choice[of "\<lambda>x l. P x \<longrightarrow> ((\<lambda>n. s n x) \<longlongrightarrow> l) sequentially"]
1.124 -    by auto
1.125 -  {
1.126 -    fix e :: real
1.127 -    assume "e > 0"
1.128 -    then obtain N where N:"\<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x \<longrightarrow> dist (s m x) (s n x) < e/2"
1.129 -      using \<open>?rhs\<close>[THEN spec[where x="e/2"]] by auto
1.130 -    {
1.131 -      fix x
1.132 -      assume "P x"
1.133 -      then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
1.134 -        using l[THEN spec[where x=x], unfolded lim_sequentially] and \<open>e > 0\<close>
1.135 -        by (auto elim!: allE[where x="e/2"])
1.136 -      fix n :: nat
1.137 -      assume "n \<ge> N"
1.138 -      then have "dist(s n x)(l x) < e"
1.139 -        using \<open>P x\<close>and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
1.140 -        using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"]
1.141 -        by (auto simp add: dist_commute)
1.142 -    }
1.143 -    then have "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
1.144 -      by auto
1.145 -  }
1.146 -  then show ?lhs by auto
1.147 -qed
1.148 -
1.149 -lemma uniformly_cauchy_imp_uniformly_convergent:
1.150 -  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::complete_space"
1.151 -  assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
1.152 -    and "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n \<longrightarrow> dist(s n x)(l x) < e)"
1.153 -  shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e"
1.154 -proof -
1.155 -  obtain l' where l:"\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist (s n x) (l' x) < e"
1.156 -    using assms(1) unfolding uniformly_convergent_eq_cauchy[symmetric] by auto
1.157 -  moreover
1.158 -  {
1.159 -    fix x
1.160 -    assume "P x"
1.161 -    then have "l x = l' x"
1.162 -      using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
1.163 -      using l and assms(2) unfolding lim_sequentially by blast
1.164 -  }
1.165 -  ultimately show ?thesis by auto
1.166 -qed
1.167 -
1.168
1.169  subsection \<open>Continuity\<close>
1.170
1.171 @@ -10960,6 +10927,109 @@
1.172    by blast
1.173
1.174
1.175 +
1.176 +subsection \<open>Continuous Extension\<close>
1.177 +
1.178 +definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
1.179 +  "clamp a b x = (if (\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)
1.180 +    then (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)
1.181 +    else a)"
1.182 +
1.183 +lemma clamp_in_interval[simp]:
1.184 +  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
1.185 +  shows "clamp a b x \<in> cbox a b"
1.186 +  unfolding clamp_def
1.187 +  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
1.188 +
1.189 +lemma clamp_cancel_cbox[simp]:
1.190 +  fixes x a b :: "'a::euclidean_space"
1.191 +  assumes x: "x \<in> cbox a b"
1.192 +  shows "clamp a b x = x"
1.193 +  using assms
1.194 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a])
1.195 +
1.196 +lemma clamp_empty_interval:
1.197 +  assumes "i \<in> Basis" "a \<bullet> i > b \<bullet> i"
1.198 +  shows "clamp a b = (\<lambda>_. a)"
1.199 +  using assms
1.200 +  by (force simp: clamp_def[abs_def] split: if_splits intro!: ext)
1.201 +
1.202 +lemma dist_clamps_le_dist_args:
1.203 +  fixes x :: "'a::euclidean_space"
1.204 +  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
1.205 +proof cases
1.206 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
1.207 +  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
1.208 +    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
1.209 +    by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
1.210 +  then show ?thesis
1.211 +    by (auto intro: real_sqrt_le_mono
1.212 +      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
1.213 +qed (auto simp: clamp_def)
1.214 +
1.215 +lemma clamp_continuous_at:
1.216 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
1.217 +    and x :: 'a
1.218 +  assumes f_cont: "continuous_on (cbox a b) f"
1.219 +  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
1.220 +proof cases
1.221 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
1.222 +  show ?thesis
1.223 +    unfolding continuous_at_eps_delta
1.224 +  proof safe
1.225 +    fix x :: 'a
1.226 +    fix e :: real
1.227 +    assume "e > 0"
1.228 +    moreover have "clamp a b x \<in> cbox a b"
1.229 +      by (simp add: clamp_in_interval le)
1.230 +    moreover note f_cont[simplified continuous_on_iff]
1.231 +    ultimately
1.232 +    obtain d where d: "0 < d"
1.233 +      "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
1.234 +      by force
1.235 +    show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
1.236 +      dist (f (clamp a b x')) (f (clamp a b x)) < e"
1.237 +      using le
1.238 +      by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans])
1.239 +  qed
1.240 +qed (auto simp: clamp_empty_interval)
1.241 +
1.242 +lemma clamp_continuous_on:
1.243 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
1.244 +  assumes f_cont: "continuous_on (cbox a b) f"
1.245 +  shows "continuous_on S (\<lambda>x. f (clamp a b x))"
1.246 +  using assms
1.247 +  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
1.248 +
1.249 +lemma clamp_bounded:
1.250 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
1.251 +  assumes bounded: "bounded (f ` (cbox a b))"
1.252 +  shows "bounded (range (\<lambda>x. f (clamp a b x)))"
1.253 +proof cases
1.254 +  assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
1.255 +  from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
1.256 +    by (auto simp add: bounded_any_center[where a=undefined])
1.257 +  then show ?thesis
1.258 +    by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
1.259 +        simp: bounded_any_center[where a=undefined])
1.260 +qed (auto simp: clamp_empty_interval image_def)
1.261 +
1.262 +
1.263 +definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b"
1.264 +  where "ext_cont f a b = (\<lambda>x. f (clamp a b x))"
1.265 +
1.266 +lemma ext_cont_cancel_cbox[simp]:
1.267 +  fixes x a b :: "'a::euclidean_space"
1.268 +  assumes x: "x \<in> cbox a b"
1.269 +  shows "ext_cont f a b x = f x"
1.270 +  using assms
1.271 +  unfolding ext_cont_def
1.272 +  by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f])
1.273 +
1.274 +lemma continuous_on_ext_cont[continuous_intros]:
1.275 +  "continuous_on (cbox a b) f \<Longrightarrow> continuous_on S (ext_cont f a b)"
1.276 +  by (auto intro!: clamp_continuous_on simp: ext_cont_def)
1.277 +
1.278  no_notation
1.279    eucl_less (infix "<e" 50)
1.280
```