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