# HG changeset patch # User huffman # Date 1314898879 25200 # Node ID 897f32a827f29f8fe1354588bf2b5831ebc44d55 # Parent e4de7750cdebc1a7e256dfa734d05ff6af5a7ef2 simplify some proofs about uniform continuity, and add some new ones; rename some theorems according to standard naming scheme; diff -r e4de7750cdeb -r 897f32a827f2 NEWS --- a/NEWS Thu Sep 01 09:02:14 2011 -0700 +++ b/NEWS Thu Sep 01 10:41:19 2011 -0700 @@ -243,6 +243,8 @@ continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] continuous_on_inverse ~> continuous_on_inv + uniformly_continuous_on_neg ~> uniformly_continuous_on_minus + uniformly_continuous_on_sub ~> uniformly_continuous_on_diff subset_interior ~> interior_mono subset_closure ~> closure_mono closure_univ ~> closure_UNIV diff -r e4de7750cdeb -r 897f32a827f2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 01 09:02:14 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Sep 01 10:41:19 2011 -0700 @@ -3253,7 +3253,7 @@ assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto qed -lemma uniformly_continuous_on_sequentially': +lemma uniformly_continuous_on_sequentially: "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ ((\n. dist (x n) (y n)) ---> 0) sequentially \ ((\n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs") @@ -3295,15 +3295,6 @@ thus ?lhs unfolding uniformly_continuous_on_def by blast qed -lemma uniformly_continuous_on_sequentially: - fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" - shows "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ - ((\n. x n - y n) ---> 0) sequentially - \ ((\n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs") -(* BH: maybe the previous lemma should replace this one? *) -unfolding uniformly_continuous_on_sequentially' -unfolding dist_norm tendsto_norm_zero_iff .. - text{* The usual transformation theorems. *} lemma continuous_transform_within: @@ -3330,7 +3321,7 @@ using continuous_transform_within [of d x UNIV f g] assms by (simp add: within_UNIV) -text{* Combination results for pointwise continuity. *} +subsubsection {* Structural rules for pointwise continuity *} lemma continuous_within_id: "continuous (at a within s) (\x. x)" unfolding continuous_within by (rule tendsto_ident_at_within) @@ -3413,7 +3404,7 @@ continuous_inner continuous_euclidean_component continuous_at_inverse continuous_at_within_inverse -text{* Same thing for setwise continuity. *} +subsubsection {* Structural rules for setwise continuity *} lemma continuous_on_id: "continuous_on s (\x. x)" unfolding continuous_on_def by (fast intro: tendsto_ident_at_within) @@ -3486,62 +3477,83 @@ shows "continuous_on s (\x. inverse (f x))" using assms unfolding continuous_on by (fast intro: tendsto_inverse) -text{* Same thing for uniform continuity, using sequential formulations. *} +subsubsection {* Structural rules for uniform continuity *} lemma uniformly_continuous_on_id: - "uniformly_continuous_on s (\x. x)" + shows "uniformly_continuous_on s (\x. x)" unfolding uniformly_continuous_on_def by auto lemma uniformly_continuous_on_const: - "uniformly_continuous_on s (\x. c)" + shows "uniformly_continuous_on s (\x. c)" unfolding uniformly_continuous_on_def by simp +lemma uniformly_continuous_on_dist: + fixes f g :: "'a::metric_space \ 'b::metric_space" + assumes "uniformly_continuous_on s f" + assumes "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. dist (f x) (g x))" +proof - + { fix a b c d :: 'b have "\dist a b - dist c d\ \ dist a c + dist b d" + using dist_triangle2 [of a b c] dist_triangle2 [of b c d] + using dist_triangle3 [of c d a] dist_triangle [of a d b] + by arith + } note le = this + { fix x y + assume f: "(\n. dist (f (x n)) (f (y n))) ----> 0" + assume g: "(\n. dist (g (x n)) (g (y n))) ----> 0" + have "(\n. \dist (f (x n)) (g (x n)) - dist (f (y n)) (g (y n))\) ----> 0" + by (rule Lim_transform_bound [OF _ tendsto_add_zero [OF f g]], + simp add: le) + } + thus ?thesis using assms unfolding uniformly_continuous_on_sequentially + unfolding dist_real_def by simp +qed + +lemma uniformly_continuous_on_norm: + assumes "uniformly_continuous_on s f" + shows "uniformly_continuous_on s (\x. norm (f x))" + unfolding norm_conv_dist using assms + by (intro uniformly_continuous_on_dist uniformly_continuous_on_const) + +lemma (in bounded_linear) uniformly_continuous_on: + assumes "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. f (g x))" + using assms unfolding uniformly_continuous_on_sequentially + unfolding dist_norm tendsto_norm_zero_iff diff[symmetric] + by (auto intro: tendsto_zero) + lemma uniformly_continuous_on_cmul: fixes f :: "'a::metric_space \ 'b::real_normed_vector" assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" -proof- - { fix x y assume "((\n. f (x n) - f (y n)) ---> 0) sequentially" - hence "((\n. c *\<^sub>R f (x n) - c *\<^sub>R f (y n)) ---> 0) sequentially" - using tendsto_scaleR [OF tendsto_const, of "(\n. f (x n) - f (y n))" 0 sequentially c] - unfolding scaleR_zero_right scaleR_right_diff_distrib by auto - } - thus ?thesis using assms unfolding uniformly_continuous_on_sequentially' - unfolding dist_norm tendsto_norm_zero_iff by auto -qed + using bounded_linear_scaleR_right assms + by (rule bounded_linear.uniformly_continuous_on) lemma dist_minus: fixes x y :: "'a::real_normed_vector" shows "dist (- x) (- y) = dist x y" unfolding dist_norm minus_diff_minus norm_minus_cancel .. -lemma uniformly_continuous_on_neg: +lemma uniformly_continuous_on_minus: fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "uniformly_continuous_on s f - ==> uniformly_continuous_on s (\x. -(f x))" + shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. - f x)" unfolding uniformly_continuous_on_def dist_minus . lemma uniformly_continuous_on_add: fixes f g :: "'a::metric_space \ 'b::real_normed_vector" - assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g" + assumes "uniformly_continuous_on s f" + assumes "uniformly_continuous_on s g" shows "uniformly_continuous_on s (\x. f x + g x)" -proof- - { fix x y assume "((\n. f (x n) - f (y n)) ---> 0) sequentially" - "((\n. g (x n) - g (y n)) ---> 0) sequentially" - hence "((\xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially" - using tendsto_add[of "\ n. f (x n) - f (y n)" 0 sequentially "\ n. g (x n) - g (y n)" 0] by auto - hence "((\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 } - thus ?thesis using assms unfolding uniformly_continuous_on_sequentially' - unfolding dist_norm tendsto_norm_zero_iff by auto -qed - -lemma uniformly_continuous_on_sub: + using assms unfolding uniformly_continuous_on_sequentially + unfolding dist_norm tendsto_norm_zero_iff add_diff_add + by (auto intro: tendsto_add_zero) + +lemma uniformly_continuous_on_diff: fixes f :: "'a::metric_space \ 'b::real_normed_vector" - shows "uniformly_continuous_on s f \ uniformly_continuous_on s g - ==> uniformly_continuous_on s (\x. f x - g x)" - unfolding ab_diff_minus - using uniformly_continuous_on_add[of s f "\x. - g x"] - using uniformly_continuous_on_neg[of s g] by auto + assumes "uniformly_continuous_on s f" and "uniformly_continuous_on s g" + shows "uniformly_continuous_on s (\x. f x - g x)" + unfolding ab_diff_minus using assms + by (intro uniformly_continuous_on_add uniformly_continuous_on_minus) text{* Continuity of all kinds is preserved under composition. *} @@ -3587,10 +3599,11 @@ continuous_on_add continuous_on_minus continuous_on_diff continuous_on_scaleR continuous_on_mult continuous_on_inverse continuous_on_inner continuous_on_euclidean_component - uniformly_continuous_on_add uniformly_continuous_on_const - uniformly_continuous_on_id uniformly_continuous_on_compose - uniformly_continuous_on_cmul uniformly_continuous_on_neg - uniformly_continuous_on_sub + uniformly_continuous_on_id uniformly_continuous_on_const + uniformly_continuous_on_dist uniformly_continuous_on_norm + uniformly_continuous_on_compose uniformly_continuous_on_add + uniformly_continuous_on_minus uniformly_continuous_on_diff + uniformly_continuous_on_cmul text{* Continuity in terms of open preimages. *}