src/HOL/Analysis/Topology_Euclidean_Space.thy
 author immler Wed Jan 16 19:34:48 2019 -0500 (4 months ago) changeset 69676 56acd449da41 parent 69619 3f7d8e05e0f2 child 69712 dc85b5b3a532 permissions -rw-r--r--
chapters for analysis manual
 lp15@63938 ` 1` ```(* Author: L C Paulson, University of Cambridge ``` himmelma@33175 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` himmelma@33175 ` 3` ``` Author: Robert Himmelmann, TU Muenchen ``` huffman@44075 ` 4` ``` Author: Brian Huffman, Portland State University ``` himmelma@33175 ` 5` ```*) ``` himmelma@33175 ` 6` immler@69676 ` 7` ```chapter \Vector Analysis\ ``` himmelma@33175 ` 8` himmelma@33175 ` 9` ```theory Topology_Euclidean_Space ``` immler@69516 ` 10` ``` imports ``` immler@69544 ` 11` ``` Elementary_Normed_Spaces ``` immler@69516 ` 12` ``` Linear_Algebra ``` immler@69516 ` 13` ``` Norm_Arith ``` hoelzl@51343 ` 14` ```begin ``` hoelzl@51343 ` 15` immler@69676 ` 16` ```section \Elementary Topology in Euclidean Space\ ``` immler@69676 ` 17` hoelzl@50526 ` 18` ```lemma euclidean_dist_l2: ``` hoelzl@50526 ` 19` ``` fixes x y :: "'a :: euclidean_space" ``` nipkow@67155 ` 20` ``` shows "dist x y = L2_set (\i. dist (x \ i) (y \ i)) Basis" ``` nipkow@67155 ` 21` ``` unfolding dist_norm norm_eq_sqrt_inner L2_set_def ``` hoelzl@50526 ` 22` ``` by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left) ``` hoelzl@50526 ` 23` immler@67685 ` 24` ```lemma norm_nth_le: "norm (x \ i) \ norm x" if "i \ Basis" ``` immler@67685 ` 25` ```proof - ``` immler@67685 ` 26` ``` have "(x \ i)\<^sup>2 = (\i\{i}. (x \ i)\<^sup>2)" ``` immler@67685 ` 27` ``` by simp ``` immler@67685 ` 28` ``` also have "\ \ (\i\Basis. (x \ i)\<^sup>2)" ``` immler@67685 ` 29` ``` by (intro sum_mono2) (auto simp: that) ``` immler@67685 ` 30` ``` finally show ?thesis ``` immler@67685 ` 31` ``` unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def ``` immler@67685 ` 32` ``` by (auto intro!: real_le_rsqrt) ``` immler@67685 ` 33` ```qed ``` immler@67685 ` 34` immler@67685 ` 35` immler@69613 ` 36` ```subsection%unimportant\Balls in Euclidean Space\ ``` immler@69613 ` 37` immler@69613 ` 38` ```lemma cball_subset_cball_iff: ``` immler@69613 ` 39` ``` fixes a :: "'a :: euclidean_space" ``` immler@69613 ` 40` ``` shows "cball a r \ cball a' r' \ dist a a' + r \ r' \ r < 0" ``` immler@69613 ` 41` ``` (is "?lhs \ ?rhs") ``` immler@69613 ` 42` ```proof ``` immler@69613 ` 43` ``` assume ?lhs ``` immler@69613 ` 44` ``` then show ?rhs ``` immler@69613 ` 45` ``` proof (cases "r < 0") ``` immler@69613 ` 46` ``` case True ``` immler@69613 ` 47` ``` then show ?rhs by simp ``` immler@69613 ` 48` ``` next ``` immler@69613 ` 49` ``` case False ``` immler@69613 ` 50` ``` then have [simp]: "r \ 0" by simp ``` immler@69613 ` 51` ``` have "norm (a - a') + r \ r'" ``` immler@69613 ` 52` ``` proof (cases "a = a'") ``` immler@69613 ` 53` ``` case True ``` immler@69613 ` 54` ``` then show ?thesis ``` immler@69613 ` 55` ``` using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = a, OF \?lhs\] ``` immler@69613 ` 56` ``` by (force simp: SOME_Basis dist_norm) ``` immler@69613 ` 57` ``` next ``` immler@69613 ` 58` ``` case False ``` immler@69613 ` 59` ``` have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))" ``` immler@69613 ` 60` ``` by (simp add: algebra_simps) ``` immler@69613 ` 61` ``` also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))" ``` immler@69613 ` 62` ``` by (simp add: algebra_simps) ``` immler@69613 ` 63` ``` also from \a \ a'\ have "... = \- norm (a - a') - r\" ``` immler@69613 ` 64` ``` by (simp add: abs_mult_pos field_simps) ``` immler@69613 ` 65` ``` finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \norm (a - a') + r\" ``` immler@69613 ` 66` ``` by linarith ``` immler@69613 ` 67` ``` from \a \ a'\ show ?thesis ``` immler@69613 ` 68` ``` using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \?lhs\] ``` immler@69613 ` 69` ``` by (simp add: dist_norm scaleR_add_left) ``` immler@69613 ` 70` ``` qed ``` immler@69613 ` 71` ``` then show ?rhs ``` immler@69613 ` 72` ``` by (simp add: dist_norm) ``` immler@69613 ` 73` ``` qed ``` immler@69613 ` 74` ```next ``` immler@69613 ` 75` ``` assume ?rhs ``` immler@69613 ` 76` ``` then show ?lhs ``` immler@69613 ` 77` ``` by (auto simp: ball_def dist_norm) ``` immler@69613 ` 78` ``` (metis add.commute add_le_cancel_right dist_norm dist_triangle3 order_trans) ``` immler@69613 ` 79` ```qed ``` immler@69613 ` 80` immler@69613 ` 81` ```lemma cball_subset_ball_iff: "cball a r \ ball a' r' \ dist a a' + r < r' \ r < 0" ``` immler@69613 ` 82` ``` (is "?lhs \ ?rhs") ``` immler@69613 ` 83` ``` for a :: "'a::euclidean_space" ``` immler@69613 ` 84` ```proof ``` immler@69613 ` 85` ``` assume ?lhs ``` immler@69613 ` 86` ``` then show ?rhs ``` immler@69613 ` 87` ``` proof (cases "r < 0") ``` immler@69613 ` 88` ``` case True then ``` immler@69613 ` 89` ``` show ?rhs by simp ``` immler@69613 ` 90` ``` next ``` immler@69613 ` 91` ``` case False ``` immler@69613 ` 92` ``` then have [simp]: "r \ 0" by simp ``` immler@69613 ` 93` ``` have "norm (a - a') + r < r'" ``` immler@69613 ` 94` ``` proof (cases "a = a'") ``` immler@69613 ` 95` ``` case True ``` immler@69613 ` 96` ``` then show ?thesis ``` immler@69613 ` 97` ``` using subsetD [where c = "a + r *\<^sub>R (SOME i. i \ Basis)", OF \?lhs\] subsetD [where c = a, OF \?lhs\] ``` immler@69613 ` 98` ``` by (force simp: SOME_Basis dist_norm) ``` immler@69613 ` 99` ``` next ``` immler@69613 ` 100` ``` case False ``` immler@69613 ` 101` ``` have False if "norm (a - a') + r \ r'" ``` immler@69613 ` 102` ``` proof - ``` immler@69613 ` 103` ``` from that have "\r' - norm (a - a')\ \ r" ``` immler@69613 ` 104` ``` by (simp split: abs_split) ``` immler@69613 ` 105` ``` (metis \0 \ r\ \?lhs\ centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq) ``` immler@69613 ` 106` ``` then show ?thesis ``` immler@69613 ` 107` ``` using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \?lhs\] \a \ a'\ ``` immler@69613 ` 108` ``` by (simp add: dist_norm field_simps) ``` immler@69613 ` 109` ``` (simp add: diff_divide_distrib scaleR_left_diff_distrib) ``` immler@69613 ` 110` ``` qed ``` immler@69613 ` 111` ``` then show ?thesis by force ``` immler@69613 ` 112` ``` qed ``` immler@69613 ` 113` ``` then show ?rhs by (simp add: dist_norm) ``` immler@69613 ` 114` ``` qed ``` immler@69613 ` 115` ```next ``` immler@69613 ` 116` ``` assume ?rhs ``` immler@69613 ` 117` ``` then show ?lhs ``` immler@69613 ` 118` ``` by (auto simp: ball_def dist_norm) ``` immler@69613 ` 119` ``` (metis add.commute add_le_cancel_right dist_norm dist_triangle3 le_less_trans) ``` immler@69613 ` 120` ```qed ``` immler@69613 ` 121` immler@69613 ` 122` ```lemma ball_subset_cball_iff: "ball a r \ cball a' r' \ dist a a' + r \ r' \ r \ 0" ``` immler@69613 ` 123` ``` (is "?lhs = ?rhs") ``` immler@69613 ` 124` ``` for a :: "'a::euclidean_space" ``` immler@69613 ` 125` ```proof (cases "r \ 0") ``` immler@69613 ` 126` ``` case True ``` immler@69613 ` 127` ``` then show ?thesis ``` immler@69613 ` 128` ``` using dist_not_less_zero less_le_trans by force ``` immler@69613 ` 129` ```next ``` immler@69613 ` 130` ``` case False ``` immler@69613 ` 131` ``` show ?thesis ``` immler@69613 ` 132` ``` proof ``` immler@69613 ` 133` ``` assume ?lhs ``` immler@69613 ` 134` ``` then have "(cball a r \ cball a' r')" ``` immler@69613 ` 135` ``` by (metis False closed_cball closure_ball closure_closed closure_mono not_less) ``` immler@69613 ` 136` ``` with False show ?rhs ``` immler@69613 ` 137` ``` by (fastforce iff: cball_subset_cball_iff) ``` immler@69613 ` 138` ``` next ``` immler@69613 ` 139` ``` assume ?rhs ``` immler@69613 ` 140` ``` with False show ?lhs ``` immler@69613 ` 141` ``` using ball_subset_cball cball_subset_cball_iff by blast ``` immler@69613 ` 142` ``` qed ``` immler@69613 ` 143` ```qed ``` immler@69613 ` 144` immler@69613 ` 145` ```lemma ball_subset_ball_iff: ``` immler@69613 ` 146` ``` fixes a :: "'a :: euclidean_space" ``` immler@69613 ` 147` ``` shows "ball a r \ ball a' r' \ dist a a' + r \ r' \ r \ 0" ``` immler@69613 ` 148` ``` (is "?lhs = ?rhs") ``` immler@69613 ` 149` ```proof (cases "r \ 0") ``` immler@69613 ` 150` ``` case True then show ?thesis ``` immler@69613 ` 151` ``` using dist_not_less_zero less_le_trans by force ``` immler@69613 ` 152` ```next ``` immler@69613 ` 153` ``` case False show ?thesis ``` immler@69613 ` 154` ``` proof ``` immler@69613 ` 155` ``` assume ?lhs ``` immler@69613 ` 156` ``` then have "0 < r'" ``` immler@69613 ` 157` ``` by (metis (no_types) False \?lhs\ centre_in_ball dist_norm le_less_trans mem_ball norm_ge_zero not_less set_mp) ``` immler@69613 ` 158` ``` then have "(cball a r \ cball a' r')" ``` immler@69613 ` 159` ``` by (metis False\?lhs\ closure_ball closure_mono not_less) ``` immler@69613 ` 160` ``` then show ?rhs ``` immler@69613 ` 161` ``` using False cball_subset_cball_iff by fastforce ``` immler@69613 ` 162` ``` next ``` immler@69613 ` 163` ``` assume ?rhs then show ?lhs ``` immler@69613 ` 164` ``` apply (auto simp: ball_def) ``` immler@69613 ` 165` ``` apply (metis add.commute add_le_cancel_right dist_commute dist_triangle_lt not_le order_trans) ``` immler@69613 ` 166` ``` using dist_not_less_zero order.strict_trans2 apply blast ``` immler@69613 ` 167` ``` done ``` immler@69613 ` 168` ``` qed ``` immler@69613 ` 169` ```qed ``` immler@69613 ` 170` immler@69613 ` 171` immler@69613 ` 172` ```lemma ball_eq_ball_iff: ``` immler@69613 ` 173` ``` fixes x :: "'a :: euclidean_space" ``` immler@69613 ` 174` ``` shows "ball x d = ball y e \ d \ 0 \ e \ 0 \ x=y \ d=e" ``` immler@69613 ` 175` ``` (is "?lhs = ?rhs") ``` immler@69613 ` 176` ```proof ``` immler@69613 ` 177` ``` assume ?lhs ``` immler@69613 ` 178` ``` then show ?rhs ``` immler@69613 ` 179` ``` proof (cases "d \ 0 \ e \ 0") ``` immler@69613 ` 180` ``` case True ``` immler@69613 ` 181` ``` with \?lhs\ show ?rhs ``` immler@69613 ` 182` ``` by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric]) ``` immler@69613 ` 183` ``` next ``` immler@69613 ` 184` ``` case False ``` immler@69613 ` 185` ``` with \?lhs\ show ?rhs ``` immler@69613 ` 186` ``` apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps) ``` immler@69613 ` 187` ``` apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans) ``` immler@69613 ` 188` ``` apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero) ``` immler@69613 ` 189` ``` done ``` immler@69613 ` 190` ``` qed ``` immler@69613 ` 191` ```next ``` immler@69613 ` 192` ``` assume ?rhs then show ?lhs ``` immler@69613 ` 193` ``` by (auto simp: set_eq_subset ball_subset_ball_iff) ``` immler@69613 ` 194` ```qed ``` immler@69613 ` 195` immler@69613 ` 196` ```lemma cball_eq_cball_iff: ``` immler@69613 ` 197` ``` fixes x :: "'a :: euclidean_space" ``` immler@69613 ` 198` ``` shows "cball x d = cball y e \ d < 0 \ e < 0 \ x=y \ d=e" ``` immler@69613 ` 199` ``` (is "?lhs = ?rhs") ``` immler@69613 ` 200` ```proof ``` immler@69613 ` 201` ``` assume ?lhs ``` immler@69613 ` 202` ``` then show ?rhs ``` immler@69613 ` 203` ``` proof (cases "d < 0 \ e < 0") ``` immler@69613 ` 204` ``` case True ``` immler@69613 ` 205` ``` with \?lhs\ show ?rhs ``` immler@69613 ` 206` ``` by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric]) ``` immler@69613 ` 207` ``` next ``` immler@69613 ` 208` ``` case False ``` immler@69613 ` 209` ``` with \?lhs\ show ?rhs ``` immler@69613 ` 210` ``` apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps) ``` immler@69613 ` 211` ``` apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans) ``` immler@69613 ` 212` ``` apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero) ``` immler@69613 ` 213` ``` done ``` immler@69613 ` 214` ``` qed ``` immler@69613 ` 215` ```next ``` immler@69613 ` 216` ``` assume ?rhs then show ?lhs ``` immler@69613 ` 217` ``` by (auto simp: set_eq_subset cball_subset_cball_iff) ``` immler@69613 ` 218` ```qed ``` immler@69613 ` 219` immler@69613 ` 220` ```lemma ball_eq_cball_iff: ``` immler@69613 ` 221` ``` fixes x :: "'a :: euclidean_space" ``` immler@69613 ` 222` ``` shows "ball x d = cball y e \ d \ 0 \ e < 0" (is "?lhs = ?rhs") ``` immler@69613 ` 223` ```proof ``` immler@69613 ` 224` ``` assume ?lhs ``` immler@69613 ` 225` ``` then show ?rhs ``` immler@69613 ` 226` ``` apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps) ``` immler@69613 ` 227` ``` apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist) ``` immler@69613 ` 228` ``` apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le) ``` immler@69613 ` 229` ``` using \?lhs\ ball_eq_empty cball_eq_empty apply blast+ ``` immler@69613 ` 230` ``` done ``` immler@69613 ` 231` ```next ``` immler@69613 ` 232` ``` assume ?rhs then show ?lhs by auto ``` immler@69613 ` 233` ```qed ``` immler@69613 ` 234` immler@69613 ` 235` ```lemma cball_eq_ball_iff: ``` immler@69613 ` 236` ``` fixes x :: "'a :: euclidean_space" ``` immler@69613 ` 237` ``` shows "cball x d = ball y e \ d < 0 \ e \ 0" ``` immler@69613 ` 238` ``` using ball_eq_cball_iff by blast ``` immler@69613 ` 239` immler@69613 ` 240` ```lemma finite_ball_avoid: ``` immler@69613 ` 241` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69613 ` 242` ``` assumes "open S" "finite X" "p \ S" ``` immler@69613 ` 243` ``` shows "\e>0. \w\ball p e. w\S \ (w\p \ w\X)" ``` immler@69613 ` 244` ```proof - ``` immler@69613 ` 245` ``` obtain e1 where "0 < e1" and e1_b:"ball p e1 \ S" ``` immler@69613 ` 246` ``` using open_contains_ball_eq[OF \open S\] assms by auto ``` immler@69613 ` 247` ``` obtain e2 where "0 < e2" and "\x\X. x \ p \ e2 \ dist p x" ``` immler@69613 ` 248` ``` using finite_set_avoid[OF \finite X\,of p] by auto ``` immler@69613 ` 249` ``` hence "\w\ball p (min e1 e2). w\S \ (w\p \ w\X)" using e1_b by auto ``` immler@69613 ` 250` ``` thus "\e>0. \w\ball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ \e1>0\ ``` immler@69613 ` 251` ``` apply (rule_tac x="min e1 e2" in exI) ``` immler@69613 ` 252` ``` by auto ``` immler@69613 ` 253` ```qed ``` immler@69613 ` 254` immler@69613 ` 255` ```lemma finite_cball_avoid: ``` immler@69613 ` 256` ``` fixes S :: "'a :: euclidean_space set" ``` immler@69613 ` 257` ``` assumes "open S" "finite X" "p \ S" ``` immler@69613 ` 258` ``` shows "\e>0. \w\cball p e. w\S \ (w\p \ w\X)" ``` immler@69613 ` 259` ```proof - ``` immler@69613 ` 260` ``` obtain e1 where "e1>0" and e1: "\w\ball p e1. w\S \ (w\p \ w\X)" ``` immler@69613 ` 261` ``` using finite_ball_avoid[OF assms] by auto ``` immler@69613 ` 262` ``` define e2 where "e2 \ e1/2" ``` immler@69613 ` 263` ``` have "e2>0" and "e2 < e1" unfolding e2_def using \e1>0\ by auto ``` immler@69613 ` 264` ``` then have "cball p e2 \ ball p e1" by (subst cball_subset_ball_iff,auto) ``` immler@69613 ` 265` ``` then show "\e>0. \w\cball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ e1 by auto ``` immler@69613 ` 266` ```qed ``` immler@69613 ` 267` immler@69619 ` 268` ```lemma dim_cball: ``` immler@69619 ` 269` ``` assumes "e > 0" ``` immler@69619 ` 270` ``` shows "dim (cball (0 :: 'n::euclidean_space) e) = DIM('n)" ``` immler@69619 ` 271` ```proof - ``` immler@69619 ` 272` ``` { ``` immler@69619 ` 273` ``` fix x :: "'n::euclidean_space" ``` immler@69619 ` 274` ``` define y where "y = (e / norm x) *\<^sub>R x" ``` immler@69619 ` 275` ``` then have "y \ cball 0 e" ``` immler@69619 ` 276` ``` using assms by auto ``` immler@69619 ` 277` ``` moreover have *: "x = (norm x / e) *\<^sub>R y" ``` immler@69619 ` 278` ``` using y_def assms by simp ``` immler@69619 ` 279` ``` moreover from * have "x = (norm x/e) *\<^sub>R y" ``` immler@69619 ` 280` ``` by auto ``` immler@69619 ` 281` ``` ultimately have "x \ span (cball 0 e)" ``` immler@69619 ` 282` ``` using span_scale[of y "cball 0 e" "norm x/e"] ``` immler@69619 ` 283` ``` span_superset[of "cball 0 e"] ``` immler@69619 ` 284` ``` by (simp add: span_base) ``` immler@69619 ` 285` ``` } ``` immler@69619 ` 286` ``` then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)" ``` immler@69619 ` 287` ``` by auto ``` immler@69619 ` 288` ``` then show ?thesis ``` immler@69619 ` 289` ``` using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV) ``` immler@69619 ` 290` ```qed ``` immler@69619 ` 291` immler@69613 ` 292` wenzelm@60420 ` 293` ```subsection \Boxes\ ``` immler@56189 ` 294` hoelzl@57447 ` 295` ```abbreviation One :: "'a::euclidean_space" ``` hoelzl@57447 ` 296` ``` where "One \ \Basis" ``` hoelzl@57447 ` 297` lp15@63114 ` 298` ```lemma One_non_0: assumes "One = (0::'a::euclidean_space)" shows False ``` lp15@63114 ` 299` ```proof - ``` lp15@63114 ` 300` ``` have "dependent (Basis :: 'a set)" ``` lp15@63114 ` 301` ``` apply (simp add: dependent_finite) ``` lp15@63114 ` 302` ``` apply (rule_tac x="\i. 1" in exI) ``` lp15@63114 ` 303` ``` using SOME_Basis apply (auto simp: assms) ``` lp15@63114 ` 304` ``` done ``` lp15@63114 ` 305` ``` with independent_Basis show False by force ``` lp15@63114 ` 306` ```qed ``` lp15@63114 ` 307` lp15@63114 ` 308` ```corollary One_neq_0[iff]: "One \ 0" ``` lp15@63114 ` 309` ``` by (metis One_non_0) ``` lp15@63114 ` 310` lp15@63114 ` 311` ```corollary Zero_neq_One[iff]: "0 \ One" ``` lp15@63114 ` 312` ``` by (metis One_non_0) ``` lp15@63114 ` 313` immler@67962 ` 314` ```definition%important (in euclidean_space) eucl_less (infix " (\i\Basis. a \ i < b \ i)" ``` immler@54775 ` 316` immler@67962 ` 317` ```definition%important box_eucl_less: "box a b = {x. a x i\Basis. a \ i \ x \ i \ x \ i \ b \ i}" ``` immler@54775 ` 319` immler@54775 ` 320` ```lemma box_def: "box a b = {x. \i\Basis. a \ i < x \ i \ x \ i < b \ i}" ``` immler@54775 ` 321` ``` and in_box_eucl_less: "x \ box a b \ a x box a b \ (\i\Basis. a \ i < x \ i \ x \ i < b \ i)" ``` immler@56188 ` 323` ``` "x \ cbox a b \ (\i\Basis. a \ i \ x \ i \ x \ i \ b \ i)" ``` immler@56188 ` 324` ``` by (auto simp: box_eucl_less eucl_less_def cbox_def) ``` immler@56188 ` 325` lp15@60615 ` 326` ```lemma cbox_Pair_eq: "cbox (a, c) (b, d) = cbox a b \ cbox c d" ``` lp15@60615 ` 327` ``` by (force simp: cbox_def Basis_prod_def) ``` lp15@60615 ` 328` lp15@60615 ` 329` ```lemma cbox_Pair_iff [iff]: "(x, y) \ cbox (a, c) (b, d) \ x \ cbox a b \ y \ cbox c d" ``` lp15@60615 ` 330` ``` by (force simp: cbox_Pair_eq) ``` lp15@60615 ` 331` lp15@65587 ` 332` ```lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\(x,y). Complex x y) ` (cbox a b \ cbox c d)" ``` lp15@65587 ` 333` ``` apply (auto simp: cbox_def Basis_complex_def) ``` lp15@65587 ` 334` ``` apply (rule_tac x = "(Re x, Im x)" in image_eqI) ``` lp15@65587 ` 335` ``` using complex_eq by auto ``` lp15@65587 ` 336` lp15@60615 ` 337` ```lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \ cbox a b = {} \ cbox c d = {}" ``` lp15@60615 ` 338` ``` by (force simp: cbox_Pair_eq) ``` lp15@60615 ` 339` lp15@60615 ` 340` ```lemma swap_cbox_Pair [simp]: "prod.swap ` cbox (c, a) (d, b) = cbox (a,c) (b,d)" ``` lp15@60615 ` 341` ``` by auto ``` lp15@60615 ` 342` immler@56188 ` 343` ```lemma mem_box_real[simp]: ``` immler@56188 ` 344` ``` "(x::real) \ box a b \ a < x \ x < b" ``` immler@56188 ` 345` ``` "(x::real) \ cbox a b \ a \ x \ x \ b" ``` immler@56188 ` 346` ``` by (auto simp: mem_box) ``` immler@56188 ` 347` immler@56188 ` 348` ```lemma box_real[simp]: ``` immler@56188 ` 349` ``` fixes a b:: real ``` immler@56188 ` 350` ``` shows "box a b = {a <..< b}" "cbox a b = {a .. b}" ``` immler@56188 ` 351` ``` by auto ``` hoelzl@50526 ` 352` hoelzl@57447 ` 353` ```lemma box_Int_box: ``` hoelzl@57447 ` 354` ``` fixes a :: "'a::euclidean_space" ``` hoelzl@57447 ` 355` ``` shows "box a b \ box c d = ``` hoelzl@57447 ` 356` ``` box (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\i) *\<^sub>R i)" ``` hoelzl@57447 ` 357` ``` unfolding set_eq_iff and Int_iff and mem_box by auto ``` hoelzl@57447 ` 358` immler@50087 ` 359` ```lemma rational_boxes: ``` wenzelm@61076 ` 360` ``` fixes x :: "'a::euclidean_space" ``` wenzelm@53291 ` 361` ``` assumes "e > 0" ``` lp15@66643 ` 362` ``` shows "\a b. (\i\Basis. a \ i \ \ \ b \ i \ \) \ x \ box a b \ box a b \ ball x e" ``` immler@50087 ` 363` ```proof - ``` wenzelm@63040 ` 364` ``` define e' where "e' = e / (2 * sqrt (real (DIM ('a))))" ``` wenzelm@53291 ` 365` ``` then have e: "e' > 0" ``` nipkow@56541 ` 366` ``` using assms by (auto simp: DIM_positive) ``` hoelzl@50526 ` 367` ``` have "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i") ``` immler@50087 ` 368` ``` proof ``` wenzelm@53255 ` 369` ``` fix i ``` wenzelm@53255 ` 370` ``` from Rats_dense_in_real[of "x \ i - e'" "x \ i"] e ``` wenzelm@53255 ` 371` ``` show "?th i" by auto ``` immler@50087 ` 372` ``` qed ``` wenzelm@55522 ` 373` ``` from choice[OF this] obtain a where ``` wenzelm@55522 ` 374` ``` a: "\xa. a xa \ \ \ a xa < x \ xa \ x \ xa - a xa < e'" .. ``` hoelzl@50526 ` 375` ``` have "\i. \y. y \ \ \ x \ i < y \ y - x \ i < e'" (is "\i. ?th i") ``` immler@50087 ` 376` ``` proof ``` wenzelm@53255 ` 377` ``` fix i ``` wenzelm@53255 ` 378` ``` from Rats_dense_in_real[of "x \ i" "x \ i + e'"] e ``` wenzelm@53255 ` 379` ``` show "?th i" by auto ``` immler@50087 ` 380` ``` qed ``` wenzelm@55522 ` 381` ``` from choice[OF this] obtain b where ``` wenzelm@55522 ` 382` ``` b: "\xa. b xa \ \ \ x \ xa < b xa \ b xa - x \ xa < e'" .. ``` hoelzl@50526 ` 383` ``` let ?a = "\i\Basis. a i *\<^sub>R i" and ?b = "\i\Basis. b i *\<^sub>R i" ``` hoelzl@50526 ` 384` ``` show ?thesis ``` hoelzl@50526 ` 385` ``` proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) ``` wenzelm@53255 ` 386` ``` fix y :: 'a ``` wenzelm@53255 ` 387` ``` assume *: "y \ box ?a ?b" ``` wenzelm@53015 ` 388` ``` have "dist x y = sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2)" ``` nipkow@67155 ` 389` ``` unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) ``` hoelzl@50526 ` 390` ``` also have "\ < sqrt (\(i::'a)\Basis. e^2 / real (DIM('a)))" ``` nipkow@64267 ` 391` ``` proof (rule real_sqrt_less_mono, rule sum_strict_mono) ``` wenzelm@53255 ` 392` ``` fix i :: "'a" ``` wenzelm@53255 ` 393` ``` assume i: "i \ Basis" ``` wenzelm@53255 ` 394` ``` have "a i < y\i \ y\i < b i" ``` wenzelm@53255 ` 395` ``` using * i by (auto simp: box_def) ``` wenzelm@53255 ` 396` ``` moreover have "a i < x\i" "x\i - a i < e'" ``` wenzelm@53255 ` 397` ``` using a by auto ``` wenzelm@53255 ` 398` ``` moreover have "x\i < b i" "b i - x\i < e'" ``` wenzelm@53255 ` 399` ``` using b by auto ``` wenzelm@53255 ` 400` ``` ultimately have "\x\i - y\i\ < 2 * e'" ``` wenzelm@53255 ` 401` ``` by auto ``` hoelzl@50526 ` 402` ``` then have "dist (x \ i) (y \ i) < e/sqrt (real (DIM('a)))" ``` immler@50087 ` 403` ``` unfolding e'_def by (auto simp: dist_real_def) ``` wenzelm@53015 ` 404` ``` then have "(dist (x \ i) (y \ i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" ``` immler@50087 ` 405` ``` by (rule power_strict_mono) auto ``` wenzelm@53015 ` 406` ``` then show "(dist (x \ i) (y \ i))\<^sup>2 < e\<^sup>2 / real DIM('a)" ``` immler@50087 ` 407` ``` by (simp add: power_divide) ``` immler@50087 ` 408` ``` qed auto ``` wenzelm@53255 ` 409` ``` also have "\ = e" ``` lp15@61609 ` 410` ``` using \0 < e\ by simp ``` wenzelm@53255 ` 411` ``` finally show "y \ ball x e" ``` wenzelm@53255 ` 412` ``` by (auto simp: ball_def) ``` hoelzl@50526 ` 413` ``` qed (insert a b, auto simp: box_def) ``` hoelzl@50526 ` 414` ```qed ``` immler@51103 ` 415` hoelzl@50526 ` 416` ```lemma open_UNION_box: ``` wenzelm@61076 ` 417` ``` fixes M :: "'a::euclidean_space set" ``` wenzelm@53282 ` 418` ``` assumes "open M" ``` hoelzl@50526 ` 419` ``` defines "a' \ \f :: 'a \ real \ real. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)" ``` hoelzl@50526 ` 420` ``` defines "b' \ \f :: 'a \ real \ real. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)" ``` wenzelm@53015 ` 421` ``` defines "I \ {f\Basis \\<^sub>E \ \ \. box (a' f) (b' f) \ M}" ``` hoelzl@50526 ` 422` ``` shows "M = (\f\I. box (a' f) (b' f))" ``` wenzelm@52624 ` 423` ```proof - ``` wenzelm@60462 ` 424` ``` have "x \ (\f\I. box (a' f) (b' f))" if "x \ M" for x ``` wenzelm@60462 ` 425` ``` proof - ``` wenzelm@52624 ` 426` ``` obtain e where e: "e > 0" "ball x e \ M" ``` wenzelm@60420 ` 427` ``` using openE[OF \open M\ \x \ M\] by auto ``` wenzelm@53282 ` 428` ``` moreover obtain a b where ab: ``` wenzelm@53282 ` 429` ``` "x \ box a b" ``` wenzelm@53282 ` 430` ``` "\i \ Basis. a \ i \ \" ``` wenzelm@53282 ` 431` ``` "\i\Basis. b \ i \ \" ``` wenzelm@53282 ` 432` ``` "box a b \ ball x e" ``` wenzelm@52624 ` 433` ``` using rational_boxes[OF e(1)] by metis ``` wenzelm@60462 ` 434` ``` ultimately show ?thesis ``` wenzelm@52624 ` 435` ``` by (intro UN_I[of "\i\Basis. (a \ i, b \ i)"]) ``` wenzelm@52624 ` 436` ``` (auto simp: euclidean_representation I_def a'_def b'_def) ``` wenzelm@60462 ` 437` ``` qed ``` wenzelm@52624 ` 438` ``` then show ?thesis by (auto simp: I_def) ``` wenzelm@52624 ` 439` ```qed ``` wenzelm@52624 ` 440` lp15@66154 ` 441` ```corollary open_countable_Union_open_box: ``` lp15@66154 ` 442` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@66154 ` 443` ``` assumes "open S" ``` lp15@66154 ` 444` ``` obtains \ where "countable \" "\ \ Pow S" "\X. X \ \ \ \a b. X = box a b" "\\ = S" ``` lp15@66154 ` 445` ```proof - ``` lp15@66154 ` 446` ``` let ?a = "\f. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)" ``` lp15@66154 ` 447` ``` let ?b = "\f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)" ``` lp15@66154 ` 448` ``` let ?I = "{f\Basis \\<^sub>E \ \ \. box (?a f) (?b f) \ S}" ``` lp15@66154 ` 449` ``` let ?\ = "(\f. box (?a f) (?b f)) ` ?I" ``` lp15@66154 ` 450` ``` show ?thesis ``` lp15@66154 ` 451` ``` proof ``` lp15@66154 ` 452` ``` have "countable ?I" ``` lp15@66154 ` 453` ``` by (simp add: countable_PiE countable_rat) ``` lp15@66154 ` 454` ``` then show "countable ?\" ``` lp15@66154 ` 455` ``` by blast ``` lp15@66154 ` 456` ``` show "\?\ = S" ``` lp15@66154 ` 457` ``` using open_UNION_box [OF assms] by metis ``` lp15@66154 ` 458` ``` qed auto ``` lp15@66154 ` 459` ```qed ``` lp15@66154 ` 460` lp15@66154 ` 461` ```lemma rational_cboxes: ``` lp15@66154 ` 462` ``` fixes x :: "'a::euclidean_space" ``` lp15@66154 ` 463` ``` assumes "e > 0" ``` lp15@66154 ` 464` ``` shows "\a b. (\i\Basis. a \ i \ \ \ b \ i \ \) \ x \ cbox a b \ cbox a b \ ball x e" ``` lp15@66154 ` 465` ```proof - ``` lp15@66154 ` 466` ``` define e' where "e' = e / (2 * sqrt (real (DIM ('a))))" ``` lp15@66154 ` 467` ``` then have e: "e' > 0" ``` lp15@66154 ` 468` ``` using assms by auto ``` lp15@66154 ` 469` ``` have "\i. \y. y \ \ \ y < x \ i \ x \ i - y < e'" (is "\i. ?th i") ``` lp15@66154 ` 470` ``` proof ``` lp15@66154 ` 471` ``` fix i ``` lp15@66154 ` 472` ``` from Rats_dense_in_real[of "x \ i - e'" "x \ i"] e ``` lp15@66154 ` 473` ``` show "?th i" by auto ``` lp15@66154 ` 474` ``` qed ``` lp15@66154 ` 475` ``` from choice[OF this] obtain a where ``` lp15@66154 ` 476` ``` a: "\u. a u \ \ \ a u < x \ u \ x \ u - a u < e'" .. ``` lp15@66154 ` 477` ``` have "\i. \y. y \ \ \ x \ i < y \ y - x \ i < e'" (is "\i. ?th i") ``` lp15@66154 ` 478` ``` proof ``` lp15@66154 ` 479` ``` fix i ``` lp15@66154 ` 480` ``` from Rats_dense_in_real[of "x \ i" "x \ i + e'"] e ``` lp15@66154 ` 481` ``` show "?th i" by auto ``` lp15@66154 ` 482` ``` qed ``` lp15@66154 ` 483` ``` from choice[OF this] obtain b where ``` lp15@66154 ` 484` ``` b: "\u. b u \ \ \ x \ u < b u \ b u - x \ u < e'" .. ``` lp15@66154 ` 485` ``` let ?a = "\i\Basis. a i *\<^sub>R i" and ?b = "\i\Basis. b i *\<^sub>R i" ``` lp15@66154 ` 486` ``` show ?thesis ``` lp15@66154 ` 487` ``` proof (rule exI[of _ ?a], rule exI[of _ ?b], safe) ``` lp15@66154 ` 488` ``` fix y :: 'a ``` lp15@66154 ` 489` ``` assume *: "y \ cbox ?a ?b" ``` lp15@66154 ` 490` ``` have "dist x y = sqrt (\i\Basis. (dist (x \ i) (y \ i))\<^sup>2)" ``` nipkow@67155 ` 491` ``` unfolding L2_set_def[symmetric] by (rule euclidean_dist_l2) ``` lp15@66154 ` 492` ``` also have "\ < sqrt (\(i::'a)\Basis. e^2 / real (DIM('a)))" ``` lp15@66154 ` 493` ``` proof (rule real_sqrt_less_mono, rule sum_strict_mono) ``` lp15@66154 ` 494` ``` fix i :: "'a" ``` lp15@66154 ` 495` ``` assume i: "i \ Basis" ``` lp15@66154 ` 496` ``` have "a i \ y\i \ y\i \ b i" ``` lp15@66154 ` 497` ``` using * i by (auto simp: cbox_def) ``` lp15@66154 ` 498` ``` moreover have "a i < x\i" "x\i - a i < e'" ``` lp15@66154 ` 499` ``` using a by auto ``` lp15@66154 ` 500` ``` moreover have "x\i < b i" "b i - x\i < e'" ``` lp15@66154 ` 501` ``` using b by auto ``` lp15@66154 ` 502` ``` ultimately have "\x\i - y\i\ < 2 * e'" ``` lp15@66154 ` 503` ``` by auto ``` lp15@66154 ` 504` ``` then have "dist (x \ i) (y \ i) < e/sqrt (real (DIM('a)))" ``` lp15@66154 ` 505` ``` unfolding e'_def by (auto simp: dist_real_def) ``` lp15@66154 ` 506` ``` then have "(dist (x \ i) (y \ i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2" ``` lp15@66154 ` 507` ``` by (rule power_strict_mono) auto ``` lp15@66154 ` 508` ``` then show "(dist (x \ i) (y \ i))\<^sup>2 < e\<^sup>2 / real DIM('a)" ``` lp15@66154 ` 509` ``` by (simp add: power_divide) ``` lp15@66154 ` 510` ``` qed auto ``` lp15@66154 ` 511` ``` also have "\ = e" ``` lp15@66154 ` 512` ``` using \0 < e\ by simp ``` lp15@66154 ` 513` ``` finally show "y \ ball x e" ``` lp15@66154 ` 514` ``` by (auto simp: ball_def) ``` lp15@66154 ` 515` ``` next ``` lp15@66154 ` 516` ``` show "x \ cbox (\i\Basis. a i *\<^sub>R i) (\i\Basis. b i *\<^sub>R i)" ``` lp15@66154 ` 517` ``` using a b less_imp_le by (auto simp: cbox_def) ``` lp15@66154 ` 518` ``` qed (use a b cbox_def in auto) ``` lp15@66154 ` 519` ```qed ``` lp15@66154 ` 520` lp15@66154 ` 521` ```lemma open_UNION_cbox: ``` lp15@66154 ` 522` ``` fixes M :: "'a::euclidean_space set" ``` lp15@66154 ` 523` ``` assumes "open M" ``` lp15@66154 ` 524` ``` defines "a' \ \f. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)" ``` lp15@66154 ` 525` ``` defines "b' \ \f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)" ``` lp15@66154 ` 526` ``` defines "I \ {f\Basis \\<^sub>E \ \ \. cbox (a' f) (b' f) \ M}" ``` lp15@66154 ` 527` ``` shows "M = (\f\I. cbox (a' f) (b' f))" ``` lp15@66154 ` 528` ```proof - ``` lp15@66154 ` 529` ``` have "x \ (\f\I. cbox (a' f) (b' f))" if "x \ M" for x ``` lp15@66154 ` 530` ``` proof - ``` lp15@66154 ` 531` ``` obtain e where e: "e > 0" "ball x e \ M" ``` lp15@66154 ` 532` ``` using openE[OF \open M\ \x \ M\] by auto ``` lp15@66154 ` 533` ``` moreover obtain a b where ab: "x \ cbox a b" "\i \ Basis. a \ i \ \" ``` lp15@66154 ` 534` ``` "\i \ Basis. b \ i \ \" "cbox a b \ ball x e" ``` lp15@66154 ` 535` ``` using rational_cboxes[OF e(1)] by metis ``` lp15@66154 ` 536` ``` ultimately show ?thesis ``` lp15@66154 ` 537` ``` by (intro UN_I[of "\i\Basis. (a \ i, b \ i)"]) ``` lp15@66154 ` 538` ``` (auto simp: euclidean_representation I_def a'_def b'_def) ``` lp15@66154 ` 539` ``` qed ``` lp15@66154 ` 540` ``` then show ?thesis by (auto simp: I_def) ``` lp15@66154 ` 541` ```qed ``` lp15@66154 ` 542` lp15@66154 ` 543` ```corollary open_countable_Union_open_cbox: ``` lp15@66154 ` 544` ``` fixes S :: "'a :: euclidean_space set" ``` lp15@66154 ` 545` ``` assumes "open S" ``` lp15@66154 ` 546` ``` obtains \ where "countable \" "\ \ Pow S" "\X. X \ \ \ \a b. X = cbox a b" "\\ = S" ``` lp15@66154 ` 547` ```proof - ``` lp15@66154 ` 548` ``` let ?a = "\f. (\(i::'a)\Basis. fst (f i) *\<^sub>R i)" ``` lp15@66154 ` 549` ``` let ?b = "\f. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)" ``` lp15@66154 ` 550` ``` let ?I = "{f\Basis \\<^sub>E \ \ \. cbox (?a f) (?b f) \ S}" ``` lp15@66154 ` 551` ``` let ?\ = "(\f. cbox (?a f) (?b f)) ` ?I" ``` lp15@66154 ` 552` ``` show ?thesis ``` lp15@66154 ` 553` ``` proof ``` lp15@66154 ` 554` ``` have "countable ?I" ``` lp15@66154 ` 555` ``` by (simp add: countable_PiE countable_rat) ``` lp15@66154 ` 556` ``` then show "countable ?\" ``` lp15@66154 ` 557` ``` by blast ``` lp15@66154 ` 558` ``` show "\?\ = S" ``` lp15@66154 ` 559` ``` using open_UNION_cbox [OF assms] by metis ``` lp15@66154 ` 560` ``` qed auto ``` lp15@66154 ` 561` ```qed ``` lp15@66154 ` 562` immler@56189 ` 563` ```lemma box_eq_empty: ``` immler@56189 ` 564` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 565` ``` shows "(box a b = {} \ (\i\Basis. b\i \ a\i))" (is ?th1) ``` immler@56189 ` 566` ``` and "(cbox a b = {} \ (\i\Basis. b\i < a\i))" (is ?th2) ``` immler@56189 ` 567` ```proof - ``` immler@56189 ` 568` ``` { ``` immler@56189 ` 569` ``` fix i x ``` immler@56189 ` 570` ``` assume i: "i\Basis" and as:"b\i \ a\i" and x:"x\box a b" ``` immler@56189 ` 571` ``` then have "a \ i < x \ i \ x \ i < b \ i" ``` immler@56189 ` 572` ``` unfolding mem_box by (auto simp: box_def) ``` immler@56189 ` 573` ``` then have "a\i < b\i" by auto ``` immler@56189 ` 574` ``` then have False using as by auto ``` immler@56189 ` 575` ``` } ``` immler@56189 ` 576` ``` moreover ``` immler@56189 ` 577` ``` { ``` immler@56189 ` 578` ``` assume as: "\i\Basis. \ (b\i \ a\i)" ``` immler@56189 ` 579` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` immler@56189 ` 580` ``` { ``` immler@56189 ` 581` ``` fix i :: 'a ``` immler@56189 ` 582` ``` assume i: "i \ Basis" ``` immler@56189 ` 583` ``` have "a\i < b\i" ``` immler@56189 ` 584` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@56189 ` 585` ``` then have "a\i < ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i < b\i" ``` immler@56189 ` 586` ``` by (auto simp: inner_add_left) ``` immler@56189 ` 587` ``` } ``` immler@56189 ` 588` ``` then have "box a b \ {}" ``` immler@56189 ` 589` ``` using mem_box(1)[of "?x" a b] by auto ``` immler@56189 ` 590` ``` } ``` immler@56189 ` 591` ``` ultimately show ?th1 by blast ``` immler@56189 ` 592` immler@56189 ` 593` ``` { ``` immler@56189 ` 594` ``` fix i x ``` immler@56189 ` 595` ``` assume i: "i \ Basis" and as:"b\i < a\i" and x:"x\cbox a b" ``` immler@56189 ` 596` ``` then have "a \ i \ x \ i \ x \ i \ b \ i" ``` immler@56189 ` 597` ``` unfolding mem_box by auto ``` immler@56189 ` 598` ``` then have "a\i \ b\i" by auto ``` immler@56189 ` 599` ``` then have False using as by auto ``` immler@56189 ` 600` ``` } ``` immler@56189 ` 601` ``` moreover ``` immler@56189 ` 602` ``` { ``` immler@56189 ` 603` ``` assume as:"\i\Basis. \ (b\i < a\i)" ``` immler@56189 ` 604` ``` let ?x = "(1/2) *\<^sub>R (a + b)" ``` immler@56189 ` 605` ``` { ``` immler@56189 ` 606` ``` fix i :: 'a ``` immler@56189 ` 607` ``` assume i:"i \ Basis" ``` immler@56189 ` 608` ``` have "a\i \ b\i" ``` immler@56189 ` 609` ``` using as[THEN bspec[where x=i]] i by auto ``` immler@56189 ` 610` ``` then have "a\i \ ((1/2) *\<^sub>R (a+b)) \ i" "((1/2) *\<^sub>R (a+b)) \ i \ b\i" ``` immler@56189 ` 611` ``` by (auto simp: inner_add_left) ``` immler@56189 ` 612` ``` } ``` immler@56189 ` 613` ``` then have "cbox a b \ {}" ``` immler@56189 ` 614` ``` using mem_box(2)[of "?x" a b] by auto ``` immler@56189 ` 615` ``` } ``` immler@56189 ` 616` ``` ultimately show ?th2 by blast ``` immler@56189 ` 617` ```qed ``` immler@56189 ` 618` immler@56189 ` 619` ```lemma box_ne_empty: ``` immler@56189 ` 620` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 621` ``` shows "cbox a b \ {} \ (\i\Basis. a\i \ b\i)" ``` immler@56189 ` 622` ``` and "box a b \ {} \ (\i\Basis. a\i < b\i)" ``` immler@56189 ` 623` ``` unfolding box_eq_empty[of a b] by fastforce+ ``` immler@56189 ` 624` immler@56189 ` 625` ```lemma ``` immler@56189 ` 626` ``` fixes a :: "'a::euclidean_space" ``` lp15@66112 ` 627` ``` shows cbox_sing [simp]: "cbox a a = {a}" ``` lp15@66112 ` 628` ``` and box_sing [simp]: "box a a = {}" ``` immler@56189 ` 629` ``` unfolding set_eq_iff mem_box eq_iff [symmetric] ``` immler@56189 ` 630` ``` by (auto intro!: euclidean_eqI[where 'a='a]) ``` immler@56189 ` 631` ``` (metis all_not_in_conv nonempty_Basis) ``` immler@56189 ` 632` immler@56189 ` 633` ```lemma subset_box_imp: ``` immler@56189 ` 634` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 635` ``` shows "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ cbox c d \ cbox a b" ``` immler@56189 ` 636` ``` and "(\i\Basis. a\i < c\i \ d\i < b\i) \ cbox c d \ box a b" ``` immler@56189 ` 637` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ cbox a b" ``` immler@56189 ` 638` ``` and "(\i\Basis. a\i \ c\i \ d\i \ b\i) \ box c d \ box a b" ``` immler@56189 ` 639` ``` unfolding subset_eq[unfolded Ball_def] unfolding mem_box ``` wenzelm@58757 ` 640` ``` by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ ``` immler@56189 ` 641` immler@56189 ` 642` ```lemma box_subset_cbox: ``` immler@56189 ` 643` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 644` ``` shows "box a b \ cbox a b" ``` immler@56189 ` 645` ``` unfolding subset_eq [unfolded Ball_def] mem_box ``` immler@56189 ` 646` ``` by (fast intro: less_imp_le) ``` immler@56189 ` 647` immler@56189 ` 648` ```lemma subset_box: ``` immler@56189 ` 649` ``` fixes a :: "'a::euclidean_space" ``` wenzelm@64539 ` 650` ``` shows "cbox c d \ cbox a b \ (\i\Basis. c\i \ d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th1) ``` wenzelm@64539 ` 651` ``` and "cbox c d \ box a b \ (\i\Basis. c\i \ d\i) \ (\i\Basis. a\i < c\i \ d\i < b\i)" (is ?th2) ``` wenzelm@64539 ` 652` ``` and "box c d \ cbox a b \ (\i\Basis. c\i < d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th3) ``` wenzelm@64539 ` 653` ``` and "box c d \ box a b \ (\i\Basis. c\i < d\i) \ (\i\Basis. a\i \ c\i \ d\i \ b\i)" (is ?th4) ``` immler@56189 ` 654` ```proof - ``` lp15@68120 ` 655` ``` let ?lesscd = "\i\Basis. c\i < d\i" ``` lp15@68120 ` 656` ``` let ?lerhs = "\i\Basis. a\i \ c\i \ d\i \ b\i" ``` lp15@68120 ` 657` ``` show ?th1 ?th2 ``` lp15@68120 ` 658` ``` by (fastforce simp: mem_box)+ ``` lp15@68120 ` 659` ``` have acdb: "a\i \ c\i \ d\i \ b\i" ``` lp15@68120 ` 660` ``` if i: "i \ Basis" and box: "box c d \ cbox a b" and cd: "\i. i \ Basis \ c\i < d\i" for i ``` lp15@68120 ` 661` ``` proof - ``` lp15@68120 ` 662` ``` have "box c d \ {}" ``` lp15@68120 ` 663` ``` using that ``` lp15@68120 ` 664` ``` unfolding box_eq_empty by force ``` lp15@68120 ` 665` ``` { let ?x = "(\j\Basis. (if j=i then ((min (a\j) (d\j))+c\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` lp15@68120 ` 666` ``` assume *: "a\i > c\i" ``` lp15@68120 ` 667` ``` then have "c \ j < ?x \ j \ ?x \ j < d \ j" if "j \ Basis" for j ``` lp15@68120 ` 668` ``` using cd that by (fastforce simp add: i *) ``` lp15@68120 ` 669` ``` then have "?x \ box c d" ``` lp15@68120 ` 670` ``` unfolding mem_box by auto ``` lp15@68120 ` 671` ``` moreover have "?x \ cbox a b" ``` lp15@68120 ` 672` ``` using i cd * by (force simp: mem_box) ``` lp15@68120 ` 673` ``` ultimately have False using box by auto ``` immler@56189 ` 674` ``` } ``` lp15@68120 ` 675` ``` then have "a\i \ c\i" by force ``` immler@56189 ` 676` ``` moreover ``` lp15@68120 ` 677` ``` { let ?x = "(\j\Basis. (if j=i then ((max (b\j) (c\j))+d\j)/2 else (c\j+d\j)/2) *\<^sub>R j)::'a" ``` lp15@68120 ` 678` ``` assume *: "b\i < d\i" ``` lp15@68120 ` 679` ``` then have "d \ j > ?x \ j \ ?x \ j > c \ j" if "j \ Basis" for j ``` lp15@68120 ` 680` ``` using cd that by (fastforce simp add: i *) ``` lp15@68120 ` 681` ``` then have "?x \ box c d" ``` immler@56189 ` 682` ``` unfolding mem_box by auto ``` lp15@68120 ` 683` ``` moreover have "?x \ cbox a b" ``` lp15@68120 ` 684` ``` using i cd * by (force simp: mem_box) ``` lp15@68120 ` 685` ``` ultimately have False using box by auto ``` immler@56189 ` 686` ``` } ``` immler@56189 ` 687` ``` then have "b\i \ d\i" by (rule ccontr) auto ``` lp15@68120 ` 688` ``` ultimately show ?thesis by auto ``` lp15@68120 ` 689` ``` qed ``` immler@56189 ` 690` ``` show ?th3 ``` lp15@68120 ` 691` ``` using acdb by (fastforce simp add: mem_box) ``` lp15@68120 ` 692` ``` have acdb': "a\i \ c\i \ d\i \ b\i" ``` lp15@68120 ` 693` ``` if "i \ Basis" "box c d \ box a b" "\i. i \ Basis \ c\i < d\i" for i ``` lp15@68120 ` 694` ``` using box_subset_cbox[of a b] that acdb by auto ``` immler@56189 ` 695` ``` show ?th4 ``` lp15@68120 ` 696` ``` using acdb' by (fastforce simp add: mem_box) ``` immler@56189 ` 697` ```qed ``` immler@56189 ` 698` lp15@63945 ` 699` ```lemma eq_cbox: "cbox a b = cbox c d \ cbox a b = {} \ cbox c d = {} \ a = c \ b = d" ``` lp15@63945 ` 700` ``` (is "?lhs = ?rhs") ``` lp15@63945 ` 701` ```proof ``` lp15@63945 ` 702` ``` assume ?lhs ``` lp15@63945 ` 703` ``` then have "cbox a b \ cbox c d" "cbox c d \ cbox a b" ``` lp15@63945 ` 704` ``` by auto ``` lp15@63945 ` 705` ``` then show ?rhs ``` lp15@66643 ` 706` ``` by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI) ``` lp15@63945 ` 707` ```next ``` lp15@63945 ` 708` ``` assume ?rhs ``` lp15@63945 ` 709` ``` then show ?lhs ``` lp15@63945 ` 710` ``` by force ``` lp15@63945 ` 711` ```qed ``` lp15@63945 ` 712` lp15@63945 ` 713` ```lemma eq_cbox_box [simp]: "cbox a b = box c d \ cbox a b = {} \ box c d = {}" ``` wenzelm@64539 ` 714` ``` (is "?lhs \ ?rhs") ``` lp15@63945 ` 715` ```proof ``` lp15@68120 ` 716` ``` assume L: ?lhs ``` lp15@68120 ` 717` ``` then have "cbox a b \ box c d" "box c d \ cbox a b" ``` lp15@63945 ` 718` ``` by auto ``` lp15@63945 ` 719` ``` then show ?rhs ``` hoelzl@63957 ` 720` ``` apply (simp add: subset_box) ``` lp15@68120 ` 721` ``` using L box_ne_empty box_sing apply (fastforce simp add:) ``` lp15@63945 ` 722` ``` done ``` lp15@68120 ` 723` ```qed force ``` lp15@63945 ` 724` lp15@63945 ` 725` ```lemma eq_box_cbox [simp]: "box a b = cbox c d \ box a b = {} \ cbox c d = {}" ``` lp15@63945 ` 726` ``` by (metis eq_cbox_box) ``` lp15@63945 ` 727` lp15@63945 ` 728` ```lemma eq_box: "box a b = box c d \ box a b = {} \ box c d = {} \ a = c \ b = d" ``` wenzelm@64539 ` 729` ``` (is "?lhs \ ?rhs") ``` lp15@63945 ` 730` ```proof ``` lp15@68120 ` 731` ``` assume L: ?lhs ``` lp15@63945 ` 732` ``` then have "box a b \ box c d" "box c d \ box a b" ``` lp15@63945 ` 733` ``` by auto ``` lp15@63945 ` 734` ``` then show ?rhs ``` lp15@63945 ` 735` ``` apply (simp add: subset_box) ``` lp15@68120 ` 736` ``` using box_ne_empty(2) L ``` lp15@63945 ` 737` ``` apply auto ``` lp15@63945 ` 738` ``` apply (meson euclidean_eqI less_eq_real_def not_less)+ ``` lp15@63945 ` 739` ``` done ``` lp15@68120 ` 740` ```qed force ``` lp15@63945 ` 741` eberlm@66466 ` 742` ```lemma subset_box_complex: ``` lp15@66643 ` 743` ``` "cbox a b \ cbox c d \ ``` eberlm@66466 ` 744` ``` (Re a \ Re b \ Im a \ Im b) \ Re a \ Re c \ Im a \ Im c \ Re b \ Re d \ Im b \ Im d" ``` lp15@66643 ` 745` ``` "cbox a b \ box c d \ ``` eberlm@66466 ` 746` ``` (Re a \ Re b \ Im a \ Im b) \ Re a > Re c \ Im a > Im c \ Re b < Re d \ Im b < Im d" ``` eberlm@66466 ` 747` ``` "box a b \ cbox c d \ ``` eberlm@66466 ` 748` ``` (Re a < Re b \ Im a < Im b) \ Re a \ Re c \ Im a \ Im c \ Re b \ Re d \ Im b \ Im d" ``` lp15@66643 ` 749` ``` "box a b \ box c d \ ``` eberlm@66466 ` 750` ``` (Re a < Re b \ Im a < Im b) \ Re a \ Re c \ Im a \ Im c \ Re b \ Re d \ Im b \ Im d" ``` eberlm@66466 ` 751` ``` by (subst subset_box; force simp: Basis_complex_def)+ ``` eberlm@66466 ` 752` lp15@63945 ` 753` ```lemma Int_interval: ``` immler@56189 ` 754` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 755` ``` shows "cbox a b \ cbox c d = ``` immler@56189 ` 756` ``` cbox (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\i) *\<^sub>R i)" ``` immler@56189 ` 757` ``` unfolding set_eq_iff and Int_iff and mem_box ``` immler@56189 ` 758` ``` by auto ``` immler@56189 ` 759` immler@56189 ` 760` ```lemma disjoint_interval: ``` immler@56189 ` 761` ``` fixes a::"'a::euclidean_space" ``` immler@56189 ` 762` ``` shows "cbox a b \ cbox c d = {} \ (\i\Basis. (b\i < a\i \ d\i < c\i \ b\i < c\i \ d\i < a\i))" (is ?th1) ``` immler@56189 ` 763` ``` and "cbox a b \ box c d = {} \ (\i\Basis. (b\i < a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th2) ``` immler@56189 ` 764` ``` and "box a b \ cbox c d = {} \ (\i\Basis. (b\i \ a\i \ d\i < c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th3) ``` immler@56189 ` 765` ``` and "box a b \ box c d = {} \ (\i\Basis. (b\i \ a\i \ d\i \ c\i \ b\i \ c\i \ d\i \ a\i))" (is ?th4) ``` immler@56189 ` 766` ```proof - ``` immler@56189 ` 767` ``` let ?z = "(\i\Basis. (((max (a\i) (c\i)) + (min (b\i) (d\i))) / 2) *\<^sub>R i)::'a" ``` immler@56189 ` 768` ``` have **: "\P Q. (\i :: 'a. i \ Basis \ Q ?z i \ P i) \ ``` immler@56189 ` 769` ``` (\i x :: 'a. i \ Basis \ P i \ Q x i) \ (\x. \i\Basis. Q x i) \ (\i\Basis. P i)" ``` immler@56189 ` 770` ``` by blast ``` immler@56189 ` 771` ``` note * = set_eq_iff Int_iff empty_iff mem_box ball_conj_distrib[symmetric] eq_False ball_simps(10) ``` immler@56189 ` 772` ``` show ?th1 unfolding * by (intro **) auto ``` immler@56189 ` 773` ``` show ?th2 unfolding * by (intro **) auto ``` immler@56189 ` 774` ``` show ?th3 unfolding * by (intro **) auto ``` immler@56189 ` 775` ``` show ?th4 unfolding * by (intro **) auto ``` immler@56189 ` 776` ```qed ``` immler@56189 ` 777` hoelzl@57447 ` 778` ```lemma UN_box_eq_UNIV: "(\i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One)) = UNIV" ``` hoelzl@57447 ` 779` ```proof - ``` wenzelm@61942 ` 780` ``` have "\x \ b\ < real_of_int (\Max ((\b. \x \ b\)`Basis)\ + 1)" ``` wenzelm@60462 ` 781` ``` if [simp]: "b \ Basis" for x b :: 'a ``` wenzelm@60462 ` 782` ``` proof - ``` wenzelm@61942 ` 783` ``` have "\x \ b\ \ real_of_int \\x \ b\\" ``` lp15@61609 ` 784` ``` by (rule le_of_int_ceiling) ``` wenzelm@61942 ` 785` ``` also have "\ \ real_of_int \Max ((\b. \x \ b\)`Basis)\" ``` nipkow@59587 ` 786` ``` by (auto intro!: ceiling_mono) ``` wenzelm@61942 ` 787` ``` also have "\ < real_of_int (\Max ((\b. \x \ b\)`Basis)\ + 1)" ``` hoelzl@57447 ` 788` ``` by simp ``` wenzelm@60462 ` 789` ``` finally show ?thesis . ``` wenzelm@60462 ` 790` ``` qed ``` wenzelm@60462 ` 791` ``` then have "\n::nat. \b\Basis. \x \ b\ < real n" for x :: 'a ``` nipkow@59587 ` 792` ``` by (metis order.strict_trans reals_Archimedean2) ``` hoelzl@57447 ` 793` ``` moreover have "\x b::'a. \n::nat. \x \ b\ < real n \ - real n < x \ b \ x \ b < real n" ``` hoelzl@57447 ` 794` ``` by auto ``` hoelzl@57447 ` 795` ``` ultimately show ?thesis ``` nipkow@64267 ` 796` ``` by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases) ``` hoelzl@57447 ` 797` ```qed ``` hoelzl@57447 ` 798` immler@69613 ` 799` ```lemma image_affinity_cbox: fixes m::real ``` immler@69613 ` 800` ``` fixes a b c :: "'a::euclidean_space" ``` immler@69613 ` 801` ``` shows "(\x. m *\<^sub>R x + c) ` cbox a b = ``` immler@69613 ` 802` ``` (if cbox a b = {} then {} ``` immler@69613 ` 803` ``` else (if 0 \ m then cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c) ``` immler@69613 ` 804` ``` else cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c)))" ``` immler@69613 ` 805` ```proof (cases "m = 0") ``` immler@69613 ` 806` ``` case True ``` immler@69613 ` 807` ``` { ``` immler@69613 ` 808` ``` fix x ``` immler@69613 ` 809` ``` assume "\i\Basis. x \ i \ c \ i" "\i\Basis. c \ i \ x \ i" ``` immler@69613 ` 810` ``` then have "x = c" ``` immler@69613 ` 811` ``` by (simp add: dual_order.antisym euclidean_eqI) ``` immler@69613 ` 812` ``` } ``` immler@69613 ` 813` ``` moreover have "c \ cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)" ``` immler@69613 ` 814` ``` unfolding True by (auto simp: cbox_sing) ``` immler@69613 ` 815` ``` ultimately show ?thesis using True by (auto simp: cbox_def) ``` immler@69613 ` 816` ```next ``` immler@69613 ` 817` ``` case False ``` immler@69613 ` 818` ``` { ``` immler@69613 ` 819` ``` fix y ``` immler@69613 ` 820` ``` assume "\i\Basis. a \ i \ y \ i" "\i\Basis. y \ i \ b \ i" "m > 0" ``` immler@69613 ` 821` ``` then have "\i\Basis. (m *\<^sub>R a + c) \ i \ (m *\<^sub>R y + c) \ i" and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>R b + c) \ i" ``` immler@69613 ` 822` ``` by (auto simp: inner_distrib) ``` immler@69613 ` 823` ``` } ``` immler@69613 ` 824` ``` moreover ``` immler@69613 ` 825` ``` { ``` immler@69613 ` 826` ``` fix y ``` immler@69613 ` 827` ``` assume "\i\Basis. a \ i \ y \ i" "\i\Basis. y \ i \ b \ i" "m < 0" ``` immler@69613 ` 828` ``` then have "\i\Basis. (m *\<^sub>R b + c) \ i \ (m *\<^sub>R y + c) \ i" and "\i\Basis. (m *\<^sub>R y + c) \ i \ (m *\<^sub>R a + c) \ i" ``` immler@69613 ` 829` ``` by (auto simp: mult_left_mono_neg inner_distrib) ``` immler@69613 ` 830` ``` } ``` immler@69613 ` 831` ``` moreover ``` immler@69613 ` 832` ``` { ``` immler@69613 ` 833` ``` fix y ``` immler@69613 ` 834` ``` assume "m > 0" and "\i\Basis. (m *\<^sub>R a + c) \ i \ y \ i" and "\i\Basis. y \ i \ (m *\<^sub>R b + c) \ i" ``` immler@69613 ` 835` ``` then have "y \ (\x. m *\<^sub>R x + c) ` cbox a b" ``` immler@69613 ` 836` ``` unfolding image_iff Bex_def mem_box ``` immler@69613 ` 837` ``` apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) ``` immler@69613 ` 838` ``` apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left) ``` immler@69613 ` 839` ``` done ``` immler@69613 ` 840` ``` } ``` immler@69613 ` 841` ``` moreover ``` immler@69613 ` 842` ``` { ``` immler@69613 ` 843` ``` fix y ``` immler@69613 ` 844` ``` assume "\i\Basis. (m *\<^sub>R b + c) \ i \ y \ i" "\i\Basis. y \ i \ (m *\<^sub>R a + c) \ i" "m < 0" ``` immler@69613 ` 845` ``` then have "y \ (\x. m *\<^sub>R x + c) ` cbox a b" ``` immler@69613 ` 846` ``` unfolding image_iff Bex_def mem_box ``` immler@69613 ` 847` ``` apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) ``` immler@69613 ` 848` ``` apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left) ``` immler@69613 ` 849` ``` done ``` immler@69613 ` 850` ``` } ``` immler@69613 ` 851` ``` ultimately show ?thesis using False by (auto simp: cbox_def) ``` immler@69613 ` 852` ```qed ``` immler@69613 ` 853` immler@69613 ` 854` ```lemma image_smult_cbox:"(\x. m *\<^sub>R (x::_::euclidean_space)) ` cbox a b = ``` immler@69613 ` 855` ``` (if cbox a b = {} then {} else if 0 \ m then cbox (m *\<^sub>R a) (m *\<^sub>R b) else cbox (m *\<^sub>R b) (m *\<^sub>R a))" ``` immler@69613 ` 856` ``` using image_affinity_cbox[of m 0 a b] by auto ``` immler@69613 ` 857` immler@69619 ` 858` ```lemma swap_continuous: ``` immler@69619 ` 859` ``` assumes "continuous_on (cbox (a,c) (b,d)) (\(x,y). f x y)" ``` immler@69619 ` 860` ``` shows "continuous_on (cbox (c,a) (d,b)) (\(x, y). f y x)" ``` immler@69619 ` 861` ```proof - ``` immler@69619 ` 862` ``` have "(\(x, y). f y x) = (\(x, y). f x y) \ prod.swap" ``` immler@69619 ` 863` ``` by auto ``` immler@69619 ` 864` ``` then show ?thesis ``` immler@69619 ` 865` ``` apply (rule ssubst) ``` immler@69619 ` 866` ``` apply (rule continuous_on_compose) ``` immler@69619 ` 867` ``` apply (simp add: split_def) ``` immler@69619 ` 868` ``` apply (rule continuous_intros | simp add: assms)+ ``` immler@69619 ` 869` ``` done ``` immler@69619 ` 870` ```qed ``` immler@69619 ` 871` immler@69516 ` 872` nipkow@69508 ` 873` ```subsection \General Intervals\ ``` immler@67962 ` 874` immler@67962 ` 875` ```definition%important "is_interval (s::('a::euclidean_space) set) \ ``` immler@56189 ` 876` ``` (\a\s. \b\s. \x. (\i\Basis. ((a\i \ x\i \ x\i \ b\i) \ (b\i \ x\i \ x\i \ a\i))) \ x \ s)" ``` immler@56189 ` 877` immler@67685 ` 878` ```lemma is_interval_1: ``` immler@67685 ` 879` ``` "is_interval (s::real set) \ (\a\s. \b\s. \ x. a \ x \ x \ b \ x \ s)" ``` immler@67685 ` 880` ``` unfolding is_interval_def by auto ``` immler@67685 ` 881` immler@67685 ` 882` ```lemma is_interval_inter: "is_interval X \ is_interval Y \ is_interval (X \ Y)" ``` immler@67685 ` 883` ``` unfolding is_interval_def ``` immler@67685 ` 884` ``` by blast ``` immler@67685 ` 885` lp15@66089 ` 886` ```lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1) ``` lp15@66089 ` 887` ``` and is_interval_box [simp]: "is_interval (box a b)" (is ?th2) ``` immler@56189 ` 888` ``` unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff ``` immler@56189 ` 889` ``` by (meson order_trans le_less_trans less_le_trans less_trans)+ ``` immler@56189 ` 890` lp15@61609 ` 891` ```lemma is_interval_empty [iff]: "is_interval {}" ``` lp15@61609 ` 892` ``` unfolding is_interval_def by simp ``` lp15@61609 ` 893` lp15@61609 ` 894` ```lemma is_interval_univ [iff]: "is_interval UNIV" ``` lp15@61609 ` 895` ``` unfolding is_interval_def by simp ``` immler@56189 ` 896` immler@56189 ` 897` ```lemma mem_is_intervalI: ``` immler@56189 ` 898` ``` assumes "is_interval s" ``` wenzelm@64539 ` 899` ``` and "a \ s" "b \ s" ``` wenzelm@64539 ` 900` ``` and "\i. i \ Basis \ a \ i \ x \ i \ x \ i \ b \ i \ b \ i \ x \ i \ x \ i \ a \ i" ``` immler@56189 ` 901` ``` shows "x \ s" ``` immler@56189 ` 902` ``` by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)]) ``` immler@56189 ` 903` immler@56189 ` 904` ```lemma interval_subst: ``` immler@56189 ` 905` ``` fixes S::"'a::euclidean_space set" ``` immler@56189 ` 906` ``` assumes "is_interval S" ``` wenzelm@64539 ` 907` ``` and "x \ S" "y j \ S" ``` wenzelm@64539 ` 908` ``` and "j \ Basis" ``` immler@56189 ` 909` ``` shows "(\i\Basis. (if i = j then y i \ i else x \ i) *\<^sub>R i) \ S" ``` immler@56189 ` 910` ``` by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms) ``` immler@56189 ` 911` immler@56189 ` 912` ```lemma mem_box_componentwiseI: ``` immler@56189 ` 913` ``` fixes S::"'a::euclidean_space set" ``` immler@56189 ` 914` ``` assumes "is_interval S" ``` immler@56189 ` 915` ``` assumes "\i. i \ Basis \ x \ i \ ((\x. x \ i) ` S)" ``` immler@56189 ` 916` ``` shows "x \ S" ``` immler@56189 ` 917` ```proof - ``` immler@56189 ` 918` ``` from assms have "\i \ Basis. \s \ S. x \ i = s \ i" ``` immler@56189 ` 919` ``` by auto ``` wenzelm@64539 ` 920` ``` with finite_Basis obtain s and bs::"'a list" ``` wenzelm@64539 ` 921` ``` where s: "\i. i \ Basis \ x \ i = s i \ i" "\i. i \ Basis \ s i \ S" ``` wenzelm@64539 ` 922` ``` and bs: "set bs = Basis" "distinct bs" ``` immler@56189 ` 923` ``` by (metis finite_distinct_list) ``` wenzelm@64539 ` 924` ``` from nonempty_Basis s obtain j where j: "j \ Basis" "s j \ S" ``` wenzelm@64539 ` 925` ``` by blast ``` wenzelm@63040 ` 926` ``` define y where ``` wenzelm@63040 ` 927` ``` "y = rec_list (s j) (\j _ Y. (\i\Basis. (if i = j then s i \ i else Y \ i) *\<^sub>R i))" ``` immler@56189 ` 928` ``` have "x = (\i\Basis. (if i \ set bs then s i \ i else s j \ i) *\<^sub>R i)" ``` lp15@66643 ` 929` ``` using bs by (auto simp: s(1)[symmetric] euclidean_representation) ``` immler@56189 ` 930` ``` also have [symmetric]: "y bs = \" ``` immler@56189 ` 931` ``` using bs(2) bs(1)[THEN equalityD1] ``` immler@56189 ` 932` ``` by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a]) ``` immler@56189 ` 933` ``` also have "y bs \ S" ``` immler@56189 ` 934` ``` using bs(1)[THEN equalityD1] ``` immler@56189 ` 935` ``` apply (induct bs) ``` wenzelm@64539 ` 936` ``` apply (auto simp: y_def j) ``` immler@56189 ` 937` ``` apply (rule interval_subst[OF assms(1)]) ``` wenzelm@64539 ` 938` ``` apply (auto simp: s) ``` immler@56189 ` 939` ``` done ``` immler@56189 ` 940` ``` finally show ?thesis . ``` immler@56189 ` 941` ```qed ``` immler@56189 ` 942` lp15@63007 ` 943` ```lemma cbox01_nonempty [simp]: "cbox 0 One \ {}" ``` nipkow@64267 ` 944` ``` by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg) ``` lp15@63007 ` 945` lp15@63007 ` 946` ```lemma box01_nonempty [simp]: "box 0 One \ {}" ``` lp15@66089 ` 947` ``` by (simp add: box_ne_empty inner_Basis inner_sum_left) ``` lp15@63075 ` 948` lp15@64773 ` 949` ```lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)" ``` lp15@64773 ` 950` ``` using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast ``` lp15@64773 ` 951` lp15@66089 ` 952` ```lemma interval_subset_is_interval: ``` lp15@66089 ` 953` ``` assumes "is_interval S" ``` lp15@66089 ` 954` ``` shows "cbox a b \ S \ cbox a b = {} \ a \ S \ b \ S" (is "?lhs = ?rhs") ``` lp15@66089 ` 955` ```proof ``` lp15@66089 ` 956` ``` assume ?lhs ``` lp15@66089 ` 957` ``` then show ?rhs using box_ne_empty(1) mem_box(2) by fastforce ``` lp15@66089 ` 958` ```next ``` lp15@66089 ` 959` ``` assume ?rhs ``` lp15@66089 ` 960` ``` have "cbox a b \ S" if "a \ S" "b \ S" ``` lp15@66089 ` 961` ``` using assms unfolding is_interval_def ``` lp15@66089 ` 962` ``` apply (clarsimp simp add: mem_box) ``` lp15@66089 ` 963` ``` using that by blast ``` lp15@66089 ` 964` ``` with \?rhs\ show ?lhs ``` lp15@66089 ` 965` ``` by blast ``` lp15@66089 ` 966` ```qed ``` lp15@66089 ` 967` immler@67685 ` 968` ```lemma is_real_interval_union: ``` immler@67685 ` 969` ``` "is_interval (X \ Y)" ``` immler@67685 ` 970` ``` if X: "is_interval X" and Y: "is_interval Y" and I: "(X \ {} \ Y \ {} \ X \ Y \ {})" ``` immler@67685 ` 971` ``` for X Y::"real set" ``` immler@67685 ` 972` ```proof - ``` immler@67685 ` 973` ``` consider "X \ {}" "Y \ {}" | "X = {}" | "Y = {}" by blast ``` immler@67685 ` 974` ``` then show ?thesis ``` immler@67685 ` 975` ``` proof cases ``` immler@67685 ` 976` ``` case 1 ``` immler@67685 ` 977` ``` then obtain r where "r \ X \ X \ Y = {}" "r \ Y \ X \ Y = {}" ``` immler@67685 ` 978` ``` by blast ``` immler@67685 ` 979` ``` then show ?thesis ``` immler@67685 ` 980` ``` using I 1 X Y unfolding is_interval_1 ``` immler@67685 ` 981` ``` by (metis (full_types) Un_iff le_cases) ``` immler@67685 ` 982` ``` qed (use that in auto) ``` immler@67685 ` 983` ```qed ``` immler@67685 ` 984` immler@67685 ` 985` ```lemma is_interval_translationI: ``` immler@67685 ` 986` ``` assumes "is_interval X" ``` immler@67685 ` 987` ``` shows "is_interval ((+) x ` X)" ``` immler@67685 ` 988` ``` unfolding is_interval_def ``` immler@67685 ` 989` ```proof safe ``` immler@67685 ` 990` ``` fix b d e ``` immler@67685 ` 991` ``` assume "b \ X" "d \ X" ``` immler@67685 ` 992` ``` "\i\Basis. (x + b) \ i \ e \ i \ e \ i \ (x + d) \ i \ ``` immler@67685 ` 993` ``` (x + d) \ i \ e \ i \ e \ i \ (x + b) \ i" ``` immler@67685 ` 994` ``` hence "e - x \ X" ``` immler@67685 ` 995` ``` by (intro mem_is_intervalI[OF assms \b \ X\ \d \ X\, of "e - x"]) ``` immler@67685 ` 996` ``` (auto simp: algebra_simps) ``` immler@67685 ` 997` ``` thus "e \ (+) x ` X" by force ``` immler@67685 ` 998` ```qed ``` immler@67685 ` 999` immler@67685 ` 1000` ```lemma is_interval_uminusI: ``` immler@67685 ` 1001` ``` assumes "is_interval X" ``` immler@67685 ` 1002` ``` shows "is_interval (uminus ` X)" ``` immler@67685 ` 1003` ``` unfolding is_interval_def ``` immler@67685 ` 1004` ```proof safe ``` immler@67685 ` 1005` ``` fix b d e ``` immler@67685 ` 1006` ``` assume "b \ X" "d \ X" ``` immler@67685 ` 1007` ``` "\i\Basis. (- b) \ i \ e \ i \ e \ i \ (- d) \ i \ ``` immler@67685 ` 1008` ``` (- d) \ i \ e \ i \ e \ i \ (- b) \ i" ``` immler@67685 ` 1009` ``` hence "- e \ X" ``` immler@67685 ` 1010` ``` by (intro mem_is_intervalI[OF assms \b \ X\ \d \ X\, of "- e"]) ``` immler@67685 ` 1011` ``` (auto simp: algebra_simps) ``` immler@67685 ` 1012` ``` thus "e \ uminus ` X" by force ``` immler@67685 ` 1013` ```qed ``` immler@67685 ` 1014` immler@67685 ` 1015` ```lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x" ``` immler@67685 ` 1016` ``` using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"] ``` immler@67685 ` 1017` ``` by (auto simp: image_image) ``` immler@67685 ` 1018` immler@67685 ` 1019` ```lemma is_interval_neg_translationI: ``` immler@67685 ` 1020` ``` assumes "is_interval X" ``` immler@67685 ` 1021` ``` shows "is_interval ((-) x ` X)" ``` immler@67685 ` 1022` ```proof - ``` immler@67685 ` 1023` ``` have "(-) x ` X = (+) x ` uminus ` X" ``` immler@67685 ` 1024` ``` by (force simp: algebra_simps) ``` immler@67685 ` 1025` ``` also have "is_interval \" ``` immler@67685 ` 1026` ``` by (metis is_interval_uminusI is_interval_translationI assms) ``` immler@67685 ` 1027` ``` finally show ?thesis . ``` immler@67685 ` 1028` ```qed ``` immler@67685 ` 1029` immler@67685 ` 1030` ```lemma is_interval_translation[simp]: ``` immler@67685 ` 1031` ``` "is_interval ((+) x ` X) = is_interval X" ``` immler@67685 ` 1032` ``` using is_interval_neg_translationI[of "(+) x ` X" x] ``` immler@67685 ` 1033` ``` by (auto intro!: is_interval_translationI simp: image_image) ``` immler@67685 ` 1034` immler@67685 ` 1035` ```lemma is_interval_minus_translation[simp]: ``` immler@67685 ` 1036` ``` shows "is_interval ((-) x ` X) = is_interval X" ``` immler@67685 ` 1037` ```proof - ``` immler@67685 ` 1038` ``` have "(-) x ` X = (+) x ` uminus ` X" ``` immler@67685 ` 1039` ``` by (force simp: algebra_simps) ``` immler@67685 ` 1040` ``` also have "is_interval \ = is_interval X" ``` immler@67685 ` 1041` ``` by simp ``` immler@67685 ` 1042` ``` finally show ?thesis . ``` immler@67685 ` 1043` ```qed ``` immler@67685 ` 1044` immler@67685 ` 1045` ```lemma is_interval_minus_translation'[simp]: ``` immler@67685 ` 1046` ``` shows "is_interval ((\x. x - c) ` X) = is_interval X" ``` immler@67685 ` 1047` ``` using is_interval_translation[of "-c" X] ``` immler@67685 ` 1048` ``` by (metis image_cong uminus_add_conv_diff) ``` immler@67685 ` 1049` immler@69611 ` 1050` immler@69611 ` 1051` ```subsection%unimportant \Bounded Projections\ ``` immler@62127 ` 1052` immler@69611 ` 1053` ```lemma bounded_inner_imp_bdd_above: ``` immler@69611 ` 1054` ``` assumes "bounded s" ``` immler@69611 ` 1055` ``` shows "bdd_above ((\x. x \ a) ` s)" ``` immler@69611 ` 1056` ```by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left) ``` himmelma@33175 ` 1057` immler@69611 ` 1058` ```lemma bounded_inner_imp_bdd_below: ``` immler@69611 ` 1059` ``` assumes "bounded s" ``` immler@69611 ` 1060` ``` shows "bdd_below ((\x. x \ a) ` s)" ``` immler@69611 ` 1061` ```by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left) ``` huffman@44632 ` 1062` wenzelm@53282 ` 1063` immler@69611 ` 1064` ```subsection%unimportant \Structural rules for pointwise continuity\ ``` himmelma@33175 ` 1065` hoelzl@51361 ` 1066` ```lemma continuous_infnorm[continuous_intros]: ``` wenzelm@53282 ` 1067` ``` "continuous F f \ continuous F (\x. infnorm (f x))" ``` huffman@44647 ` 1068` ``` unfolding continuous_def by (rule tendsto_infnorm) ``` himmelma@33175 ` 1069` hoelzl@51361 ` 1070` ```lemma continuous_inner[continuous_intros]: ``` wenzelm@53282 ` 1071` ``` assumes "continuous F f" ``` wenzelm@53282 ` 1072` ``` and "continuous F g" ``` huffman@44647 ` 1073` ``` shows "continuous F (\x. inner (f x) (g x))" ``` huffman@44647 ` 1074` ``` using assms unfolding continuous_def by (rule tendsto_inner) ``` huffman@44647 ` 1075` immler@69516 ` 1076` immler@69611 ` 1077` ```subsection%unimportant \Structural rules for setwise continuity\ ``` himmelma@33175 ` 1078` hoelzl@56371 ` 1079` ```lemma continuous_on_infnorm[continuous_intros]: ``` wenzelm@53282 ` 1080` ``` "continuous_on s f \ continuous_on s (\x. infnorm (f x))" ``` huffman@44647 ` 1081` ``` unfolding continuous_on by (fast intro: tendsto_infnorm) ``` huffman@44647 ` 1082` hoelzl@56371 ` 1083` ```lemma continuous_on_inner[continuous_intros]: ``` huffman@44531 ` 1084` ``` fixes g :: "'a::topological_space \ 'b::real_inner" ``` wenzelm@53282 ` 1085` ``` assumes "continuous_on s f" ``` wenzelm@53282 ` 1086` ``` and "continuous_on s g" ``` huffman@44531 ` 1087` ``` shows "continuous_on s (\x. inner (f x) (g x))" ``` huffman@44531 ` 1088` ``` using bounded_bilinear_inner assms ``` huffman@44531 ` 1089` ``` by (rule bounded_bilinear.continuous_on) ``` huffman@44531 ` 1090` immler@69613 ` 1091` immler@69613 ` 1092` ```subsection%unimportant \Openness of halfspaces.\ ``` himmelma@33175 ` 1093` himmelma@33175 ` 1094` ```lemma open_halfspace_lt: "open {x. inner a x < b}" ``` hoelzl@63332 ` 1095` ``` by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) ``` himmelma@33175 ` 1096` himmelma@33175 ` 1097` ```lemma open_halfspace_gt: "open {x. inner a x > b}" ``` hoelzl@63332 ` 1098` ``` by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) ``` himmelma@33175 ` 1099` wenzelm@53282 ` 1100` ```lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\i < a}" ``` hoelzl@63332 ` 1101` ``` by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) ``` himmelma@33175 ` 1102` wenzelm@53282 ` 1103` ```lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\i > a}" ``` hoelzl@63332 ` 1104` ``` by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id) ``` himmelma@33175 ` 1105` immler@69611 ` 1106` ```lemma eucl_less_eq_halfspaces: ``` immler@69611 ` 1107` ``` fixes a :: "'a::euclidean_space" ``` immler@69611 ` 1108` ``` shows "{x. x i\Basis. {x. x \ i < a \ i})" ``` immler@69611 ` 1109` ``` "{x. a i\Basis. {x. a \ i < x \ i})" ``` immler@69611 ` 1110` ``` by (auto simp: eucl_less_def) ``` immler@69611 ` 1111` immler@69611 ` 1112` ```lemma open_Collect_eucl_less[simp, intro]: ``` immler@69611 ` 1113` ``` fixes a :: "'a::euclidean_space" ``` immler@69611 ` 1114` ``` shows "open {x. x Closure of halfspaces and hyperplanes\ ``` immler@69613 ` 1118` immler@69613 ` 1119` ```lemma continuous_at_inner: "continuous (at x) (inner a)" ``` immler@69613 ` 1120` ``` unfolding continuous_at by (intro tendsto_intros) ``` immler@69613 ` 1121` immler@69613 ` 1122` ```lemma closed_halfspace_le: "closed {x. inner a x \ b}" ``` immler@69613 ` 1123` ``` by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1124` immler@69613 ` 1125` ```lemma closed_halfspace_ge: "closed {x. inner a x \ b}" ``` immler@69613 ` 1126` ``` by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1127` immler@69613 ` 1128` ```lemma closed_hyperplane: "closed {x. inner a x = b}" ``` immler@69613 ` 1129` ``` by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1130` immler@69613 ` 1131` ```lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\i \ a}" ``` immler@69613 ` 1132` ``` by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1133` immler@69613 ` 1134` ```lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\i \ a}" ``` immler@69613 ` 1135` ``` by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1136` immler@69613 ` 1137` ```lemma closed_interval_left: ``` immler@69613 ` 1138` ``` fixes b :: "'a::euclidean_space" ``` immler@69613 ` 1139` ``` shows "closed {x::'a. \i\Basis. x\i \ b\i}" ``` immler@69613 ` 1140` ``` by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1141` immler@69613 ` 1142` ```lemma closed_interval_right: ``` immler@69613 ` 1143` ``` fixes a :: "'a::euclidean_space" ``` immler@69613 ` 1144` ``` shows "closed {x::'a. \i\Basis. a\i \ x\i}" ``` immler@69613 ` 1145` ``` by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id) ``` immler@69613 ` 1146` immler@69613 ` 1147` immler@69613 ` 1148` ```subsection%unimportant\Some more convenient intermediate-value theorem formulations\ ``` immler@69613 ` 1149` immler@69613 ` 1150` ```lemma connected_ivt_hyperplane: ``` immler@69613 ` 1151` ``` assumes "connected S" and xy: "x \ S" "y \ S" and b: "inner a x \ b" "b \ inner a y" ``` immler@69613 ` 1152` ``` shows "\z \ S. inner a z = b" ``` immler@69613 ` 1153` ```proof (rule ccontr) ``` immler@69613 ` 1154` ``` assume as:"\ (\z\S. inner a z = b)" ``` immler@69613 ` 1155` ``` let ?A = "{x. inner a x < b}" ``` immler@69613 ` 1156` ``` let ?B = "{x. inner a x > b}" ``` immler@69613 ` 1157` ``` have "open ?A" "open ?B" ``` immler@69613 ` 1158` ``` using open_halfspace_lt and open_halfspace_gt by auto ``` immler@69613 ` 1159` ``` moreover have "?A \ ?B = {}" by auto ``` immler@69613 ` 1160` ``` moreover have "S \ ?A \ ?B" using as by auto ``` immler@69613 ` 1161` ``` ultimately show False ``` immler@69613 ` 1162` ``` using \connected S\[unfolded connected_def not_ex, ``` immler@69613 ` 1163` ``` THEN spec[where x="?A"], THEN spec[where x="?B"]] ``` immler@69613 ` 1164` ``` using xy b by auto ``` immler@69613 ` 1165` ```qed ``` immler@69613 ` 1166` immler@69613 ` 1167` ```lemma connected_ivt_component: ``` immler@69613 ` 1168` ``` fixes x::"'a::euclidean_space" ``` immler@69613 ` 1169` ``` shows "connected S \ x \ S \ y \ S \ x\k \ a \ a \ y\k \ (\z\S. z\k = a)" ``` immler@69613 ` 1170` ``` using connected_ivt_hyperplane[of S x y "k::'a" a] ``` immler@69613 ` 1171` ``` by (auto simp: inner_commute) ``` immler@69613 ` 1172` immler@69611 ` 1173` immler@69611 ` 1174` ```subsection \Limit Component Bounds\ ``` himmelma@33175 ` 1175` immler@69613 ` 1176` ```lemma Lim_component_le: ``` immler@69613 ` 1177` ``` fixes f :: "'a \ 'b::euclidean_space" ``` immler@69613 ` 1178` ``` assumes "(f \ l) net" ``` immler@69613 ` 1179` ``` and "\ (trivial_limit net)" ``` immler@69613 ` 1180` ``` and "eventually (\x. f(x)\i \ b) net" ``` immler@69613 ` 1181` ``` shows "l\i \ b" ``` immler@69613 ` 1182` ``` by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)]) ``` immler@69613 ` 1183` immler@69613 ` 1184` ```lemma Lim_component_ge: ``` immler@69613 ` 1185` ``` fixes f :: "'a \ 'b::euclidean_space" ``` immler@69613 ` 1186` ``` assumes "(f \ l) net" ``` immler@69613 ` 1187` ``` and "\ (trivial_limit net)" ``` immler@69613 ` 1188` ``` and "eventually (\x. b \ (f x)\i) net" ``` immler@69613 ` 1189` ``` shows "b \ l\i" ``` immler@69613 ` 1190` ``` by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)]) ``` immler@69613 ` 1191` immler@69613 ` 1192` ```lemma Lim_component_eq: ``` immler@69613 ` 1193` ``` fixes f :: "'a \ 'b::euclidean_space" ``` immler@69613 ` 1194` ``` assumes net: "(f \ l) net" "\ trivial_limit net" ``` immler@69613 ` 1195` ``` and ev:"eventually (\x. f(x)\i = b) net" ``` immler@69613 ` 1196` ``` shows "l\i = b" ``` immler@69613 ` 1197` ``` using ev[unfolded order_eq_iff eventually_conj_iff] ``` immler@69613 ` 1198` ``` using Lim_component_ge[OF net, of b i] ``` immler@69613 ` 1199` ``` using Lim_component_le[OF net, of i b] ``` immler@69613 ` 1200` ``` by auto ``` immler@69613 ` 1201` immler@56189 ` 1202` ```lemma open_box[intro]: "open (box a b)" ``` immler@56189 ` 1203` ```proof - ``` nipkow@67399 ` 1204` ``` have "open (\i\Basis. ((\) i) -` {a \ i <..< b \ i})" ``` lp15@62533 ` 1205` ``` by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const) ``` nipkow@67399 ` 1206` ``` also have "(\i\Basis. ((\) i) -` {a \ i <..< b \ i}) = box a b" ``` lp15@66643 ` 1207` ``` by (auto simp: box_def inner_commute) ``` immler@56189 ` 1208` ``` finally show ?thesis . ``` immler@56189 ` 1209` ```qed ``` immler@56189 ` 1210` immler@56189 ` 1211` ```lemma closed_cbox[intro]: ``` immler@56189 ` 1212` ``` fixes a b :: "'a::euclidean_space" ``` immler@56189 ` 1213` ``` shows "closed (cbox a b)" ``` immler@56189 ` 1214` ```proof - ``` immler@56189 ` 1215` ``` have "closed (\i\Basis. (\x. x\i) -` {a\i .. b\i})" ``` immler@56189 ` 1216` ``` by (intro closed_INT ballI continuous_closed_vimage allI ``` immler@56189 ` 1217` ``` linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left) ``` immler@56189 ` 1218` ``` also have "(\i\Basis. (\x. x\i) -` {a\i .. b\i}) = cbox a b" ``` lp15@66643 ` 1219` ``` by (auto simp: cbox_def) ``` immler@56189 ` 1220` ``` finally show "closed (cbox a b)" . ``` immler@56189 ` 1221` ```qed ``` immler@56189 ` 1222` lp15@62618 ` 1223` ```lemma interior_cbox [simp]: ``` immler@56189 ` 1224` ``` fixes a b :: "'a::euclidean_space" ``` immler@56189 ` 1225` ``` shows "interior (cbox a b) = box a b" (is "?L = ?R") ``` immler@56189 ` 1226` ```proof(rule subset_antisym) ``` immler@56189 ` 1227` ``` show "?R \ ?L" ``` immler@56189 ` 1228` ``` using box_subset_cbox open_box ``` immler@56189 ` 1229` ``` by (rule interior_maximal) ``` immler@56189 ` 1230` ``` { ``` immler@56189 ` 1231` ``` fix x ``` immler@56189 ` 1232` ``` assume "x \ interior (cbox a b)" ``` immler@56189 ` 1233` ``` then obtain s where s: "open s" "x \ s" "s \ cbox a b" .. ``` immler@56189 ` 1234` ``` then obtain e where "e>0" and e:"\x'. dist x' x < e \ x' \ cbox a b" ``` immler@56189 ` 1235` ``` unfolding open_dist and subset_eq by auto ``` immler@56189 ` 1236` ``` { ``` immler@56189 ` 1237` ``` fix i :: 'a ``` immler@56189 ` 1238` ``` assume i: "i \ Basis" ``` immler@56189 ` 1239` ``` have "dist (x - (e / 2) *\<^sub>R i) x < e" ``` immler@56189 ` 1240` ``` and "dist (x + (e / 2) *\<^sub>R i) x < e" ``` immler@56189 ` 1241` ``` unfolding dist_norm ``` immler@56189 ` 1242` ``` apply auto ``` immler@56189 ` 1243` ``` unfolding norm_minus_cancel ``` wenzelm@60420 ` 1244` ``` using norm_Basis[OF i] \e>0\ ``` immler@56189 ` 1245` ``` apply auto ``` immler@56189 ` 1246` ``` done ``` immler@56189 ` 1247` ``` then have "a \ i \ (x - (e / 2) *\<^sub>R i) \ i" and "(x + (e / 2) *\<^sub>R i) \ i \ b \ i" ``` immler@56189 ` 1248` ``` using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]] ``` immler@56189 ` 1249` ``` and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]] ``` immler@56189 ` 1250` ``` unfolding mem_box ``` immler@56189 ` 1251` ``` using i ``` immler@56189 ` 1252` ``` by blast+ ``` immler@56189 ` 1253` ``` then have "a \ i < x \ i" and "x \ i < b \ i" ``` wenzelm@60420 ` 1254` ``` using \e>0\ i ``` immler@56189 ` 1255` ``` by (auto simp: inner_diff_left inner_Basis inner_add_left) ``` immler@56189 ` 1256` ``` } ``` immler@56189 ` 1257` ``` then have "x \ box a b" ``` immler@56189 ` 1258` ``` unfolding mem_box by auto ``` immler@56189 ` 1259` ``` } ``` immler@56189 ` 1260` ``` then show "?L \ ?R" .. ``` immler@56189 ` 1261` ```qed ``` immler@56189 ` 1262` lp15@63928 ` 1263` ```lemma bounded_cbox [simp]: ``` immler@56189 ` 1264` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1265` ``` shows "bounded (cbox a b)" ``` immler@56189 ` 1266` ```proof - ``` immler@56189 ` 1267` ``` let ?b = "\i\Basis. \a\i\ + \b\i\" ``` immler@56189 ` 1268` ``` { ``` immler@56189 ` 1269` ``` fix x :: "'a" ``` lp15@68120 ` 1270` ``` assume "\i. i\Basis \ a \ i \ x \ i \ x \ i \ b \ i" ``` immler@56189 ` 1271` ``` then have "(\i\Basis. \x \ i\) \ ?b" ``` lp15@68120 ` 1272` ``` by (force simp: intro!: sum_mono) ``` immler@56189 ` 1273` ``` then have "norm x \ ?b" ``` immler@56189 ` 1274` ``` using norm_le_l1[of x] by auto ``` immler@56189 ` 1275` ``` } ``` immler@56189 ` 1276` ``` then show ?thesis ``` lp15@68120 ` 1277` ``` unfolding cbox_def bounded_iff by force ``` immler@56189 ` 1278` ```qed ``` immler@56189 ` 1279` lp15@62618 ` 1280` ```lemma bounded_box [simp]: ``` immler@56189 ` 1281` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1282` ``` shows "bounded (box a b)" ``` lp15@68120 ` 1283` ``` using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"] ``` immler@56189 ` 1284` ``` by simp ``` immler@56189 ` 1285` lp15@62618 ` 1286` ```lemma not_interval_UNIV [simp]: ``` immler@56189 ` 1287` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1288` ``` shows "cbox a b \ UNIV" "box a b \ UNIV" ``` lp15@62618 ` 1289` ``` using bounded_box[of a b] bounded_cbox[of a b] by force+ ``` lp15@62618 ` 1290` lp15@63945 ` 1291` ```lemma not_interval_UNIV2 [simp]: ``` lp15@63945 ` 1292` ``` fixes a :: "'a::euclidean_space" ``` lp15@63945 ` 1293` ``` shows "UNIV \ cbox a b" "UNIV \ box a b" ``` lp15@63945 ` 1294` ``` using bounded_box[of a b] bounded_cbox[of a b] by force+ ``` lp15@63945 ` 1295` immler@56189 ` 1296` ```lemma box_midpoint: ``` immler@56189 ` 1297` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1298` ``` assumes "box a b \ {}" ``` immler@56189 ` 1299` ``` shows "((1/2) *\<^sub>R (a + b)) \ box a b" ``` immler@56189 ` 1300` ```proof - ``` lp15@68120 ` 1301` ``` have "a \ i < ((1 / 2) *\<^sub>R (a + b)) \ i \ ((1 / 2) *\<^sub>R (a + b)) \ i < b \ i" if "i \ Basis" for i ``` lp15@68120 ` 1302` ``` using assms that by (auto simp: inner_add_left box_ne_empty) ``` immler@56189 ` 1303` ``` then show ?thesis unfolding mem_box by auto ``` immler@56189 ` 1304` ```qed ``` immler@56189 ` 1305` immler@56189 ` 1306` ```lemma open_cbox_convex: ``` immler@56189 ` 1307` ``` fixes x :: "'a::euclidean_space" ``` immler@56189 ` 1308` ``` assumes x: "x \ box a b" ``` immler@56189 ` 1309` ``` and y: "y \ cbox a b" ``` immler@56189 ` 1310` ``` and e: "0 < e" "e \ 1" ``` immler@56189 ` 1311` ``` shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ box a b" ``` immler@56189 ` 1312` ```proof - ``` immler@56189 ` 1313` ``` { ``` immler@56189 ` 1314` ``` fix i :: 'a ``` immler@56189 ` 1315` ``` assume i: "i \ Basis" ``` immler@56189 ` 1316` ``` have "a \ i = e * (a \ i) + (1 - e) * (a \ i)" ``` immler@56189 ` 1317` ``` unfolding left_diff_distrib by simp ``` immler@56189 ` 1318` ``` also have "\ < e * (x \ i) + (1 - e) * (y \ i)" ``` lp15@68120 ` 1319` ``` proof (rule add_less_le_mono) ``` lp15@68120 ` 1320` ``` show "e * (a \ i) < e * (x \ i)" ``` lp15@68120 ` 1321` ``` using \0 < e\ i mem_box(1) x by auto ``` lp15@68120 ` 1322` ``` show "(1 - e) * (a \ i) \ (1 - e) * (y \ i)" ``` lp15@68120 ` 1323` ``` by (meson diff_ge_0_iff_ge \e \ 1\ i mem_box(2) mult_left_mono y) ``` lp15@68120 ` 1324` ``` qed ``` immler@56189 ` 1325` ``` finally have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i" ``` immler@56189 ` 1326` ``` unfolding inner_simps by auto ``` immler@56189 ` 1327` ``` moreover ``` immler@56189 ` 1328` ``` { ``` immler@56189 ` 1329` ``` have "b \ i = e * (b\i) + (1 - e) * (b\i)" ``` immler@56189 ` 1330` ``` unfolding left_diff_distrib by simp ``` immler@56189 ` 1331` ``` also have "\ > e * (x \ i) + (1 - e) * (y \ i)" ``` lp15@66827 ` 1332` ``` proof (rule add_less_le_mono) ``` lp15@66827 ` 1333` ``` show "e * (x \ i) < e * (b \ i)" ``` lp15@68120 ` 1334` ``` using \0 < e\ i mem_box(1) x by auto ``` lp15@66827 ` 1335` ``` show "(1 - e) * (y \ i) \ (1 - e) * (b \ i)" ``` lp15@68120 ` 1336` ``` by (meson diff_ge_0_iff_ge \e \ 1\ i mem_box(2) mult_left_mono y) ``` lp15@66827 ` 1337` ``` qed ``` immler@56189 ` 1338` ``` finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i < b \ i" ``` immler@56189 ` 1339` ``` unfolding inner_simps by auto ``` immler@56189 ` 1340` ``` } ``` immler@56189 ` 1341` ``` ultimately have "a \ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i \ (e *\<^sub>R x + (1 - e) *\<^sub>R y) \ i < b \ i" ``` immler@56189 ` 1342` ``` by auto ``` immler@56189 ` 1343` ``` } ``` immler@56189 ` 1344` ``` then show ?thesis ``` immler@56189 ` 1345` ``` unfolding mem_box by auto ``` immler@56189 ` 1346` ```qed ``` immler@56189 ` 1347` lp15@63881 ` 1348` ```lemma closure_cbox [simp]: "closure (cbox a b) = cbox a b" ``` lp15@63881 ` 1349` ``` by (simp add: closed_cbox) ``` lp15@63881 ` 1350` lp15@63881 ` 1351` ```lemma closure_box [simp]: ``` immler@56189 ` 1352` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1353` ``` assumes "box a b \ {}" ``` immler@56189 ` 1354` ``` shows "closure (box a b) = cbox a b" ``` immler@56189 ` 1355` ```proof - ``` immler@56189 ` 1356` ``` have ab: "a cbox a b" ``` wenzelm@63040 ` 1362` ``` define f where [abs_def]: "f n = x + (inverse (real n + 1)) *\<^sub>R (?c - x)" for n ``` immler@56189 ` 1363` ``` { ``` immler@56189 ` 1364` ``` fix n ``` immler@56189 ` 1365` ``` assume fn: "f n a f n = x" and xc: "x \ ?c" ``` immler@56189 ` 1366` ``` have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \ 1" ``` immler@56189 ` 1367` ``` unfolding inverse_le_1_iff by auto ``` immler@56189 ` 1368` ``` have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x = ``` immler@56189 ` 1369` ``` x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)" ``` lp15@66643 ` 1370` ``` by (auto simp: algebra_simps) ``` immler@56189 ` 1371` ``` then have "f n (f \ x) sequentially" ``` immler@56189 ` 1380` ``` { ``` immler@56189 ` 1381` ``` fix e :: real ``` immler@56189 ` 1382` ``` assume "e > 0" ``` lp15@61609 ` 1383` ``` then obtain N :: nat where N: "inverse (real (N + 1)) < e" ``` lp15@68120 ` 1384` ``` using reals_Archimedean by auto ``` lp15@61609 ` 1385` ``` have "inverse (real n + 1) < e" if "N \ n" for n ``` lp15@61609 ` 1386` ``` by (auto intro!: that le_less_trans [OF _ N]) ``` immler@56189 ` 1387` ``` then have "\N::nat. \n\N. inverse (real n + 1) < e" by auto ``` immler@56189 ` 1388` ``` } ``` wenzelm@61973 ` 1389` ``` then have "((\n. inverse (real n + 1)) \ 0) sequentially" ``` lp15@66643 ` 1390` ``` unfolding lim_sequentially by(auto simp: dist_norm) ``` wenzelm@61973 ` 1391` ``` then have "(f \ x) sequentially" ``` immler@56189 ` 1392` ``` unfolding f_def ``` immler@56189 ` 1393` ``` using tendsto_add[OF tendsto_const, of "\n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] ``` immler@56189 ` 1394` ``` using tendsto_scaleR [OF _ tendsto_const, of "\n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] ``` immler@56189 ` 1395` ``` by auto ``` immler@56189 ` 1396` ``` } ``` immler@56189 ` 1397` ``` ultimately have "x \ closure (box a b)" ``` lp15@68120 ` 1398` ``` using as box_midpoint[OF assms] ``` lp15@68120 ` 1399` ``` unfolding closure_def islimpt_sequential ``` immler@56189 ` 1400` ``` by (cases "x=?c") (auto simp: in_box_eucl_less) ``` immler@56189 ` 1401` ``` } ``` immler@56189 ` 1402` ``` then show ?thesis ``` immler@56189 ` 1403` ``` using closure_minimal[OF box_subset_cbox, of a b] by blast ``` immler@56189 ` 1404` ```qed ``` immler@56189 ` 1405` immler@56189 ` 1406` ```lemma bounded_subset_box_symmetric: ``` lp15@68120 ` 1407` ``` fixes S :: "('a::euclidean_space) set" ``` lp15@68120 ` 1408` ``` assumes "bounded S" ``` lp15@68120 ` 1409` ``` obtains a where "S \ box (-a) a" ``` immler@56189 ` 1410` ```proof - ``` lp15@68120 ` 1411` ``` obtain b where "b>0" and b: "\x\S. norm x \ b" ``` immler@56189 ` 1412` ``` using assms[unfolded bounded_pos] by auto ``` wenzelm@63040 ` 1413` ``` define a :: 'a where "a = (\i\Basis. (b + 1) *\<^sub>R i)" ``` lp15@68120 ` 1414` ``` have "(-a)\i < x\i" and "x\i < a\i" if "x \ S" and i: "i \ Basis" for x i ``` lp15@68120 ` 1415` ``` using b Basis_le_norm[OF i, of x] that by (auto simp: a_def) ``` lp15@68120 ` 1416` ``` then have "S \ box (-a) a" ``` lp15@68120 ` 1417` ``` by (auto simp: simp add: box_def) ``` lp15@68120 ` 1418` ``` then show ?thesis .. ``` immler@56189 ` 1419` ```qed ``` immler@56189 ` 1420` immler@56189 ` 1421` ```lemma bounded_subset_cbox_symmetric: ``` lp15@68120 ` 1422` ``` fixes S :: "('a::euclidean_space) set" ``` lp15@68120 ` 1423` ``` assumes "bounded S" ``` lp15@68120 ` 1424` ``` obtains a where "S \ cbox (-a) a" ``` immler@56189 ` 1425` ```proof - ``` lp15@68120 ` 1426` ``` obtain a where "S \ box (-a) a" ``` immler@56189 ` 1427` ``` using bounded_subset_box_symmetric[OF assms] by auto ``` immler@56189 ` 1428` ``` then show ?thesis ``` lp15@68120 ` 1429` ``` by (meson box_subset_cbox dual_order.trans that) ``` immler@56189 ` 1430` ```qed ``` immler@56189 ` 1431` immler@56189 ` 1432` ```lemma frontier_cbox: ``` immler@56189 ` 1433` ``` fixes a b :: "'a::euclidean_space" ``` immler@56189 ` 1434` ``` shows "frontier (cbox a b) = cbox a b - box a b" ``` immler@56189 ` 1435` ``` unfolding frontier_def unfolding interior_cbox and closure_closed[OF closed_cbox] .. ``` immler@56189 ` 1436` immler@56189 ` 1437` ```lemma frontier_box: ``` immler@56189 ` 1438` ``` fixes a b :: "'a::euclidean_space" ``` immler@56189 ` 1439` ``` shows "frontier (box a b) = (if box a b = {} then {} else cbox a b - box a b)" ``` immler@56189 ` 1440` ```proof (cases "box a b = {}") ``` immler@56189 ` 1441` ``` case True ``` immler@56189 ` 1442` ``` then show ?thesis ``` immler@56189 ` 1443` ``` using frontier_empty by auto ``` immler@56189 ` 1444` ```next ``` immler@56189 ` 1445` ``` case False ``` immler@56189 ` 1446` ``` then show ?thesis ``` immler@56189 ` 1447` ``` unfolding frontier_def and closure_box[OF False] and interior_open[OF open_box] ``` immler@56189 ` 1448` ``` by auto ``` immler@56189 ` 1449` ```qed ``` immler@56189 ` 1450` lp15@66884 ` 1451` ```lemma Int_interval_mixed_eq_empty: ``` immler@56189 ` 1452` ``` fixes a :: "'a::euclidean_space" ``` immler@56189 ` 1453` ``` assumes "box c d \ {}" ``` immler@56189 ` 1454` ``` shows "box a b \ cbox c d = {} \ box a b \ box c d = {}" ``` immler@56189 ` 1455` ``` unfolding closure_box[OF assms, symmetric] ``` lp15@62843 ` 1456` ``` unfolding open_Int_closure_eq_empty[OF open_box] .. ``` immler@56189 ` 1457` immler@69611 ` 1458` ```subsection \Class Instances\ ``` immler@69611 ` 1459` immler@69611 ` 1460` ```lemma compact_lemma: ``` immler@69611 ` 1461` ``` fixes f :: "nat \ 'a::euclidean_space" ``` immler@69611 ` 1462` ``` assumes "bounded (range f)" ``` immler@69611 ` 1463` ``` shows "\d\Basis. \l::'a. \ r. ``` immler@69611 ` 1464` ``` strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" ``` immler@69611 ` 1465` ``` by (rule compact_lemma_general[where unproj="\e. \i\Basis. e i *\<^sub>R i"]) ``` immler@69611 ` 1466` ``` (auto intro!: assms bounded_linear_inner_left bounded_linear_image ``` immler@69611 ` 1467` ``` simp: euclidean_representation) ``` immler@69611 ` 1468` immler@69611 ` 1469` ```instance%important euclidean_space \ heine_borel ``` immler@69611 ` 1470` ```proof%unimportant ``` immler@69611 ` 1471` ``` fix f :: "nat \ 'a" ``` immler@69611 ` 1472` ``` assume f: "bounded (range f)" ``` immler@69611 ` 1473` ``` then obtain l::'a and r where r: "strict_mono r" ``` immler@69611 ` 1474` ``` and l: "\e>0. eventually (\n. \i\Basis. dist (f (r n) \ i) (l \ i) < e) sequentially" ``` immler@69611 ` 1475` ``` using compact_lemma [OF f] by blast ``` immler@69611 ` 1476` ``` { ``` immler@69611 ` 1477` ``` fix e::real ``` immler@69611 ` 1478` ``` assume "e > 0" ``` immler@69611 ` 1479` ``` hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive) ``` immler@69611 ` 1480` ``` with l have "eventually (\n. \i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))) sequentially" ``` immler@69611 ` 1481` ``` by simp ``` immler@69611 ` 1482` ``` moreover ``` immler@69611 ` 1483` ``` { ``` immler@69611 ` 1484` ``` fix n ``` immler@69611 ` 1485` ``` assume n: "\i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))" ``` immler@69611 ` 1486` ``` have "dist (f (r n)) l \ (\i\Basis. dist (f (r n) \ i) (l \ i))" ``` immler@69611 ` 1487` ``` apply (subst euclidean_dist_l2) ``` immler@69611 ` 1488` ``` using zero_le_dist ``` immler@69611 ` 1489` ``` apply (rule L2_set_le_sum) ``` immler@69611 ` 1490` ``` done ``` immler@69611 ` 1491` ``` also have "\ < (\i\(Basis::'a set). e / (real_of_nat DIM('a)))" ``` immler@69611 ` 1492` ``` apply (rule sum_strict_mono) ``` immler@69611 ` 1493` ``` using n ``` immler@69611 ` 1494` ``` apply auto ``` immler@69611 ` 1495` ``` done ``` immler@69611 ` 1496` ``` finally have "dist (f (r n)) l < e" ``` immler@69611 ` 1497` ``` by auto ``` immler@69611 ` 1498` ``` } ``` immler@69611 ` 1499` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` immler@69611 ` 1500` ``` by (rule eventually_mono) ``` immler@69611 ` 1501` ``` } ``` immler@69611 ` 1502` ``` then have *: "((f \ r) \ l) sequentially" ``` immler@69611 ` 1503` ``` unfolding o_def tendsto_iff by simp ``` immler@69611 ` 1504` ``` with r show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" ``` immler@69611 ` 1505` ``` by auto ``` immler@69611 ` 1506` ```qed ``` immler@69611 ` 1507` immler@69611 ` 1508` ```instance%important euclidean_space \ banach .. ``` immler@69611 ` 1509` immler@69611 ` 1510` ```instance euclidean_space \ second_countable_topology ``` immler@69611 ` 1511` ```proof ``` immler@69611 ` 1512` ``` define a where "a f = (\i\Basis. fst (f i) *\<^sub>R i)" for f :: "'a \ real \ real" ``` immler@69611 ` 1513` ``` then have a: "\f. (\i\Basis. fst (f i) *\<^sub>R i) = a f" ``` immler@69611 ` 1514` ``` by simp ``` immler@69611 ` 1515` ``` define b where "b f = (\i\Basis. snd (f i) *\<^sub>R i)" for f :: "'a \ real \ real" ``` immler@69611 ` 1516` ``` then have b: "\f. (\i\Basis. snd (f i) *\<^sub>R i) = b f" ``` immler@69611 ` 1517` ``` by simp ``` immler@69611 ` 1518` ``` define B where "B = (\f. box (a f) (b f)) ` (Basis \\<^sub>E (\ \ \))" ``` immler@69611 ` 1519` immler@69611 ` 1520` ``` have "Ball B open" by (simp add: B_def open_box) ``` immler@69611 ` 1521` ``` moreover have "(\A. open A \ (\B'\B. \B' = A))" ``` immler@69611 ` 1522` ``` proof safe ``` immler@69611 ` 1523` ``` fix A::"'a set" ``` immler@69611 ` 1524` ``` assume "open A" ``` immler@69611 ` 1525` ``` show "\B'\B. \B' = A" ``` immler@69611 ` 1526` ``` apply (rule exI[of _ "{b\B. b \ A}"]) ``` immler@69611 ` 1527` ``` apply (subst (3) open_UNION_box[OF \open A\]) ``` immler@69611 ` 1528` ``` apply (auto simp: a b B_def) ``` immler@69611 ` 1529` ``` done ``` immler@69611 ` 1530` ``` qed ``` immler@69611 ` 1531` ``` ultimately ``` immler@69611 ` 1532` ``` have "topological_basis B" ``` immler@69611 ` 1533` ``` unfolding topological_basis_def by blast ``` immler@69611 ` 1534` ``` moreover ``` immler@69611 ` 1535` ``` have "countable B" ``` immler@69611 ` 1536` ``` unfolding B_def ``` immler@69611 ` 1537` ``` by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat) ``` immler@69611 ` 1538` ``` ultimately show "\B::'a set set. countable B \ open = generate_topology B" ``` immler@69611 ` 1539` ``` by (blast intro: topological_basis_imp_subbasis) ``` immler@69611 ` 1540` ```qed ``` immler@69611 ` 1541` immler@69611 ` 1542` ```instance euclidean_space \ polish_space .. ``` immler@69611 ` 1543` immler@69611 ` 1544` immler@69611 ` 1545` ```subsection \Compact Boxes\ ``` immler@69611 ` 1546` immler@69611 ` 1547` ```lemma compact_cbox [simp]: ``` wenzelm@61076 ` 1548` ``` fixes a :: "'a::euclidean_space" ``` immler@69611 ` 1549` ``` shows "compact (cbox a b)" ``` immler@69611 ` 1550` ``` using bounded_closed_imp_seq_compact[of "cbox a b"] using bounded_cbox[of a b] ``` immler@69611 ` 1551` ``` by (auto simp: compact_eq_seq_compact_metric) ``` immler@69611 ` 1552` immler@69611 ` 1553` ```proposition is_interval_compact: ``` immler@69611 ` 1554` ``` "is_interval S \ compact S \ (\a b. S = cbox a b)" (is "?lhs = ?rhs") ``` immler@69611 ` 1555` ```proof (cases "S = {}") ``` immler@69611 ` 1556` ``` case True ``` immler@69611 ` 1557` ``` with empty_as_interval show ?thesis by auto ``` immler@69611 ` 1558` ```next ``` immler@69611 ` 1559` ``` case False ``` immler@69611 ` 1560` ``` show ?thesis ``` immler@69611 ` 1561` ``` proof ``` immler@69611 ` 1562` ``` assume L: ?lhs ``` immler@69611 ` 1563` ``` then have "is_interval S" "compact S" by auto ``` immler@69611 ` 1564` ``` define a where "a \ \i\Basis. (INF x\S. x \ i) *\<^sub>R i" ``` immler@69611 ` 1565` ``` define b where "b \ \i\Basis. (SUP x\S. x \ i) *\<^sub>R i" ``` immler@69611 ` 1566` ``` have 1: "\x i. \x \ S; i \ Basis\ \ (INF x\S. x \ i) \ x \ i" ``` immler@69611 ` 1567` ``` by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L) ``` immler@69611 ` 1568` ``` have 2: "\x i. \x \ S; i \ Basis\ \ x \ i \ (SUP x\S. x \ i)" ``` immler@69611 ` 1569` ``` by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L) ``` immler@69611 ` 1570` ``` have 3: "x \ S" if inf: "\i. i \ Basis \ (INF x\S. x \ i) \ x \ i" ``` immler@69611 ` 1571` ``` and sup: "\i. i \ Basis \ x \ i \ (SUP x\S. x \ i)" for x ``` immler@69611 ` 1572` ``` proof (rule mem_box_componentwiseI [OF \is_interval S\]) ``` immler@69611 ` 1573` ``` fix i::'a ``` immler@69611 ` 1574` ``` assume i: "i \ Basis" ``` immler@69611 ` 1575` ``` have cont: "continuous_on S (\x. x \ i)" ``` immler@69611 ` 1576` ``` by (intro continuous_intros) ``` immler@69611 ` 1577` ``` obtain a where "a \ S" and a: "\y. y\S \ a \ i \ y \ i" ``` immler@69611 ` 1578` ``` using continuous_attains_inf [OF \compact S\ False cont] by blast ``` immler@69611 ` 1579` ``` obtain b where "b \ S" and b: "\y. y\S \ y \ i \ b \ i" ``` immler@69611 ` 1580` ``` using continuous_attains_sup [OF \compact S\ False cont] by blast ``` immler@69611 ` 1581` ``` have "a \ i \ (INF x\S. x \ i)" ``` immler@69611 ` 1582` ``` by (simp add: False a cINF_greatest) ``` immler@69611 ` 1583` ``` also have "\ \ x \ i" ``` immler@69611 ` 1584` ``` by (simp add: i inf) ``` immler@69611 ` 1585` ``` finally have ai: "a \ i \ x \ i" . ``` immler@69611 ` 1586` ``` have "x \ i \ (SUP x\S. x \ i)" ``` immler@69611 ` 1587` ``` by (simp add: i sup) ``` immler@69611 ` 1588` ``` also have "(SUP x\S. x \ i) \ b \ i" ``` immler@69611 ` 1589` ``` by (simp add: False b cSUP_least) ``` immler@69611 ` 1590` ``` finally have bi: "x \ i \ b \ i" . ``` immler@69611 ` 1591` ``` show "x \ i \ (\x. x \ i) ` S" ``` immler@69611 ` 1592` ``` apply (rule_tac x="\j\Basis. (if j = i then x \ i else a \ j) *\<^sub>R j" in image_eqI) ``` immler@69611 ` 1593` ``` apply (simp add: i) ``` immler@69611 ` 1594` ``` apply (rule mem_is_intervalI [OF \is_interval S\ \a \ S\ \b \ S\]) ``` immler@69611 ` 1595` ``` using i ai bi apply force ``` immler@69611 ` 1596` ``` done ``` immler@69611 ` 1597` ``` qed ``` immler@69611 ` 1598` ``` have "S = cbox a b" ``` immler@69611 ` 1599` ``` by (auto simp: a_def b_def mem_box intro: 1 2 3) ``` immler@69611 ` 1600` ``` then show ?rhs ``` immler@69611 ` 1601` ``` by blast ``` immler@69611 ` 1602` ``` next ``` immler@69611 ` 1603` ``` assume R: ?rhs ``` immler@69611 ` 1604` ``` then show ?lhs ``` immler@69611 ` 1605` ``` using compact_cbox is_interval_cbox by blast ``` immler@69611 ` 1606` ``` qed ``` immler@69611 ` 1607` ```qed ``` immler@69611 ` 1608` immler@69611 ` 1609` immler@69615 ` 1610` ```subsection%unimportant\Componentwise limits and continuity\ ``` immler@69615 ` 1611` immler@69615 ` 1612` ```text\But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\ ``` immler@69615 ` 1613` ```lemma Euclidean_dist_upper: "i \ Basis \ dist (x \ i) (y \ i) \ dist x y" ``` immler@69615 ` 1614` ``` by (metis (no_types) member_le_L2_set euclidean_dist_l2 finite_Basis) ``` immler@69615 ` 1615` immler@69615 ` 1616` ```text\But is the premise \<^term>\i \ Basis\ really necessary?\ ``` immler@69615 ` 1617` ```lemma open_preimage_inner: ``` immler@69615 ` 1618` ``` assumes "open S" "i \ Basis" ``` immler@69615 ` 1619` ``` shows "open {x. x \ i \ S}" ``` immler@69615 ` 1620` ```proof (rule openI, simp) ``` immler@69615 ` 1621` ``` fix x ``` immler@69615 ` 1622` ``` assume x: "x \ i \ S" ``` immler@69615 ` 1623` ``` with assms obtain e where "0 < e" and e: "ball (x \ i) e \ S" ``` immler@69615 ` 1624` ``` by (auto simp: open_contains_ball_eq) ``` immler@69615 ` 1625` ``` have "\e>0. ball (y \ i) e \ S" if dxy: "dist x y < e / 2" for y ``` immler@69615 ` 1626` ``` proof (intro exI conjI) ``` immler@69615 ` 1627` ``` have "dist (x \ i) (y \ i) < e / 2" ``` immler@69615 ` 1628` ``` by (meson \i \ Basis\ dual_order.trans Euclidean_dist_upper not_le that) ``` immler@69615 ` 1629` ``` then have "dist (x \ i) z < e" if "dist (y \ i) z < e / 2" for z ``` immler@69615 ` 1630` ``` by (metis dist_commute dist_triangle_half_l that) ``` immler@69615 ` 1631` ``` then have "ball (y \ i) (e / 2) \ ball (x \ i) e" ``` immler@69615 ` 1632` ``` using mem_ball by blast ``` immler@69615 ` 1633` ``` with e show "ball (y \ i) (e / 2) \ S" ``` immler@69615 ` 1634` ``` by (metis order_trans) ``` immler@69615 ` 1635` ``` qed (simp add: \0 < e\) ``` immler@69615 ` 1636` ``` then show "\e>0. ball x e \ {s. s \ i \ S}" ``` immler@69615 ` 1637` ``` by (metis (no_types, lifting) \0 < e\ \open S\ half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI) ``` immler@69615 ` 1638` ```qed ``` immler@69615 ` 1639` immler@69615 ` 1640` ```proposition tendsto_componentwise_iff: ``` immler@69615 ` 1641` ``` fixes f :: "_ \ 'b::euclidean_space" ``` immler@69615 ` 1642` ``` shows "(f \ l) F \ (\i \ Basis. ((\x. (f x \ i)) \ (l \ i)) F)" ``` immler@69615 ` 1643` ``` (is "?lhs = ?rhs") ``` immler@69615 ` 1644` ```proof ``` immler@69615 ` 1645` ``` assume ?lhs ``` immler@69615 ` 1646` ``` then show ?rhs ``` immler@69615 ` 1647` ``` unfolding tendsto_def ``` immler@69615 ` 1648` ``` apply clarify ``` immler@69615 ` 1649` ``` apply (drule_tac x="{s. s \ i \ S}" in spec) ``` immler@69615 ` 1650` ``` apply (auto simp: open_preimage_inner) ``` immler@69615 ` 1651` ``` done ``` immler@69615 ` 1652` ```next ``` immler@69615 ` 1653` ``` assume R: ?rhs ``` immler@69615 ` 1654` ``` then have "\e. e > 0 \ \i\Basis. \\<^sub>F x in F. dist (f x \ i) (l \ i) < e" ``` immler@69615 ` 1655` ``` unfolding tendsto_iff by blast ``` immler@69615 ` 1656` ``` then have R': "\e. e > 0 \ \\<^sub>F x in F. \i\Basis. dist (f x \ i) (l \ i) < e" ``` immler@69615 ` 1657` ``` by (simp add: eventually_ball_finite_distrib [symmetric]) ``` immler@69615 ` 1658` ``` show ?lhs ``` immler@69615 ` 1659` ``` unfolding tendsto_iff ``` immler@69615 ` 1660` ``` proof clarify ``` immler@69615 ` 1661` ``` fix e::real ``` immler@69615 ` 1662` ``` assume "0 < e" ``` immler@69615 ` 1663` ``` have *: "L2_set (\i. dist (f x \ i) (l \ i)) Basis < e" ``` immler@69615 ` 1664` ``` if "\i\Basis. dist (f x \ i) (l \ i) < e / real DIM('b)" for x ``` immler@69615 ` 1665` ``` proof - ``` immler@69615 ` 1666` ``` have "L2_set (\i. dist (f x \ i) (l \ i)) Basis \ sum (\i. dist (f x \ i) (l \ i)) Basis" ``` immler@69615 ` 1667` ``` by (simp add: L2_set_le_sum) ``` immler@69615 ` 1668` ``` also have "... < DIM('b) * (e / real DIM('b))" ``` immler@69615 ` 1669` ``` apply (rule sum_bounded_above_strict) ``` immler@69615 ` 1670` ``` using that by auto ``` immler@69615 ` 1671` ``` also have "... = e" ``` immler@69615 ` 1672` ``` by (simp add: field_simps) ``` immler@69615 ` 1673` ``` finally show "L2_set (\i. dist (f x \ i) (l \ i)) Basis < e" . ``` immler@69615 ` 1674` ``` qed ``` immler@69615 ` 1675` ``` have "\\<^sub>F x in F. \i\Basis. dist (f x \ i) (l \ i) < e / DIM('b)" ``` immler@69615 ` 1676` ``` apply (rule R') ``` immler@69615 ` 1677` ``` using \0 < e\ by simp ``` immler@69615 ` 1678` ``` then show "\\<^sub>F x in F. dist (f x) l < e" ``` immler@69615 ` 1679` ``` apply (rule eventually_mono) ``` immler@69615 ` 1680` ``` apply (subst euclidean_dist_l2) ``` immler@69615 ` 1681` ``` using * by blast ``` immler@69615 ` 1682` ``` qed ``` immler@69615 ` 1683` ```qed ``` immler@69615 ` 1684` immler@69615 ` 1685` immler@69615 ` 1686` ```corollary continuous_componentwise: ``` immler@69615 ` 1687` ``` "continuous F f \ (\i \ Basis. continuous F (\x. (f x \ i)))" ``` immler@69615 ` 1688` ```by (simp add: continuous_def tendsto_componentwise_iff [symmetric]) ``` immler@69615 ` 1689` immler@69615 ` 1690` ```corollary continuous_on_componentwise: ``` immler@69615 ` 1691` ``` fixes S :: "'a :: t2_space set" ``` immler@69615 ` 1692` ``` shows "continuous_on S f \ (\i \ Basis. continuous_on S (\x. (f x \ i)))" ``` immler@69615 ` 1693` ``` apply (simp add: continuous_on_eq_continuous_within) ``` immler@69615 ` 1694` ``` using continuous_componentwise by blast ``` immler@69615 ` 1695` immler@69615 ` 1696` ```lemma linear_componentwise_iff: ``` immler@69615 ` 1697` ``` "(linear f') \ (\i\Basis. linear (\x. f' x \ i))" ``` immler@69615 ` 1698` ``` apply (auto simp: linear_iff inner_left_distrib) ``` immler@69615 ` 1699` ``` apply (metis inner_left_distrib euclidean_eq_iff) ``` immler@69615 ` 1700` ``` by (metis euclidean_eqI inner_scaleR_left) ``` immler@69615 ` 1701` immler@69615 ` 1702` ```lemma bounded_linear_componentwise_iff: ``` immler@69615 ` 1703` ``` "(bounded_linear f') \ (\i\Basis. bounded_linear (\x. f' x \ i))" ``` immler@69615 ` 1704` ``` (is "?lhs = ?rhs") ``` immler@69615 ` 1705` ```proof ``` immler@69615 ` 1706` ``` assume ?lhs then show ?rhs ``` immler@69615 ` 1707` ``` by (simp add: bounded_linear_inner_left_comp) ``` immler@69615 ` 1708` ```next ``` immler@69615 ` 1709` ``` assume ?rhs ``` immler@69615 ` 1710` ``` then have "(\i\Basis. \K. \x. \f' x \ i\ \ norm x * K)" "linear f'" ``` immler@69615 ` 1711` ``` by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib) ``` immler@69615 ` 1712` ``` then obtain F where F: "\i x. i \ Basis \ \f' x \ i\ \ norm x * F i" ``` immler@69615 ` 1713` ``` by metis ``` immler@69615 ` 1714` ``` have "norm (f' x) \ norm x * sum F Basis" for x ``` immler@69615 ` 1715` ``` proof - ``` immler@69615 ` 1716` ``` have "norm (f' x) \ (\i\Basis. \f' x \ i\)" ``` immler@69615 ` 1717` ``` by (rule norm_le_l1) ``` immler@69615 ` 1718` ``` also have "... \ (\i\Basis. norm x * F i)" ``` immler@69615 ` 1719` ``` by (metis F sum_mono) ``` immler@69615 ` 1720` ``` also have "... = norm x * sum F Basis" ``` immler@69615 ` 1721` ``` by (simp add: sum_distrib_left) ``` immler@69615 ` 1722` ``` finally show ?thesis . ``` immler@69615 ` 1723` ``` qed ``` immler@69615 ` 1724` ``` then show ?lhs ``` immler@69615 ` 1725` ``` by (force simp: bounded_linear_def bounded_linear_axioms_def \linear f'\) ``` immler@69615 ` 1726` ```qed ``` immler@69615 ` 1727` immler@69615 ` 1728` ```subsection%unimportant \Continuous Extension\ ``` immler@69615 ` 1729` immler@69615 ` 1730` ```definition clamp :: "'a::euclidean_space \ 'a \ 'a \ 'a" where ``` immler@69615 ` 1731` ``` "clamp a b x = (if (\i\Basis. a \ i \ b \ i) ``` immler@69615 ` 1732` ``` then (\i\Basis. (if x\i < a\i then a\i else if x\i \ b\i then x\i else b\i) *\<^sub>R i) ``` immler@69615 ` 1733` ``` else a)" ``` immler@69615 ` 1734` immler@69615 ` 1735` ```lemma clamp_in_interval[simp]: ``` immler@69615 ` 1736` ``` assumes "\i. i \ Basis \ a \ i \ b \ i" ``` immler@69615 ` 1737` ``` shows "clamp a b x \ cbox a b" ``` immler@69615 ` 1738` ``` unfolding clamp_def ``` immler@69615 ` 1739` ``` using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def) ``` immler@69615 ` 1740` immler@69615 ` 1741` ```lemma clamp_cancel_cbox[simp]: ``` immler@69615 ` 1742` ``` fixes x a b :: "'a::euclidean_space" ``` immler@69615 ` 1743` ``` assumes x: "x \ cbox a b" ``` immler@69615 ` 1744` ``` shows "clamp a b x = x" ``` immler@69615 ` 1745` ``` using assms ``` immler@69615 ` 1746` ``` by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a]) ``` immler@69615 ` 1747` immler@69615 ` 1748` ```lemma clamp_empty_interval: ``` immler@69615 ` 1749` ``` assumes "i \ Basis" "a \ i > b \ i" ``` immler@69615 ` 1750` ``` shows "clamp a b = (\_. a)" ``` immler@69615 ` 1751` ``` using assms ``` immler@69615 ` 1752` ``` by (force simp: clamp_def[abs_def] split: if_splits intro!: ext) ``` immler@69615 ` 1753` immler@69615 ` 1754` ```lemma dist_clamps_le_dist_args: ``` immler@69615 ` 1755` ``` fixes x :: "'a::euclidean_space" ``` immler@69615 ` 1756` ``` shows "dist (clamp a b y) (clamp a b x) \ dist y x" ``` immler@69615 ` 1757` ```proof cases ``` immler@69615 ` 1758` ``` assume le: "(\i\Basis. a \ i \ b \ i)" ``` immler@69615 ` 1759` ``` then have "(\i\Basis. (dist (clamp a b y \ i) (clamp a b x \ i))\<^sup>2) \ ``` immler@69615 ` 1760` ``` (\i\Basis. (dist (y \ i) (x \ i))\<^sup>2)" ``` immler@69615 ` 1761` ``` by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric]) ``` immler@69615 ` 1762` ``` then show ?thesis ``` immler@69615 ` 1763` ``` by (auto intro: real_sqrt_le_mono ``` immler@69615 ` 1764` ``` simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] L2_set_def) ``` immler@69615 ` 1765` ```qed (auto simp: clamp_def) ``` immler@69615 ` 1766` immler@69615 ` 1767` ```lemma clamp_continuous_at: ``` immler@69615 ` 1768` ``` fixes f :: "'a::euclidean_space \ 'b::metric_space" ``` immler@69615 ` 1769` ``` and x :: 'a ``` immler@69615 ` 1770` ``` assumes f_cont: "continuous_on (cbox a b) f" ``` immler@69615 ` 1771` ``` shows "continuous (at x) (\x. f (clamp a b x))" ``` immler@69615 ` 1772` ```proof cases ``` immler@69615 ` 1773` ``` assume le: "(\i\Basis. a \ i \ b \ i)" ``` immler@69615 ` 1774` ``` show ?thesis ``` immler@69615 ` 1775` ``` unfolding continuous_at_eps_delta ``` immler@69615 ` 1776` ``` proof safe ``` immler@69615 ` 1777` ``` fix x :: 'a ``` immler@69615 ` 1778` ``` fix e :: real ``` immler@69615 ` 1779` ``` assume "e > 0" ``` immler@69615 ` 1780` ``` moreover have "clamp a b x \ cbox a b" ``` immler@69615 ` 1781` ``` by (simp add: clamp_in_interval le) ``` immler@69615 ` 1782` ``` moreover note f_cont[simplified continuous_on_iff] ``` immler@69615 ` 1783` ``` ultimately ``` immler@69615 ` 1784` ``` obtain d where d: "0 < d" ``` immler@69615 ` 1785` ``` "\x'. x' \ cbox a b \ dist x' (clamp a b x) < d \ dist (f x') (f (clamp a b x)) < e" ``` immler@69615 ` 1786` ``` by force ``` immler@69615 ` 1787` ``` show "\d>0. \x'. dist x' x < d \ ``` immler@69615 ` 1788` ``` dist (f (clamp a b x')) (f (clamp a b x)) < e" ``` immler@69615 ` 1789` ``` using le ``` immler@69615 ` 1790` ``` by (auto intro!: d clamp_in_interval dist_clamps_le_dist_args[THEN le_less_trans]) ``` immler@69615 ` 1791` ``` qed ``` immler@69615 ` 1792` ```qed (auto simp: clamp_empty_interval) ``` immler@69615 ` 1793` immler@69615 ` 1794` ```lemma clamp_continuous_on: ``` immler@69615 ` 1795` ``` fixes f :: "'a::euclidean_space \ 'b::metric_space" ``` immler@69615 ` 1796` ``` assumes f_cont: "continuous_on (cbox a b) f" ``` immler@69615 ` 1797` ``` shows "continuous_on S (\x. f (clamp a b x))" ``` immler@69615 ` 1798` ``` using assms ``` immler@69615 ` 1799` ``` by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at) ``` immler@69615 ` 1800` immler@69615 ` 1801` ```lemma clamp_bounded: ``` immler@69615 ` 1802` ``` fixes f :: "'a::euclidean_space \ 'b::metric_space" ``` immler@69615 ` 1803` ``` assumes bounded: "bounded (f ` (cbox a b))" ``` immler@69615 ` 1804` ``` shows "bounded (range (\x. f (clamp a b x)))" ``` immler@69615 ` 1805` ```proof cases ``` immler@69615 ` 1806` ``` assume le: "(\i\Basis. a \ i \ b \ i)" ``` immler@69615 ` 1807` ``` from bounded obtain c where f_bound: "\x\f ` cbox a b. dist undefined x \ c" ``` immler@69615 ` 1808` ``` by (auto simp: bounded_any_center[where a=undefined]) ``` immler@69615 ` 1809` ``` then show ?thesis ``` immler@69615 ` 1810` ``` by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]] ``` immler@69615 ` 1811` ``` simp: bounded_any_center[where a=undefined]) ``` immler@69615 ` 1812` ```qed (auto simp: clamp_empty_interval image_def) ``` immler@69615 ` 1813` immler@69615 ` 1814` immler@69615 ` 1815` ```definition ext_cont :: "('a::euclidean_space \ 'b::metric_space) \ 'a \ 'a \ 'a \ 'b" ``` immler@69615 ` 1816` ``` where "ext_cont f a b = (\x. f (clamp a b x))" ``` immler@69615 ` 1817` immler@69615 ` 1818` ```lemma ext_cont_cancel_cbox[simp]: ``` immler@69615 ` 1819` ``` fixes x a b :: "'a::euclidean_space" ``` immler@69615 ` 1820` ``` assumes x: "x \ cbox a b" ``` immler@69615 ` 1821` ``` shows "ext_cont f a b x = f x" ``` immler@69615 ` 1822` ``` using assms ``` immler@69615 ` 1823` ``` unfolding ext_cont_def ``` immler@69615 ` 1824` ``` by (auto simp: clamp_def mem_box intro!: euclidean_eqI[where 'a='a] arg_cong[where f=f]) ``` immler@69615 ` 1825` immler@69615 ` 1826` ```lemma continuous_on_ext_cont[continuous_intros]: ``` immler@69615 ` 1827` ``` "continuous_on (cbox a b) f \ continuous_on S (ext_cont f a b)" ``` immler@69615 ` 1828` ``` by (auto intro!: clamp_continuous_on simp: ext_cont_def) ``` immler@69615 ` 1829` immler@69615 ` 1830` immler@69615 ` 1831` ```subsection \Separability\ ``` immler@69615 ` 1832` immler@69615 ` 1833` ```lemma univ_second_countable_sequence: ``` immler@69615 ` 1834` ``` obtains B :: "nat \ 'a::euclidean_space set" ``` immler@69615 ` 1835` ``` where "inj B" "\n. open(B n)" "\S. open S \ \k. S = \{B n |n. n \ k}" ``` immler@69615 ` 1836` ```proof - ``` immler@69615 ` 1837` ``` obtain \ :: "'a set set" ``` immler@69615 ` 1838` ``` where "countable \" ``` immler@69615 ` 1839` ``` and opn: "\C. C \ \ \ open C" ``` immler@69615 ` 1840` ``` and Un: "\S. open S \ \U. U \ \ \ S = \U" ``` immler@69615 ` 1841` ``` using univ_second_countable by blast ``` immler@69615 ` 1842` ``` have *: "infinite (range (\n. ball (0::'a) (inverse(Suc n))))" ``` immler@69615 ` 1843` ``` apply (rule Infinite_Set.range_inj_infinite) ``` immler@69615 ` 1844` ``` apply (simp add: inj_on_def ball_eq_ball_iff) ``` immler@69615 ` 1845` ``` done ``` immler@69615 ` 1846` ``` have "infinite \" ``` immler@69615 ` 1847` ``` proof ``` immler@69615 ` 1848` ``` assume "finite \" ``` immler@69615 ` 1849` ``` then have "finite (Union ` (Pow \))" ``` immler@69615 ` 1850` ``` by simp ``` immler@69615 ` 1851` ``` then have "finite (range (\n. ball (0::'a) (inverse(Suc n))))" ``` immler@69615 ` 1852` ``` apply (rule rev_finite_subset) ``` immler@69615 ` 1853` ``` by (metis (no_types, lifting) PowI image_eqI image_subset_iff Un [OF open_ball]) ``` immler@69615 ` 1854` ``` with * show False by simp ``` immler@69615 ` 1855` ``` qed ``` immler@69615 ` 1856` ``` obtain f :: "nat \ 'a set" where "\ = range f" "inj f" ``` immler@69615 ` 1857` ``` by (blast intro: countable_as_injective_image [OF \countable \\ \infinite \\]) ``` immler@69615 ` 1858` ``` have *: "\k. S = \{f n |n. n \ k}" if "open S" for S ``` immler@69615 ` 1859` ``` using Un [OF that] ``` immler@69615 ` 1860` ``` apply clarify ``` immler@69615 ` 1861` ``` apply (rule_tac x="f-`U" in exI) ``` immler@69615 ` 1862` ``` using \inj f\ \\ = range f\ apply force ``` immler@69615 ` 1863` ``` done ``` immler@69615 ` 1864` ``` show ?thesis ``` immler@69615 ` 1865` ``` apply (rule that [OF \inj f\ _ *]) ``` immler@69615 ` 1866` ``` apply (auto simp: \\ = range f\ opn) ``` immler@69615 ` 1867` ``` done ``` immler@69615 ` 1868` ```qed ``` immler@69615 ` 1869` immler@69615 ` 1870` ```proposition separable: ``` immler@69615 ` 1871` ``` fixes S :: "'a::{metric_space, second_countable_topology} set" ``` immler@69615 ` 1872` ``` obtains T where "countable T" "T \ S" "S \ closure T" ``` immler@69615 ` 1873` ```proof - ``` immler@69615 ` 1874` ``` obtain \ :: "'a set set" ``` immler@69615 ` 1875` ``` where "countable \" ``` immler@69615 ` 1876` ``` and "{} \ \" ``` immler@69615 ` 1877` ``` and ope: "\C. C \ \ \ openin(subtopology euclidean S) C" ``` immler@69615 ` 1878` ``` and if_ope: "\T. openin(subtopology euclidean S) T \ \\. \ \ \ \ T = \\" ``` immler@69615 ` 1879` ``` by (meson subset_second_countable) ``` immler@69615 ` 1880` ``` then obtain f where f: "\C. C \ \ \ f C \ C" ``` immler@69615 ` 1881` ``` by (metis equals0I) ``` immler@69615 ` 1882` ``` show ?thesis ``` immler@69615 ` 1883` ``` proof ``` immler@69615 ` 1884` ``` show "countable (f ` \)" ``` immler@69615 ` 1885` ``` by (simp add: \countable \\) ``` immler@69615 ` 1886` ``` show "f ` \ \ S" ``` immler@69615 ` 1887` ``` using ope f openin_imp_subset by blast ``` immler@69615 ` 1888` ``` show "S \ closure (f ` \)" ``` immler@69615 ` 1889` ``` proof (clarsimp simp: closure_approachable) ``` immler@69615 ` 1890` ``` fix x and e::real ``` immler@69615 ` 1891` ``` assume "x \ S" "0 < e" ``` immler@69615 ` 1892` ``` have "openin (subtopology euclidean S) (S \ ball x e)" ``` immler@69615 ` 1893` ``` by (simp add: openin_Int_open) ``` immler@69615 ` 1894` ``` with if_ope obtain \ where \: "\ \ \" "S \ ball x e = \\" ``` immler@69615 ` 1895` ``` by meson ``` immler@69615 ` 1896` ``` show "\C \ \. dist (f C) x < e" ``` immler@69615 ` 1897` ``` proof (cases "\ = {}") ``` immler@69615 ` 1898` ``` case True ``` immler@69615 ` 1899` ``` then show ?thesis ``` immler@69615 ` 1900` ``` using \0 < e\ \ \x \ S\ by auto ``` immler@69615 ` 1901` ``` next ``` immler@69615 ` 1902` ``` case False ``` immler@69615 ` 1903` ``` then obtain C where "C \ \" by blast ``` immler@69615 ` 1904` ``` show ?thesis ``` immler@69615 ` 1905` ``` proof ``` immler@69615 ` 1906` ``` show "dist (f C) x < e" ``` immler@69615 ` 1907` ``` by (metis Int_iff Union_iff \ \C \ \\ dist_commute f mem_ball subsetCE) ``` immler@69615 ` 1908` ``` show "C \ \" ``` immler@69615 ` 1909` ``` using \\ \ \\ \C \ \\ by blast ``` immler@69615 ` 1910` ``` qed ``` immler@69615 ` 1911` ``` qed ``` immler@69615 ` 1912` ``` qed ``` immler@69615 ` 1913` ``` qed ``` immler@69615 ` 1914` ```qed ``` immler@69615 ` 1915` immler@69615 ` 1916` immler@69613 ` 1917` ```subsection%unimportant \Diameter\ ``` immler@69613 ` 1918` immler@69613 ` 1919` ```lemma diameter_cball [simp]: ``` immler@69613 ` 1920` ``` fixes a :: "'a::euclidean_space" ``` immler@69613 ` 1921` ``` shows "diameter(cball a r) = (if r < 0 then 0 else 2*r)" ``` immler@69613 ` 1922` ```proof - ``` immler@69613 ` 1923` ``` have "diameter(cball a r) = 2*r" if "r \ 0" ``` immler@69613 ` 1924` ``` proof (rule order_antisym) ``` immler@69613 ` 1925` ``` show "diameter (cball a r) \ 2*r" ``` immler@69613 ` 1926` ``` proof (rule diameter_le) ``` immler@69613 ` 1927` ``` fix x y assume "x \ cball a r" "y \ cball a r" ``` immler@69613 ` 1928` ``` then have "norm (x - a) \ r" "norm (a - y) \ r" ``` immler@69613 ` 1929` ``` by (auto simp: dist_norm norm_minus_commute) ``` immler@69613 ` 1930` ``` then have "norm (x - y) \ r+r" ``` immler@69613 ` 1931` ``` using norm_diff_triangle_le by blast ``` immler@69613 ` 1932` ``` then show "norm (x - y) \ 2*r" by simp ``` immler@69613 ` 1933` ``` qed (simp add: that) ``` immler@69613 ` 1934` ``` have "2*r = dist (a + r *\<^sub>R (SOME i. i \ Basis)) (a - r *\<^sub>R (SOME i. i \ Basis))" ``` immler@69613 ` 1935` ``` apply (simp add: dist_norm) ``` immler@69613 ` 1936` ``` by (metis abs_of_nonneg mult.right_neutral norm_numeral norm_scaleR norm_some_Basis real_norm_def scaleR_2 that) ``` immler@69613 ` 1937` ``` also have "... \ diameter (cball a r)" ``` immler@69613 ` 1938` ``` apply (rule diameter_bounded_bound) ``` immler@69613 ` 1939` ``` using that by (auto simp: dist_norm) ``` immler@69613 ` 1940` ``` finally show "2*r \ diameter (cball a r)" . ``` immler@69613 ` 1941` ``` qed ``` immler@69613 ` 1942` ``` then show ?thesis by simp ``` immler@69613 ` 1943` ```qed ``` immler@69613 ` 1944` immler@69613 ` 1945` ```lemma diameter_ball [simp]: ``` immler@69613 ` 1946` ``` fixes a :: "'a::euclidean_space" ``` immler@69613 ` 1947` ``` shows "diameter(ball a r) = (if r < 0 then 0 else 2*r)" ``` immler@69613 ` 1948` ```proof - ``` immler@69613 ` 1949` ``` have "diameter(ball a r) = 2*r" if "r > 0" ``` immler@69613 ` 1950` ``` by (metis bounded_ball diameter_closure closure_ball diameter_cball less_eq_real_def linorder_not_less that) ``` immler@69613 ` 1951` ``` then show ?thesis ``` immler@69613 ` 1952` ``` by (simp add: diameter_def) ``` immler@69613 ` 1953` ```qed ``` immler@69613 ` 1954` immler@69613 ` 1955` ```lemma diameter_closed_interval [simp]: "diameter {a..b} = (if b < a then 0 else b-a)" ``` immler@69613 ` 1956` ```proof - ``` immler@69613 ` 1957` ``` have "{a .. b} = cball ((a+b)/2) ((b-a)/2)" ``` immler@69613 ` 1958` ``` by (auto simp: dist_norm abs_if divide_simps split: if_split_asm) ``` immler@69613 ` 1959` ``` then show ?thesis ``` immler@69613 ` 1960` ``` by simp ``` immler@69613 ` 1961` ```qed ``` immler@69613 ` 1962` immler@69613 ` 1963` ```lemma diameter_open_interval [simp]: "diameter {a<..i \ Basis. a \ i \ b \ i) \ diameter (cbox a b) = dist a b" ``` immler@69613 ` 1974` ``` by (force simp: diameter_def intro!: cSup_eq_maximum L2_set_mono ``` immler@69613 ` 1975` ``` simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm) ``` immler@69613 ` 1976` immler@69613 ` 1977` immler@69617 ` 1978` ```subsection%unimportant\Relating linear images to open/closed/interior/closure/connected\ ``` immler@56189 ` 1979` immler@69611 ` 1980` ```proposition open_surjective_linear_image: ``` immler@69611 ` 1981` ``` fixes f :: "'a::real_normed_vector \ 'b::euclidean_space" ``` immler@69611 ` 1982` ``` assumes "open A" "linear f" "surj f" ``` immler@69611 ` 1983` ``` shows "open(f ` A)" ``` immler@69611 ` 1984` ```unfolding open_dist ``` immler@69611 ` 1985` ```proof clarify ``` immler@69611 ` 1986` ``` fix x ``` immler@69611 ` 1987` ``` assume "x \ A" ``` immler@69611 ` 1988` ``` have "bounded (inv f ` Basis)" ``` immler@69611 ` 1989` ``` by (simp add: finite_imp_bounded) ``` immler@69611 ` 1990` ``` with bounded_pos obtain B where "B > 0" and B: "\x. x \ inv f ` Basis \ norm x \ B" ``` immler@69611 ` 1991` ``` by metis ``` immler@69611 ` 1992` ``` obtain e where "e > 0" and e: "\z. dist z x < e \ z \ A" ``` immler@69611 ` 1993` ``` by (metis open_dist \x \ A\ \open A\) ``` immler@69611 ` 1994` ``` define \ where "\ \ e / B / DIM('b)" ``` immler@69611 ` 1995` ``` show "\e>0. \y. dist y (f x) < e \ y \ f ` A" ``` immler@69611 ` 1996` ``` proof (intro exI conjI) ``` immler@69611 ` 1997` ``` show "\ > 0" ``` immler@69611 ` 1998` ``` using \e > 0\ \B > 0\ by (simp add: \_def divide_simps) ``` immler@69611 ` 1999` ``` have "y \ f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y ``` immler@69611 ` 2000` ``` proof - ``` immler@69611 ` 2001` ``` define u where "u \ y - f x" ``` immler@69611 ` 2002` ``` show ?thesis ``` immler@69611 ` 2003` ``` proof (rule image_eqI) ``` immler@69611 ` 2004` ``` show "y = f (x + (\i\Basis. (u \ i) *\<^sub>R inv f i))" ``` immler@69611 ` 2005` ``` apply (simp add: linear_add linear_sum linear.scaleR \linear f\ surj_f_inv_f \surj f\) ``` immler@69611 ` 2006` ``` apply (simp add: euclidean_representation u_def) ``` immler@69611 ` 2007` ``` done ``` immler@69611 ` 2008` ``` have "dist (x + (\i\Basis. (u \ i) *\<^sub>R inv f i)) x \ (\i\Basis. norm ((u \ i) *\<^sub>R inv f i))" ``` immler@69611 ` 2009` ``` by (simp add: dist_norm sum_norm_le) ``` immler@69611 ` 2010` ``` also have "... = (\i\Basis. \u \ i\ * norm (inv f i))" ``` immler@69611 ` 2011` ``` by simp ``` immler@69611 ` 2012` ``` also have "... \ (\i\Basis. \u \ i\) * B" ``` immler@69611 ` 2013` ``` by (simp add: B sum_distrib_right sum_mono mult_left_mono) ``` immler@69611 ` 2014` ``` also have "... \ DIM('b) * dist y (f x) * B" ``` immler@69611 ` 2015` ``` apply (rule mult_right_mono [OF sum_bounded_above]) ``` immler@69611 ` 2016` ``` using \0 < B\ by (auto simp: Basis_le_norm dist_norm u_def) ``` immler@69611 ` 2017` ``` also have "... < e" ``` immler@69611 ` 2018` ``` by (metis mult.commute mult.left_commute that) ``` immler@69611 ` 2019` ``` finally show "x + (\i\Basis. (u \ i) *\<^sub>R inv f i) \ A" ``` immler@69611 ` 2020` ``` by (rule e) ``` immler@69611 ` 2021` ``` qed ``` immler@69611 ` 2022` ``` qed ``` immler@69611 ` 2023` ``` then show "\y. dist y (f x) < \ \ y \ f ` A" ``` immler@69611 ` 2024` ``` using \e > 0\ \B > 0\ ``` immler@69611 ` 2025` ``` by (auto simp: \_def divide_simps mult_less_0_iff) ``` immler@69611 ` 2026` ``` qed ``` immler@69611 ` 2027` ```qed ``` immler@69611 ` 2028` immler@69611 ` 2029` ```corollary open_bijective_linear_image_eq: ``` immler@69611 ` 2030` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` immler@69611 ` 2031` ``` assumes "linear f" "bij f" ``` immler@69611 ` 2032` ``` shows "open(f ` A) \ open A" ``` immler@69611 ` 2033` ```proof ``` immler@69611 ` 2034` ``` assume "open(f ` A)" ``` immler@69611 ` 2035` ``` then have "open(f -` (f ` A))" ``` immler@69611 ` 2036` ``` using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage) ``` immler@69611 ` 2037` ``` then show "open A" ``` immler@69611 ` 2038` ``` by (simp add: assms bij_is_inj inj_vimage_image_eq) ``` immler@69611 ` 2039` ```next ``` immler@69611 ` 2040` ``` assume "open A" ``` immler@69611 ` 2041` ``` then show "open(f ` A)" ``` immler@69611 ` 2042` ``` by (simp add: assms bij_is_surj open_surjective_linear_image) ``` immler@69611 ` 2043` ```qed ``` immler@69611 ` 2044` immler@69611 ` 2045` ```corollary interior_bijective_linear_image: ``` immler@69611 ` 2046` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` immler@69611 ` 2047` ``` assumes "linear f" "bij f" ``` immler@69611 ` 2048` ``` shows "interior (f ` S) = f ` interior S" (is "?lhs = ?rhs") ``` immler@69611 ` 2049` ```proof safe ``` immler@69611 ` 2050` ``` fix x ``` immler@69611 ` 2051` ``` assume x: "x \ ?lhs" ``` immler@69611 ` 2052` ``` then obtain T where "open T" and "x \ T" and "T \ f ` S" ``` immler@69611 ` 2053` ``` by (metis interiorE) ``` immler@69611 ` 2054` ``` then show "x \ ?rhs" ``` immler@69611 ` 2055` ``` by (metis (no_types, hide_lams) assms subsetD interior_maximal open_bijective_linear_image_eq subset_image_iff) ``` immler@69611 ` 2056` ```next ``` immler@69611 ` 2057` ``` fix x ``` immler@69611 ` 2058` ``` assume x: "x \ interior S" ``` immler@69611 ` 2059` ``` then show "f x \ interior (f ` S)" ``` immler@69611 ` 2060` ``` by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior) ``` immler@69611 ` 2061` ```qed ``` immler@69611 ` 2062` immler@69611 ` 2063` ```lemma interior_injective_linear_image: ``` immler@69611 ` 2064` ``` fixes f :: "'a::euclidean_space \ 'a::euclidean_space" ``` immler@69611 ` 2065` ``` assumes "linear f" "inj f" ``` immler@69611 ` 2066` ``` shows "interior(f ` S) = f ` (interior S)" ``` immler@69611 ` 2067` ``` by (simp add: linear_injective_imp_surjective assms bijI interior_bijective_linear_image) ``` immler@69611 ` 2068` immler@69611 ` 2069` ```lemma interior_surjective_linear_image: ``` immler@69611 ` 2070` ``` fixes f :: "'a::euclidean_space \ 'a::euclidean_space" ``` immler@69611 ` 2071` ``` assumes "linear f" "surj f" ``` immler@69611 ` 2072` ``` shows "interior(f ` S) = f ` (interior S)" ``` immler@69611 ` 2073` ``` by (simp add: assms interior_injective_linear_image linear_surjective_imp_injective) ``` immler@69611 ` 2074` immler@69611 ` 2075` ```lemma interior_negations: ``` immler@69611 ` 2076` ``` fixes S :: "'a::euclidean_space set" ``` immler@69611 ` 2077` ``` shows "interior(uminus ` S) = image uminus (interior S)" ``` immler@69611 ` 2078` ``` by (simp add: bij_uminus interior_bijective_linear_image linear_uminus) ``` immler@56189 ` 2079` immler@69617 ` 2080` ```lemma connected_linear_image: ``` immler@69617 ` 2081` ``` fixes f :: "'a::euclidean_space \ 'b::real_normed_vector" ``` immler@69617 ` 2082` ``` assumes "linear f" and "connected s" ``` immler@69617 ` 2083` ``` shows "connected (f ` s)" ``` immler@69617 ` 2084` ```using connected_continuous_image assms linear_continuous_on linear_conv_bounded_linear by blast ``` immler@69617 ` 2085` immler@69617 ` 2086` immler@69613 ` 2087` ```subsection%unimportant \"Isometry" (up to constant bounds) of Injective Linear Map\ ``` immler@69613 ` 2088` immler@69613 ` 2089` ```proposition injective_imp_isometric: ``` immler@69613 ` 2090` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` immler@69613 ` 2091` ``` assumes s: "closed s" "subspace s" ``` immler@69613 ` 2092` ``` and f: "bounded_linear f" "\x\s. f x = 0 \ x = 0" ``` immler@69613 ` 2093` ``` shows "\e>0. \x\s. norm (f x) \ e * norm x" ``` immler@69613 ` 2094` ```proof (cases "s \ {0::'a}") ``` immler@69613 ` 2095` ``` case True ``` immler@69613 ` 2096` ``` have "norm x \ norm (f x)" if "x \ s" for x ``` immler@69613 ` 2097` ``` proof - ``` immler@69613 ` 2098` ``` from True that have "x = 0" by auto ``` immler@69613 ` 2099` ``` then show ?thesis by simp ``` immler@69613 ` 2100` ``` qed ``` immler@69613 ` 2101` ``` then show ?thesis ``` immler@69613 ` 2102` ``` by (auto intro!: exI[where x=1]) ``` immler@69613 ` 2103` ```next ``` immler@69613 ` 2104` ``` case False ``` immler@69613 ` 2105` ``` interpret f: bounded_linear f by fact ``` immler@69613 ` 2106` ``` from False obtain a where a: "a \ 0" "a \ s" ``` immler@69613 ` 2107` ``` by auto ``` immler@69613 ` 2108` ``` from False have "s \ {}" ``` immler@69613 ` 2109` ``` by auto ``` immler@69613 ` 2110` ``` let ?S = "{f x| x. x \ s \ norm x = norm a}" ``` immler@69613 ` 2111` ``` let ?S' = "{x::'a. x\s \ norm x = norm a}" ``` immler@69613 ` 2112` ``` let ?S'' = "{x::'a. norm x = norm a}" ``` immler@69613 ` 2113` immler@69613 ` 2114` ``` have "?S'' = frontier (cball 0 (norm a))" ``` immler@69613 ` 2115` ``` by (simp add: sphere_def dist_norm) ``` immler@69613 ` 2116` ``` then have "compact ?S''" by (metis compact_cball compact_frontier) ``` immler@69613 ` 2117` ``` moreover have "?S' = s \ ?S''" by auto ``` immler@69613 ` 2118` ``` ultimately have "compact ?S'" ``` immler@69613 ` 2119` ``` using closed_Int_compact[of s ?S''] using s(1) by auto ``` immler@69613 ` 2120` ``` moreover have *:"f ` ?S' = ?S" by auto ``` immler@69613 ` 2121` ``` ultimately have "compact ?S" ``` immler@69613 ` 2122` ``` using compact_continuous_image[OF linear_continuous_on[OF f(1)], of ?S'] by auto ``` immler@69613 ` 2123` ``` then have "closed ?S" ``` immler@69613 ` 2124` ``` using compact_imp_closed by auto ``` immler@69613 ` 2125` ``` moreover from a have "?S \ {}" by auto ``` immler@69613 ` 2126` ``` ultimately obtain b' where "b'\?S" "\y\?S. norm b' \ norm y" ``` immler@69613 ` 2127` ``` using distance_attains_inf[of ?S 0] unfolding dist_0_norm by auto ``` immler@69613 ` 2128` ``` then obtain b where "b\s" ``` immler@69613 ` 2129` ``` and ba: "norm b = norm a" ``` immler@69613 ` 2130` ``` and b: "\x\{x \ s. norm x = norm a}. norm (f b) \ norm (f x)" ``` immler@69613 ` 2131` ``` unfolding *[symmetric] unfolding image_iff by auto ``` immler@69613 ` 2132` immler@69613 ` 2133` ``` let ?e = "norm (f b) / norm b" ``` immler@69613 ` 2134` ``` have "norm b > 0" ``` immler@69613 ` 2135` ``` using ba and a and norm_ge_zero by auto ``` immler@69613 ` 2136` ``` moreover have "norm (f b) > 0" ``` immler@69613 ` 2137` ``` using f(2)[THEN bspec[where x=b], OF \b\s\] ``` immler@69613 ` 2138` ``` using \norm b >0\ by simp ``` immler@69613 ` 2139` ``` ultimately have "0 < norm (f b) / norm b" by simp ``` immler@69613 ` 2140` ``` moreover ``` immler@69613 ` 2141` ``` have "norm (f b) / norm b * norm x \ norm (f x)" if "x\s" for x ``` immler@69613 ` 2142` ``` proof (cases "x = 0") ``` immler@69613 ` 2143` ``` case True ``` immler@69613 ` 2144` ``` then show "norm (f b) / norm b * norm x \ norm (f x)" ``` immler@69613 ` 2145` ``` by auto ``` immler@69613 ` 2146` ``` next ``` immler@69613 ` 2147` ``` case False ``` immler@69613 ` 2148` ``` with \a \ 0\ have *: "0 < norm a / norm x" ``` immler@69613 ` 2149` ``` unfolding zero_less_norm_iff[symmetric] by simp ``` immler@69613 ` 2150` ``` have "\x\s. c *\<^sub>R x \ s" for c ``` immler@69613 ` 2151` ``` using s[unfolded subspace_def] by simp ``` immler@69613 ` 2152` ``` with \x \ s\ \x \ 0\ have "(norm a / norm x) *\<^sub>R x \ {x \ s. norm x = norm a}" ``` immler@69613 ` 2153` ``` by simp ``` immler@69613 ` 2154` ``` with \x \ 0\ \a \ 0\ show "norm (f b) / norm b * norm x \ norm (f x)" ``` immler@69613 ` 2155` ``` using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]] ``` immler@69613 ` 2156` ``` unfolding f.scaleR and ba ``` immler@69613 ` 2157` ``` by (auto simp: mult.commute pos_le_divide_eq pos_divide_le_eq) ``` immler@69613 ` 2158` ``` qed ``` immler@69613 ` 2159` ``` ultimately show ?thesis by auto ``` immler@69613 ` 2160` ```qed ``` immler@69613 ` 2161` immler@69613 ` 2162` ```proposition closed_injective_image_subspace: ``` immler@69613 ` 2163` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` immler@69613 ` 2164` ``` assumes "subspace s" "bounded_linear f" "\x\s. f x = 0 \ x = 0" "closed s" ``` immler@69613 ` 2165` ``` shows "closed(f ` s)" ``` immler@69613 ` 2166` ```proof - ``` immler@69613 ` 2167` ``` obtain e where "e > 0" and e: "\x\s. e * norm x \ norm (f x)" ``` immler@69613 ` 2168` ``` using injective_imp_isometric[OF assms(4,1,2,3)] by auto ``` immler@69613 ` 2169` ``` show ?thesis ``` immler@69613 ` 2170` ``` using complete_isometric_image[OF \e>0\ assms(1,2) e] and assms(4) ``` immler@69613 ` 2171` ``` unfolding complete_eq_closed[symmetric] by auto ``` immler@69613 ` 2172` ```qed ``` immler@69613 ` 2173` immler@69613 ` 2174` immler@69613 ` 2175` ```subsection%unimportant \Some properties of a canonical subspace\ ``` immler@69613 ` 2176` immler@69613 ` 2177` ```lemma closed_substandard: "closed {x::'a::euclidean_space. \i\Basis. P i \ x\i = 0}" ``` immler@69613 ` 2178` ``` (is "closed ?A") ``` immler@69613 ` 2179` ```proof - ``` immler@69613 ` 2180` ``` let ?D = "{i\Basis. P i}" ``` immler@69613 ` 2181` ``` have "closed (\i\?D. {x::'a. x\i = 0})" ``` immler@69613 ` 2182` ``` by (simp add: closed_INT closed_Collect_eq continuous_on_inner ``` immler@69613 ` 2183` ``` continuous_on_const continuous_on_id) ``` immler@69613 ` 2184` ``` also have "(\i\?D. {x::'a. x\i = 0}) = ?A" ``` immler@69613 ` 2185` ``` by auto ``` immler@69613 ` 2186` ``` finally show "closed ?A" . ``` immler@69613 ` 2187` ```qed ``` immler@69613 ` 2188` immler@69613 ` 2189` ```lemma closed_subspace: ``` immler@69613 ` 2190` ``` fixes s :: "'a::euclidean_space set" ``` immler@69613 ` 2191` ``` assumes "subspace s" ``` immler@69613 ` 2192` ``` shows "closed s" ``` immler@69613 ` 2193` ```proof - ``` immler@69613 ` 2194` ``` have "dim s \ card (Basis :: 'a set)" ``` immler@69613 ` 2195` ``` using dim_subset_UNIV by auto ``` immler@69613 ` 2196` ``` with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \ Basis" ``` immler@69613 ` 2197` ``` by auto ``` immler@69613 ` 2198` ``` let ?t = "{x::'a. \i\Basis. i \ d \ x\i = 0}" ``` immler@69613 ` 2199` ``` have "\f. linear f \ f ` {x::'a. \i\Basis. i \ d \ x \ i = 0} = s \ ``` immler@69613 ` 2200` ``` inj_on f {x::'a. \i\Basis. i \ d \ x \ i = 0}" ``` immler@69613 ` 2201` ``` using dim_substandard[of d] t d assms ``` immler@69613 ` 2202` ``` by (intro subspace_isomorphism[OF subspace_substandard[of "\i. i \ d"]]) (auto simp: inner_Basis) ``` immler@69613 ` 2203` ``` then obtain f where f: ``` immler@69613 ` 2204` ``` "linear f" ``` immler@69613 ` 2205` ``` "f ` {x. \i\Basis. i \ d \ x \ i = 0} = s" ``` immler@69613 ` 2206` ``` "inj_on f {x. \i\Basis. i \ d \ x \ i = 0}" ``` immler@69613 ` 2207` ``` by blast ``` immler@69613 ` 2208` ``` interpret f: bounded_linear f ``` immler@69613 ` 2209` ``` using f by (simp add: linear_conv_bounded_linear) ``` immler@69613 ` 2210` ``` have "x \ ?t \ f x = 0 \ x = 0" for x ``` immler@69613 ` 2211` ``` using f.zero d f(3)[THEN inj_onD, of x 0] by auto ``` immler@69613 ` 2212` ``` moreover have "closed ?t" by (rule closed_substandard) ``` immler@69613 ` 2213` ``` moreover have "subspace ?t" by (rule subspace_substandard) ``` immler@69613 ` 2214` ``` ultimately show ?thesis ``` immler@69613 ` 2215` ``` using closed_injective_image_subspace[of ?t f] ``` immler@69613 ` 2216` ``` unfolding f(2) using f(1) unfolding linear_conv_bounded_linear by auto ``` immler@69613 ` 2217` ```qed ``` immler@69613 ` 2218` immler@69613 ` 2219` ```lemma complete_subspace: "subspace s \ complete s" ``` immler@69613 ` 2220` ``` for s :: "'a::euclidean_space set" ``` immler@69613 ` 2221` ``` using complete_eq_closed closed_subspace by auto ``` immler@69613 ` 2222` immler@69613 ` 2223` ```lemma closed_span [iff]: "closed (span s)" ``` immler@69613 ` 2224` ``` for s :: "'a::euclidean_space set" ``` immler@69613 ` 2225` ``` by (simp add: closed_subspace subspace_span) ``` immler@69613 ` 2226` immler@69613 ` 2227` ```lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d") ``` immler@69613 ` 2228` ``` for s :: "'a::euclidean_space set" ``` immler@69613 ` 2229` ```proof - ``` immler@69613 ` 2230` ``` have "?dc \ ?d" ``` immler@69613 ` 2231` ``` using closure_minimal[OF span_superset, of s] ``` immler@69613 ` 2232` ``` using closed_subspace[OF subspace_span, of s] ``` immler@69613 ` 2233` ``` using dim_subset[of "closure s" "span s"] ``` immler@69613 ` 2234` ``` by simp ``` immler@69613 ` 2235` ``` then show ?thesis ``` immler@69613 ` 2236` ``` using dim_subset[OF closure_subset, of s] ``` immler@69613 ` 2237` ``` by simp ``` immler@69613 ` 2238` ```qed ``` immler@69613 ` 2239` immler@69613 ` 2240` immler@69618 ` 2241` ```subsection \Set Distance\ ``` immler@69618 ` 2242` immler@69618 ` 2243` ```lemma setdist_compact_closed: ``` immler@69618 ` 2244` ``` fixes S :: "'a::{heine_borel,real_normed_vector} set" ``` immler@69618 ` 2245` ``` assumes S: "compact S" and T: "closed T" ``` immler@69618 ` 2246` ``` and "S \ {}" "T \ {}" ``` immler@69618 ` 2247` ``` shows "\x \ S. \y \ T. dist x y = setdist S T" ``` immler@69618 ` 2248` ```proof - ``` immler@69618 ` 2249` ``` have "(\x\ S. \y \ T. {x - y}) \ {}" ``` immler@69618 ` 2250` ``` using assms by blast ``` immler@69618 ` 2251` ``` then have "\x \ S. \y \ T. dist x y \ setdist S T" ``` immler@69618 ` 2252` ``` apply (rule distance_attains_inf [where a=0, OF compact_closed_differences [OF S T]]) ``` immler@69618 ` 2253` ``` apply (simp add: dist_norm le_setdist_iff) ``` immler@69618 ` 2254` ``` apply blast ``` immler@69618 ` 2255` ``` done ``` immler@69618 ` 2256` ``` then show ?thesis ``` immler@69618 ` 2257` ``` by (blast intro!: antisym [OF _ setdist_le_dist] ) ``` immler@69618 ` 2258` ```qed ``` immler@69618 ` 2259` immler@69618 ` 2260` ```lemma setdist_closed_compact: ``` immler@69618 ` 2261` ``` fixes S :: "'a::{heine_borel,real_normed_vector} set" ``` immler@69618 ` 2262` ``` assumes S: "closed S" and T: "compact T" ``` immler@69618 ` 2263` ``` and "S \ {}" "T \ {}" ``` immler@69618 ` 2264` ``` shows "\x \ S. \y \ T. dist x y = setdist S T" ``` immler@69618 ` 2265` ``` using setdist_compact_closed [OF T S \T \ {}\ \S \ {}\] ``` immler@69618 ` 2266` ``` by (metis dist_commute setdist_sym) ``` immler@69618 ` 2267` immler@69618 ` 2268` ```lemma setdist_eq_0_compact_closed: ``` immler@69618 ` 2269` ``` fixes S :: "'a::{heine_borel,real_normed_vector} set" ``` immler@69618 ` 2270` ``` assumes S: "compact S" and T: "closed T" ``` immler@69618 ` 2271` ``` shows "setdist S T = 0 \ S = {} \ T = {} \ S \ T \ {}" ``` immler@69618 ` 2272` ``` apply (cases "S = {} \ T = {}", force) ``` immler@69618 ` 2273` ``` using setdist_compact_closed [OF S T] ```