simplify some proofs about uniform continuity, and add some new ones;
authorhuffman
Thu Sep 01 10:41:19 2011 -0700 (2011-09-01)
changeset 44648897f32a827f2
parent 44647 e4de7750cdeb
child 44649 3d7b737d200a
child 44656 22bbd0d1b943
simplify some proofs about uniform continuity, and add some new ones;
rename some theorems according to standard naming scheme;
NEWS
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/NEWS	Thu Sep 01 09:02:14 2011 -0700
     1.2 +++ b/NEWS	Thu Sep 01 10:41:19 2011 -0700
     1.3 @@ -243,6 +243,8 @@
     1.4    continuous_on_inner ~> continuous_on_inner [OF continuous_on_const]
     1.5    continuous_on_norm ~> continuous_on_norm [OF continuous_on_id]
     1.6    continuous_on_inverse ~> continuous_on_inv
     1.7 +  uniformly_continuous_on_neg ~> uniformly_continuous_on_minus
     1.8 +  uniformly_continuous_on_sub ~> uniformly_continuous_on_diff
     1.9    subset_interior ~> interior_mono
    1.10    subset_closure ~> closure_mono
    1.11    closure_univ ~> closure_UNIV
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 09:02:14 2011 -0700
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Sep 01 10:41:19 2011 -0700
     2.3 @@ -3253,7 +3253,7 @@
     2.4    assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
     2.5  qed
     2.6  
     2.7 -lemma uniformly_continuous_on_sequentially':
     2.8 +lemma uniformly_continuous_on_sequentially:
     2.9    "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
    2.10                      ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
    2.11                      \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
    2.12 @@ -3295,15 +3295,6 @@
    2.13    thus ?lhs unfolding uniformly_continuous_on_def by blast
    2.14  qed
    2.15  
    2.16 -lemma uniformly_continuous_on_sequentially:
    2.17 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    2.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>
    2.19 -                    ((\<lambda>n. x n - y n) ---> 0) sequentially
    2.20 -                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
    2.21 -(* BH: maybe the previous lemma should replace this one? *)
    2.22 -unfolding uniformly_continuous_on_sequentially'
    2.23 -unfolding dist_norm tendsto_norm_zero_iff ..
    2.24 -
    2.25  text{* The usual transformation theorems. *}
    2.26  
    2.27  lemma continuous_transform_within:
    2.28 @@ -3330,7 +3321,7 @@
    2.29    using continuous_transform_within [of d x UNIV f g] assms
    2.30    by (simp add: within_UNIV)
    2.31  
    2.32 -text{* Combination results for pointwise continuity. *}
    2.33 +subsubsection {* Structural rules for pointwise continuity *}
    2.34  
    2.35  lemma continuous_within_id: "continuous (at a within s) (\<lambda>x. x)"
    2.36    unfolding continuous_within by (rule tendsto_ident_at_within)
    2.37 @@ -3413,7 +3404,7 @@
    2.38    continuous_inner continuous_euclidean_component
    2.39    continuous_at_inverse continuous_at_within_inverse
    2.40  
    2.41 -text{* Same thing for setwise continuity. *}
    2.42 +subsubsection {* Structural rules for setwise continuity *}
    2.43  
    2.44  lemma continuous_on_id: "continuous_on s (\<lambda>x. x)"
    2.45    unfolding continuous_on_def by (fast intro: tendsto_ident_at_within)
    2.46 @@ -3486,62 +3477,83 @@
    2.47    shows "continuous_on s (\<lambda>x. inverse (f x))"
    2.48    using assms unfolding continuous_on by (fast intro: tendsto_inverse)
    2.49  
    2.50 -text{* Same thing for uniform continuity, using sequential formulations. *}
    2.51 +subsubsection {* Structural rules for uniform continuity *}
    2.52  
    2.53  lemma uniformly_continuous_on_id:
    2.54 - "uniformly_continuous_on s (\<lambda>x. x)"
    2.55 +  shows "uniformly_continuous_on s (\<lambda>x. x)"
    2.56    unfolding uniformly_continuous_on_def by auto
    2.57  
    2.58  lemma uniformly_continuous_on_const:
    2.59 - "uniformly_continuous_on s (\<lambda>x. c)"
    2.60 +  shows "uniformly_continuous_on s (\<lambda>x. c)"
    2.61    unfolding uniformly_continuous_on_def by simp
    2.62  
    2.63 +lemma uniformly_continuous_on_dist:
    2.64 +  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    2.65 +  assumes "uniformly_continuous_on s f"
    2.66 +  assumes "uniformly_continuous_on s g"
    2.67 +  shows "uniformly_continuous_on s (\<lambda>x. dist (f x) (g x))"
    2.68 +proof -
    2.69 +  { fix a b c d :: 'b have "\<bar>dist a b - dist c d\<bar> \<le> dist a c + dist b d"
    2.70 +      using dist_triangle2 [of a b c] dist_triangle2 [of b c d]
    2.71 +      using dist_triangle3 [of c d a] dist_triangle [of a d b]
    2.72 +      by arith
    2.73 +  } note le = this
    2.74 +  { fix x y
    2.75 +    assume f: "(\<lambda>n. dist (f (x n)) (f (y n))) ----> 0"
    2.76 +    assume g: "(\<lambda>n. dist (g (x n)) (g (y n))) ----> 0"
    2.77 +    have "(\<lambda>n. \<bar>dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\<bar>) ----> 0"
    2.78 +      by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]],
    2.79 +        simp add: le)
    2.80 +  }
    2.81 +  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially
    2.82 +    unfolding dist_real_def by simp
    2.83 +qed
    2.84 +
    2.85 +lemma uniformly_continuous_on_norm:
    2.86 +  assumes "uniformly_continuous_on s f"
    2.87 +  shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
    2.88 +  unfolding norm_conv_dist using assms
    2.89 +  by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
    2.90 +
    2.91 +lemma (in bounded_linear) uniformly_continuous_on:
    2.92 +  assumes "uniformly_continuous_on s g"
    2.93 +  shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
    2.94 +  using assms unfolding uniformly_continuous_on_sequentially
    2.95 +  unfolding dist_norm tendsto_norm_zero_iff diff[symmetric]
    2.96 +  by (auto intro: tendsto_zero)
    2.97 +
    2.98  lemma uniformly_continuous_on_cmul:
    2.99    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   2.100    assumes "uniformly_continuous_on s f"
   2.101    shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
   2.102 -proof-
   2.103 -  { fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   2.104 -    hence "((\<lambda>n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially"
   2.105 -      using tendsto_scaleR [OF tendsto_const, of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
   2.106 -      unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   2.107 -  }
   2.108 -  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   2.109 -    unfolding dist_norm tendsto_norm_zero_iff by auto
   2.110 -qed
   2.111 +  using bounded_linear_scaleR_right assms
   2.112 +  by (rule bounded_linear.uniformly_continuous_on)
   2.113  
   2.114  lemma dist_minus:
   2.115    fixes x y :: "'a::real_normed_vector"
   2.116    shows "dist (- x) (- y) = dist x y"
   2.117    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
   2.118  
   2.119 -lemma uniformly_continuous_on_neg:
   2.120 +lemma uniformly_continuous_on_minus:
   2.121    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   2.122 -  shows "uniformly_continuous_on s f
   2.123 -         ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
   2.124 +  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. - f x)"
   2.125    unfolding uniformly_continuous_on_def dist_minus .
   2.126  
   2.127  lemma uniformly_continuous_on_add:
   2.128    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   2.129 -  assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
   2.130 +  assumes "uniformly_continuous_on s f"
   2.131 +  assumes "uniformly_continuous_on s g"
   2.132    shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
   2.133 -proof-
   2.134 -  {  fix x y assume "((\<lambda>n. f (x n) - f (y n)) ---> 0) sequentially"
   2.135 -                    "((\<lambda>n. g (x n) - g (y n)) ---> 0) sequentially"
   2.136 -    hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
   2.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
   2.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  }
   2.139 -  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
   2.140 -    unfolding dist_norm tendsto_norm_zero_iff by auto
   2.141 -qed
   2.142 -
   2.143 -lemma uniformly_continuous_on_sub:
   2.144 +  using assms unfolding uniformly_continuous_on_sequentially
   2.145 +  unfolding dist_norm tendsto_norm_zero_iff add_diff_add
   2.146 +  by (auto intro: tendsto_add_zero)
   2.147 +
   2.148 +lemma uniformly_continuous_on_diff:
   2.149    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   2.150 -  shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
   2.151 -           ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   2.152 -  unfolding ab_diff_minus
   2.153 -  using uniformly_continuous_on_add[of s f "\<lambda>x. - g x"]
   2.154 -  using uniformly_continuous_on_neg[of s g] by auto
   2.155 +  assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g"
   2.156 +  shows "uniformly_continuous_on s (\<lambda>x. f x - g x)"
   2.157 +  unfolding ab_diff_minus using assms
   2.158 +  by (intro uniformly_continuous_on_add uniformly_continuous_on_minus)
   2.159  
   2.160  text{* Continuity of all kinds is preserved under composition. *}
   2.161  
   2.162 @@ -3587,10 +3599,11 @@
   2.163    continuous_on_add continuous_on_minus continuous_on_diff
   2.164    continuous_on_scaleR continuous_on_mult continuous_on_inverse
   2.165    continuous_on_inner continuous_on_euclidean_component
   2.166 -  uniformly_continuous_on_add uniformly_continuous_on_const
   2.167 -  uniformly_continuous_on_id uniformly_continuous_on_compose
   2.168 -  uniformly_continuous_on_cmul uniformly_continuous_on_neg
   2.169 -  uniformly_continuous_on_sub
   2.170 +  uniformly_continuous_on_id uniformly_continuous_on_const
   2.171 +  uniformly_continuous_on_dist uniformly_continuous_on_norm
   2.172 +  uniformly_continuous_on_compose uniformly_continuous_on_add
   2.173 +  uniformly_continuous_on_minus uniformly_continuous_on_diff
   2.174 +  uniformly_continuous_on_cmul
   2.175  
   2.176  text{* Continuity in terms of open preimages. *}
   2.177