src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44648 897f32a827f2
parent 44647 e4de7750cdeb
child 44668 31d41a0f6b5d
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 10:41:19 2011 -0700
     1.3 @@ -3253,7 +3253,7 @@
     1.4    assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
     1.5  qed
     1.6  
     1.7 -lemma uniformly_continuous_on_sequentially':
     1.8 +lemma uniformly_continuous_on_sequentially:
     1.9    "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
    1.10                      ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
    1.11                      \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
    1.12 @@ -3295,15 +3295,6 @@
    1.13    thus ?lhs unfolding uniformly_continuous_on_def by blast
    1.14  qed
    1.15  
    1.16 -lemma uniformly_continuous_on_sequentially:
    1.17 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    1.18 -  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
    1.19 -                    ((\<lambda>n. x n - y n) ---> 0) sequentially
    1.20 -                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
    1.21 -(* BH: maybe the previous lemma should replace this one? *)
    1.22 -unfolding uniformly_continuous_on_sequentially'
    1.23 -unfolding dist_norm tendsto_norm_zero_iff ..
    1.24 -
    1.25  text{* The usual transformation theorems. *}
    1.26  
    1.27  lemma continuous_transform_within:
    1.28 @@ -3330,7 +3321,7 @@
    1.29    using continuous_transform_within [of d x UNIV f g] assms
    1.30    by (simp add: within_UNIV)
    1.31  
    1.32 -text{* Combination results for pointwise continuity. *}
    1.33 +subsubsection {* Structural rules for pointwise continuity *}
    1.34  
    1.35  lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
    1.36    unfolding continuous_within by (rule tendsto_ident_at_within)
    1.37 @@ -3413,7 +3404,7 @@
    1.38    continuous_inner continuous_euclidean_component
    1.39    continuous_at_inverse continuous_at_within_inverse
    1.40  
    1.41 -text{* Same thing for setwise continuity. *}
    1.42 +subsubsection {* Structural rules for setwise continuity *}
    1.43  
    1.44  lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
    1.45    unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
    1.46 @@ -3486,62 +3477,83 @@
    1.47    shows "continuous_on s (\<lambda>x. inverse (f x))"
    1.48    using assms unfolding continuous_on by (fast intro: tendsto_inverse)
    1.49  
    1.50 -text{* Same thing for uniform continuity, using sequential formulations. *}
    1.51 +subsubsection {* Structural rules for uniform continuity *}
    1.52  
    1.53  lemma uniformly_continuous_on_id:
    1.54 - "uniformly_continuous_on s (\<lambda>x. x)"
    1.55 +  shows "uniformly_continuous_on s (\<lambda>x. x)"
    1.56    unfolding uniformly_continuous_on_def by auto
    1.57  
    1.58  lemma uniformly_continuous_on_const:
    1.59 - "uniformly_continuous_on s (\<lambda>x. c)"
    1.60 +  shows "uniformly_continuous_on s (\<lambda>x. c)"
    1.61    unfolding uniformly_continuous_on_def by simp
    1.62  
    1.63 +lemma uniformly_continuous_on_dist:
    1.64 +  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    1.65 +  assumes "uniformly_continuous_on s f"
    1.66 +  assumes "uniformly_continuous_on s g"
    1.67 +  shows "uniformly_continuous_on s (\<lambda>x. dist (f x) (g x))"
    1.68 +proof -
    1.69 +  { fix a b c d :: 'b have "\<bar>dist a b - dist c d\<bar> \<le> dist a c + dist b d"
    1.70 +      using dist_triangle2 [of a b c] dist_triangle2 [of b c d]
    1.71 +      using dist_triangle3 [of c d a] dist_triangle [of a d b]
    1.72 +      by arith
    1.73 +  } note le = this
    1.74 +  { fix x y
    1.75 +    assume f: "(\<lambda>n. dist (f (x n)) (f (y n))) ----> 0"
    1.76 +    assume g: "(\<lambda>n. dist (g (x n)) (g (y n))) ----> 0"
    1.77 +    have "(\<lambda>n. \<bar>dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\<bar>) ----> 0"
    1.78 +      by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]],
    1.79 +        simp add: le)
    1.80 +  }
    1.81 +  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially
    1.82 +    unfolding dist_real_def by simp
    1.83 +qed
    1.84 +
    1.85 +lemma uniformly_continuous_on_norm:
    1.86 +  assumes "uniformly_continuous_on s f"
    1.87 +  shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
    1.88 +  unfolding norm_conv_dist using assms
    1.89 +  by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
    1.90 +
    1.91 +lemma (in bounded_linear) uniformly_continuous_on:
    1.92 +  assumes "uniformly_continuous_on s g"
    1.93 +  shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
    1.94 +  using assms unfolding uniformly_continuous_on_sequentially
    1.95 +  unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
    1.96 +  by (auto intro: tendsto_zero)
    1.97 +
    1.98  lemma uniformly_continuous_on_cmul:
    1.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.100    assumes "uniformly_continuous_on s f"
   1.101    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
   1.102 -proof-
   1.103 -  { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   1.104 -    hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
   1.105 -      using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   1.106 -      unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   1.107 -  }
   1.108 -  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   1.109 -    unfolding dist_norm tendsto_norm_zero_iff by auto
   1.110 -qed
   1.111 +  using bounded_linear_scaleR_right assms
   1.112 +  by (rule bounded_linear.uniformly_continuous_on)
   1.113  
   1.114  lemma dist_minus:
   1.115    fixes x y :: "'a::real_normed_vector"
   1.116    shows "dist (- x) (- y) = dist x y"
   1.117    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
   1.118  
   1.119 -lemma uniformly_continuous_on_neg:
   1.120 +lemma uniformly_continuous_on_minus:
   1.121    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.122 -  shows "uniformly_continuous_on s f
   1.123 -         ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
   1.124 +  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
   1.125    unfolding uniformly_continuous_on_def dist_minus .
   1.126  
   1.127  lemma uniformly_continuous_on_add:
   1.128    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.129 -  assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
   1.130 +  assumes "uniformly_continuous_on s f"
   1.131 +  assumes "uniformly_continuous_on s g"
   1.132    shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
   1.133 -proof-
   1.134 -  {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   1.135 -                    "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
   1.136 -    hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
   1.137 -      using tendsto_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
   1.138 -    hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
   1.139 -  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   1.140 -    unfolding dist_norm tendsto_norm_zero_iff by auto
   1.141 -qed
   1.142 -
   1.143 -lemma uniformly_continuous_on_sub:
   1.144 +  using assms unfolding uniformly_continuous_on_sequentially
   1.145 +  unfolding dist_norm tendsto_norm_zero_iff add_diff_add
   1.146 +  by (auto intro: tendsto_add_zero)
   1.147 +
   1.148 +lemma uniformly_continuous_on_diff:
   1.149    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   1.150 -  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
   1.151 -           ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   1.152 -  unfolding ab_diff_minus
   1.153 -  using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
   1.154 -  using uniformly_continuous_on_neg[of s g] by auto
   1.155 +  assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g"
   1.156 +  shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
   1.157 +  unfolding ab_diff_minus using assms
   1.158 +  by (intro uniformly_continuous_on_add uniformly_continuous_on_minus)
   1.159  
   1.160  text{* Continuity of all kinds is preserved under composition. *}
   1.161  
   1.162 @@ -3587,10 +3599,11 @@
   1.163    continuous_on_add continuous_on_minus continuous_on_diff
   1.164    continuous_on_scaleR continuous_on_mult continuous_on_inverse
   1.165    continuous_on_inner continuous_on_euclidean_component
   1.166 -  uniformly_continuous_on_add uniformly_continuous_on_const
   1.167 -  uniformly_continuous_on_id uniformly_continuous_on_compose
   1.168 -  uniformly_continuous_on_cmul uniformly_continuous_on_neg
   1.169 -  uniformly_continuous_on_sub
   1.170 +  uniformly_continuous_on_id uniformly_continuous_on_const
   1.171 +  uniformly_continuous_on_dist uniformly_continuous_on_norm
   1.172 +  uniformly_continuous_on_compose uniformly_continuous_on_add
   1.173 +  uniformly_continuous_on_minus uniformly_continuous_on_diff
   1.174 +  uniformly_continuous_on_cmul
   1.175  
   1.176  text{* Continuity in terms of open preimages. *}
   1.177