# HG changeset patch # User paulson # Date 1456242459 0 # Node ID a6479cb85944c71f64dd4961bb044c7f640c9f63 # Parent 340738057c8cf868f7a228e56da4910c43f179d8 New and revised material for (multivariate) analysis diff -r 340738057c8c -r a6479cb85944 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Limits.thy Tue Feb 23 15:47:39 2016 +0000 @@ -1534,10 +1534,6 @@ text\Transformation of limit.\ -lemma eventually_at2: - "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" - unfolding eventually_at by auto - lemma Lim_transform: fixes a b :: "'a::real_normed_vector" shows "\(g \ a) F; ((\x. f x - g x) \ 0) F\ \ (f \ a) F" diff -r 340738057c8c -r a6479cb85944 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Meson.thy Tue Feb 23 15:47:39 2016 +0000 @@ -93,7 +93,7 @@ subsection \Lemmas for Forward Proof\ -text\There is a similarity to congruence rules\ +text\There is a similarity to congruence rules. They are also useful in ordinary proofs.\ (*NOTE: could handle conjunctions (faster?) by nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) @@ -103,6 +103,9 @@ lemma disj_forward: "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q" by blast +lemma imp_forward: "[| P' \ Q'; P ==> P'; Q' ==> Q |] ==> P \ Q" +by blast + (*Version of @{text disj_forward} for removal of duplicate literals*) lemma disj_forward2: "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q" diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Feb 23 15:47:39 2016 +0000 @@ -1998,7 +1998,7 @@ apply (rule retract_fixpoint_property[OF *, of "\x. scaleR 2 a - x"]) apply (blast intro: brouwer_ball[OF assms]) apply (intro continuous_intros) - unfolding frontier_cball subset_eq Ball_def image_iff dist_norm + unfolding frontier_cball subset_eq Ball_def image_iff dist_norm sphere_def apply (auto simp add: ** norm_minus_commute) done then have "scaleR 2 a = scaleR 1 x + scaleR 1 x" diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Feb 23 15:47:39 2016 +0000 @@ -74,7 +74,7 @@ shows "continuous_on s exp" by (simp add: continuous_on_exp continuous_on_id) -lemma holomorphic_on_exp: "exp holomorphic_on s" +lemma holomorphic_on_exp [holomorphic_intros]: "exp holomorphic_on s" by (simp add: complex_differentiable_within_exp holomorphic_on_def) subsection\Euler and de Moivre formulas.\ diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Feb 23 15:47:39 2016 +0000 @@ -324,10 +324,24 @@ unfolding one_add_one [symmetric] scaleR_left_distrib by simp lemma vector_choose_size: - "0 \ c \ \x::'a::euclidean_space. norm x = c" - apply (rule exI [where x="c *\<^sub>R (SOME i. i \ Basis)"]) - apply (auto simp: SOME_Basis) - done + assumes "0 \ c" + obtains x :: "'a::{real_normed_vector, perfect_space}" where "norm x = c" +proof - + obtain a::'a where "a \ 0" + using UNIV_not_singleton UNIV_eq_I set_zero singletonI by fastforce + then show ?thesis + by (rule_tac x="scaleR (c / norm a) a" in that) (simp add: assms) +qed + +lemma vector_choose_dist: + assumes "0 \ c" + obtains y :: "'a::{real_normed_vector, perfect_space}" where "dist x y = c" +by (metis add_diff_cancel_left' assms dist_commute dist_norm vector_choose_size) + +lemma sphere_eq_empty [simp]: + fixes a :: "'a::{real_normed_vector, perfect_space}" + shows "sphere a r = {} \ r < 0" +by (auto simp: sphere_def dist_norm) (metis dist_norm le_less_linear vector_choose_dist) lemma setsum_delta_notmem: assumes "x \ s" @@ -4300,8 +4314,7 @@ and "\y\s. dist a (closest_point s a) \ dist a y" unfolding closest_point_def apply(rule_tac[!] someI2_ex) - using distance_attains_inf[OF assms(1,2), of a] - apply auto + apply (auto intro: distance_attains_inf[OF assms(1,2), of a]) done lemma closest_point_in_set: "closed s \ s \ {} \ closest_point s a \ s" @@ -4446,9 +4459,8 @@ and "z \ s" shows "\a b. \y\s. inner a z < b \ inner a y = b \ (\x\s. inner a x \ b)" proof - - from distance_attains_inf[OF assms(2-3)] obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" - by auto + by (metis distance_attains_inf[OF assms(2-3)]) show ?thesis apply (rule_tac x="y - z" in exI) apply (rule_tac x="inner (y - z) y" in exI) @@ -4497,7 +4509,7 @@ next case False obtain y where "y \ s" and y: "\x\s. dist z y \ dist z x" - using distance_attains_inf[OF assms(2) False] by auto + by (metis distance_attains_inf[OF assms(2) False]) show ?thesis apply (rule_tac x="y - z" in exI) apply (rule_tac x="inner (y - z) z + (norm (y - z))\<^sup>2 / 2" in exI) @@ -4657,16 +4669,8 @@ shows "\a. a \ 0 \ (\x\s. 0 \ inner a x)" proof - let ?k = "\c. {x::'a. 0 \ inner c x}" - have "frontier (cball 0 1) \ (\(?k ` s)) \ {}" - apply (rule compact_imp_fip) - apply (rule compact_frontier[OF compact_cball]) - defer - apply rule - apply rule - apply (erule conjE) + have *: "frontier (cball 0 1) \ \f \ {}" if as: "f \ ?k ` s" "finite f" for f proof - - fix f - assume as: "f \ ?k ` s" "finite f" obtain c where c: "f = ?k ` c" "c \ s" "finite c" using finite_subset_image[OF as(2,1)] by auto then obtain a b where ab: "a \ 0" "0 < b" "\x\convex hull c. b < inner a x" @@ -4680,14 +4684,17 @@ unfolding subset_eq and inner_scaleR by (auto simp add: inner_commute del: ballE elim!: ballE) then show "frontier (cball 0 1) \ \f \ {}" - unfolding c(1) frontier_cball dist_norm by auto - qed (insert closed_halfspace_ge, auto) + unfolding c(1) frontier_cball sphere_def dist_norm by auto + qed + have "frontier (cball 0 1) \ (\(?k ` s)) \ {}" + apply (rule compact_imp_fip) + apply (rule compact_frontier[OF compact_cball]) + using * closed_halfspace_ge + by auto then obtain x where "norm x = 1" "\y\s. x\?k y" - unfolding frontier_cball dist_norm by auto + unfolding frontier_cball dist_norm sphere_def by auto then show ?thesis - apply (rule_tac x=x in exI) - apply (auto simp add: inner_commute) - done + by (metis inner_commute mem_Collect_eq norm_eq_zero zero_neq_one) qed lemma separating_hyperplane_sets: @@ -9928,8 +9935,9 @@ using assms by blast then have "\x \ s. \y \ t. dist x y \ setdist s t" - using distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms - apply (clarsimp simp: dist_norm le_setdist_iff, blast) + apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]]) + apply (simp add: dist_norm le_setdist_iff) + apply blast done then show ?thesis by (blast intro!: antisym [OF _ setdist_le_dist] ) @@ -10009,5 +10017,4 @@ lemma setdist_le_sing: "x \ s ==> setdist s t \ setdist {x} t" using setdist_subset_left by auto - end diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Feb 23 15:47:39 2016 +0000 @@ -1697,15 +1697,15 @@ also continuous. So if we know for some other reason that the inverse function exists, it's OK.\ -lemma has_derivative_locally_injective: +proposition has_derivative_locally_injective: fixes f :: "'n::euclidean_space \ 'm::euclidean_space" assumes "a \ s" - and "open s" - and "bounded_linear g'" - and "g' \ f' a = id" - and "\x\s. (f has_derivative f' x) (at x)" - and "\e>0. \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e" - obtains t where "a \ t" "open t" "\x\t. \x'\t. f x' = f x \ x' = x" + and "open s" + and "bounded_linear g'" + and "g' \ f' a = id" + and "\x. x \ s \ (f has_derivative f' x) (at x)" + and "\e. e > 0 \ \d>0. \x. dist a x < d \ onorm (\v. f' x v - f' a v) < e" + obtains r where "r > 0" "ball a r \ s" "inj_on f (ball a r)" proof - interpret bounded_linear g' using assms by auto @@ -1738,9 +1738,11 @@ using real_lbound_gt_zero[OF d1(1) d2(1)] by blast show ?thesis proof - show "a \ ball a d" - using d by auto - show "\x\ball a d. \x'\ball a d. f x' = f x \ x' = x" + show "0 < d" by (fact d) + show "ball a d \ s" + using \d < d2\ \ball a d2 \ s\ by auto + show "inj_on f (ball a d)" + unfolding inj_on_def proof (intro strip) fix x y assume as: "x \ ball a d" "y \ ball a d" "f x = f y" @@ -1749,7 +1751,7 @@ unfolding ph_def o_def unfolding diff using f'g' - by (auto simp add: algebra_simps) + by (auto simp: algebra_simps) have "norm (ph x - ph y) \ (1 / 2) * norm (x - y)" apply (rule differentiable_bound[OF convex_ball _ _ as(1-2), where f'="\x v. v - g'(f' x v)"]) apply (rule_tac[!] ballI) @@ -1788,7 +1790,7 @@ using d1(2)[of u] using onorm_neg[where f="\x. f' u x - f' a x"] using d and u and onorm_pos_le[OF assms(3)] - apply (auto simp add: algebra_simps) + apply (auto simp: algebra_simps) done also have "\ \ 1 / 2" unfolding k_def by auto @@ -1804,7 +1806,7 @@ ultimately show "x = y" unfolding norm_minus_commute by auto qed - qed auto + qed qed diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Feb 23 15:47:39 2016 +0000 @@ -1019,7 +1019,7 @@ shows "\e > 0. ball z e \ path_image g = {}" proof - obtain a where "a \ path_image g" "\y \ path_image g. dist z a \ dist z y" - using distance_attains_inf[OF _ path_image_nonempty, of g z] + apply (rule distance_attains_inf[OF _ path_image_nonempty, of g z]) using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto then show ?thesis apply (rule_tac x="dist z a" in exI) @@ -1661,6 +1661,50 @@ apply (auto simp: cball_diff_eq_sphere dist_norm) done +proposition connected_open_delete: + assumes "open S" "connected S" and 2: "2 \ DIM('N::euclidean_space)" + shows "connected(S - {a::'N})" +proof (cases "a \ S") + case True + with \open S\ obtain \ where "\ > 0" and \: "cball a \ \ S" + using open_contains_cball_eq by blast + have "dist a (a + \ *\<^sub>R (SOME i. i \ Basis)) = \" + by (simp add: dist_norm SOME_Basis \0 < \\ less_imp_le) + with \ have "\{S - ball a r |r. 0 < r \ r < \} \ {} \ False" + apply (drule_tac c="a + scaleR (\) ((SOME i. i \ Basis))" in subsetD) + by auto + then have nonemp: "(\{S - ball a r |r. 0 < r \ r < \}) = {} \ False" + by auto + have con: "\r. r < \ \ connected (S - ball a r)" + using \ by (force intro: connected_diff_ball [OF \connected S\ _ 2]) + have "x \ \{S - ball a r |r. 0 < r \ r < \}" if "x \ S - {a}" for x + apply (rule UnionI [of "S - ball a (min \ (dist a x) / 2)"]) + using that \0 < \\ apply (simp_all add:) + apply (rule_tac x="min \ (dist a x) / 2" in exI) + apply auto + done + then have "S - {a} = \{S - ball a r | r. 0 < r \ r < \}" + by auto + then show ?thesis + by (auto intro: connected_Union con dest!: nonemp) +next + case False then show ?thesis + by (simp add: \connected S\) +qed + +corollary path_connected_open_delete: + assumes "open S" "connected S" and 2: "2 \ DIM('N::euclidean_space)" + shows "path_connected(S - {a::'N})" +by (simp add: assms connected_open_delete connected_open_path_connected open_delete) + +corollary path_connected_punctured_ball: + "2 \ DIM('N::euclidean_space) \ path_connected(ball a r - {a::'N})" +by (simp add: path_connected_open_delete) + +lemma connected_punctured_ball: + "2 \ DIM('N::euclidean_space) \ connected(ball a r - {a::'N})" +by (simp add: connected_open_delete) + subsection\Relations between components and path components\ lemma open_connected_component: @@ -1961,7 +2005,10 @@ lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)" by (simp add: Int_commute frontier_def interior_closure) -lemma connected_inter_frontier: +lemma frontier_interior_subset: "frontier(interior S) \ frontier S" + by (simp add: Diff_mono frontier_interiors interior_mono interior_subset) + +lemma connected_Int_frontier: "\connected s; s \ t \ {}; s - t \ {}\ \ (s \ frontier t \ {})" apply (simp add: frontier_interiors connected_open_in, safe) apply (drule_tac x="s \ interior t" in spec, safe) @@ -1969,6 +2016,44 @@ apply (auto simp: disjoint_eq_subset_Compl dest: interior_subset [THEN subsetD]) done +lemma frontier_not_empty: + fixes S :: "'a :: real_normed_vector set" + shows "\S \ {}; S \ UNIV\ \ frontier S \ {}" + using connected_Int_frontier [of UNIV S] by auto + +lemma frontier_eq_empty: + fixes S :: "'a :: real_normed_vector set" + shows "frontier S = {} \ S = {} \ S = UNIV" +using frontier_UNIV frontier_empty frontier_not_empty by blast + +lemma frontier_of_connected_component_subset: + fixes S :: "'a::real_normed_vector set" + shows "frontier(connected_component_set S x) \ frontier S" +proof - + { fix y + assume y1: "y \ closure (connected_component_set S x)" + and y2: "y \ interior (connected_component_set S x)" + have 1: "y \ closure S" + using y1 closure_mono connected_component_subset by blast + have "z \ interior (connected_component_set S x)" + if "0 < e" "ball y e \ interior S" "dist y z < e" for e z + proof - + have "ball y e \ connected_component_set S y" + apply (rule connected_component_maximal) + using that interior_subset mem_ball apply auto + done + then show ?thesis + using y1 apply (simp add: closure_approachable open_contains_ball_eq [OF open_interior]) + by (metis (no_types, hide_lams) connected_component_eq_eq connected_component_in subsetD + dist_commute mem_Collect_eq mem_ball mem_interior \0 < e\ y2) + qed + then have 2: "y \ interior S" + using y2 by (force simp: open_contains_ball_eq [OF open_interior]) + note 1 2 + } + then show ?thesis by (auto simp: frontier_def) +qed + lemma connected_component_UNIV: fixes x :: "'a::real_normed_vector" shows "connected_component_set UNIV x = UNIV" @@ -1992,7 +2077,7 @@ assume x: "x \ interior s" and y: "y \ s" and cc: "connected_component (- frontier s) x y" have "connected_component_set (- frontier s) x \ frontier s \ {}" - apply (rule connected_inter_frontier, simp) + apply (rule connected_Int_frontier, simp) apply (metis IntI cc connected_component_in connected_component_refl empty_iff interiorE mem_Collect_eq set_rev_mp x) using y cc by blast diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Summation.thy --- a/src/HOL/Multivariate_Analysis/Summation.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Summation.thy Tue Feb 23 15:47:39 2016 +0000 @@ -583,7 +583,6 @@ "conv_radius f = liminf (\n. inverse (ereal (root n (norm (f n)))))" by (subst Liminf_inverse_ereal) (simp_all add: real_root_ge_zero conv_radius_def) - lemma abs_summable_in_conv_radius: fixes f :: "nat \ 'a :: {banach, real_normed_div_algebra}" assumes "ereal (norm z) < conv_radius f" @@ -905,7 +904,16 @@ from r have "summable (\n. (\i\n. (f i * of_real r^i) * (g (n - i) * of_real r^(n - i))))" by (intro summable_Cauchy_product abs_summable_in_conv_radius) simp_all thus "summable (\n. (\i\n. f i * g (n - i)) * of_real r ^ n)" - by (simp add: algebra_simps of_real_def scaleR_power power_add [symmetric] scaleR_setsum_right) + by (simp add: algebra_simps of_real_def power_add [symmetric] scaleR_setsum_right) qed +lemma le_conv_radius_iff: + fixes a :: "nat \ 'a::{real_normed_div_algebra,banach}" + shows "r \ conv_radius a \ (\x. norm (x-\) < r \ summable (\i. a i * (x - \) ^ i))" +apply (intro iffI allI impI summable_in_conv_radius conv_radius_geI_ex) +apply (meson less_ereal.simps(1) not_le order_trans) +apply (rule_tac x="of_real ra" in exI, simp) +apply (metis abs_of_nonneg add_diff_cancel_left' less_eq_real_def norm_of_real) +done + end diff -r 340738057c8c -r a6479cb85944 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Feb 22 14:37:56 2016 +0000 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Feb 23 15:47:39 2016 +0000 @@ -897,12 +897,15 @@ lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. +lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" + by (auto simp: open_contains_ball) + lemma openE[elim?]: assumes "open S" "x\S" obtains e where "e>0" "ball x e \ S" using assms unfolding open_contains_ball by auto -lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ S)" +lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" by (metis open_contains_ball subset_eq centre_in_ball) lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" @@ -2251,6 +2254,9 @@ using frontier_complement frontier_subset_eq[of "- S"] unfolding open_closed by auto +lemma frontier_UNIV [simp]: "frontier UNIV = {}" + using frontier_complement frontier_empty by fastforce + subsection \Filters and the ``eventually true'' quantifier\ @@ -2339,7 +2345,7 @@ lemma Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_at2) + by (auto simp add: tendsto_iff eventually_at) lemma Lim_at_infinity: "(f \ l) at_infinity \ (\e>0. \b. \x. norm x \ b \ dist (f x) l < e)" @@ -2355,6 +2361,23 @@ lemma Lim_eventually: "eventually (\x. f x = l) net \ (f \ l) net" by (rule topological_tendstoI, auto elim: eventually_mono) +lemma Lim_transform_within_set: + fixes a l :: "'a::real_normed_vector" + shows "\(f \ l) (at a within s); eventually (\x. x \ s \ x \ t) (at a)\ + \ (f \ l) (at a within t)" +apply (clarsimp simp: eventually_at Lim_within) +apply (drule_tac x=e in spec, clarify) +apply (rename_tac k) +apply (rule_tac x="min d k" in exI) +apply (simp add:) +done + +lemma Lim_transform_within_set_eq: + fixes a l :: "'a::real_normed_vector" + shows "eventually (\x. x \ s \ x \ t) (at a) + \ ((f \ l) (at a within s) \ (f \ l) (at a within t))" +by (force intro: Lim_transform_within_set elim: eventually_mono) + text\The expected monotonicity property.\ lemma Lim_Un: @@ -2514,6 +2537,36 @@ using assms(1) tendsto_norm_zero [OF assms(2)] by (rule Lim_null_comparison) +lemma lim_null_mult_right_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes f: "(f \ 0) F" and g: "eventually (\x. norm(g x) \ B) F" + shows "((\z. f z * g z) \ 0) F" +proof - + have *: "((\x. norm (f x) * B) \ 0) F" + by (simp add: f tendsto_mult_left_zero tendsto_norm_zero) + have "((\x. norm (f x) * norm (g x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_left_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + +lemma lim_null_mult_left_bounded: + fixes f :: "'a \ 'b::real_normed_div_algebra" + assumes g: "eventually (\x. norm(g x) \ B) F" and f: "(f \ 0) F" + shows "((\z. g z * f z) \ 0) F" +proof - + have *: "((\x. B * norm (f x)) \ 0) F" + by (simp add: f tendsto_mult_right_zero tendsto_norm_zero) + have "((\x. norm (g x) * norm (f x)) \ 0) F" + apply (rule Lim_null_comparison [OF _ *]) + apply (simp add: eventually_mono [OF g] mult_right_mono) + done + then show ?thesis + by (subst tendsto_norm_zero_iff [symmetric]) (simp add: norm_mult) +qed + text\Deducing things about the limit from the elements.\ lemma Lim_in_closed_set: @@ -3149,21 +3202,18 @@ by auto qed -lemma frontier_ball: +lemma interior_ball [simp]: "interior (ball x e) = ball x e" + by (simp add: interior_open) + +lemma frontier_ball [simp]: fixes a :: "'a::real_normed_vector" - shows "0 < e \ frontier(ball a e) = {x. dist a x = e}" - apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) - apply (simp add: set_eq_iff) - apply arith - done - -lemma frontier_cball: + shows "0 < e \ frontier (ball a e) = sphere a e" + by (force simp: frontier_def) + +lemma frontier_cball [simp]: fixes a :: "'a::{real_normed_vector, perfect_space}" - shows "frontier (cball a e) = {x. dist a x = e}" - apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) - apply (simp add: set_eq_iff) - apply arith - done + shows "frontier (cball a e) = sphere a e" + by (force simp: frontier_def) lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0" apply (simp add: set_eq_iff not_le) @@ -3340,7 +3390,7 @@ lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" by (metis Diff_subset bounded_subset) -lemma not_bounded_UNIV[simp, intro]: +lemma not_bounded_UNIV[simp]: "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" proof (auto simp add: bounded_pos not_le) obtain x :: 'a where "x \ 0" @@ -4446,6 +4496,11 @@ shows "\compact s; c \ components s\ \ compact c" by (meson bounded_subset closed_components in_components_subset compact_eq_bounded_closed) +lemma not_compact_UNIV[simp]: + fixes s :: "'a::{real_normed_vector,perfect_space,heine_borel} set" + shows "~ compact (UNIV::'a set)" + by (simp add: compact_eq_bounded_closed) + (* TODO: is this lemma necessary? *) lemma bounded_increasing_convergent: fixes s :: "nat \ real" @@ -4927,12 +4982,17 @@ using compact_eq_bounded_closed compact_frontier_bounded by blast +corollary compact_sphere: + fixes a :: "'a::{real_normed_vector,perfect_space,heine_borel}" + shows "compact (sphere a r)" +using compact_frontier [of "cball a r"] by simp + lemma frontier_subset_compact: fixes s :: "'a::heine_borel set" shows "compact s \ frontier s \ s" using frontier_subset_closed compact_eq_bounded_closed by blast - + subsection\Relations among convergence and absolute convergence for power series.\ lemma summable_imp_bounded: @@ -5757,11 +5817,12 @@ lemma continuous_constant_on_closure: fixes f :: "_ \ 'b::t1_space" - assumes "continuous_on (closure s) f" - and "\x \ s. f x = a" - shows "\x \ (closure s). f x = a" - using continuous_closed_preimage_constant[of "closure s" f a] - assms closure_minimal[of s "{x \ closure s. f x = a}"] closure_subset + assumes "continuous_on (closure S) f" + and "\x. x \ S \ f x = a" + and "x \ closure S" + shows "f x = a" + using continuous_closed_preimage_constant[of "closure S" f a] + assms closure_minimal[of S "{x \ closure S. f x = a}"] closure_subset unfolding subset_eq by auto @@ -5851,6 +5912,27 @@ qed qed +subsection \A function constant on a set\ + +definition constant_on (infixl "(constant'_on)" 50) + where "f constant_on A \ \y. \x\A. f x = y" + +lemma constant_on_subset: "\f constant_on A; B \ A\ \ f constant_on B" + unfolding constant_on_def by blast + +lemma injective_not_constant: + fixes S :: "'a::{perfect_space} set" + shows "\open S; inj_on f S; f constant_on S\ \ S = {}" +unfolding constant_on_def +by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def) + +lemma constant_on_closureI: + fixes f :: "_ \ 'b::t1_space" + assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f" + shows "f constant_on (closure S)" +using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def +by metis + text \Making a continuous function avoid some value in a neighbourhood.\ lemma continuous_within_avoid: @@ -6317,25 +6399,24 @@ lemma distance_attains_inf: fixes a :: "'a::heine_borel" - assumes "closed s" - and "s \ {}" - shows "\x\s. \y\s. dist a x \ dist a y" + assumes "closed s" and "s \ {}" + obtains x where "x\s" "\y. y \ s \ dist a x \ dist a y" proof - - from assms(2) obtain b where "b \ s" by auto + from assms obtain b where "b \ s" by auto let ?B = "s \ cball a (dist b a)" have "?B \ {}" using \b \ s\ - by (auto simp add: dist_commute) + by (auto simp: dist_commute) moreover have "continuous_on ?B (dist a)" by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const) moreover have "compact ?B" by (intro closed_inter_compact \closed s\ compact_cball) ultimately obtain x where "x \