src/HOL/Analysis/Elementary_Metric_Spaces.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago) changeset 69981 3dced198b9ec parent 69922 4a9167f377b0 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
 immler@69544  1 (* Author: L C Paulson, University of Cambridge  immler@69544  2  Author: Amine Chaieb, University of Cambridge  immler@69544  3  Author: Robert Himmelmann, TU Muenchen  immler@69544  4  Author: Brian Huffman, Portland State University  immler@69544  5 *)  immler@69544  6 immler@69676  7 chapter \Functional Analysis\  immler@69544  8 immler@69544  9 theory Elementary_Metric_Spaces  immler@69544  10  imports  immler@69616  11  Abstract_Topology_2  immler@69544  12 begin  immler@69544  13 immler@69676  14 section \Elementary Metric Spaces\  immler@69676  15 immler@69544  16 subsection \Open and closed balls\  immler@69544  17 immler@69544  18 definition%important ball :: "'a::metric_space \ real \ 'a set"  immler@69544  19  where "ball x e = {y. dist x y < e}"  immler@69544  20 immler@69544  21 definition%important cball :: "'a::metric_space \ real \ 'a set"  immler@69544  22  where "cball x e = {y. dist x y \ e}"  immler@69544  23 immler@69544  24 definition%important sphere :: "'a::metric_space \ real \ 'a set"  immler@69544  25  where "sphere x e = {y. dist x y = e}"  immler@69544  26 immler@69544  27 lemma mem_ball [simp]: "y \ ball x e \ dist x y < e"  immler@69544  28  by (simp add: ball_def)  immler@69544  29 immler@69544  30 lemma mem_cball [simp]: "y \ cball x e \ dist x y \ e"  immler@69544  31  by (simp add: cball_def)  immler@69544  32 immler@69544  33 lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e"  immler@69544  34  by (simp add: sphere_def)  immler@69544  35 immler@69544  36 lemma ball_trivial [simp]: "ball x 0 = {}"  immler@69544  37  by (simp add: ball_def)  immler@69544  38 immler@69544  39 lemma cball_trivial [simp]: "cball x 0 = {x}"  immler@69544  40  by (simp add: cball_def)  immler@69544  41 immler@69544  42 lemma sphere_trivial [simp]: "sphere x 0 = {x}"  immler@69544  43  by (simp add: sphere_def)  immler@69544  44 immler@69544  45 lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}"  immler@69544  46  using dist_triangle_less_add not_le by fastforce  immler@69544  47 immler@69544  48 lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}"  immler@69544  49  by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball)  immler@69544  50 immler@69544  51 lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}"  immler@69544  52  for a :: "'a::metric_space"  immler@69544  53  by auto  immler@69544  54 immler@69544  55 lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e"  immler@69544  56  by simp  immler@69544  57 immler@69544  58 lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e"  immler@69544  59  by simp  immler@69544  60 immler@69544  61 lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e"  immler@69544  62  by (simp add: subset_eq)  immler@69544  63 immler@69544  64 lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e"  immler@69544  65  by (auto simp: mem_ball mem_cball)  immler@69544  66 immler@69544  67 lemma sphere_cball [simp,intro]: "sphere z r \ cball z r"  immler@69544  68  by force  immler@69544  69 immler@69544  70 lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"  immler@69544  71  by auto  immler@69544  72 immler@69544  73 lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e"  immler@69544  74  by (simp add: subset_eq)  immler@69544  75 immler@69544  76 lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e"  immler@69544  77  by (simp add: subset_eq)  immler@69544  78 immler@69544  79 lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f"  immler@69544  80  by (auto simp: mem_ball mem_cball)  immler@69544  81 immler@69544  82 lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f"  immler@69544  83  by (auto simp: mem_ball mem_cball)  immler@69544  84 immler@69544  85 lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)"  immler@69544  86  unfolding mem_cball  immler@69544  87 proof -  immler@69544  88  have "dist z x \ dist z y + dist y x"  immler@69544  89  by (rule dist_triangle)  immler@69544  90  also assume "dist z y \ b"  immler@69544  91  also assume "dist y x \ a"  immler@69544  92  finally show "dist z x \ b + a" by arith  immler@69544  93 qed  immler@69544  94 immler@69544  95 lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s"  immler@69544  96  by (simp add: set_eq_iff) arith  immler@69544  97 immler@69544  98 lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s"  immler@69544  99  by (simp add: set_eq_iff)  immler@69544  100 immler@69544  101 lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s"  immler@69544  102  by (simp add: set_eq_iff) arith  immler@69544  103 immler@69544  104 lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s"  immler@69544  105  by (simp add: set_eq_iff)  immler@69544  106 immler@69544  107 lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r"  immler@69544  108  by (auto simp: cball_def ball_def dist_commute)  immler@69544  109 immler@69544  110 lemma open_ball [intro, simp]: "open (ball x e)"  immler@69544  111 proof -  immler@69544  112  have "open (dist x - {.. (\x\S. \e>0. ball x e \ S)"  immler@69544  120  by (simp add: open_dist subset_eq mem_ball Ball_def dist_commute)  immler@69544  121 immler@69544  122 lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S"  immler@69544  123  by (auto simp: open_contains_ball)  immler@69544  124 immler@69544  125 lemma openE[elim?]:  immler@69544  126  assumes "open S" "x\S"  immler@69544  127  obtains e where "e>0" "ball x e \ S"  immler@69544  128  using assms unfolding open_contains_ball by auto  immler@69544  129 immler@69544  130 lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)"  immler@69544  131  by (metis open_contains_ball subset_eq centre_in_ball)  immler@69544  132 immler@69544  133 lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0"  immler@69544  134  unfolding mem_ball set_eq_iff  immler@69544  135  apply (simp add: not_less)  immler@69544  136  apply (metis zero_le_dist order_trans dist_self)  immler@69544  137  done  immler@69544  138 immler@69544  139 lemma ball_empty: "e \ 0 \ ball x e = {}" by simp  immler@69544  140 immler@69544  141 lemma closed_cball [iff]: "closed (cball x e)"  immler@69544  142 proof -  immler@69544  143  have "closed (dist x - {..e})"  immler@69544  144  by (intro closed_vimage closed_atMost continuous_intros)  immler@69544  145  also have "dist x - {..e} = cball x e"  immler@69544  146  by auto  immler@69544  147  finally show ?thesis .  immler@69544  148 qed  immler@69544  149 immler@69544  150 lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)"  immler@69544  151 proof -  immler@69544  152  {  immler@69544  153  fix x and e::real  immler@69544  154  assume "x\S" "e>0" "ball x e \ S"  immler@69544  155  then have "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)  immler@69544  156  }  immler@69544  157  moreover  immler@69544  158  {  immler@69544  159  fix x and e::real  immler@69544  160  assume "x\S" "e>0" "cball x e \ S"  immler@69544  161  then have "\d>0. ball x d \ S"  immler@69544  162  unfolding subset_eq  immler@69544  163  apply (rule_tac x="e/2" in exI, auto)  immler@69544  164  done  immler@69544  165  }  immler@69544  166  ultimately show ?thesis  immler@69544  167  unfolding open_contains_ball by auto  immler@69544  168 qed  immler@69544  169 immler@69544  170 lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))"  immler@69544  171  by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball)  immler@69544  172 immler@69544  173 lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)"  immler@69544  174  by (rule eventually_nhds_in_open) simp_all  immler@69544  175 immler@69544  176 lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)"  immler@69544  177  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)  immler@69544  178 immler@69544  179 lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)"  immler@69544  180  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)  immler@69544  181 immler@69544  182 lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y"  immler@69544  183  by (subst at_within_open) auto  immler@69544  184 immler@69544  185 lemma atLeastAtMost_eq_cball:  immler@69544  186  fixes a b::real  immler@69544  187  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"  immler@69544  188  by (auto simp: dist_real_def field_simps mem_cball)  immler@69544  189 immler@69544  190 lemma greaterThanLessThan_eq_ball:  immler@69544  191  fixes a b::real  immler@69544  192  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"  immler@69544  193  by (auto simp: dist_real_def field_simps mem_ball)  immler@69544  194 immler@69611  195 lemma interior_ball [simp]: "interior (ball x e) = ball x e"  immler@69611  196  by (simp add: interior_open)  immler@69611  197 immler@69611  198 lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0"  immler@69611  199  apply (simp add: set_eq_iff not_le)  immler@69611  200  apply (metis zero_le_dist dist_self order_less_le_trans)  immler@69611  201  done  immler@69611  202 immler@69611  203 lemma cball_empty [simp]: "e < 0 \ cball x e = {}"  immler@69611  204  by simp  immler@69611  205 immler@69611  206 lemma cball_sing:  immler@69611  207  fixes x :: "'a::metric_space"  immler@69611  208  shows "e = 0 \ cball x e = {x}"  immler@69611  209  by (auto simp: set_eq_iff)  immler@69611  210 immler@69611  211 lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e"  immler@69611  212  apply (cases "e \ 0")  immler@69611  213  apply (simp add: ball_empty divide_simps)  immler@69611  214  apply (rule subset_ball)  immler@69611  215  apply (simp add: divide_simps)  immler@69611  216  done  immler@69611  217 immler@69611  218 lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e"  immler@69611  219  using ball_divide_subset one_le_numeral by blast  immler@69611  220 immler@69611  221 lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e"  immler@69611  222  apply (cases "e < 0")  immler@69611  223  apply (simp add: divide_simps)  immler@69611  224  apply (rule subset_cball)  immler@69611  225  apply (metis div_by_1 frac_le not_le order_refl zero_less_one)  immler@69611  226  done  immler@69611  227 immler@69611  228 lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e"  immler@69611  229  using cball_divide_subset one_le_numeral by blast  immler@69611  230 immler@69544  231 immler@69544  232 subsection \Limit Points\  immler@69544  233 immler@69544  234 lemma islimpt_approachable:  immler@69544  235  fixes x :: "'a::metric_space"  immler@69544  236  shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)"  immler@69544  237  unfolding islimpt_iff_eventually eventually_at by fast  immler@69544  238 immler@69544  239 lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)"  immler@69544  240  for x :: "'a::metric_space"  immler@69544  241  unfolding islimpt_approachable  immler@69544  242  using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x",  immler@69544  243  THEN arg_cong [where f=Not]]  immler@69544  244  by (simp add: Bex_def conj_commute conj_left_commute)  immler@69544  245 immler@69544  246 lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S"  immler@69544  247  for x :: "'a::metric_space"  immler@69544  248  apply (clarsimp simp add: islimpt_approachable)  immler@69544  249  apply (drule_tac x="e/2" in spec)  immler@69544  250  apply (auto simp: simp del: less_divide_eq_numeral1)  immler@69544  251  apply (drule_tac x="dist x' x" in spec)  immler@69544  252  apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)  immler@69544  253  apply (erule rev_bexI)  immler@69544  254  apply (metis dist_commute dist_triangle_half_r less_trans less_irrefl)  immler@69544  255  done  immler@69544  256 immler@69544  257 lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}"  immler@69544  258  using closed_limpt limpt_of_limpts by blast  immler@69544  259 immler@69544  260 lemma limpt_of_closure: "x islimpt closure S \ x islimpt S"  immler@69544  261  for x :: "'a::metric_space"  immler@69544  262  by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts)  immler@69544  263 immler@69544  264 lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))"  immler@69544  265  apply (simp add: islimpt_eq_acc_point, safe)  immler@69544  266  apply (metis Int_commute open_ball centre_in_ball)  immler@69544  267  by (metis open_contains_ball Int_mono finite_subset inf_commute subset_refl)  immler@69544  268 immler@69544  269 lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))"  immler@69544  270  apply (simp add: islimpt_eq_infinite_ball, safe)  immler@69544  271  apply (meson Int_mono ball_subset_cball finite_subset order_refl)  immler@69544  272  by (metis open_ball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq)  immler@69544  273 immler@69544  274 immler@69611  275 subsection \Perfect Metric Spaces\  immler@69611  276 immler@69611  277 lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r"  immler@69611  278  for x :: "'a::{perfect_space,metric_space}"  immler@69611  279  using islimpt_UNIV [of x] by (simp add: islimpt_approachable)  immler@69611  280 immler@69611  281 lemma cball_eq_sing:  immler@69611  282  fixes x :: "'a::{metric_space,perfect_space}"  immler@69611  283  shows "cball x e = {x} \ e = 0"  immler@69611  284 proof (rule linorder_cases)  immler@69611  285  assume e: "0 < e"  immler@69611  286  obtain a where "a \ x" "dist a x < e"  immler@69611  287  using perfect_choose_dist [OF e] by auto  immler@69611  288  then have "a \ x" "dist x a \ e"  immler@69611  289  by (auto simp: dist_commute)  immler@69611  290  with e show ?thesis by (auto simp: set_eq_iff)  immler@69611  291 qed auto  immler@69611  292 immler@69611  293 immler@69544  294 subsection \?\  immler@69544  295 immler@69544  296 lemma finite_ball_include:  immler@69544  297  fixes a :: "'a::metric_space"  immler@69544  298  assumes "finite S"  immler@69544  299  shows "\e>0. S \ ball a e"  immler@69544  300  using assms  immler@69544  301 proof induction  immler@69544  302  case (insert x S)  immler@69544  303  then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto  immler@69544  304  define e where "e = max e0 (2 * dist a x)"  immler@69544  305  have "e>0" unfolding e_def using \e0>0\ by auto  immler@69544  306  moreover have "insert x S \ ball a e"  immler@69544  307  using e0 \e>0\ unfolding e_def by auto  immler@69544  308  ultimately show ?case by auto  immler@69544  309 qed (auto intro: zero_less_one)  immler@69544  310 immler@69544  311 lemma finite_set_avoid:  immler@69544  312  fixes a :: "'a::metric_space"  immler@69544  313  assumes "finite S"  immler@69544  314  shows "\d>0. \x\S. x \ a \ d \ dist a x"  immler@69544  315  using assms  immler@69544  316 proof induction  immler@69544  317  case (insert x S)  immler@69544  318  then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x"  immler@69544  319  by blast  immler@69544  320  show ?case  immler@69544  321  proof (cases "x = a")  immler@69544  322  case True  immler@69544  323  with \d > 0 \d show ?thesis by auto  immler@69544  324  next  immler@69544  325  case False  immler@69544  326  let ?d = "min d (dist a x)"  immler@69544  327  from False \d > 0\ have dp: "?d > 0"  immler@69544  328  by auto  immler@69544  329  from d have d': "\x\S. x \ a \ ?d \ dist a x"  immler@69544  330  by auto  immler@69544  331  with dp False show ?thesis  immler@69544  332  by (metis insert_iff le_less min_less_iff_conj not_less)  immler@69544  333  qed  immler@69544  334 qed (auto intro: zero_less_one)  immler@69544  335 immler@69544  336 lemma discrete_imp_closed:  immler@69544  337  fixes S :: "'a::metric_space set"  immler@69544  338  assumes e: "0 < e"  immler@69544  339  and d: "\x \ S. \y \ S. dist y x < e \ y = x"  immler@69544  340  shows "closed S"  immler@69544  341 proof -  immler@69544  342  have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x  immler@69544  343  proof -  immler@69544  344  from e have e2: "e/2 > 0" by arith  immler@69544  345  from C[rule_format, OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2"  immler@69544  346  by blast  immler@69544  347  let ?m = "min (e/2) (dist x y) "  immler@69544  348  from e2 y(2) have mp: "?m > 0"  immler@69544  349  by simp  immler@69544  350  from C[OF mp] obtain z where z: "z \ S" "z \ x" "dist z x < ?m"  immler@69544  351  by blast  immler@69544  352  from z y have "dist z y < e"  immler@69544  353  by (intro dist_triangle_lt [where z=x]) simp  immler@69544  354  from d[rule_format, OF y(1) z(1) this] y z show ?thesis  immler@69544  355  by (auto simp: dist_commute)  immler@69544  356  qed  immler@69544  357  then show ?thesis  immler@69544  358  by (metis islimpt_approachable closed_limpt [where 'a='a])  immler@69544  359 qed  immler@69544  360 immler@69544  361 immler@69544  362 subsection \Interior\  immler@69544  363 immler@69544  364 lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)"  immler@69544  365  using open_contains_ball_eq [where S="interior S"]  immler@69544  366  by (simp add: open_subset_interior)  immler@69544  367 immler@69611  368 lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)"  immler@69611  369  by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior  immler@69611  370  subset_trans)  immler@69611  371 immler@69544  372 immler@69544  373 subsection \Frontier\  immler@69544  374 immler@69544  375 lemma frontier_straddle:  immler@69544  376  fixes a :: "'a::metric_space"  immler@69544  377  shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))"  immler@69544  378  unfolding frontier_def closure_interior  immler@69544  379  by (auto simp: mem_interior subset_eq ball_def)  immler@69544  380 immler@69544  381 immler@69544  382 subsection \Limits\  immler@69544  383 immler@69544  384 proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)"  immler@69544  385  by (auto simp: tendsto_iff trivial_limit_eq)  immler@69544  386 immler@69544  387 text \Show that they yield usual definitions in the various cases.\  immler@69544  388 immler@69544  389 proposition Lim_within_le: "(f \ l)(at a within S) \  immler@69544  390  (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)"  immler@69544  391  by (auto simp: tendsto_iff eventually_at_le)  immler@69544  392 immler@69544  393 proposition Lim_within: "(f \ l) (at a within S) \  immler@69544  394  (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)"  immler@69544  395  by (auto simp: tendsto_iff eventually_at)  immler@69544  396 immler@69544  397 corollary Lim_withinI [intro?]:  immler@69544  398  assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e"  immler@69544  399  shows "(f \ l) (at a within S)"  immler@69544  400  apply (simp add: Lim_within, clarify)  immler@69544  401  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)  immler@69544  402  done  immler@69544  403 immler@69544  404 proposition Lim_at: "(f \ l) (at a) \  immler@69544  405  (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)"  immler@69544  406  by (auto simp: tendsto_iff eventually_at)  immler@69544  407 immler@69544  408 lemma Lim_transform_within_set:  immler@69544  409  fixes a :: "'a::metric_space" and l :: "'b::metric_space"  immler@69544  410  shows "$$f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\  immler@69544  411  \ (f \ l) (at a within T)"  immler@69544  412 apply (clarsimp simp: eventually_at Lim_within)  immler@69544  413 apply (drule_tac x=e in spec, clarify)  immler@69544  414 apply (rename_tac k)  immler@69544  415 apply (rule_tac x="min d k" in exI, simp)  immler@69544  416 done  immler@69544  417 immler@69544  418 text \Another limit point characterization.\  immler@69544  419 immler@69544  420 lemma limpt_sequential_inj:  immler@69544  421  fixes x :: "'a::metric_space"  immler@69544  422  shows "x islimpt S \  immler@69544  423  (\f. (\n::nat. f n \ S - {x}) \ inj f \ (f \ x) sequentially)"  immler@69544  424  (is "?lhs = ?rhs")  immler@69544  425 proof  immler@69544  426  assume ?lhs  immler@69544  427  then have "\e>0. \x'\S. x' \ x \ dist x' x < e"  immler@69544  428  by (force simp: islimpt_approachable)  immler@69544  429  then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e"  immler@69544  430  by metis  immler@69544  431  define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))"  immler@69544  432  have [simp]: "f 0 = y 1"  immler@69544  433  "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n  immler@69544  434  by (simp_all add: f_def)  immler@69544  435  have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n  immler@69544  436  proof (induction n)  immler@69544  437  case 0 show ?case  immler@69544  438  by (simp add: y)  immler@69544  439  next  immler@69544  440  case (Suc n) then show ?case  immler@69544  441  apply (auto simp: y)  immler@69544  442  by (metis half_gt_zero_iff inverse_positive_iff_positive less_divide_eq_numeral1(1) min_less_iff_conj y zero_less_dist_iff zero_less_numeral zero_less_power)  immler@69544  443  qed  immler@69544  444  show ?rhs  immler@69544  445  proof (rule_tac x=f in exI, intro conjI allI)  immler@69544  446  show "\n. f n \ S - {x}"  immler@69544  447  using f by blast  immler@69544  448  have "dist (f n) x < dist (f m) x" if "m < n" for m n  immler@69544  449  using that  immler@69544  450  proof (induction n)  immler@69544  451  case 0 then show ?case by simp  immler@69544  452  next  immler@69544  453  case (Suc n)  immler@69544  454  then consider "m < n" | "m = n" using less_Suc_eq by blast  immler@69544  455  then show ?case  immler@69544  456  proof cases  immler@69544  457  assume "m < n"  immler@69544  458  have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"  immler@69544  459  by simp  immler@69544  460  also have "\ < dist (f n) x"  immler@69544  461  by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)  immler@69544  462  also have "\ < dist (f m) x"  immler@69544  463  using Suc.IH \m < n\ by blast  immler@69544  464  finally show ?thesis .  immler@69544  465  next  immler@69544  466  assume "m = n" then show ?case  immler@69544  467  by simp (metis dist_pos_lt f half_gt_zero_iff inverse_positive_iff_positive min_less_iff_conj y zero_less_numeral zero_less_power)  immler@69544  468  qed  immler@69544  469  qed  immler@69544  470  then show "inj f"  immler@69544  471  by (metis less_irrefl linorder_injI)  immler@69544  472  show "f \ x"  immler@69544  473  apply (rule tendstoI)  immler@69544  474  apply (rule_tac c="nat (ceiling(1/e))" in eventually_sequentiallyI)  immler@69544  475  apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]])  immler@69544  476  apply (simp add: field_simps)  immler@69544  477  by (meson le_less_trans mult_less_cancel_left not_le of_nat_less_two_power)  immler@69544  478  qed  immler@69544  479 next  immler@69544  480  assume ?rhs  immler@69544  481  then show ?lhs  immler@69544  482  by (fastforce simp add: islimpt_approachable lim_sequentially)  immler@69544  483 qed  immler@69544  484 immler@69544  485 lemma Lim_dist_ubound:  immler@69544  486  assumes "\(trivial_limit net)"  immler@69544  487  and "(f \ l) net"  immler@69544  488  and "eventually (\x. dist a (f x) \ e) net"  immler@69544  489  shows "dist a l \ e"  immler@69544  490  using assms by (fast intro: tendsto_le tendsto_intros)  immler@69544  491 immler@69544  492 immler@69613  493 subsection \Continuity\  immler@69613  494 immler@69613  495 text\Derive the epsilon-delta forms, which we often use as "definitions"\  immler@69613  496 immler@69613  497 proposition continuous_within_eps_delta:  immler@69613  498  "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)"  immler@69613  499  unfolding continuous_within and Lim_within by fastforce  immler@69613  500 immler@69613  501 corollary continuous_at_eps_delta:  immler@69613  502  "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)"  immler@69613  503  using continuous_within_eps_delta [of x UNIV f] by simp  immler@69613  504 immler@69613  505 lemma continuous_at_right_real_increasing:  immler@69613  506  fixes f :: "real \ real"  immler@69613  507  assumes nondecF: "\x y. x \ y \ f x \ f y"  immler@69613  508  shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)"  immler@69613  509  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)  immler@69613  510  apply (intro all_cong ex_cong, safe)  immler@69613  511  apply (erule_tac x="a + d" in allE, simp)  immler@69613  512  apply (simp add: nondecF field_simps)  immler@69613  513  apply (drule nondecF, simp)  immler@69613  514  done  immler@69613  515 immler@69613  516 lemma continuous_at_left_real_increasing:  immler@69613  517  assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)"  immler@69613  518  shows "(continuous (at_left (a :: real)) f) = (\e > 0. \delta > 0. f a - f (a - delta) < e)"  immler@69613  519  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)  immler@69613  520  apply (intro all_cong ex_cong, safe)  immler@69613  521  apply (erule_tac x="a - d" in allE, simp)  immler@69613  522  apply (simp add: nondecF field_simps)  immler@69613  523  apply (cut_tac x="a - d" and y=x in nondecF, simp_all)  immler@69613  524  done  immler@69613  525 immler@69613  526 text\Versions in terms of open balls.\  immler@69613  527 immler@69613  528 lemma continuous_within_ball:  immler@69613  529  "continuous (at x within s) f \  immler@69613  530  (\e > 0. \d > 0. f  (ball x d \ s) \ ball (f x) e)"  immler@69613  531  (is "?lhs = ?rhs")  immler@69613  532 proof  immler@69613  533  assume ?lhs  immler@69613  534  {  immler@69613  535  fix e :: real  immler@69613  536  assume "e > 0"  immler@69613  537  then obtain d where d: "d>0" "\xa\s. 0 < dist xa x \ dist xa x < d \ dist (f xa) (f x) < e"  immler@69613  538  using \?lhs$unfolded continuous_within Lim_within] by auto  immler@69613  539  {  immler@69613  540  fix y  immler@69613  541  assume "y \ f  (ball x d \ s)"  immler@69613  542  then have "y \ ball (f x) e"  immler@69613  543  using d(2)  immler@69613  544  apply (auto simp: dist_commute)  immler@69613  545  apply (erule_tac x=xa in ballE, auto)  immler@69613  546  using \e > 0\  immler@69613  547  apply auto  immler@69613  548  done  immler@69613  549  }  immler@69613  550  then have "\d>0. f  (ball x d \ s) \ ball (f x) e"  immler@69613  551  using \d > 0\  immler@69613  552  unfolding subset_eq ball_def by (auto simp: dist_commute)  immler@69613  553  }  immler@69613  554  then show ?rhs by auto  immler@69613  555 next  immler@69613  556  assume ?rhs  immler@69613  557  then show ?lhs  immler@69613  558  unfolding continuous_within Lim_within ball_def subset_eq  immler@69613  559  apply (auto simp: dist_commute)  immler@69613  560  apply (erule_tac x=e in allE, auto)  immler@69613  561  done  immler@69613  562 qed  immler@69613  563 immler@69613  564 lemma continuous_at_ball:  immler@69613  565  "continuous (at x) f \ (\e>0. \d>0. f  (ball x d) \ ball (f x) e)" (is "?lhs = ?rhs")  immler@69613  566 proof  immler@69613  567  assume ?lhs  immler@69613  568  then show ?rhs  immler@69613  569  unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball  immler@69613  570  apply auto  immler@69613  571  apply (erule_tac x=e in allE, auto)  immler@69613  572  apply (rule_tac x=d in exI, auto)  immler@69613  573  apply (erule_tac x=xa in allE)  immler@69613  574  apply (auto simp: dist_commute)  immler@69613  575  done  immler@69613  576 next  immler@69613  577  assume ?rhs  immler@69613  578  then show ?lhs  immler@69613  579  unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball  immler@69613  580  apply auto  immler@69613  581  apply (erule_tac x=e in allE, auto)  immler@69613  582  apply (rule_tac x=d in exI, auto)  immler@69613  583  apply (erule_tac x="f xa" in allE)  immler@69613  584  apply (auto simp: dist_commute)  immler@69613  585  done  immler@69613  586 qed  immler@69613  587 immler@69613  588 text\Define setwise continuity in terms of limits within the set.\  immler@69613  589 immler@69613  590 lemma continuous_on_iff:  immler@69613  591  "continuous_on s f \  immler@69613  592  (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)"  immler@69613  593  unfolding continuous_on_def Lim_within  immler@69613  594  by (metis dist_pos_lt dist_self)  immler@69613  595 immler@69613  596 lemma continuous_within_E:  immler@69613  597  assumes "continuous (at x within s) f" "e>0"  immler@69613  598  obtains d where "d>0" "\x'. \x'\ s; dist x' x \ d\ \ dist (f x') (f x) < e"  immler@69613  599  using assms apply (simp add: continuous_within_eps_delta)  immler@69613  600  apply (drule spec [of _ e], clarify)  immler@69613  601  apply (rule_tac d="d/2" in that, auto)  immler@69613  602  done  immler@69613  603 immler@69613  604 lemma continuous_onI [intro?]:  immler@69613  605  assumes "\x e. \e > 0; x \ s\ \ \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) \ e"  immler@69613  606  shows "continuous_on s f"  immler@69613  607 apply (simp add: continuous_on_iff, clarify)  immler@69613  608 apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)  immler@69613  609 done  immler@69613  610 immler@69613  611 text\Some simple consequential lemmas.\  immler@69613  612 immler@69613  613 lemma continuous_onE:  immler@69613  614  assumes "continuous_on s f" "x\s" "e>0"  immler@69613  615  obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e"  immler@69613  616  using assms  immler@69613  617  apply (simp add: continuous_on_iff)  immler@69613  618  apply (elim ballE allE)  immler@69613  619  apply (auto intro: that [where d="d/2" for d])  immler@69613  620  done  immler@69613  621 immler@69613  622 text\The usual transformation theorems.\  immler@69613  623 immler@69613  624 lemma continuous_transform_within:  immler@69613  625  fixes f g :: "'a::metric_space \ 'b::topological_space"  immler@69613  626  assumes "continuous (at x within s) f"  immler@69613  627  and "0 < d"  immler@69613  628  and "x \ s"  immler@69613  629  and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'"  immler@69613  630  shows "continuous (at x within s) g"  immler@69613  631  using assms  immler@69613  632  unfolding continuous_within  immler@69613  633  by (force intro: Lim_transform_within)  immler@69613  634 immler@69613  635 immler@69544  636 subsection \Closure and Limit Characterization\  immler@69544  637 immler@69544  638 lemma closure_approachable:  immler@69544  639  fixes S :: "'a::metric_space set"  immler@69544  640  shows "x \ closure S \ (\e>0. \y\S. dist y x < e)"  immler@69544  641  apply (auto simp: closure_def islimpt_approachable)  immler@69544  642  apply (metis dist_self)  immler@69544  643  done  immler@69544  644 immler@69544  645 lemma closure_approachable_le:  immler@69544  646  fixes S :: "'a::metric_space set"  immler@69544  647  shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)"  immler@69544  648  unfolding closure_approachable  immler@69544  649  using dense by force  immler@69544  650 immler@69544  651 lemma closure_approachableD:  immler@69544  652  assumes "x \ closure S" "e>0"  immler@69544  653  shows "\y\S. dist x y < e"  immler@69544  654  using assms unfolding closure_approachable by (auto simp: dist_commute)  immler@69544  655 immler@69544  656 lemma closed_approachable:  immler@69544  657  fixes S :: "'a::metric_space set"  immler@69544  658  shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S"  immler@69544  659  by (metis closure_closed closure_approachable)  immler@69544  660 immler@69544  661 lemma closure_contains_Inf:  immler@69544  662  fixes S :: "real set"  immler@69544  663  assumes "S \ {}" "bdd_below S"  immler@69544  664  shows "Inf S \ closure S"  immler@69544  665 proof -  immler@69544  666  have *: "\x\S. Inf S \ x"  immler@69544  667  using cInf_lower[of _ S] assms by metis  immler@69544  668  {  immler@69544  669  fix e :: real  immler@69544  670  assume "e > 0"  immler@69544  671  then have "Inf S < Inf S + e" by simp  immler@69544  672  with assms obtain x where "x \ S" "x < Inf S + e"  immler@69544  673  by (subst (asm) cInf_less_iff) auto  immler@69544  674  with * have "\x\S. dist x (Inf S) < e"  immler@69544  675  by (intro bexI[of _ x]) (auto simp: dist_real_def)  immler@69544  676  }  immler@69544  677  then show ?thesis unfolding closure_approachable by auto  immler@69544  678 qed  immler@69544  679 immler@69544  680 lemma not_trivial_limit_within_ball:  immler@69544  681  "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})"  immler@69544  682  (is "?lhs \ ?rhs")  immler@69544  683 proof  immler@69544  684  show ?rhs if ?lhs  immler@69544  685  proof -  immler@69544  686  {  immler@69544  687  fix e :: real  immler@69544  688  assume "e > 0"  immler@69544  689  then obtain y where "y \ S - {x}" and "dist y x < e"  immler@69544  690  using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]  immler@69544  691  by auto  immler@69544  692  then have "y \ S \ ball x e - {x}"  immler@69544  693  unfolding ball_def by (simp add: dist_commute)  immler@69544  694  then have "S \ ball x e - {x} \ {}" by blast  immler@69544  695  }  immler@69544  696  then show ?thesis by auto  immler@69544  697  qed  immler@69544  698  show ?lhs if ?rhs  immler@69544  699  proof -  immler@69544  700  {  immler@69544  701  fix e :: real  immler@69544  702  assume "e > 0"  immler@69544  703  then obtain y where "y \ S \ ball x e - {x}"  immler@69544  704  using \?rhs\ by blast  immler@69544  705  then have "y \ S - {x}" and "dist y x < e"  immler@69544  706  unfolding ball_def by (simp_all add: dist_commute)  immler@69544  707  then have "\y \ S - {x}. dist y x < e"  immler@69544  708  by auto  immler@69544  709  }  immler@69544  710  then show ?thesis  immler@69544  711  using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]  immler@69544  712  by auto  immler@69544  713  qed  immler@69544  714 qed  immler@69544  715 immler@69613  716 immler@69544  717 subsection \Boundedness\  immler@69544  718 immler@69544  719  (* FIXME: This has to be unified with BSEQ!! *)  immler@69544  720 definition%important (in metric_space) bounded :: "'a set \ bool"  immler@69544  721  where "bounded S \ (\x e. \y\S. dist x y \ e)"  immler@69544  722 immler@69544  723 lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)"  immler@69544  724  unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist)  immler@69544  725 immler@69544  726 lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)"  immler@69544  727  unfolding bounded_def  immler@69544  728  by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)  immler@69544  729 immler@69544  730 lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)"  immler@69544  731  unfolding bounded_any_center [where a=0]  immler@69544  732  by (simp add: dist_norm)  immler@69544  733 immler@69544  734 lemma bdd_above_norm: "bdd_above (norm  X) \ bounded X"  immler@69544  735  by (simp add: bounded_iff bdd_above_def)  immler@69544  736 immler@69544  737 lemma bounded_norm_comp: "bounded ((\x. norm (f x))  S) = bounded (f  S)"  immler@69544  738  by (simp add: bounded_iff)  immler@69544  739 immler@69544  740 lemma boundedI:  immler@69544  741  assumes "\x. x \ S \ norm x \ B"  immler@69544  742  shows "bounded S"  immler@69544  743  using assms bounded_iff by blast  immler@69544  744 immler@69544  745 lemma bounded_empty [simp]: "bounded {}"  immler@69544  746  by (simp add: bounded_def)  immler@69544  747 immler@69544  748 lemma bounded_subset: "bounded T \ S \ T \ bounded S"  immler@69544  749  by (metis bounded_def subset_eq)  immler@69544  750 immler@69544  751 lemma bounded_interior[intro]: "bounded S \ bounded(interior S)"  immler@69544  752  by (metis bounded_subset interior_subset)  immler@69544  753 immler@69544  754 lemma bounded_closure[intro]:  immler@69544  755  assumes "bounded S"  immler@69544  756  shows "bounded (closure S)"  immler@69544  757 proof -  immler@69544  758  from assms obtain x and a where a: "\y\S. dist x y \ a"  immler@69544  759  unfolding bounded_def by auto  immler@69544  760  {  immler@69544  761  fix y  immler@69544  762  assume "y \ closure S"  immler@69544  763  then obtain f where f: "\n. f n \ S" "(f \ y) sequentially"  immler@69544  764  unfolding closure_sequential by auto  immler@69544  765  have "\n. f n \ S \ dist x (f n) \ a" using a by simp  immler@69544  766  then have "eventually (\n. dist x (f n) \ a) sequentially"  immler@69544  767  by (simp add: f(1))  immler@69544  768  have "dist x y \ a"  immler@69544  769  apply (rule Lim_dist_ubound [of sequentially f])  immler@69544  770  apply (rule trivial_limit_sequentially)  immler@69544  771  apply (rule f(2))  immler@69544  772  apply fact  immler@69544  773  done  immler@69544  774  }  immler@69544  775  then show ?thesis  immler@69544  776  unfolding bounded_def by auto  immler@69544  777 qed  immler@69544  778 immler@69544  779 lemma bounded_closure_image: "bounded (f  closure S) \ bounded (f  S)"  immler@69544  780  by (simp add: bounded_subset closure_subset image_mono)  immler@69544  781 immler@69544  782 lemma bounded_cball[simp,intro]: "bounded (cball x e)"  immler@69544  783  apply (simp add: bounded_def)  immler@69544  784  apply (rule_tac x=x in exI)  immler@69544  785  apply (rule_tac x=e in exI, auto)  immler@69544  786  done  immler@69544  787 immler@69544  788 lemma bounded_ball[simp,intro]: "bounded (ball x e)"  immler@69544  789  by (metis ball_subset_cball bounded_cball bounded_subset)  immler@69544  790 immler@69544  791 lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T"  immler@69544  792  by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)  immler@69544  793 immler@69544  794 lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)"  immler@69544  795  by (induct rule: finite_induct[of F]) auto  immler@69544  796 immler@69544  797 lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)"  immler@69544  798  by (induct set: finite) auto  immler@69544  799 immler@69544  800 lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S"  immler@69544  801 proof -  immler@69544  802  have "\y\{x}. dist x y \ 0"  immler@69544  803  by simp  immler@69544  804  then have "bounded {x}"  immler@69544  805  unfolding bounded_def by fast  immler@69544  806  then show ?thesis  immler@69544  807  by (metis insert_is_Un bounded_Un)  immler@69544  808 qed  immler@69544  809 immler@69544  810 lemma bounded_subset_ballI: "S \ ball x r \ bounded S"  immler@69544  811  by (meson bounded_ball bounded_subset)  immler@69544  812 immler@69544  813 lemma bounded_subset_ballD:  immler@69544  814  assumes "bounded S" shows "\r. 0 < r \ S \ ball x r"  immler@69544  815 proof -  immler@69544  816  obtain e::real and y where "S \ cball y e" "0 \ e"  immler@69544  817  using assms by (auto simp: bounded_subset_cball)  immler@69544  818  then show ?thesis  immler@69544  819  apply (rule_tac x="dist x y + e + 1" in exI)  immler@69544  820  apply (simp add: add.commute add_pos_nonneg)  immler@69544  821  apply (erule subset_trans)  immler@69544  822  apply (clarsimp simp add: cball_def)  immler@69544  823  by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)  immler@69544  824 qed  immler@69544  825 immler@69544  826 lemma finite_imp_bounded [intro]: "finite S \ bounded S"  immler@69544  827  by (induct set: finite) simp_all  immler@69544  828 immler@69544  829 lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)"  immler@69544  830  by (metis Int_lower1 Int_lower2 bounded_subset)  immler@69544  831 immler@69544  832 lemma bounded_diff[intro]: "bounded S \ bounded (S - T)"  immler@69544  833  by (metis Diff_subset bounded_subset)  immler@69544  834 immler@69544  835 lemma bounded_dist_comp:  immler@69544  836  assumes "bounded (f  S)" "bounded (g  S)"  immler@69544  837  shows "bounded ((\x. dist (f x) (g x))  S)"  immler@69544  838 proof -  immler@69544  839  from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x  immler@69544  840  by (auto simp: bounded_any_center[of _ undefined] dist_commute)  immler@69544  841  have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x  immler@69544  842  using *[OF that]  immler@69544  843  by (rule order_trans[OF dist_triangle add_mono])  immler@69544  844  then show ?thesis  immler@69544  845  by (auto intro!: boundedI)  immler@69544  846 qed  immler@69544  847 immler@69613  848 lemma bounded_Times:  immler@69613  849  assumes "bounded s" "bounded t"  immler@69613  850  shows "bounded (s \ t)"  immler@69613  851 proof -  immler@69613  852  obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b"  immler@69613  853  using assms [unfolded bounded_def] by auto  immler@69613  854  then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)"  immler@69613  855  by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)  immler@69613  856  then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto  immler@69613  857 qed  immler@69611  858 immler@69611  859 immler@69544  860 subsection \Compactness\  immler@69544  861 immler@69544  862 lemma compact_imp_bounded:  immler@69544  863  assumes "compact U"  immler@69544  864  shows "bounded U"  immler@69544  865 proof -  immler@69544  866  have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)"  immler@69544  867  using assms by auto  immler@69544  868  then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)"  immler@69544  869  by (metis compactE_image)  immler@69544  870  from \finite D\ have "bounded (\x\D. ball x 1)"  immler@69544  871  by (simp add: bounded_UN)  immler@69544  872  then show "bounded U" using \U \ (\x\D. ball x 1)\  immler@69544  873  by (rule bounded_subset)  immler@69544  874 qed  immler@69544  875 immler@69544  876 lemma closure_Int_ball_not_empty:  immler@69544  877  assumes "S \ closure T" "x \ S" "r > 0"  immler@69544  878  shows "T \ ball x r \ {}"  immler@69544  879  using assms centre_in_ball closure_iff_nhds_not_empty by blast  immler@69544  880 immler@69613  881 lemma compact_sup_maxdistance:  immler@69613  882  fixes s :: "'a::metric_space set"  immler@69613  883  assumes "compact s"  immler@69613  884  and "s \ {}"  immler@69613  885  shows "\x\s. \y\s. \u\s. \v\s. dist u v \ dist x y"  immler@69613  886 proof -  immler@69613  887  have "compact (s \ s)"  immler@69613  888  using \compact s\ by (intro compact_Times)  immler@69613  889  moreover have "s \ s \ {}"  immler@69613  890  using \s \ {}\ by auto  immler@69613  891  moreover have "continuous_on (s \ s) (\x. dist (fst x) (snd x))"  immler@69613  892  by (intro continuous_at_imp_continuous_on ballI continuous_intros)  immler@69613  893  ultimately show ?thesis  immler@69613  894  using continuous_attains_sup[of "s \ s" "\x. dist (fst x) (snd x)"] by auto  immler@69613  895 qed  immler@69613  896 immler@69613  897 immler@69544  898 subsubsection\Totally bounded\  immler@69544  899 immler@69544  900 lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N \ dist (s m) (s n) < e)"  immler@69544  901  unfolding Cauchy_def by metis  immler@69544  902 immler@69544  903 proposition seq_compact_imp_totally_bounded:  immler@69544  904  assumes "seq_compact s"  immler@69544  905  shows "\e>0. \k. finite k \ k \ s \ s \ (\x\k. ball x e)"  immler@69544  906 proof -  immler@69544  907  { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ s \ \ s \ (\x\k. ball x e)"  immler@69544  908  let ?Q = "\x n r. r \ s \ (\m < (n::nat). \ (dist (x m) r < e))"  immler@69544  909  have "\x. \n::nat. ?Q x n (x n)"  immler@69544  910  proof (rule dependent_wellorder_choice)  immler@69544  911  fix n x assume "\y. y < n \ ?Q x y (x y)"  immler@69544  912  then have "\ s \ (\x\x  {0..s" "z \ (\x\x  {0..r. ?Q x n r"  immler@69544  917  using z by auto  immler@69544  918  qed simp  immler@69544  919  then obtain x where "\n::nat. x n \ s" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)"  immler@69544  920  by blast  immler@69544  921  then obtain l r where "l \ s" and r:"strict_mono r" and "((x \ r) \ l) sequentially"  immler@69544  922  using assms by (metis seq_compact_def)  immler@69544  923  from this(3) have "Cauchy (x \ r)"  immler@69544  924  using LIMSEQ_imp_Cauchy by auto  immler@69544  925  then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e"  immler@69544  926  unfolding cauchy_def using \e > 0\ by blast  immler@69544  927  then have False  immler@69544  928  using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }  immler@69544  929  then show ?thesis  immler@69544  930  by metis  immler@69544  931 qed  immler@69544  932 immler@69544  933 subsubsection\Heine-Borel theorem\  immler@69544  934 immler@69544  935 proposition seq_compact_imp_Heine_Borel:  immler@69544  936  fixes s :: "'a :: metric_space set"  immler@69544  937  assumes "seq_compact s"  immler@69544  938  shows "compact s"  immler@69544  939 proof -  immler@69544  940  from seq_compact_imp_totally_bounded[OF \seq_compact s$  immler@69544  941  obtain f where f: "\e>0. finite (f e) \ f e \ s \ s \ (\x\f e. ball x e)"  immler@69544  942  unfolding choice_iff' ..  immler@69544  943  define K where "K = (\(x, r). ball x r)  ((\e \ \ \ {0 <..}. f e) \$$"  immler@69544  944  have "countably_compact s"  immler@69544  945  using \seq_compact s\ by (rule seq_compact_imp_countably_compact)  immler@69544  946  then show "compact s"  immler@69544  947  proof (rule countably_compact_imp_compact)  immler@69544  948  show "countable K"  immler@69544  949  unfolding K_def using f  immler@69544  950  by (auto intro: countable_finite countable_subset countable_rat  immler@69544  951  intro!: countable_image countable_SIGMA countable_UN)  immler@69544  952  show "\b\K. open b" by (auto simp: K_def)  immler@69544  953  next  immler@69544  954  fix T x  immler@69544  955  assume T: "open T" "x \ T" and x: "x \ s"  immler@69544  956  from openE[OF T] obtain e where "0 < e" "ball x e \ T"  immler@69544  957  by auto  immler@69544  958  then have "0 < e / 2" "ball x (e / 2) \ T"  immler@69544  959  by auto  immler@69544  960  from Rats_dense_in_real[OF \0 < e / 2\] obtain r where "r \ \" "0 < r" "r < e / 2"  immler@69544  961  by auto  immler@69544  962  from f[rule_format, of r] \0 < r\ \x \ s\ obtain k where "k \ f r" "x \ ball k r"  immler@69544  963  by auto  immler@69544  964  from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K"  immler@69544  965  by (auto simp: K_def)  immler@69544  966  then show "\b\K. x \ b \ b \ s \ T"  immler@69544  967  proof (rule bexI[rotated], safe)  immler@69544  968  fix y  immler@69544  969  assume "y \ ball k r"  immler@69544  970  with \r < e / 2\ \x \ ball k r\ have "dist x y < e"  immler@69544  971  by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute)  immler@69544  972  with \ball x e \ T\ show "y \ T"  immler@69544  973  by auto  immler@69544  974  next  immler@69544  975  show "x \ ball k r" by fact  immler@69544  976  qed  immler@69544  977  qed  immler@69544  978 qed  immler@69544  979 immler@69544  980 proposition compact_eq_seq_compact_metric:  immler@69544  981  "compact (s :: 'a::metric_space set) \ seq_compact s"  immler@69544  982  using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast  immler@69544  983 immler@69544  984 proposition compact_def: \ \this is the definition of compactness in HOL Light\  immler@69544  985  "compact (S :: 'a::metric_space set) \  immler@69544  986  (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))"  immler@69544  987  unfolding compact_eq_seq_compact_metric seq_compact_def by auto  immler@69544  988 immler@69544  989 subsubsection \Complete the chain of compactness variants\  immler@69544  990 immler@69544  991 proposition compact_eq_Bolzano_Weierstrass:  immler@69544  992  fixes s :: "'a::metric_space set"  immler@69544  993  shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))"  immler@69544  994  (is "?lhs = ?rhs")  immler@69544  995 proof  immler@69544  996  assume ?lhs  immler@69544  997  then show ?rhs  immler@69544  998  using Heine_Borel_imp_Bolzano_Weierstrass[of s] by auto  immler@69544  999 next  immler@69544  1000  assume ?rhs  immler@69544  1001  then show ?lhs  immler@69544  1002  unfolding compact_eq_seq_compact_metric by (rule Bolzano_Weierstrass_imp_seq_compact)  immler@69544  1003 qed  immler@69544  1004 immler@69544  1005 proposition Bolzano_Weierstrass_imp_bounded:  immler@69544  1006  "\t. infinite t \ t \ s \ (\x \ s. x islimpt t) \ bounded s"  immler@69544  1007  using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass .  immler@69544  1008 immler@69544  1009 immler@69613  1010 subsection \Banach fixed point theorem\  immler@69613  1011   immler@69613  1012 theorem banach_fix:\ \TODO: rename to \Banach_fix\\  immler@69613  1013  assumes s: "complete s" "s \ {}"  immler@69613  1014  and c: "0 \ c" "c < 1"  immler@69613  1015  and f: "f  s \ s"  immler@69613  1016  and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y"  immler@69613  1017  shows "\!x\s. f x = x"  immler@69613  1018 proof -  immler@69613  1019  from c have "1 - c > 0" by simp  immler@69613  1020 immler@69613  1021  from s(2) obtain z0 where z0: "z0 \ s" by blast  immler@69613  1022  define z where "z n = (f ^^ n) z0" for n  immler@69613  1023  with f z0 have z_in_s: "z n \ s" for n :: nat  immler@69613  1024  by (induct n) auto  immler@69613  1025  define d where "d = dist (z 0) (z 1)"  immler@69613  1026 immler@69613  1027  have fzn: "f (z n) = z (Suc n)" for n  immler@69613  1028  by (simp add: z_def)  immler@69613  1029  have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat  immler@69613  1030  proof (induct n)  immler@69613  1031  case 0  immler@69613  1032  then show ?case  immler@69613  1033  by (simp add: d_def)  immler@69613  1034  next  immler@69613  1035  case (Suc m)  immler@69613  1036  with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d"  immler@69613  1037  using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp  immler@69613  1038  then show ?case  immler@69613  1039  using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]  immler@69613  1040  by (simp add: fzn mult_le_cancel_left)  immler@69613  1041  qed  immler@69613  1042 immler@69613  1043  have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat  immler@69613  1044  proof (induct n)  immler@69613  1045  case 0  immler@69613  1046  show ?case by simp  immler@69613  1047  next  immler@69613  1048  case (Suc k)  immler@69613  1049  from c have "(1 - c) * dist (z m) (z (m + Suc k)) \  immler@69613  1050  (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))"  immler@69613  1051  by (simp add: dist_triangle)  immler@69613  1052  also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)"  immler@69613  1053  by simp  immler@69613  1054  also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d"  immler@69613  1055  by (simp add: field_simps)  immler@69613  1056  also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"  immler@69613  1057  by (simp add: power_add field_simps)  immler@69613  1058  also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)"  immler@69613  1059  by (simp add: field_simps)  immler@69613  1060  finally show ?case by simp  immler@69613  1061  qed  immler@69613  1062 immler@69613  1063  have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e  immler@69613  1064  proof (cases "d = 0")  immler@69613  1065  case True  immler@69613  1066  from \1 - c > 0\ have "(1 - c) * x \ 0 \ x \ 0" for x  immler@69613  1067  by (metis mult_zero_left mult.commute real_mult_le_cancel_iff1)  immler@69613  1068  with c cf_z2[of 0] True have "z n = z0" for n  immler@69613  1069  by (simp add: z_def)  immler@69613  1070  with \e > 0\ show ?thesis by simp  immler@69613  1071  next  immler@69613  1072  case False  immler@69613  1073  with zero_le_dist[of "z 0" "z 1"] have "d > 0"  immler@69613  1074  by (metis d_def less_le)  immler@69613  1075  with \1 - c > 0\ \e > 0\ have "0 < e * (1 - c) / d"  immler@69613  1076  by simp  immler@69613  1077  with c obtain N where N: "c ^ N < e * (1 - c) / d"  immler@69613  1078  using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto  immler@69613  1079  have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat  immler@69613  1080  proof -  immler@69613  1081  from c \n \ N\ have *: "c ^ n \ c ^ N"  immler@69613  1082  using power_decreasing[OF \n\N\, of c] by simp  immler@69613  1083  from c \m > n\ have "1 - c ^ (m - n) > 0"  immler@69613  1084  using power_strict_mono[of c 1 "m - n"] by simp  immler@69613  1085  with \d > 0\ \0 < 1 - c\ have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"  immler@69613  1086  by simp  immler@69613  1087  from cf_z2[of n "m - n"] \m > n\  immler@69613  1088  have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"  immler@69613  1089  by (simp add: pos_le_divide_eq[OF \1 - c > 0\] mult.commute dist_commute)  immler@69613  1090  also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"  immler@69613  1091  using mult_right_mono[OF * order_less_imp_le[OF **]]  immler@69613  1092  by (simp add: mult.assoc)  immler@69613  1093  also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"  immler@69613  1094  using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)  immler@69613  1095  also from c \d > 0\ \1 - c > 0\ have "\ = e * (1 - c ^ (m - n))"  immler@69613  1096  by simp  immler@69613  1097  also from c \1 - c ^ (m - n) > 0\ \e > 0\ have "\ \ e"  immler@69613  1098  using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto  immler@69613  1099  finally show ?thesis by simp  immler@69613  1100  qed  immler@69613  1101  have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat  immler@69613  1102  proof (cases "n = m")  immler@69613  1103  case True  immler@69613  1104  with \e > 0\ show ?thesis by simp  immler@69613  1105  next  immler@69613  1106  case False  immler@69613  1107  with *[of n m] *[of m n] and that show ?thesis  immler@69613  1108  by (auto simp: dist_commute nat_neq_iff)  immler@69613  1109  qed  immler@69613  1110  then show ?thesis by auto  immler@69613  1111  qed  immler@69613  1112  then have "Cauchy z"  immler@69613  1113  by (simp add: cauchy_def)  immler@69613  1114  then obtain x where "x\s" and x:"(z \ x) sequentially"  immler@69613  1115  using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto  immler@69613  1116 immler@69613  1117  define e where "e = dist (f x) x"  immler@69613  1118  have "e = 0"  immler@69613  1119  proof (rule ccontr)  immler@69613  1120  assume "e \ 0"  immler@69613  1121  then have "e > 0"  immler@69613  1122  unfolding e_def using zero_le_dist[of "f x" x]  immler@69613  1123  by (metis dist_eq_0_iff dist_nz e_def)  immler@69613  1124  then obtain N where N:"\n\N. dist (z n) x < e / 2"  immler@69613  1125  using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto  immler@69613  1126  then have N':"dist (z N) x < e / 2" by auto  immler@69613  1127  have *: "c * dist (z N) x \ dist (z N) x"  immler@69613  1128  unfolding mult_le_cancel_right2  immler@69613  1129  using zero_le_dist[of "z N" x] and c  immler@69613  1130  by (metis dist_eq_0_iff dist_nz order_less_asym less_le)  immler@69613  1131  have "dist (f (z N)) (f x) \ c * dist (z N) x"  immler@69613  1132  using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]  immler@69613  1133  using z_in_s[of N] \x\s\  immler@69613  1134  using c  immler@69613  1135  by auto  immler@69613  1136  also have "\ < e / 2"  immler@69613  1137  using N' and c using * by auto  immler@69613  1138  finally show False  immler@69613  1139  unfolding fzn  immler@69613  1140  using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]  immler@69613  1141  unfolding e_def  immler@69613  1142  by auto  immler@69613  1143  qed  immler@69613  1144  then have "f x = x" by (auto simp: e_def)  immler@69613  1145  moreover have "y = x" if "f y = y" "y \ s" for y  immler@69613  1146  proof -  immler@69613  1147  from \x \ s\ \f x = x\ that have "dist x y \ c * dist x y"  immler@69613  1148  using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp  immler@69613  1149  with c and zero_le_dist[of x y] have "dist x y = 0"  immler@69613  1150  by (simp add: mult_le_cancel_right1)  immler@69613  1151  then show ?thesis by simp  immler@69613  1152  qed  immler@69613  1153  ultimately show ?thesis  immler@69613  1154  using \x\s\ by blast  immler@69613  1155 qed  immler@69613  1156 immler@69613  1157 immler@69613  1158 subsection \Edelstein fixed point theorem\  immler@69613  1159 immler@69613  1160 theorem edelstein_fix:\ \TODO: rename to \Edelstein_fix\\  immler@69613  1161  fixes s :: "'a::metric_space set"  immler@69613  1162  assumes s: "compact s" "s \ {}"  immler@69613  1163  and gs: "(g  s) \ s"  immler@69613  1164  and dist: "\x\s. \y\s. x \ y \ dist (g x) (g y) < dist x y"  immler@69613  1165  shows "\!x\s. g x = x"  immler@69613  1166 proof -  immler@69613  1167  let ?D = "(\x. (x, x))  s"  immler@69613  1168  have D: "compact ?D" "?D \ {}"  immler@69613  1169  by (rule compact_continuous_image)  immler@69613  1170  (auto intro!: s continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within)  immler@69613  1171 immler@69613  1172  have "\x y e. x \ s \ y \ s \ 0 < e \ dist y x < e \ dist (g y) (g x) < e"  immler@69613  1173  using dist by fastforce  immler@69613  1174  then have "continuous_on s g"  immler@69613  1175  by (auto simp: continuous_on_iff)  immler@69613  1176  then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))"  immler@69613  1177  unfolding continuous_on_eq_continuous_within  immler@69613  1178  by (intro continuous_dist ballI continuous_within_compose)  immler@69613  1179  (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image)  immler@69613  1180 immler@69613  1181  obtain a where "a \ s" and le: "\x. x \ s \ dist (g a) a \ dist (g x) x"  immler@69613  1182  using continuous_attains_inf[OF D cont] by auto  immler@69613  1183 immler@69613  1184  have "g a = a"  immler@69613  1185  proof (rule ccontr)  immler@69613  1186  assume "g a \ a"  immler@69613  1187  with \a \ s\ gs have "dist (g (g a)) (g a) < dist (g a) a"  immler@69613  1188  by (intro dist[rule_format]) auto  immler@69613  1189  moreover have "dist (g a) a \ dist (g (g a)) (g a)"  immler@69613  1190  using \a \ s\ gs by (intro le) auto  immler@69613  1191  ultimately show False by auto  immler@69613  1192  qed  immler@69613  1193  moreover have "\x. x \ s \ g x = x \ x = a"  immler@69613  1194  using dist[THEN bspec[where x=a]] \g a = a\ and \a\s\ by auto  immler@69613  1195  ultimately show "\!x\s. g x = x"  immler@69613  1196  using \a \ s\ by blast  immler@69613  1197 qed  immler@69613  1198 immler@69613  1199 subsection \The diameter of a set\  immler@69613  1200 immler@69613  1201 definition%important diameter :: "'a::metric_space set \ real" where  immler@69613  1202  "diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)"  immler@69613  1203 immler@69613  1204 lemma diameter_empty [simp]: "diameter{} = 0"  immler@69613  1205  by (auto simp: diameter_def)  immler@69613  1206 immler@69613  1207 lemma diameter_singleton [simp]: "diameter{x} = 0"  immler@69613  1208  by (auto simp: diameter_def)  immler@69613  1209 immler@69613  1210 lemma diameter_le:  immler@69613  1211  assumes "S \ {} \ 0 \ d"  immler@69613  1212  and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d"  immler@69613  1213  shows "diameter S \ d"  immler@69613  1214 using assms  immler@69613  1215  by (auto simp: dist_norm diameter_def intro: cSUP_least)  immler@69613  1216 immler@69613  1217 lemma diameter_bounded_bound:  immler@69613  1218  fixes s :: "'a :: metric_space set"  immler@69613  1219  assumes s: "bounded s" "x \ s" "y \ s"  immler@69613  1220  shows "dist x y \ diameter s"  immler@69613  1221 proof -  immler@69613  1222  from s obtain z d where z: "\x. x \ s \ dist z x \ d"  immler@69613  1223  unfolding bounded_def by auto  immler@69613  1224  have "bdd_above (case_prod dist  (s\s))"  immler@69613  1225  proof (intro bdd_aboveI, safe)  immler@69613  1226  fix a b  immler@69613  1227  assume "a \ s" "b \ s"  immler@69613  1228  with z[of a] z[of b] dist_triangle[of a b z]  immler@69613  1229  show "dist a b \ 2 * d"  immler@69613  1230  by (simp add: dist_commute)  immler@69613  1231  qed  immler@69613  1232  moreover have "(x,y) \ s\s" using s by auto  immler@69613  1233  ultimately have "dist x y \ (SUP (x,y)\s\s. dist x y)"  immler@69613  1234  by (rule cSUP_upper2) simp  immler@69613  1235  with \x \ s\ show ?thesis  immler@69613  1236  by (auto simp: diameter_def)  immler@69613  1237 qed  immler@69613  1238 immler@69613  1239 lemma diameter_lower_bounded:  immler@69613  1240  fixes s :: "'a :: metric_space set"  immler@69613  1241  assumes s: "bounded s"  immler@69613  1242  and d: "0 < d" "d < diameter s"  immler@69613  1243  shows "\x\s. \y\s. d < dist x y"  immler@69613  1244 proof (rule ccontr)  immler@69613  1245  assume contr: "\ ?thesis"  immler@69613  1246  moreover have "s \ {}"  immler@69613  1247  using d by (auto simp: diameter_def)  immler@69613  1248  ultimately have "diameter s \ d"  immler@69613  1249  by (auto simp: not_less diameter_def intro!: cSUP_least)  immler@69613  1250  with \d < diameter s\ show False by auto  immler@69613  1251 qed  immler@69613  1252 immler@69613  1253 lemma diameter_bounded:  immler@69613  1254  assumes "bounded s"  immler@69613  1255  shows "\x\s. \y\s. dist x y \ diameter s"  immler@69613  1256  and "\d>0. d < diameter s \ (\x\s. \y\s. dist x y > d)"  immler@69613  1257  using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms  immler@69613  1258  by auto  immler@69613  1259 immler@69613  1260 lemma bounded_two_points:  immler@69613  1261  "bounded S \ (\e. \x\S. \y\S. dist x y \ e)"  immler@69613  1262  apply (rule iffI)  immler@69613  1263  subgoal using diameter_bounded(1) by auto  immler@69613  1264  subgoal using bounded_any_center[of S] by meson  immler@69613  1265  done  immler@69613  1266 immler@69613  1267 lemma diameter_compact_attained:  immler@69613  1268  assumes "compact s"  immler@69613  1269  and "s \ {}"  immler@69613  1270  shows "\x\s. \y\s. dist x y = diameter s"  immler@69613  1271 proof -  immler@69613  1272  have b: "bounded s" using assms(1)  immler@69613  1273  by (rule compact_imp_bounded)  immler@69613  1274  then obtain x y where xys: "x\s" "y\s"  immler@69613  1275  and xy: "\u\s. \v\s. dist u v \ dist x y"  immler@69613  1276  using compact_sup_maxdistance[OF assms] by auto  immler@69613  1277  then have "diameter s \ dist x y"  immler@69613  1278  unfolding diameter_def  immler@69613  1279  apply clarsimp  immler@69613  1280  apply (rule cSUP_least, fast+)  immler@69613  1281  done  immler@69613  1282  then show ?thesis  immler@69613  1283  by (metis b diameter_bounded_bound order_antisym xys)  immler@69613  1284 qed  immler@69613  1285 immler@69613  1286 lemma diameter_ge_0:  immler@69613  1287  assumes "bounded S" shows "0 \ diameter S"  immler@69613  1288  by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl)  immler@69613  1289 immler@69613  1290 lemma diameter_subset:  immler@69613  1291  assumes "S \ T" "bounded T"  immler@69613  1292  shows "diameter S \ diameter T"  immler@69613  1293 proof (cases "S = {} \ T = {}")  immler@69613  1294  case True  immler@69613  1295  with assms show ?thesis  immler@69613  1296  by (force simp: diameter_ge_0)  immler@69613  1297 next  immler@69613  1298  case False  immler@69613  1299  then have "bdd_above ((\x. case x of (x, xa) \ dist x xa)  (T \ T))"  immler@69613  1300  using \bounded T\ diameter_bounded_bound by (force simp: bdd_above_def)  immler@69613  1301  with False \S \ T\ show ?thesis  immler@69613  1302  apply (simp add: diameter_def)  immler@69613  1303  apply (rule cSUP_subset_mono, auto)  immler@69613  1304  done  immler@69613  1305 qed  immler@69613  1306 immler@69613  1307 lemma diameter_closure:  immler@69613  1308  assumes "bounded S"  immler@69613  1309  shows "diameter(closure S) = diameter S"  immler@69613  1310 proof (rule order_antisym)  immler@69613  1311  have "False" if "diameter S < diameter (closure S)"  immler@69613  1312  proof -  immler@69613  1313  define d where "d = diameter(closure S) - diameter(S)"  immler@69613  1314  have "d > 0"  immler@69613  1315  using that by (simp add: d_def)  immler@69613  1316  then have "diameter(closure(S)) - d / 2 < diameter(closure(S))"  immler@69613  1317  by simp  immler@69613  1318  have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2"  immler@69613  1319  by (simp add: d_def divide_simps)  immler@69613  1320  have bocl: "bounded (closure S)"  immler@69613  1321  using assms by blast  immler@69613  1322  moreover have "0 \ diameter S"  immler@69613  1323  using assms diameter_ge_0 by blast  immler@69613  1324  ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y"  immler@69613  1325  using diameter_bounded(2) [OF bocl, rule_format, of "diameter(closure(S)) - d / 2"] \d > 0\ d_def by auto  immler@69613  1326  then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4"  immler@69613  1327  using closure_approachable  immler@69613  1328  by (metis \0 < d\ zero_less_divide_iff zero_less_numeral)  immler@69613  1329  then have "dist x' y' \ diameter S"  immler@69613  1330  using assms diameter_bounded_bound by blast  immler@69613  1331  with x'y' have "dist x y \ d / 4 + diameter S + d / 4"  immler@69613  1332  by (meson add_mono_thms_linordered_semiring(1) dist_triangle dist_triangle3 less_eq_real_def order_trans)  immler@69613  1333  then show ?thesis  immler@69613  1334  using xy d_def by linarith  immler@69613  1335  qed  immler@69613  1336  then show "diameter (closure S) \ diameter S"  immler@69613  1337  by fastforce  immler@69613  1338  next  immler@69613  1339  show "diameter S \ diameter (closure S)"  immler@69613  1340  by (simp add: assms bounded_closure closure_subset diameter_subset)  immler@69613  1341 qed  immler@69613  1342 immler@69613  1343 proposition Lebesgue_number_lemma:  immler@69613  1344  assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B"  immler@69613  1345  obtains \ where "0 < \" "\T. \T \ S; diameter T < \\ \ \B \ \. T \ B"  immler@69613  1346 proof (cases "S = {}")  immler@69613  1347  case True  immler@69613  1348  then show ?thesis  immler@69613  1349  by (metis \\ \ {}\ zero_less_one empty_subsetI equals0I subset_trans that)  immler@69613  1350 next  immler@69613  1351  case False  immler@69613  1352  { fix x assume "x \ S"  immler@69613  1353  then obtain C where C: "x \ C" "C \ \"  immler@69613  1354  using \S \ \\\ by blast  immler@69613  1355  then obtain r where r: "r>0" "ball x (2*r) \ C"  immler@69613  1356  by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)  immler@69613  1357  then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \"  immler@69613  1358  using C by blast  immler@69613  1359  }  immler@69613  1360  then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)"  immler@69613  1361  by metis  immler@69613  1362  then have "S \ (\x \ S. ball x (r x))"  immler@69613  1363  by auto  immler@69613  1364  then obtain \ where "finite \" "S \ \\" and \: "\ \ (\x. ball x (r x))  S"  immler@69613  1365  by (rule compactE [OF \compact S\]) auto  immler@69613  1366  then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x))  S0"  immler@69613  1367  by (meson finite_subset_image)  immler@69613  1368  then have "S0 \ {}"  immler@69613  1369  using False \S \ \\\ by auto  immler@69613  1370  define \ where "\ = Inf (r  S0)"  immler@69613  1371  have "\ > 0"  immler@69613  1372  using \finite S0\ \S0 \ S\ \S0 \ {}\ r by (auto simp: \_def finite_less_Inf_iff)  immler@69613  1373  show ?thesis  immler@69613  1374  proof  immler@69613  1375  show "0 < \"  immler@69613  1376  by (simp add: \0 < \\)  immler@69613  1377  show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T  immler@69613  1378  proof (cases "T = {}")  immler@69613  1379  case True  immler@69613  1380  then show ?thesis  immler@69613  1381  using \\ \ {}\ by blast  immler@69613  1382  next  immler@69613  1383  case False  immler@69613  1384  then obtain y where "y \ T" by blast  immler@69613  1385  then have "y \ S"  immler@69613  1386  using \T \ S\ by auto  immler@69613  1387  then obtain x where "x \ S0" and x: "y \ ball x (r x)"  immler@69613  1388  using \S \ \\\ S0 that by blast  immler@69613  1389  have "ball y \ \ ball y (r x)"  immler@69613  1390  by (metis \_def \S0 \ {}\ \finite S0\ \x \ S0\ empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball)  immler@69613  1391  also have "... \ ball x (2*r x)"  immler@69613  1392  by clarsimp (metis dist_commute dist_triangle_less_add mem_ball mult_2 x)  immler@69613  1393  finally obtain C where "C \ \" "ball y \ \ C"  immler@69613  1394  by (meson r \S0 \ S\ \x \ S0\ dual_order.trans subsetCE)  immler@69613  1395  have "bounded T"  immler@69613  1396  using \compact S\ bounded_subset compact_imp_bounded \T \ S\ by blast  immler@69613  1397  then have "T \ ball y \"  immler@69613  1398  using \y \ T\ dia diameter_bounded_bound by fastforce  immler@69613  1399  then show ?thesis  immler@69613  1400  apply (rule_tac x=C in bexI)  immler@69613  1401  using \ball y \ \ C\ \C \ \\ by auto  immler@69613  1402  qed  immler@69613  1403  qed  immler@69613  1404 qed  immler@69613  1405 immler@69613  1406 immler@69544  1407 subsection \Metric spaces with the Heine-Borel property\  immler@69544  1408 immler@69544  1409 text \  immler@69544  1410  A metric space (or topological vector space) is said to have the  immler@69544  1411  Heine-Borel property if every closed and bounded subset is compact.  immler@69544  1412 \  immler@69544  1413 immler@69544  1414 class heine_borel = metric_space +  immler@69544  1415  assumes bounded_imp_convergent_subsequence:  immler@69544  1416  "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially"  immler@69544  1417 immler@69544  1418 proposition bounded_closed_imp_seq_compact:  immler@69544  1419  fixes s::"'a::heine_borel set"  immler@69544  1420  assumes "bounded s"  immler@69544  1421  and "closed s"  immler@69544  1422  shows "seq_compact s"  immler@69544  1423 proof (unfold seq_compact_def, clarify)  immler@69544  1424  fix f :: "nat \ 'a"  immler@69544  1425  assume f: "\n. f n \ s"  immler@69544  1426  with \bounded s\ have "bounded (range f)"  immler@69544  1427  by (auto intro: bounded_subset)  immler@69544  1428  obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially"  immler@69544  1429  using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto  immler@69544  1430  from f have fr: "\n. (f \ r) n \ s"  immler@69544  1431  by simp  immler@69544  1432  have "l \ s" using \closed s\ fr l  immler@69544  1433  by (rule closed_sequentially)  immler@69544  1434  show "\l\s. \r. strict_mono r \ ((f \ r) \ l) sequentially"  immler@69544  1435  using \l \ s\ r l by blast  immler@69544  1436 qed  immler@69544  1437 immler@69544  1438 lemma compact_eq_bounded_closed:  immler@69544  1439  fixes s :: "'a::heine_borel set"  immler@69544  1440  shows "compact s \ bounded s \ closed s"  immler@69544  1441  (is "?lhs = ?rhs")  immler@69544  1442 proof  immler@69544  1443  assume ?lhs  immler@69544  1444  then show ?rhs  immler@69544  1445  using compact_imp_closed compact_imp_bounded  immler@69544  1446  by blast  immler@69544  1447 next  immler@69544  1448  assume ?rhs  immler@69544  1449  then show ?lhs  immler@69544  1450  using bounded_closed_imp_seq_compact[of s]  immler@69544  1451  unfolding compact_eq_seq_compact_metric  immler@69544  1452  by auto  immler@69544  1453 qed  immler@69544  1454 immler@69544  1455 lemma compact_Inter:  immler@69544  1456  fixes \ :: "'a :: heine_borel set set"  immler@69544  1457  assumes com: "\S. S \ \ \ compact S" and "\ \ {}"  immler@69544  1458  shows "compact(\ \)"  immler@69544  1459  using assms  immler@69544  1460  by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed)  immler@69544  1461 immler@69544  1462 lemma compact_closure [simp]:  immler@69544  1463  fixes S :: "'a::heine_borel set"  immler@69544  1464  shows "compact(closure S) \ bounded S"  immler@69544  1465 by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)  immler@69544  1466 immler@69544  1467 instance%important real :: heine_borel  immler@69544  1468 proof%unimportant  immler@69544  1469  fix f :: "nat \ real"  immler@69544  1470  assume f: "bounded (range f)"  immler@69544  1471  obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)"  immler@69544  1472  unfolding comp_def by (metis seq_monosub)  immler@69544  1473  then have "Bseq (f \ r)"  immler@69544  1474  unfolding Bseq_eq_bounded using f  immler@69544  1475  by (metis BseqI' bounded_iff comp_apply rangeI)  immler@69544  1476  with r show "\l r. strict_mono r \ (f \ r) \ l"  immler@69544  1477  using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def)  immler@69544  1478 qed  immler@69544  1479 immler@69544  1480 lemma compact_lemma_general:  immler@69544  1481  fixes f :: "nat \ 'a"  immler@69544  1482  fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60)  immler@69544  1483  fixes unproj:: "('b \ 'c) \ 'a"  immler@69544  1484  assumes finite_basis: "finite basis"  immler@69544  1485  assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k)  range f)"  immler@69544  1486  assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k"  immler@69544  1487  assumes unproj_proj: "\x. unproj (\k. x proj k) = x"  immler@69544  1488  shows "\d\basis. \l::'a. \ r::nat\nat.  immler@69544  1489  strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)"  immler@69544  1490 proof safe  immler@69544  1491  fix d :: "'b set"  immler@69544  1492  assume d: "d \ basis"  immler@69544  1493  with finite_basis have "finite d"  immler@69544  1494  by (blast intro: finite_subset)  immler@69544  1495  from this d show "\l::'a. \r::nat\nat. strict_mono r \  immler@69544  1496  (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)"  immler@69544  1497  proof (induct d)  immler@69544  1498  case empty  immler@69544  1499  then show ?case  immler@69544  1500  unfolding strict_mono_def by auto  immler@69544  1501  next  immler@69544  1502  case (insert k d)  immler@69544  1503  have k[intro]: "k \ basis"  immler@69544  1504  using insert by auto  immler@69544  1505  have s': "bounded ((\x. x proj k)  range f)"  immler@69544  1506  using k  immler@69544  1507  by (rule bounded_proj)  immler@69544  1508  obtain l1::"'a" and r1 where r1: "strict_mono r1"  immler@69544  1509  and lr1: "\e > 0. eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"  immler@69544  1510  using insert(3) using insert(4) by auto  immler@69544  1511  have f': "\n. f (r1 n) proj k \ (\x. x proj k)  range f"  immler@69544  1512  by simp  immler@69544  1513  have "bounded (range (\i. f (r1 i) proj k))"  immler@69544  1514  by (metis (lifting) bounded_subset f' image_subsetI s')  immler@69544  1515  then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\i. f (r1 (r2 i)) proj k) \ l2) sequentially"  immler@69544  1516  using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"]  immler@69544  1517  by (auto simp: o_def)  immler@69544  1518  define r where "r = r1 \ r2"  immler@69544  1519  have r:"strict_mono r"  immler@69544  1520  using r1 and r2 unfolding r_def o_def strict_mono_def by auto  immler@69544  1521  moreover  immler@69544  1522  define l where "l = unproj (\i. if i = k then l2 else l1 proj i)"  immler@69544  1523  {  immler@69544  1524  fix e::real  immler@69544  1525  assume "e > 0"  immler@69544  1526  from lr1 \e > 0\ have N1: "eventually (\n. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"  immler@69544  1527  by blast  immler@69544  1528  from lr2 \e > 0\ have N2:"eventually (\n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"  immler@69544  1529  by (rule tendstoD)  immler@69544  1530  from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"  immler@69544  1531  by (rule eventually_subseq)  immler@69544  1532  have "eventually (\n. \i$$insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"  immler@69544  1533  using N1' N2  immler@69544  1534  by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)  immler@69544  1535  }  immler@69544  1536  ultimately show ?case by auto  immler@69544  1537  qed  immler@69544  1538 qed  immler@69544  1539 immler@69544  1540 lemma bounded_fst: "bounded s \ bounded (fst  s)"  immler@69544  1541  unfolding bounded_def  immler@69544  1542  by (metis (erased, hide_lams) dist_fst_le image_iff order_trans)  immler@69544  1543 immler@69544  1544 lemma bounded_snd: "bounded s \ bounded (snd  s)"  immler@69544  1545  unfolding bounded_def  immler@69544  1546  by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)  immler@69544  1547 immler@69544  1548 instance%important prod :: (heine_borel, heine_borel) heine_borel  immler@69544  1549 proof%unimportant  immler@69544  1550  fix f :: "nat \ 'a \ 'b"  immler@69544  1551  assume f: "bounded (range f)"  immler@69544  1552  then have "bounded (fst  range f)"  immler@69544  1553  by (rule bounded_fst)  immler@69544  1554  then have s1: "bounded (range (fst \ f))"  immler@69544  1555  by (simp add: image_comp)  immler@69544  1556  obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1"  immler@69544  1557  using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast  immler@69544  1558  from f have s2: "bounded (range (snd \ f \ r1))"  immler@69544  1559  by (auto simp: image_comp intro: bounded_snd bounded_subset)  immler@69544  1560  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\n. snd (f (r1 (r2 n)))) \ l2) sequentially"  immler@69544  1561  using bounded_imp_convergent_subsequence [OF s2]  immler@69544  1562  unfolding o_def by fast  immler@69544  1563  have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially"  immler@69544  1564  using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .  immler@69544  1565  have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially"  immler@69544  1566  using tendsto_Pair [OF l1' l2] unfolding o_def by simp  immler@69544  1567  have r: "strict_mono (r1 \ r2)"  immler@69544  1568  using r1 r2 unfolding strict_mono_def by simp  immler@69544  1569  show "\l r. strict_mono r \ ((f \ r) \ l) sequentially"  immler@69544  1570  using l r by fast  immler@69544  1571 qed  immler@69544  1572 immler@69611  1573 immler@69613  1574 subsection \Completeness\  immler@69544  1575 immler@69544  1576 proposition (in metric_space) completeI:  immler@69544  1577  assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l"  immler@69544  1578  shows "complete s"  immler@69544  1579  using assms unfolding complete_def by fast  immler@69544  1580 immler@69544  1581 proposition (in metric_space) completeE:  immler@69544  1582  assumes "complete s" and "\n. f n \ s" and "Cauchy f"  immler@69544  1583  obtains l where "l \ s" and "f \ l"  immler@69544  1584  using assms unfolding complete_def by fast  immler@69544  1585 immler@69544  1586 (* TODO: generalize to uniform spaces *)  immler@69544  1587 lemma compact_imp_complete:  immler@69544  1588  fixes s :: "'a::metric_space set"  immler@69544  1589  assumes "compact s"  immler@69544  1590  shows "complete s"  immler@69544  1591 proof -  immler@69544  1592  {  immler@69544  1593  fix f  immler@69544  1594  assume as: "(\n::nat. f n \ s)" "Cauchy f"  immler@69544  1595  from as(1) obtain l r where lr: "l\s" "strict_mono r" "(f \ r) \ l"  immler@69544  1596  using assms unfolding compact_def by blast  immler@69544  1597 immler@69544  1598  note lr' = seq_suble [OF lr(2)]  immler@69544  1599  {  immler@69544  1600  fix e :: real  immler@69544  1601  assume "e > 0"  immler@69544  1602  from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2"  immler@69544  1603  unfolding cauchy_def  immler@69544  1604  using \e > 0\  immler@69544  1605  apply (erule_tac x="e/2" in allE, auto)  immler@69544  1606  done  immler@69544  1607  from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]  immler@69544  1608  obtain M where M:"\n\M. dist ((f \ r) n) l < e/2"  immler@69544  1609  using \e > 0\ by auto  immler@69544  1610  {  immler@69544  1611  fix n :: nat  immler@69544  1612  assume n: "n \ max N M"  immler@69544  1613  have "dist ((f \ r) n) l < e/2"  immler@69544  1614  using n M by auto  immler@69544  1615  moreover have "r n \ N"  immler@69544  1616  using lr'[of n] n by auto  immler@69544  1617  then have "dist (f n) ((f \ r) n) < e / 2"  immler@69544  1618  using N and n by auto  immler@69544  1619  ultimately have "dist (f n) l < e"  immler@69544  1620  using dist_triangle_half_r[of "f (r n)" "f n" e l]  immler@69544  1621  by (auto simp: dist_commute)  immler@69544  1622  }  immler@69544  1623  then have "\N. \n\N. dist (f n) l < e" by blast  immler@69544  1624  }  immler@69544  1625  then have "\l\s. (f \ l) sequentially" using \l\s\  immler@69544  1626  unfolding lim_sequentially by auto  immler@69544  1627  }  immler@69544  1628  then show ?thesis unfolding complete_def by auto  immler@69544  1629 qed  immler@69544  1630 immler@69544  1631 proposition compact_eq_totally_bounded:  immler@69544  1632  "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))"  immler@69544  1633  (is "_ \ ?rhs")  immler@69544  1634 proof  immler@69544  1635  assume assms: "?rhs"  immler@69544  1636  then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)"  immler@69544  1637  by (auto simp: choice_iff')  immler@69544  1638 immler@69544  1639  show "compact s"  immler@69544  1640  proof cases  immler@69544  1641  assume "s = {}"  immler@69544  1642  then show "compact s" by (simp add: compact_def)  immler@69544  1643  next  immler@69544  1644  assume "s \ {}"  immler@69544  1645  show ?thesis  immler@69544  1646  unfolding compact_def  immler@69544  1647  proof safe  immler@69544  1648  fix f :: "nat \ 'a"  immler@69544  1649  assume f: "\n. f n \ s"  immler@69544  1650 immler@69544  1651  define e where "e n = 1 / (2 * Suc n)" for n  immler@69544  1652  then have [simp]: "\n. 0 < e n" by auto  immler@69544  1653  define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U  immler@69544  1654  {  immler@69544  1655  fix n U  immler@69544  1656  assume "infinite {n. f n \ U}"  immler@69544  1657  then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}"  immler@69544  1658  using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)  immler@69544  1659  then obtain a where  immler@69544  1660  "a \ k (e n)"  immler@69544  1661  "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" ..  immler@69544  1662  then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)"  immler@69544  1663  by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps)  immler@69544  1664  from someI_ex[OF this]  immler@69544  1665  have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U"  immler@69544  1666  unfolding B_def by auto  immler@69544  1667  }  immler@69544  1668  note B = this  immler@69544  1669 immler@69544  1670  define F where "F = rec_nat (B 0 UNIV) B"  immler@69544  1671  {  immler@69544  1672  fix n  immler@69544  1673  have "infinite {i. f i \ F n}"  immler@69544  1674  by (induct n) (auto simp: F_def B)  immler@69544  1675  }  immler@69544  1676  then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n"  immler@69544  1677  using B by (simp add: F_def)  immler@69544  1678  then have F_dec: "\m n. m \ n \ F n \ F m"  immler@69544  1679  using decseq_SucI[of F] by (auto simp: decseq_def)  immler@69544  1680 immler@69544  1681  obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k"  immler@69544  1682  proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)  immler@69544  1683  fix k i  immler@69544  1684  have "infinite ({n. f n \ F k} - {.. i})"  immler@69544  1685  using \infinite {n. f n \ F k}\ by auto  immler@69544  1686  from infinite_imp_nonempty[OF this]  immler@69544  1687  show "\x>i. f x \ F k"  immler@69544  1688  by (simp add: set_eq_iff not_le conj_commute)  immler@69544  1689  qed  immler@69544  1690 immler@69544  1691  define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)"  immler@69544  1692  have "strict_mono t"  immler@69544  1693  unfolding strict_mono_Suc_iff by (simp add: t_def sel)  immler@69544  1694  moreover have "\i. (f \ t) i \ s"  immler@69544  1695  using f by auto  immler@69544  1696  moreover  immler@69544  1697  {  immler@69544  1698  fix n  immler@69544  1699  have "(f \ t) n \ F n"  immler@69544  1700  by (cases n) (simp_all add: t_def sel)  immler@69544  1701  }  immler@69544  1702  note t = this  immler@69544  1703 immler@69544  1704  have "Cauchy (f \ t)"  immler@69544  1705  proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)  immler@69544  1706  fix r :: real and N n m  immler@69544  1707  assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m"  immler@69544  1708  then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r"  immler@69544  1709  using F_dec t by (auto simp: e_def field_simps of_nat_Suc)  immler@69544  1710  with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N"  immler@69544  1711  by (auto simp: subset_eq)  immler@69544  1712  with dist_triangle[of "(f \ t) m" "(f \ t) n" x] \2 * e N < r\  immler@69544  1713  show "dist ((f \ t) m) ((f \ t) n) < r"  immler@69544  1714  by (simp add: dist_commute)  immler@69544  1715  qed  immler@69544  1716 immler@69544  1717  ultimately show "\l\s. \r. strict_mono r \ (f \ r) \ l"  immler@69544  1718  using assms unfolding complete_def by blast  immler@69544  1719  qed  immler@69544  1720  qed  immler@69544  1721 qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)  immler@69544  1722 immler@69544  1723 lemma cauchy_imp_bounded:  immler@69544  1724  assumes "Cauchy s"  immler@69544  1725  shows "bounded (range s)"  immler@69544  1726 proof -  immler@69544  1727  from assms obtain N :: nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1"  immler@69544  1728  unfolding cauchy_def by force  immler@69544  1729  then have N:"\n. N \ n \ dist (s N) (s n) < 1" by auto  immler@69544  1730  moreover  immler@69544  1731  have "bounded (s  {0..N})"  immler@69544  1732  using finite_imp_bounded[of "s  {1..N}"] by auto  immler@69544  1733  then obtain a where a:"\x\s  {0..N}. dist (s N) x \ a"  immler@69544  1734  unfolding bounded_any_center [where a="s N"] by auto  immler@69544  1735  ultimately show "?thesis"  immler@69544  1736  unfolding bounded_any_center [where a="s N"]  immler@69544  1737  apply (rule_tac x="max a 1" in exI, auto)  immler@69544  1738  apply (erule_tac x=y in allE)  immler@69544  1739  apply (erule_tac x=y in ballE, auto)  immler@69544  1740  done  immler@69544  1741 qed  immler@69544  1742 immler@69544  1743 instance heine_borel < complete_space  immler@69544  1744 proof  immler@69544  1745  fix f :: "nat \ 'a" assume "Cauchy f"  immler@69544  1746  then have "bounded (range f)"  immler@69544  1747  by (rule cauchy_imp_bounded)  immler@69544  1748  then have "compact (closure (range f))"  immler@69544  1749  unfolding compact_eq_bounded_closed by auto  immler@69544  1750  then have "complete (closure (range f))"  immler@69544  1751  by (rule compact_imp_complete)  immler@69544  1752  moreover have "\n. f n \ closure (range f)"  immler@69544  1753  using closure_subset [of "range f"] by auto  immler@69544  1754  ultimately have "\l\closure (range f). (f \ l) sequentially"  immler@69544  1755  using \Cauchy f\ unfolding complete_def by auto  immler@69544  1756  then show "convergent f"  immler@69544  1757  unfolding convergent_def by auto  immler@69544  1758 qed  immler@69544  1759 immler@69544  1760 lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)"  immler@69544  1761 proof (rule completeI)  immler@69544  1762  fix f :: "nat \ 'a" assume "Cauchy f"  immler@69544  1763  then have "convergent f" by (rule Cauchy_convergent)  immler@69544  1764  then show "\l\UNIV. f \ l" unfolding convergent_def by simp  immler@69544  1765 qed  immler@69544  1766 immler@69544  1767 lemma complete_imp_closed:  immler@69544  1768  fixes S :: "'a::metric_space set"  immler@69544  1769  assumes "complete S"  immler@69544  1770  shows "closed S"  immler@69544  1771 proof (unfold closed_sequential_limits, clarify)  immler@69544  1772  fix f x assume "\n. f n \ S" and "f \ x"  immler@69544  1773  from \f \ x\ have "Cauchy f"  immler@69544  1774  by (rule LIMSEQ_imp_Cauchy)  immler@69544  1775  with \complete S\ and \\n. f n \ S\ obtain l where "l \ S" and "f \ l"  immler@69544  1776  by (rule completeE)  immler@69544  1777  from \f \ x\ and \f \ l\ have "x = l"  immler@69544  1778  by (rule LIMSEQ_unique)  immler@69544  1779  with \l \ S\ show "x \ S"  immler@69544  1780  by simp  immler@69544  1781 qed  immler@69544  1782 immler@69544  1783 lemma complete_Int_closed:  immler@69544  1784  fixes S :: "'a::metric_space set"  immler@69544  1785  assumes "complete S" and "closed t"  immler@69544  1786  shows "complete (S \ t)"  immler@69544  1787 proof (rule completeI)  immler@69544  1788  fix f assume "\n. f n \ S \ t" and "Cauchy f"  immler@69544  1789  then have "\n. f n \ S" and "\n. f n \ t"  immler@69544  1790  by simp_all  immler@69544  1791  from \complete S\ obtain l where "l \ S" and "f \ l"  immler@69544  1792  using \\n. f n \ S\ and \Cauchy f\ by (rule completeE)  immler@69544  1793  from \closed t\ and \\n. f n \ t\ and \f \ l\ have "l \ t"  immler@69544  1794  by (rule closed_sequentially)  immler@69544  1795  with \l \ S\ and \f \ l\ show "\l\S \ t. f \ l"  immler@69544  1796  by fast  immler@69544  1797 qed  immler@69544  1798 immler@69544  1799 lemma complete_closed_subset:  immler@69544  1800  fixes S :: "'a::metric_space set"  immler@69544  1801  assumes "closed S" and "S \ t" and "complete t"  immler@69544  1802  shows "complete S"  immler@69544  1803  using assms complete_Int_closed [of t S] by (simp add: Int_absorb1)  immler@69544  1804 immler@69544  1805 lemma complete_eq_closed:  immler@69544  1806  fixes S :: "('a::complete_space) set"  immler@69544  1807  shows "complete S \ closed S"  immler@69544  1808 proof  immler@69544  1809  assume "closed S" then show "complete S"  immler@69544  1810  using subset_UNIV complete_UNIV by (rule complete_closed_subset)  immler@69544  1811 next  immler@69544  1812  assume "complete S" then show "closed S"  immler@69544  1813  by (rule complete_imp_closed)  immler@69544  1814 qed  immler@69544  1815 immler@69544  1816 lemma convergent_eq_Cauchy:  immler@69544  1817  fixes S :: "nat \ 'a::complete_space"  immler@69544  1818  shows "(\l. (S \ l) sequentially) \ Cauchy S"  immler@69544  1819  unfolding Cauchy_convergent_iff convergent_def ..  immler@69544  1820 immler@69544  1821 lemma convergent_imp_bounded:  immler@69544  1822  fixes S :: "nat \ 'a::metric_space"  immler@69544  1823  shows "(S \ l) sequentially \ bounded (range S)"  immler@69544  1824  by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)  immler@69544  1825 immler@69544  1826 lemma frontier_subset_compact:  immler@69544  1827  fixes S :: "'a::heine_borel set"  immler@69544  1828  shows "compact S \ frontier S \ S"  immler@69544  1829  using frontier_subset_closed compact_eq_bounded_closed  immler@69544  1830  by blast  immler@69544  1831 immler@69613  1832 lemma continuous_closed_imp_Cauchy_continuous:  immler@69613  1833  fixes S :: "('a::complete_space) set"  immler@69613  1834  shows "\continuous_on S f; closed S; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f \$$"  immler@69613  1835  apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)  immler@69613  1836  by (meson LIMSEQ_imp_Cauchy complete_def)  immler@69613  1837 immler@69613  1838 lemma banach_fix_type:  immler@69613  1839  fixes f::"'a::complete_space\'a"  immler@69613  1840  assumes c:"0 \ c" "c < 1"  immler@69613  1841  and lipschitz:"\x. \y. dist (f x) (f y) \ c * dist x y"  immler@69613  1842  shows "\!x. (f x = x)"  immler@69613  1843  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]  immler@69613  1844  by auto  immler@69613  1845 immler@69613  1846 immler@69615  1847 subsection%unimportant\ Finite intersection property\  immler@69615  1848 immler@69615  1849 text\Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\  immler@69615  1850 immler@69615  1851 lemma closed_imp_fip:  immler@69615  1852  fixes S :: "'a::heine_borel set"  immler@69615  1853  assumes "closed S"  immler@69615  1854  and T: "T \ \" "bounded T"  immler@69615  1855  and clof: "\T. T \ \ \ closed T"  immler@69615  1856  and none: "\\'. \finite \'; \' \ \\ \ S \ \\' \ {}"  immler@69615  1857  shows "S \ \\ \ {}"  immler@69615  1858 proof -  immler@69615  1859  have "compact (S \ T)"  immler@69615  1860  using \closed S\ clof compact_eq_bounded_closed T by blast  immler@69615  1861  then have "(S \ T) \ \\ \ {}"  immler@69615  1862  apply (rule compact_imp_fip)  immler@69615  1863  apply (simp add: clof)  immler@69615  1864  by (metis Int_assoc complete_lattice_class.Inf_insert finite_insert insert_subset none \T \ \\)  immler@69615  1865  then show ?thesis by blast  immler@69615  1866 qed  immler@69615  1867 immler@69615  1868 lemma closed_imp_fip_compact:  immler@69615  1869  fixes S :: "'a::heine_borel set"  immler@69615  1870  shows  immler@69615  1871  "\closed S; \T. T \ \ \ compact T;  immler@69615  1872  \\'. \finite \'; \' \ \\ \ S \ \\' \ {}\  immler@69615  1873  \ S \ \\ \ {}"  immler@69615  1874 by (metis Inf_greatest closed_imp_fip compact_eq_bounded_closed empty_subsetI finite.emptyI inf.orderE)  immler@69615  1875 immler@69615  1876 lemma closed_fip_Heine_Borel:  immler@69615  1877  fixes \ :: "'a::heine_borel set set"  immler@69615  1878  assumes "closed S" "T \ \" "bounded T"  immler@69615  1879  and "\T. T \ \ \ closed T"  immler@69615  1880  and "\\'. \finite \'; \' \ \\ \ \\' \ {}"  immler@69615  1881  shows "\\ \ {}"  immler@69615  1882 proof -  immler@69615  1883  have "UNIV \ \\ \ {}"  immler@69615  1884  using assms closed_imp_fip [OF closed_UNIV] by auto  immler@69615  1885  then show ?thesis by simp  immler@69615  1886 qed  immler@69615  1887 immler@69615  1888 lemma compact_fip_Heine_Borel:  immler@69615  1889  fixes \ :: "'a::heine_borel set set"  immler@69615  1890  assumes clof: "\T. T \ \ \ compact T"  immler@69615  1891  and none: "\\'. \finite \'; \' \ \\ \ \\' \ {}"  immler@69615  1892  shows "\\ \ {}"  immler@69615  1893 by (metis InterI all_not_in_conv clof closed_fip_Heine_Borel compact_eq_bounded_closed none)  immler@69615  1894 immler@69615  1895 lemma compact_sequence_with_limit:  immler@69615  1896  fixes f :: "nat \ 'a::heine_borel"  immler@69615  1897  shows "(f \ l) sequentially \ compact (insert l (range f))"  immler@69615  1898 apply (simp add: compact_eq_bounded_closed, auto)  immler@69615  1899 apply (simp add: convergent_imp_bounded)  immler@69615  1900 by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)  immler@69615  1901 immler@69615  1902 immler@69613  1903 subsection \Properties of Balls and Spheres\  immler@69611  1904 immler@69611  1905 lemma compact_cball[simp]:  immler@69611  1906  fixes x :: "'a::heine_borel"  immler@69611  1907  shows "compact (cball x e)"  immler@69611  1908  using compact_eq_bounded_closed bounded_cball closed_cball  immler@69611  1909  by blast  immler@69611  1910 immler@69611  1911 lemma compact_frontier_bounded[intro]:  immler@69611  1912  fixes S :: "'a::heine_borel set"  immler@69611  1913  shows "bounded S \ compact (frontier S)"  immler@69611  1914  unfolding frontier_def  immler@69611  1915  using compact_eq_bounded_closed  immler@69611  1916  by blast  immler@69611  1917 immler@69611  1918 lemma compact_frontier[intro]:  immler@69611  1919  fixes S :: "'a::heine_borel set"  immler@69611  1920  shows "compact S \ compact (frontier S)"  immler@69611  1921  using compact_eq_bounded_closed compact_frontier_bounded  immler@69611  1922  by blast  immler@69611  1923 immler@69611  1924 immler@69613  1925 subsection \Distance from a Set\  immler@69611  1926 immler@69611  1927 lemma distance_attains_sup:  immler@69611  1928  assumes "compact s" "s \ {}"  immler@69611  1929  shows "\x\s. \y\s. dist a y \ dist a x"  immler@69611  1930 proof (rule continuous_attains_sup [OF assms])  immler@69611  1931  {  immler@69611  1932  fix x  immler@69611  1933  assume "x\s"  immler@69611  1934  have "(dist a \ dist a x) (at x within s)"  immler@69611  1935  by (intro tendsto_dist tendsto_const tendsto_ident_at)  immler@69611  1936  }  immler@69611  1937  then show "continuous_on s (dist a)"  immler@69611  1938  unfolding continuous_on ..  immler@69611  1939 qed  immler@69611  1940 immler@69611  1941 text \For \emph{minimal} distance, we only need closure, not compactness.\  immler@69611  1942 immler@69611  1943 lemma distance_attains_inf:  immler@69611  1944  fixes a :: "'a::heine_borel"  immler@69611  1945  assumes "closed s" and "s \ {}"  immler@69611  1946  obtains x where "x\s" "\y. y \ s \ dist a x \ dist a y"  immler@69611  1947 proof -  immler@69611  1948  from assms obtain b where "b \ s" by auto  immler@69611  1949  let ?B = "s \ cball a (dist b a)"  immler@69611  1950  have "?B \ {}" using \b \ s\  immler@69611  1951  by (auto simp: dist_commute)  immler@69611  1952  moreover have "continuous_on ?B (dist a)"  immler@69611  1953  by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)  immler@69611  1954  moreover have "compact ?B"  immler@69611  1955  by (intro closed_Int_compact \closed s\ compact_cball)  immler@69611  1956  ultimately obtain x where "x \ ?B" "\y\?B. dist a x \ dist a y"  immler@69611  1957  by (metis continuous_attains_inf)  immler@69611  1958  with that show ?thesis by fastforce  immler@69611  1959 qed  immler@69611  1960 immler@69613  1961 immler@69611  1962 subsection \Infimum Distance\  immler@69611  1963 immler@69611  1964 definition%important "infdist x A = (if A = {} then 0 else INF a\A. dist x a)"  immler@69611  1965 immler@69611  1966 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x  A)"  immler@69611  1967  by (auto intro!: zero_le_dist)  immler@69611  1968 immler@69611  1969 lemma infdist_notempty: "A \ {} \ infdist x A = (INF a\A. dist x a)"  immler@69611  1970  by (simp add: infdist_def)  immler@69611  1971 immler@69611  1972 lemma infdist_nonneg: "0 \ infdist x A"  immler@69611  1973  by (auto simp: infdist_def intro: cINF_greatest)  immler@69611  1974 immler@69611  1975 lemma infdist_le: "a \ A \ infdist x A \ dist x a"  immler@69611  1976  by (auto intro: cINF_lower simp add: infdist_def)  immler@69611  1977 immler@69611  1978 lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d"  immler@69611  1979  by (auto intro!: cINF_lower2 simp add: infdist_def)  immler@69611  1980 immler@69611  1981 lemma infdist_zero[simp]: "a \ A \ infdist a A = 0"  immler@69611  1982  by (auto intro!: antisym infdist_nonneg infdist_le2)  immler@69611  1983 immler@69611  1984 lemma infdist_triangle: "infdist x A \ infdist y A + dist x y"  immler@69611  1985 proof (cases "A = {}")  immler@69611  1986  case True  immler@69611  1987  then show ?thesis by (simp add: infdist_def)  immler@69611  1988 next  immler@69611  1989  case False  immler@69611  1990  then obtain a where "a \ A" by auto  immler@69611  1991  have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}"  immler@69611  1992  proof (rule cInf_greatest)  immler@69611  1993  from \A \ {}\ show "{dist x y + dist y a |a. a \ A} \ {}"  immler@69611  1994  by simp  immler@69611  1995  fix d  immler@69611  1996  assume "d \ {dist x y + dist y a |a. a \ A}"  immler@69611  1997  then obtain a where d: "d = dist x y + dist y a" "a \ A"  immler@69611  1998  by auto  immler@69611  1999  show "infdist x A \ d"  immler@69611  2000  unfolding infdist_notempty[OF \A \ {}\]  immler@69611  2001  proof (rule cINF_lower2)  immler@69611  2002  show "a \ A" by fact  immler@69611  2003  show "dist x a \ d"  immler@69611  2004  unfolding d by (rule dist_triangle)  immler@69611  2005  qed simp  immler@69611  2006  qed  immler@69611  2007  also have "\ = dist x y + infdist y A"  immler@69611  2008  proof (rule cInf_eq, safe)  immler@69611  2009  fix a  immler@69611  2010  assume "a \ A"  immler@69611  2011  then show "dist x y + infdist y A \ dist x y + dist y a"  immler@69611  2012  by (auto intro: infdist_le)  immler@69611  2013  next  immler@69611  2014  fix i  immler@69611  2015  assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d"  immler@69611  2016  then have "i - dist x y \ infdist y A"  immler@69611  2017  unfolding infdist_notempty[OF \A \ {}\] using \a \ A\  immler@69611  2018  by (intro cINF_greatest) (auto simp: field_simps)  immler@69611  2019  then show "i \ dist x y + infdist y A"  immler@69611  2020  by simp  immler@69611  2021  qed  immler@69611  2022  finally show ?thesis by simp  immler@69611  2023 qed  immler@69611  2024 immler@69611  2025 lemma in_closure_iff_infdist_zero:  immler@69611  2026  assumes "A \ {}"  immler@69611  2027  shows "x \ closure A \ infdist x A = 0"  immler@69611  2028 proof  immler@69611  2029  assume "x \ closure A"  immler@69611  2030  show "infdist x A = 0"  immler@69611  2031  proof (rule ccontr)  immler@69611  2032  assume "infdist x A \ 0"  immler@69611  2033  with infdist_nonneg[of x A] have "infdist x A > 0"  immler@69611  2034  by auto  immler@69611  2035  then have "ball x (infdist x A) \ closure A = {}"  immler@69611  2036  apply auto  immler@69611  2037  apply (metis \x \ closure A\ closure_approachable dist_commute infdist_le not_less)  immler@69611  2038  done  immler@69611  2039  then have "x \ closure A"  immler@69611  2040  by (metis \0 < infdist x A\ centre_in_ball disjoint_iff_not_equal)  immler@69611  2041  then show False using \x \ closure A\ by simp  immler@69611  2042  qed  immler@69611  2043 next  immler@69611  2044  assume x: "infdist x A = 0"  immler@69611  2045  then obtain a where "a \ A"  immler@69611  2046  by atomize_elim (metis all_not_in_conv assms)  immler@69611  2047  show "x \ closure A"  immler@69611  2048  unfolding closure_approachable  immler@69611  2049  apply safe  immler@69611  2050  proof (rule ccontr)  immler@69611  2051  fix e :: real  immler@69611  2052  assume "e > 0"  immler@69611  2053  assume "\ (\y\A. dist y x < e)"  immler@69611  2054  then have "infdist x A \ e" using \a \ A\  immler@69611  2055  unfolding infdist_def  immler@69611  2056  by (force simp: dist_commute intro: cINF_greatest)  immler@69611  2057  with x \e > 0\ show False by auto  immler@69611  2058  qed  immler@69611  2059 qed  immler@69611  2060 immler@69611  2061 lemma in_closed_iff_infdist_zero:  immler@69611  2062  assumes "closed A" "A \ {}"  immler@69611  2063  shows "x \ A \ infdist x A = 0"  immler@69611  2064 proof -  immler@69611  2065  have "x \ closure A \ infdist x A = 0"  immler@69611  2066  by (rule in_closure_iff_infdist_zero) fact  immler@69611  2067  with assms show ?thesis by simp  immler@69611  2068 qed  immler@69611  2069 immler@69611  2070 lemma infdist_pos_not_in_closed:  immler@69611  2071  assumes "closed S" "S \ {}" "x \ S"  immler@69611  2072  shows "infdist x S > 0"  immler@69611  2073 using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce  immler@69611  2074 immler@69611  2075 lemma  immler@69611  2076  infdist_attains_inf:  immler@69611  2077  fixes X::"'a::heine_borel set"  immler@69611  2078  assumes "closed X"  immler@69611  2079  assumes "X \ {}"  immler@69611  2080  obtains x where "x \ X" "infdist y X = dist y x"  immler@69611  2081 proof -  immler@69611  2082  have "bdd_below (dist y  X)"  immler@69611  2083  by auto  immler@69611  2084  from distance_attains_inf[OF assms, of y]  immler@69611  2085  obtain x where INF: "x \ X" "\z. z \ X \ dist y x \ dist y z" by auto  immler@69611  2086  have "infdist y X = dist y x"  immler@69611  2087  by (auto simp: infdist_def assms  immler@69611  2088  intro!: antisym cINF_lower[OF _ \x \ X\] cINF_greatest[OF assms(2) INF(2)])  immler@69611  2089  with \x \ X\ show ?thesis ..  immler@69611  2090 qed  immler@69611  2091 immler@69611  2092 immler@69611  2093 text \Every metric space is a T4 space:\  immler@69611  2094 immler@69611  2095 instance metric_space \ t4_space  immler@69611  2096 proof  immler@69611  2097  fix S T::"'a set" assume H: "closed S" "closed T" "S \ T = {}"  immler@69611  2098  consider "S = {}" | "T = {}" | "S \ {} \ T \ {}" by auto  immler@69611  2099  then show "\U V. open U \ open V \ S \ U \ T \ V \ U \ V = {}"  immler@69611  2100  proof (cases)  immler@69611  2101  case 1  immler@69611  2102  show ?thesis  immler@69611  2103  apply (rule exI[of _ "{}"], rule exI[of _ UNIV]) using 1 by auto  immler@69611  2104  next  immler@69611  2105  case 2  immler@69611  2106  show ?thesis  immler@69611  2107  apply (rule exI[of _ UNIV], rule exI[of _ "{}"]) using 2 by auto  immler@69611  2108  next  immler@69611  2109  case 3  immler@69611  2110  define U where "U = (\x\S. ball x ((infdist x T)/2))"  immler@69611  2111  have A: "open U" unfolding U_def by auto  immler@69611  2112  have "infdist x T > 0" if "x \ S" for x  immler@69611  2113  using H that 3 by (auto intro!: infdist_pos_not_in_closed)  immler@69611  2114  then have B: "S \ U" unfolding U_def by auto  immler@69611  2115  define V where "V = (\x\T. ball x ((infdist x S)/2))"  immler@69611  2116  have C: "open V" unfolding V_def by auto  immler@69611  2117  have "infdist x S > 0" if "x \ T" for x  immler@69611  2118  using H that 3 by (auto intro!: infdist_pos_not_in_closed)  immler@69611  2119  then have D: "T \ V" unfolding V_def by auto  immler@69611  2120 immler@69611  2121  have "(ball x ((infdist x T)/2)) \ (ball y ((infdist y S)/2)) = {}" if "x \ S" "y \ T" for x y  immler@69611  2122  proof (auto)  immler@69611  2123  fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S"  immler@69611  2124  have "2 * dist x y \ 2 * dist x z + 2 * dist y z"  immler@69611  2125  using dist_triangle[of x y z] by (auto simp add: dist_commute)  immler@69611  2126  also have "... < infdist x T + infdist y S"  immler@69611  2127  using H by auto  immler@69611  2128  finally have "dist x y < infdist x T \ dist x y < infdist y S"  immler@69611  2129  by auto  immler@69611  2130  then show False  immler@69611  2131  using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp add: dist_commute)  immler@69611  2132  qed  immler@69611  2133  then have E: "U \ V = {}"  immler@69611  2134  unfolding U_def V_def by auto  immler@69611  2135  show ?thesis  immler@69611  2136  apply (rule exI[of _ U], rule exI[of _ V]) using A B C D E by auto  immler@69611  2137  qed  immler@69611  2138 qed  immler@69611  2139 immler@69611  2140 lemma tendsto_infdist [tendsto_intros]:  immler@69611  2141  assumes f: "(f \ l) F"  immler@69611  2142  shows "((\x. infdist (f x) A) \ infdist l A) F"  immler@69611  2143 proof (rule tendstoI)  immler@69611  2144  fix e ::real  immler@69611  2145  assume "e > 0"  immler@69611  2146  from tendstoD[OF f this]  immler@69611  2147  show "eventually (\x. dist (infdist (f x) A) (infdist l A) < e) F"  immler@69611  2148  proof (eventually_elim)  immler@69611  2149  fix x  immler@69611  2150  from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]  immler@69611  2151  have "dist (infdist (f x) A) (infdist l A) \ dist (f x) l"  immler@69611  2152  by (simp add: dist_commute dist_real_def)  immler@69611  2153  also assume "dist (f x) l < e"  immler@69611  2154  finally show "dist (infdist (f x) A) (infdist l A) < e" .  immler@69611  2155  qed  immler@69611  2156 qed  immler@69611  2157 immler@69611  2158 lemma continuous_infdist[continuous_intros]:  immler@69611  2159  assumes "continuous F f"  immler@69611  2160  shows "continuous F (\x. infdist (f x) A)"  immler@69611  2161  using assms unfolding continuous_def by (rule tendsto_infdist)  immler@69611  2162 immler@69611  2163 lemma compact_infdist_le:  immler@69611  2164  fixes A::"'a::heine_borel set"  immler@69611  2165  assumes "A \ {}"  immler@69611  2166  assumes "compact A"  immler@69611  2167  assumes "e > 0"  immler@69611  2168  shows "compact {x. infdist x A \ e}"  immler@69611  2169 proof -  immler@69611  2170  from continuous_closed_vimage[of "{0..e}" "\x. infdist x A"]  immler@69611  2171  continuous_infdist[OF continuous_ident, of _ UNIV A]  immler@69611  2172  have "closed {x. infdist x A \ e}" by (auto simp: vimage_def infdist_nonneg)  immler@69611  2173  moreover  immler@69611  2174  from assms obtain x0 b where b: "\x. x \ A \ dist x0 x \ b" "closed A"  immler@69611  2175  by (auto simp: compact_eq_bounded_closed bounded_def)  immler@69611  2176  {  immler@69611  2177  fix y  immler@69611  2178  assume le: "infdist y A \ e"  immler@69611  2179  from infdist_attains_inf[OF \closed A\ \A \ {}\, of y]  immler@69611  2180  obtain z where z: "z \ A" "infdist y A = dist y z" by blast  immler@69611  2181  have "dist x0 y \ dist y z + dist x0 z"  immler@69611  2182  by (metis dist_commute dist_triangle)  immler@69611  2183  also have "dist y z \ e" using le z by simp  immler@69611  2184  also have "dist x0 z \ b" using b z by simp  immler@69611  2185  finally have "dist x0 y \ b + e" by arith  immler@69611  2186  } then  immler@69611  2187  have "bounded {x. infdist x A \ e}"  immler@69611  2188  by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])  immler@69611  2189  ultimately show "compact {x. infdist x A \ e}"  immler@69611  2190  by (simp add: compact_eq_bounded_closed)  immler@69611  2191 qed  immler@69611  2192 immler@69611  2193 immler@69613  2194 subsection \Separation between Points and Sets\  immler@69613  2195 immler@69613  2196 proposition separate_point_closed:  immler@69613  2197  fixes s :: "'a::heine_borel set"  immler@69613  2198  assumes "closed s" and "a \ s"  immler@69613  2199  shows "\d>0. \x\s. d \ dist a x"  immler@69613  2200 proof (cases "s = {}")  immler@69613  2201  case True  immler@69613  2202  then show ?thesis by(auto intro!: exI[where x=1])  immler@69544  2203 next  immler@69613  2204  case False  immler@69613  2205  from assms obtain x where "x\s" "\y\s. dist a x \ dist a y"  immler@69613  2206  using \s \ {}\ by (blast intro: distance_attains_inf [of s a])  immler@69613  2207  with \x\s\ show ?thesis using dist_pos_lt[of a x] and\a \ s\  immler@69613  2208  by blast  immler@69544  2209 qed  immler@69544  2210 immler@69613  2211 proposition separate_compact_closed:  immler@69613  2212  fixes s t :: "'a::heine_borel set"  immler@69613  2213  assumes "compact s"  immler@69613  2214  and t: "closed t" "s \ t = {}"  immler@69613  2215  shows "\d>0. \x\s. \y\t. d \ dist x y"  immler@69613  2216 proof cases  immler@69613  2217  assume "s \ {} \ t \ {}"  immler@69613  2218  then have "s \ {}" "t \ {}" by auto  immler@69613  2219  let ?inf = "\x. infdist x t"  immler@69613  2220  have "continuous_on s ?inf"  immler@69613  2221  by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident)  immler@69613  2222  then obtain x where x: "x \ s" "\y\s. ?inf x \ ?inf y"  immler@69613  2223  using continuous_attains_inf[OF \compact s\ \s \ {}\] by auto  immler@69613  2224  then have "0 < ?inf x"  immler@69613  2225  using t \t \ {}\ in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)  immler@69613  2226  moreover have "\x'\s. \y\t. ?inf x \ dist x' y"  immler@69613  2227  using x by (auto intro: order_trans infdist_le)  immler@69613  2228  ultimately show ?thesis by auto  immler@69613  2229 qed (auto intro!: exI[of _ 1])  immler@69613  2230 immler@69613  2231 proposition separate_closed_compact:  immler@69613  2232  fixes s t :: "'a::heine_borel set"  immler@69613  2233  assumes "closed s"  immler@69613  2234  and "compact t"  immler@69613  2235  and "s \ t = {}"  immler@69613  2236  shows "\d>0. \x\s. \y\t. d \ dist x y"  immler@69613  2237 proof -  immler@69613  2238  have *: "t \ s = {}"  immler@69613  2239  using assms(3) by auto  immler@69613  2240  show ?thesis  immler@69613  2241  using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)  immler@69613  2242 qed  immler@69613  2243 immler@69613  2244 proposition compact_in_open_separated:  immler@69613  2245  fixes A::"'a::heine_borel set"  immler@69613  2246  assumes "A \ {}"  immler@69613  2247  assumes "compact A"  immler@69613  2248  assumes "open B"  immler@69613  2249  assumes "A \ B"  immler@69613  2250  obtains e where "e > 0" "{x. infdist x A \ e} \ B"  immler@69613  2251 proof atomize_elim ` immler@696