src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 author huffman Mon Aug 29 13:50:47 2011 -0700 (2011-08-29) changeset 44584 08ad27488983 parent 44571 bd91b77c4cd6 child 44628 bd17b7543af1 permissions -rw-r--r--
simplify some proofs
 hoelzl@33714 ` 1` ```(* title: HOL/Library/Topology_Euclidian_Space.thy ``` 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` himmelma@33175 ` 7` ```header {* Elementary topology in Euclidean space. *} ``` himmelma@33175 ` 8` himmelma@33175 ` 9` ```theory Topology_Euclidean_Space ``` huffman@44517 ` 10` ```imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm ``` himmelma@33175 ` 11` ```begin ``` himmelma@33175 ` 12` hoelzl@37489 ` 13` ```(* to be moved elsewhere *) ``` hoelzl@37489 ` 14` hoelzl@37489 ` 15` ```lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\i. dist(x\$\$i) (y\$\$i)) {.. dist x (y::'a::euclidean_space)" ``` hoelzl@37489 ` 20` ``` apply(subst(2) euclidean_dist_l2) apply(cases "i L {} \ (\S T. L S \ L T \ L (S \ T)) \ (\K. Ball K L \ L (\ K))" ``` huffman@44170 ` 26` ```typedef (open) 'a topology = "{L::('a set) \ bool. istopology L}" ``` himmelma@33175 ` 27` ``` morphisms "openin" "topology" ``` himmelma@33175 ` 28` ``` unfolding istopology_def by blast ``` himmelma@33175 ` 29` himmelma@33175 ` 30` ```lemma istopology_open_in[intro]: "istopology(openin U)" ``` himmelma@33175 ` 31` ``` using openin[of U] by blast ``` himmelma@33175 ` 32` himmelma@33175 ` 33` ```lemma topology_inverse': "istopology U \ openin (topology U) = U" ``` huffman@44170 ` 34` ``` using topology_inverse[unfolded mem_Collect_eq] . ``` himmelma@33175 ` 35` himmelma@33175 ` 36` ```lemma topology_inverse_iff: "istopology U \ openin (topology U) = U" ``` himmelma@33175 ` 37` ``` using topology_inverse[of U] istopology_open_in[of "topology U"] by auto ``` himmelma@33175 ` 38` himmelma@33175 ` 39` ```lemma topology_eq: "T1 = T2 \ (\S. openin T1 S \ openin T2 S)" ``` himmelma@33175 ` 40` ```proof- ``` himmelma@33175 ` 41` ``` {assume "T1=T2" hence "\S. openin T1 S \ openin T2 S" by simp} ``` himmelma@33175 ` 42` ``` moreover ``` himmelma@33175 ` 43` ``` {assume H: "\S. openin T1 S \ openin T2 S" ``` huffman@44170 ` 44` ``` hence "openin T1 = openin T2" by (simp add: fun_eq_iff) ``` himmelma@33175 ` 45` ``` hence "topology (openin T1) = topology (openin T2)" by simp ``` himmelma@33175 ` 46` ``` hence "T1 = T2" unfolding openin_inverse .} ``` himmelma@33175 ` 47` ``` ultimately show ?thesis by blast ``` himmelma@33175 ` 48` ```qed ``` himmelma@33175 ` 49` himmelma@33175 ` 50` ```text{* Infer the "universe" from union of all sets in the topology. *} ``` himmelma@33175 ` 51` himmelma@33175 ` 52` ```definition "topspace T = \{S. openin T S}" ``` himmelma@33175 ` 53` huffman@44210 ` 54` ```subsubsection {* Main properties of open sets *} ``` himmelma@33175 ` 55` himmelma@33175 ` 56` ```lemma openin_clauses: ``` himmelma@33175 ` 57` ``` fixes U :: "'a topology" ``` himmelma@33175 ` 58` ``` shows "openin U {}" ``` himmelma@33175 ` 59` ``` "\S T. openin U S \ openin U T \ openin U (S\T)" ``` himmelma@33175 ` 60` ``` "\K. (\S \ K. openin U S) \ openin U (\K)" ``` huffman@44170 ` 61` ``` using openin[of U] unfolding istopology_def mem_Collect_eq ``` huffman@44170 ` 62` ``` by fast+ ``` himmelma@33175 ` 63` himmelma@33175 ` 64` ```lemma openin_subset[intro]: "openin U S \ S \ topspace U" ``` himmelma@33175 ` 65` ``` unfolding topspace_def by blast ``` himmelma@33175 ` 66` ```lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses) ``` himmelma@33175 ` 67` himmelma@33175 ` 68` ```lemma openin_Int[intro]: "openin U S \ openin U T \ openin U (S \ T)" ``` huffman@36362 ` 69` ``` using openin_clauses by simp ``` huffman@36362 ` 70` huffman@36362 ` 71` ```lemma openin_Union[intro]: "(\S \K. openin U S) \ openin U (\ K)" ``` huffman@36362 ` 72` ``` using openin_clauses by simp ``` himmelma@33175 ` 73` himmelma@33175 ` 74` ```lemma openin_Un[intro]: "openin U S \ openin U T \ openin U (S \ T)" ``` himmelma@33175 ` 75` ``` using openin_Union[of "{S,T}" U] by auto ``` himmelma@33175 ` 76` himmelma@33175 ` 77` ```lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def) ``` himmelma@33175 ` 78` himmelma@33175 ` 79` ```lemma openin_subopen: "openin U S \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" (is "?lhs \ ?rhs") ``` huffman@36584 ` 80` ```proof ``` huffman@36584 ` 81` ``` assume ?lhs then show ?rhs by auto ``` huffman@36584 ` 82` ```next ``` huffman@36584 ` 83` ``` assume H: ?rhs ``` huffman@36584 ` 84` ``` let ?t = "\{T. openin U T \ T \ S}" ``` huffman@36584 ` 85` ``` have "openin U ?t" by (simp add: openin_Union) ``` huffman@36584 ` 86` ``` also have "?t = S" using H by auto ``` huffman@36584 ` 87` ``` finally show "openin U S" . ``` himmelma@33175 ` 88` ```qed ``` himmelma@33175 ` 89` huffman@44210 ` 90` ```subsubsection {* Closed sets *} ``` himmelma@33175 ` 91` himmelma@33175 ` 92` ```definition "closedin U S \ S \ topspace U \ openin U (topspace U - S)" ``` himmelma@33175 ` 93` himmelma@33175 ` 94` ```lemma closedin_subset: "closedin U S \ S \ topspace U" by (metis closedin_def) ``` himmelma@33175 ` 95` ```lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def) ``` himmelma@33175 ` 96` ```lemma closedin_topspace[intro,simp]: ``` himmelma@33175 ` 97` ``` "closedin U (topspace U)" by (simp add: closedin_def) ``` himmelma@33175 ` 98` ```lemma closedin_Un[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" ``` himmelma@33175 ` 99` ``` by (auto simp add: Diff_Un closedin_def) ``` himmelma@33175 ` 100` himmelma@33175 ` 101` ```lemma Diff_Inter[intro]: "A - \S = \ {A - s|s. s\S}" by auto ``` himmelma@33175 ` 102` ```lemma closedin_Inter[intro]: assumes Ke: "K \ {}" and Kc: "\S \K. closedin U S" ``` himmelma@33175 ` 103` ``` shows "closedin U (\ K)" using Ke Kc unfolding closedin_def Diff_Inter by auto ``` himmelma@33175 ` 104` himmelma@33175 ` 105` ```lemma closedin_Int[intro]: "closedin U S \ closedin U T \ closedin U (S \ T)" ``` himmelma@33175 ` 106` ``` using closedin_Inter[of "{S,T}" U] by auto ``` himmelma@33175 ` 107` himmelma@33175 ` 108` ```lemma Diff_Diff_Int: "A - (A - B) = A \ B" by blast ``` himmelma@33175 ` 109` ```lemma openin_closedin_eq: "openin U S \ S \ topspace U \ closedin U (topspace U - S)" ``` himmelma@33175 ` 110` ``` apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2) ``` himmelma@33175 ` 111` ``` apply (metis openin_subset subset_eq) ``` himmelma@33175 ` 112` ``` done ``` himmelma@33175 ` 113` himmelma@33175 ` 114` ```lemma openin_closedin: "S \ topspace U \ (openin U S \ closedin U (topspace U - S))" ``` himmelma@33175 ` 115` ``` by (simp add: openin_closedin_eq) ``` himmelma@33175 ` 116` himmelma@33175 ` 117` ```lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" ``` himmelma@33175 ` 118` ```proof- ``` himmelma@33175 ` 119` ``` have "S - T = S \ (topspace U - T)" using openin_subset[of U S] oS cT ``` himmelma@33175 ` 120` ``` by (auto simp add: topspace_def openin_subset) ``` himmelma@33175 ` 121` ``` then show ?thesis using oS cT by (auto simp add: closedin_def) ``` himmelma@33175 ` 122` ```qed ``` himmelma@33175 ` 123` himmelma@33175 ` 124` ```lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)" ``` himmelma@33175 ` 125` ```proof- ``` himmelma@33175 ` 126` ``` have "S - T = S \ (topspace U - T)" using closedin_subset[of U S] oS cT ``` himmelma@33175 ` 127` ``` by (auto simp add: topspace_def ) ``` himmelma@33175 ` 128` ``` then show ?thesis using oS cT by (auto simp add: openin_closedin_eq) ``` himmelma@33175 ` 129` ```qed ``` himmelma@33175 ` 130` huffman@44210 ` 131` ```subsubsection {* Subspace topology *} ``` huffman@44170 ` 132` huffman@44170 ` 133` ```definition "subtopology U V = topology (\T. \S. T = S \ V \ openin U S)" ``` huffman@44170 ` 134` huffman@44170 ` 135` ```lemma istopology_subtopology: "istopology (\T. \S. T = S \ V \ openin U S)" ``` huffman@44170 ` 136` ``` (is "istopology ?L") ``` himmelma@33175 ` 137` ```proof- ``` huffman@44170 ` 138` ``` have "?L {}" by blast ``` huffman@44170 ` 139` ``` {fix A B assume A: "?L A" and B: "?L B" ``` himmelma@33175 ` 140` ``` from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \ V" and Sb: "openin U Sb" "B = Sb \ V" by blast ``` himmelma@33175 ` 141` ``` have "A\B = (Sa \ Sb) \ V" "openin U (Sa \ Sb)" using Sa Sb by blast+ ``` huffman@44170 ` 142` ``` then have "?L (A \ B)" by blast} ``` himmelma@33175 ` 143` ``` moreover ``` huffman@44170 ` 144` ``` {fix K assume K: "K \ Collect ?L" ``` huffman@44170 ` 145` ``` have th0: "Collect ?L = (\S. S \ V) ` Collect (openin U)" ``` nipkow@39302 ` 146` ``` apply (rule set_eqI) ``` himmelma@33175 ` 147` ``` apply (simp add: Ball_def image_iff) ``` huffman@44170 ` 148` ``` by metis ``` himmelma@33175 ` 149` ``` from K[unfolded th0 subset_image_iff] ``` huffman@44170 ` 150` ``` obtain Sk where Sk: "Sk \ Collect (openin U)" "K = (\S. S \ V) ` Sk" by blast ``` himmelma@33175 ` 151` ``` have "\K = (\Sk) \ V" using Sk by auto ``` huffman@44170 ` 152` ``` moreover have "openin U (\ Sk)" using Sk by (auto simp add: subset_eq) ``` huffman@44170 ` 153` ``` ultimately have "?L (\K)" by blast} ``` huffman@44170 ` 154` ``` ultimately show ?thesis ``` huffman@44170 ` 155` ``` unfolding subset_eq mem_Collect_eq istopology_def by blast ``` himmelma@33175 ` 156` ```qed ``` himmelma@33175 ` 157` himmelma@33175 ` 158` ```lemma openin_subtopology: ``` himmelma@33175 ` 159` ``` "openin (subtopology U V) S \ (\ T. (openin U T) \ (S = T \ V))" ``` himmelma@33175 ` 160` ``` unfolding subtopology_def topology_inverse'[OF istopology_subtopology] ``` huffman@44170 ` 161` ``` by auto ``` himmelma@33175 ` 162` himmelma@33175 ` 163` ```lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \ V" ``` himmelma@33175 ` 164` ``` by (auto simp add: topspace_def openin_subtopology) ``` himmelma@33175 ` 165` himmelma@33175 ` 166` ```lemma closedin_subtopology: ``` himmelma@33175 ` 167` ``` "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" ``` himmelma@33175 ` 168` ``` unfolding closedin_def topspace_subtopology ``` himmelma@33175 ` 169` ``` apply (simp add: openin_subtopology) ``` himmelma@33175 ` 170` ``` apply (rule iffI) ``` himmelma@33175 ` 171` ``` apply clarify ``` himmelma@33175 ` 172` ``` apply (rule_tac x="topspace U - T" in exI) ``` himmelma@33175 ` 173` ``` by auto ``` himmelma@33175 ` 174` himmelma@33175 ` 175` ```lemma openin_subtopology_refl: "openin (subtopology U V) V \ V \ topspace U" ``` himmelma@33175 ` 176` ``` unfolding openin_subtopology ``` himmelma@33175 ` 177` ``` apply (rule iffI, clarify) ``` himmelma@33175 ` 178` ``` apply (frule openin_subset[of U]) apply blast ``` himmelma@33175 ` 179` ``` apply (rule exI[where x="topspace U"]) ``` himmelma@33175 ` 180` ``` by auto ``` himmelma@33175 ` 181` himmelma@33175 ` 182` ```lemma subtopology_superset: assumes UV: "topspace U \ V" ``` himmelma@33175 ` 183` ``` shows "subtopology U V = U" ``` himmelma@33175 ` 184` ```proof- ``` himmelma@33175 ` 185` ``` {fix S ``` himmelma@33175 ` 186` ``` {fix T assume T: "openin U T" "S = T \ V" ``` himmelma@33175 ` 187` ``` from T openin_subset[OF T(1)] UV have eq: "S = T" by blast ``` himmelma@33175 ` 188` ``` have "openin U S" unfolding eq using T by blast} ``` himmelma@33175 ` 189` ``` moreover ``` himmelma@33175 ` 190` ``` {assume S: "openin U S" ``` himmelma@33175 ` 191` ``` hence "\T. openin U T \ S = T \ V" ``` himmelma@33175 ` 192` ``` using openin_subset[OF S] UV by auto} ``` himmelma@33175 ` 193` ``` ultimately have "(\T. openin U T \ S = T \ V) \ openin U S" by blast} ``` himmelma@33175 ` 194` ``` then show ?thesis unfolding topology_eq openin_subtopology by blast ``` himmelma@33175 ` 195` ```qed ``` himmelma@33175 ` 196` himmelma@33175 ` 197` ```lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U" ``` himmelma@33175 ` 198` ``` by (simp add: subtopology_superset) ``` himmelma@33175 ` 199` himmelma@33175 ` 200` ```lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" ``` himmelma@33175 ` 201` ``` by (simp add: subtopology_superset) ``` himmelma@33175 ` 202` huffman@44210 ` 203` ```subsubsection {* The standard Euclidean topology *} ``` himmelma@33175 ` 204` himmelma@33175 ` 205` ```definition ``` himmelma@33175 ` 206` ``` euclidean :: "'a::topological_space topology" where ``` himmelma@33175 ` 207` ``` "euclidean = topology open" ``` himmelma@33175 ` 208` himmelma@33175 ` 209` ```lemma open_openin: "open S \ openin euclidean S" ``` himmelma@33175 ` 210` ``` unfolding euclidean_def ``` himmelma@33175 ` 211` ``` apply (rule cong[where x=S and y=S]) ``` himmelma@33175 ` 212` ``` apply (rule topology_inverse[symmetric]) ``` himmelma@33175 ` 213` ``` apply (auto simp add: istopology_def) ``` huffman@44170 ` 214` ``` done ``` himmelma@33175 ` 215` himmelma@33175 ` 216` ```lemma topspace_euclidean: "topspace euclidean = UNIV" ``` himmelma@33175 ` 217` ``` apply (simp add: topspace_def) ``` nipkow@39302 ` 218` ``` apply (rule set_eqI) ``` himmelma@33175 ` 219` ``` by (auto simp add: open_openin[symmetric]) ``` himmelma@33175 ` 220` himmelma@33175 ` 221` ```lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S" ``` himmelma@33175 ` 222` ``` by (simp add: topspace_euclidean topspace_subtopology) ``` himmelma@33175 ` 223` himmelma@33175 ` 224` ```lemma closed_closedin: "closed S \ closedin euclidean S" ``` himmelma@33175 ` 225` ``` by (simp add: closed_def closedin_def topspace_euclidean open_openin Compl_eq_Diff_UNIV) ``` himmelma@33175 ` 226` himmelma@33175 ` 227` ```lemma open_subopen: "open S \ (\x\S. \T. open T \ x \ T \ T \ S)" ``` himmelma@33175 ` 228` ``` by (simp add: open_openin openin_subopen[symmetric]) ``` himmelma@33175 ` 229` huffman@44210 ` 230` ```text {* Basic "localization" results are handy for connectedness. *} ``` huffman@44210 ` 231` huffman@44210 ` 232` ```lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" ``` huffman@44210 ` 233` ``` by (auto simp add: openin_subtopology open_openin[symmetric]) ``` huffman@44210 ` 234` huffman@44210 ` 235` ```lemma openin_open_Int[intro]: "open S \ openin (subtopology euclidean U) (U \ S)" ``` huffman@44210 ` 236` ``` by (auto simp add: openin_open) ``` huffman@44210 ` 237` huffman@44210 ` 238` ```lemma open_openin_trans[trans]: ``` huffman@44210 ` 239` ``` "open S \ open T \ T \ S \ openin (subtopology euclidean S) T" ``` huffman@44210 ` 240` ``` by (metis Int_absorb1 openin_open_Int) ``` huffman@44210 ` 241` huffman@44210 ` 242` ```lemma open_subset: "S \ T \ open S \ openin (subtopology euclidean T) S" ``` huffman@44210 ` 243` ``` by (auto simp add: openin_open) ``` huffman@44210 ` 244` huffman@44210 ` 245` ```lemma closedin_closed: "closedin (subtopology euclidean U) S \ (\T. closed T \ S = U \ T)" ``` huffman@44210 ` 246` ``` by (simp add: closedin_subtopology closed_closedin Int_ac) ``` huffman@44210 ` 247` huffman@44210 ` 248` ```lemma closedin_closed_Int: "closed S ==> closedin (subtopology euclidean U) (U \ S)" ``` huffman@44210 ` 249` ``` by (metis closedin_closed) ``` huffman@44210 ` 250` huffman@44210 ` 251` ```lemma closed_closedin_trans: "closed S \ closed T \ T \ S \ closedin (subtopology euclidean S) T" ``` huffman@44210 ` 252` ``` apply (subgoal_tac "S \ T = T" ) ``` huffman@44210 ` 253` ``` apply auto ``` huffman@44210 ` 254` ``` apply (frule closedin_closed_Int[of T S]) ``` huffman@44210 ` 255` ``` by simp ``` huffman@44210 ` 256` huffman@44210 ` 257` ```lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" ``` huffman@44210 ` 258` ``` by (auto simp add: closedin_closed) ``` huffman@44210 ` 259` huffman@44210 ` 260` ```lemma openin_euclidean_subtopology_iff: ``` huffman@44210 ` 261` ``` fixes S U :: "'a::metric_space set" ``` huffman@44210 ` 262` ``` shows "openin (subtopology euclidean U) S ``` huffman@44210 ` 263` ``` \ S \ U \ (\x\S. \e>0. \x'\U. dist x' x < e \ x'\ S)" (is "?lhs \ ?rhs") ``` huffman@44210 ` 264` ```proof ``` huffman@44210 ` 265` ``` assume ?lhs thus ?rhs unfolding openin_open open_dist by blast ``` huffman@44210 ` 266` ```next ``` huffman@44210 ` 267` ``` def T \ "{x. \a\S. \d>0. (\y\U. dist y a < d \ y \ S) \ dist x a < d}" ``` huffman@44210 ` 268` ``` have 1: "\x\T. \e>0. \y. dist y x < e \ y \ T" ``` huffman@44210 ` 269` ``` unfolding T_def ``` huffman@44210 ` 270` ``` apply clarsimp ``` huffman@44210 ` 271` ``` apply (rule_tac x="d - dist x a" in exI) ``` huffman@44210 ` 272` ``` apply (clarsimp simp add: less_diff_eq) ``` huffman@44210 ` 273` ``` apply (erule rev_bexI) ``` huffman@44210 ` 274` ``` apply (rule_tac x=d in exI, clarify) ``` huffman@44210 ` 275` ``` apply (erule le_less_trans [OF dist_triangle]) ``` huffman@44210 ` 276` ``` done ``` huffman@44210 ` 277` ``` assume ?rhs hence 2: "S = U \ T" ``` huffman@44210 ` 278` ``` unfolding T_def ``` huffman@44210 ` 279` ``` apply auto ``` huffman@44210 ` 280` ``` apply (drule (1) bspec, erule rev_bexI) ``` huffman@44210 ` 281` ``` apply auto ``` huffman@44210 ` 282` ``` done ``` huffman@44210 ` 283` ``` from 1 2 show ?lhs ``` huffman@44210 ` 284` ``` unfolding openin_open open_dist by fast ``` huffman@44210 ` 285` ```qed ``` huffman@44210 ` 286` huffman@44210 ` 287` ```text {* These "transitivity" results are handy too *} ``` huffman@44210 ` 288` huffman@44210 ` 289` ```lemma openin_trans[trans]: "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T ``` huffman@44210 ` 290` ``` \ openin (subtopology euclidean U) S" ``` huffman@44210 ` 291` ``` unfolding open_openin openin_open by blast ``` huffman@44210 ` 292` huffman@44210 ` 293` ```lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" ``` huffman@44210 ` 294` ``` by (auto simp add: openin_open intro: openin_trans) ``` huffman@44210 ` 295` huffman@44210 ` 296` ```lemma closedin_trans[trans]: ``` huffman@44210 ` 297` ``` "closedin (subtopology euclidean T) S \ ``` huffman@44210 ` 298` ``` closedin (subtopology euclidean U) T ``` huffman@44210 ` 299` ``` ==> closedin (subtopology euclidean U) S" ``` huffman@44210 ` 300` ``` by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc) ``` huffman@44210 ` 301` huffman@44210 ` 302` ```lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \ closed T \ closed S" ``` huffman@44210 ` 303` ``` by (auto simp add: closedin_closed intro: closedin_trans) ``` huffman@44210 ` 304` huffman@44210 ` 305` huffman@44210 ` 306` ```subsection {* Open and closed balls *} ``` himmelma@33175 ` 307` himmelma@33175 ` 308` ```definition ``` himmelma@33175 ` 309` ``` ball :: "'a::metric_space \ real \ 'a set" where ``` himmelma@33175 ` 310` ``` "ball x e = {y. dist x y < e}" ``` himmelma@33175 ` 311` himmelma@33175 ` 312` ```definition ``` himmelma@33175 ` 313` ``` cball :: "'a::metric_space \ real \ 'a set" where ``` himmelma@33175 ` 314` ``` "cball x e = {y. dist x y \ e}" ``` himmelma@33175 ` 315` himmelma@33175 ` 316` ```lemma mem_ball[simp]: "y \ ball x e \ dist x y < e" by (simp add: ball_def) ``` himmelma@33175 ` 317` ```lemma mem_cball[simp]: "y \ cball x e \ dist x y \ e" by (simp add: cball_def) ``` himmelma@33175 ` 318` himmelma@33175 ` 319` ```lemma mem_ball_0 [simp]: ``` himmelma@33175 ` 320` ``` fixes x :: "'a::real_normed_vector" ``` himmelma@33175 ` 321` ``` shows "x \ ball 0 e \ norm x < e" ``` himmelma@33175 ` 322` ``` by (simp add: dist_norm) ``` himmelma@33175 ` 323` himmelma@33175 ` 324` ```lemma mem_cball_0 [simp]: ``` himmelma@33175 ` 325` ``` fixes x :: "'a::real_normed_vector" ``` himmelma@33175 ` 326` ``` shows "x \ cball 0 e \ norm x \ e" ``` himmelma@33175 ` 327` ``` by (simp add: dist_norm) ``` himmelma@33175 ` 328` himmelma@33175 ` 329` ```lemma centre_in_cball[simp]: "x \ cball x e \ 0\ e" by simp ``` himmelma@33175 ` 330` ```lemma ball_subset_cball[simp,intro]: "ball x e \ cball x e" by (simp add: subset_eq) ``` himmelma@33175 ` 331` ```lemma subset_ball[intro]: "d <= e ==> ball x d \ ball x e" by (simp add: subset_eq) ``` himmelma@33175 ` 332` ```lemma subset_cball[intro]: "d <= e ==> cball x d \ cball x e" by (simp add: subset_eq) ``` himmelma@33175 ` 333` ```lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" ``` nipkow@39302 ` 334` ``` by (simp add: set_eq_iff) arith ``` himmelma@33175 ` 335` himmelma@33175 ` 336` ```lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" ``` nipkow@39302 ` 337` ``` by (simp add: set_eq_iff) ``` himmelma@33175 ` 338` himmelma@33175 ` 339` ```lemma diff_less_iff: "(a::real) - b > 0 \ a > b" ``` himmelma@33175 ` 340` ``` "(a::real) - b < 0 \ a < b" ``` himmelma@33175 ` 341` ``` "a - b < c \ a < c +b" "a - b > c \ a > c +b" by arith+ ``` himmelma@33175 ` 342` ```lemma diff_le_iff: "(a::real) - b \ 0 \ a \ b" "(a::real) - b \ 0 \ a \ b" ``` himmelma@33175 ` 343` ``` "a - b \ c \ a \ c +b" "a - b \ c \ a \ c +b" by arith+ ``` himmelma@33175 ` 344` himmelma@33175 ` 345` ```lemma open_ball[intro, simp]: "open (ball x e)" ``` huffman@44170 ` 346` ``` unfolding open_dist ball_def mem_Collect_eq Ball_def ``` himmelma@33175 ` 347` ``` unfolding dist_commute ``` himmelma@33175 ` 348` ``` apply clarify ``` himmelma@33175 ` 349` ``` apply (rule_tac x="e - dist xa x" in exI) ``` himmelma@33175 ` 350` ``` using dist_triangle_alt[where z=x] ``` himmelma@33175 ` 351` ``` apply (clarsimp simp add: diff_less_iff) ``` himmelma@33175 ` 352` ``` apply atomize ``` himmelma@33175 ` 353` ``` apply (erule_tac x="y" in allE) ``` himmelma@33175 ` 354` ``` apply (erule_tac x="xa" in allE) ``` himmelma@33175 ` 355` ``` by arith ``` himmelma@33175 ` 356` himmelma@33175 ` 357` ```lemma centre_in_ball[simp]: "x \ ball x e \ e > 0" by (metis mem_ball dist_self) ``` himmelma@33175 ` 358` ```lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" ``` himmelma@33175 ` 359` ``` unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. ``` himmelma@33175 ` 360` hoelzl@33714 ` 361` ```lemma openE[elim?]: ``` hoelzl@33714 ` 362` ``` assumes "open S" "x\S" ``` hoelzl@33714 ` 363` ``` obtains e where "e>0" "ball x e \ S" ``` hoelzl@33714 ` 364` ``` using assms unfolding open_contains_ball by auto ``` hoelzl@33714 ` 365` himmelma@33175 ` 366` ```lemma open_contains_ball_eq: "open S \ \x. x\S \ (\e>0. ball x e \ S)" ``` himmelma@33175 ` 367` ``` by (metis open_contains_ball subset_eq centre_in_ball) ``` himmelma@33175 ` 368` himmelma@33175 ` 369` ```lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" ``` nipkow@39302 ` 370` ``` unfolding mem_ball set_eq_iff ``` himmelma@33175 ` 371` ``` apply (simp add: not_less) ``` himmelma@33175 ` 372` ``` by (metis zero_le_dist order_trans dist_self) ``` himmelma@33175 ` 373` himmelma@33175 ` 374` ```lemma ball_empty[intro]: "e \ 0 ==> ball x e = {}" by simp ``` himmelma@33175 ` 375` himmelma@33175 ` 376` himmelma@33175 ` 377` ```subsection{* Connectedness *} ``` himmelma@33175 ` 378` himmelma@33175 ` 379` ```definition "connected S \ ``` himmelma@33175 ` 380` ``` ~(\e1 e2. open e1 \ open e2 \ S \ (e1 \ e2) \ (e1 \ e2 \ S = {}) ``` himmelma@33175 ` 381` ``` \ ~(e1 \ S = {}) \ ~(e2 \ S = {}))" ``` himmelma@33175 ` 382` himmelma@33175 ` 383` ```lemma connected_local: ``` himmelma@33175 ` 384` ``` "connected S \ ~(\e1 e2. ``` himmelma@33175 ` 385` ``` openin (subtopology euclidean S) e1 \ ``` himmelma@33175 ` 386` ``` openin (subtopology euclidean S) e2 \ ``` himmelma@33175 ` 387` ``` S \ e1 \ e2 \ ``` himmelma@33175 ` 388` ``` e1 \ e2 = {} \ ``` himmelma@33175 ` 389` ``` ~(e1 = {}) \ ``` himmelma@33175 ` 390` ``` ~(e2 = {}))" ``` himmelma@33175 ` 391` ```unfolding connected_def openin_open by (safe, blast+) ``` himmelma@33175 ` 392` huffman@34105 ` 393` ```lemma exists_diff: ``` huffman@34105 ` 394` ``` fixes P :: "'a set \ bool" ``` huffman@34105 ` 395` ``` shows "(\S. P(- S)) \ (\S. P S)" (is "?lhs \ ?rhs") ``` himmelma@33175 ` 396` ```proof- ``` himmelma@33175 ` 397` ``` {assume "?lhs" hence ?rhs by blast } ``` himmelma@33175 ` 398` ``` moreover ``` himmelma@33175 ` 399` ``` {fix S assume H: "P S" ``` huffman@34105 ` 400` ``` have "S = - (- S)" by auto ``` huffman@34105 ` 401` ``` with H have "P (- (- S))" by metis } ``` himmelma@33175 ` 402` ``` ultimately show ?thesis by metis ``` himmelma@33175 ` 403` ```qed ``` himmelma@33175 ` 404` himmelma@33175 ` 405` ```lemma connected_clopen: "connected S \ ``` himmelma@33175 ` 406` ``` (\T. openin (subtopology euclidean S) T \ ``` himmelma@33175 ` 407` ``` closedin (subtopology euclidean S) T \ T = {} \ T = S)" (is "?lhs \ ?rhs") ``` himmelma@33175 ` 408` ```proof- ``` huffman@34105 ` 409` ``` have " \ connected S \ (\e1 e2. open e1 \ open (- e2) \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" ``` himmelma@33175 ` 410` ``` unfolding connected_def openin_open closedin_closed ``` himmelma@33175 ` 411` ``` apply (subst exists_diff) by blast ``` huffman@34105 ` 412` ``` hence th0: "connected S \ \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" ``` huffman@34105 ` 413` ``` (is " _ \ \ (\e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis ``` himmelma@33175 ` 414` himmelma@33175 ` 415` ``` have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))" ``` himmelma@33175 ` 416` ``` (is "_ \ \ (\t' t. ?Q t' t)") ``` himmelma@33175 ` 417` ``` unfolding connected_def openin_open closedin_closed by auto ``` himmelma@33175 ` 418` ``` {fix e2 ``` himmelma@33175 ` 419` ``` {fix e1 have "?P e2 e1 \ (\t. closed e2 \ t = S\e2 \ open e1 \ t = S\e1 \ t\{} \ t\S)" ``` himmelma@33175 ` 420` ``` by auto} ``` himmelma@33175 ` 421` ``` then have "(\e1. ?P e2 e1) \ (\t. ?Q e2 t)" by metis} ``` himmelma@33175 ` 422` ``` then have "\e2. (\e1. ?P e2 e1) \ (\t. ?Q e2 t)" by blast ``` himmelma@33175 ` 423` ``` then show ?thesis unfolding th0 th1 by simp ``` himmelma@33175 ` 424` ```qed ``` himmelma@33175 ` 425` himmelma@33175 ` 426` ```lemma connected_empty[simp, intro]: "connected {}" ``` himmelma@33175 ` 427` ``` by (simp add: connected_def) ``` himmelma@33175 ` 428` huffman@44210 ` 429` himmelma@33175 ` 430` ```subsection{* Limit points *} ``` himmelma@33175 ` 431` huffman@44207 ` 432` ```definition (in topological_space) ``` huffman@44207 ` 433` ``` islimpt:: "'a \ 'a set \ bool" (infixr "islimpt" 60) where ``` himmelma@33175 ` 434` ``` "x islimpt S \ (\T. x\T \ open T \ (\y\S. y\T \ y\x))" ``` himmelma@33175 ` 435` himmelma@33175 ` 436` ```lemma islimptI: ``` himmelma@33175 ` 437` ``` assumes "\T. x \ T \ open T \ \y\S. y \ T \ y \ x" ``` himmelma@33175 ` 438` ``` shows "x islimpt S" ``` himmelma@33175 ` 439` ``` using assms unfolding islimpt_def by auto ``` himmelma@33175 ` 440` himmelma@33175 ` 441` ```lemma islimptE: ``` himmelma@33175 ` 442` ``` assumes "x islimpt S" and "x \ T" and "open T" ``` himmelma@33175 ` 443` ``` obtains y where "y \ S" and "y \ T" and "y \ x" ``` himmelma@33175 ` 444` ``` using assms unfolding islimpt_def by auto ``` himmelma@33175 ` 445` huffman@44584 ` 446` ```lemma islimpt_iff_eventually: "x islimpt S \ \ eventually (\y. y \ S) (at x)" ``` huffman@44584 ` 447` ``` unfolding islimpt_def eventually_at_topological by auto ``` huffman@44584 ` 448` huffman@44584 ` 449` ```lemma islimpt_subset: "\x islimpt S; S \ T\ \ x islimpt T" ``` huffman@44584 ` 450` ``` unfolding islimpt_def by fast ``` himmelma@33175 ` 451` himmelma@33175 ` 452` ```lemma islimpt_approachable: ``` himmelma@33175 ` 453` ``` fixes x :: "'a::metric_space" ``` himmelma@33175 ` 454` ``` shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" ``` huffman@44584 ` 455` ``` unfolding islimpt_iff_eventually eventually_at by fast ``` himmelma@33175 ` 456` himmelma@33175 ` 457` ```lemma islimpt_approachable_le: ``` himmelma@33175 ` 458` ``` fixes x :: "'a::metric_space" ``` himmelma@33175 ` 459` ``` shows "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x <= e)" ``` himmelma@33175 ` 460` ``` unfolding islimpt_approachable ``` huffman@44584 ` 461` ``` using approachable_lt_le [where f="\y. dist y x" and P="\y. y \ S \ y = x", ``` huffman@44584 ` 462` ``` THEN arg_cong [where f=Not]] ``` huffman@44584 ` 463` ``` by (simp add: Bex_def conj_commute conj_left_commute) ``` himmelma@33175 ` 464` huffman@44571 ` 465` ```lemma islimpt_UNIV_iff: "x islimpt UNIV \ \ open {x}" ``` huffman@44571 ` 466` ``` unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast) ``` huffman@44571 ` 467` huffman@44210 ` 468` ```text {* A perfect space has no isolated points. *} ``` huffman@44210 ` 469` huffman@44571 ` 470` ```lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV" ``` huffman@44571 ` 471` ``` unfolding islimpt_UNIV_iff by (rule not_open_singleton) ``` himmelma@33175 ` 472` himmelma@33175 ` 473` ```lemma perfect_choose_dist: ``` huffman@44072 ` 474` ``` fixes x :: "'a::{perfect_space, metric_space}" ``` himmelma@33175 ` 475` ``` shows "0 < r \ \a. a \ x \ dist a x < r" ``` himmelma@33175 ` 476` ```using islimpt_UNIV [of x] ``` himmelma@33175 ` 477` ```by (simp add: islimpt_approachable) ``` himmelma@33175 ` 478` himmelma@33175 ` 479` ```lemma closed_limpt: "closed S \ (\x. x islimpt S \ x \ S)" ``` himmelma@33175 ` 480` ``` unfolding closed_def ``` himmelma@33175 ` 481` ``` apply (subst open_subopen) ``` huffman@34105 ` 482` ``` apply (simp add: islimpt_def subset_eq) ``` huffman@44170 ` 483` ``` by (metis ComplE ComplI) ``` himmelma@33175 ` 484` himmelma@33175 ` 485` ```lemma islimpt_EMPTY[simp]: "\ x islimpt {}" ``` himmelma@33175 ` 486` ``` unfolding islimpt_def by auto ``` himmelma@33175 ` 487` himmelma@33175 ` 488` ```lemma finite_set_avoid: ``` himmelma@33175 ` 489` ``` fixes a :: "'a::metric_space" ``` himmelma@33175 ` 490` ``` assumes fS: "finite S" shows "\d>0. \x\S. x \ a \ d <= dist a x" ``` himmelma@33175 ` 491` ```proof(induct rule: finite_induct[OF fS]) ``` boehmes@41863 ` 492` ``` case 1 thus ?case by (auto intro: zero_less_one) ``` himmelma@33175 ` 493` ```next ``` himmelma@33175 ` 494` ``` case (2 x F) ``` himmelma@33175 ` 495` ``` from 2 obtain d where d: "d >0" "\x\F. x\a \ d \ dist a x" by blast ``` himmelma@33175 ` 496` ``` {assume "x = a" hence ?case using d by auto } ``` himmelma@33175 ` 497` ``` moreover ``` himmelma@33175 ` 498` ``` {assume xa: "x\a" ``` himmelma@33175 ` 499` ``` let ?d = "min d (dist a x)" ``` himmelma@33175 ` 500` ``` have dp: "?d > 0" using xa d(1) using dist_nz by auto ``` himmelma@33175 ` 501` ``` from d have d': "\x\F. x\a \ ?d \ dist a x" by auto ``` himmelma@33175 ` 502` ``` with dp xa have ?case by(auto intro!: exI[where x="?d"]) } ``` himmelma@33175 ` 503` ``` ultimately show ?case by blast ``` himmelma@33175 ` 504` ```qed ``` himmelma@33175 ` 505` himmelma@33175 ` 506` ```lemma islimpt_finite: ``` himmelma@33175 ` 507` ``` fixes S :: "'a::metric_space set" ``` himmelma@33175 ` 508` ``` assumes fS: "finite S" shows "\ a islimpt S" ``` himmelma@33175 ` 509` ``` unfolding islimpt_approachable ``` himmelma@33175 ` 510` ``` using finite_set_avoid[OF fS, of a] by (metis dist_commute not_le) ``` himmelma@33175 ` 511` himmelma@33175 ` 512` ```lemma islimpt_Un: "x islimpt (S \ T) \ x islimpt S \ x islimpt T" ``` himmelma@33175 ` 513` ``` apply (rule iffI) ``` himmelma@33175 ` 514` ``` defer ``` himmelma@33175 ` 515` ``` apply (metis Un_upper1 Un_upper2 islimpt_subset) ``` himmelma@33175 ` 516` ``` unfolding islimpt_def ``` himmelma@33175 ` 517` ``` apply (rule ccontr, clarsimp, rename_tac A B) ``` himmelma@33175 ` 518` ``` apply (drule_tac x="A \ B" in spec) ``` himmelma@33175 ` 519` ``` apply (auto simp add: open_Int) ``` himmelma@33175 ` 520` ``` done ``` himmelma@33175 ` 521` himmelma@33175 ` 522` ```lemma discrete_imp_closed: ``` himmelma@33175 ` 523` ``` fixes S :: "'a::metric_space set" ``` himmelma@33175 ` 524` ``` assumes e: "0 < e" and d: "\x \ S. \y \ S. dist y x < e \ y = x" ``` himmelma@33175 ` 525` ``` shows "closed S" ``` himmelma@33175 ` 526` ```proof- ``` himmelma@33175 ` 527` ``` {fix x assume C: "\e>0. \x'\S. x' \ x \ dist x' x < e" ``` himmelma@33175 ` 528` ``` from e have e2: "e/2 > 0" by arith ``` himmelma@33175 ` 529` ``` from C[rule_format, OF e2] obtain y where y: "y \ S" "y\x" "dist y x < e/2" by blast ``` himmelma@33175 ` 530` ``` let ?m = "min (e/2) (dist x y) " ``` himmelma@33175 ` 531` ``` from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym]) ``` himmelma@33175 ` 532` ``` from C[rule_format, OF mp] obtain z where z: "z \ S" "z\x" "dist z x < ?m" by blast ``` himmelma@33175 ` 533` ``` have th: "dist z y < e" using z y ``` himmelma@33175 ` 534` ``` by (intro dist_triangle_lt [where z=x], simp) ``` himmelma@33175 ` 535` ``` from d[rule_format, OF y(1) z(1) th] y z ``` himmelma@33175 ` 536` ``` have False by (auto simp add: dist_commute)} ``` himmelma@33175 ` 537` ``` then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) ``` himmelma@33175 ` 538` ```qed ``` himmelma@33175 ` 539` huffman@44210 ` 540` huffman@44210 ` 541` ```subsection {* Interior of a Set *} ``` huffman@44210 ` 542` huffman@44519 ` 543` ```definition "interior S = \{T. open T \ T \ S}" ``` huffman@44519 ` 544` huffman@44519 ` 545` ```lemma interiorI [intro?]: ``` huffman@44519 ` 546` ``` assumes "open T" and "x \ T" and "T \ S" ``` huffman@44519 ` 547` ``` shows "x \ interior S" ``` huffman@44519 ` 548` ``` using assms unfolding interior_def by fast ``` huffman@44519 ` 549` huffman@44519 ` 550` ```lemma interiorE [elim?]: ``` huffman@44519 ` 551` ``` assumes "x \ interior S" ``` huffman@44519 ` 552` ``` obtains T where "open T" and "x \ T" and "T \ S" ``` huffman@44519 ` 553` ``` using assms unfolding interior_def by fast ``` huffman@44519 ` 554` huffman@44519 ` 555` ```lemma open_interior [simp, intro]: "open (interior S)" ``` huffman@44519 ` 556` ``` by (simp add: interior_def open_Union) ``` huffman@44519 ` 557` huffman@44519 ` 558` ```lemma interior_subset: "interior S \ S" ``` huffman@44519 ` 559` ``` by (auto simp add: interior_def) ``` huffman@44519 ` 560` huffman@44519 ` 561` ```lemma interior_maximal: "T \ S \ open T \ T \ interior S" ``` huffman@44519 ` 562` ``` by (auto simp add: interior_def) ``` huffman@44519 ` 563` huffman@44519 ` 564` ```lemma interior_open: "open S \ interior S = S" ``` huffman@44519 ` 565` ``` by (intro equalityI interior_subset interior_maximal subset_refl) ``` himmelma@33175 ` 566` himmelma@33175 ` 567` ```lemma interior_eq: "interior S = S \ open S" ``` huffman@44519 ` 568` ``` by (metis open_interior interior_open) ``` huffman@44519 ` 569` huffman@44519 ` 570` ```lemma open_subset_interior: "open S \ S \ interior T \ S \ T" ``` himmelma@33175 ` 571` ``` by (metis interior_maximal interior_subset subset_trans) ``` himmelma@33175 ` 572` huffman@44519 ` 573` ```lemma interior_empty [simp]: "interior {} = {}" ``` huffman@44519 ` 574` ``` using open_empty by (rule interior_open) ``` huffman@44519 ` 575` huffman@44522 ` 576` ```lemma interior_UNIV [simp]: "interior UNIV = UNIV" ``` huffman@44522 ` 577` ``` using open_UNIV by (rule interior_open) ``` huffman@44522 ` 578` huffman@44519 ` 579` ```lemma interior_interior [simp]: "interior (interior S) = interior S" ``` huffman@44519 ` 580` ``` using open_interior by (rule interior_open) ``` huffman@44519 ` 581` huffman@44522 ` 582` ```lemma interior_mono: "S \ T \ interior S \ interior T" ``` huffman@44522 ` 583` ``` by (auto simp add: interior_def) ``` huffman@44519 ` 584` huffman@44519 ` 585` ```lemma interior_unique: ``` huffman@44519 ` 586` ``` assumes "T \ S" and "open T" ``` huffman@44519 ` 587` ``` assumes "\T'. T' \ S \ open T' \ T' \ T" ``` huffman@44519 ` 588` ``` shows "interior S = T" ``` huffman@44519 ` 589` ``` by (intro equalityI assms interior_subset open_interior interior_maximal) ``` huffman@44519 ` 590` huffman@44519 ` 591` ```lemma interior_inter [simp]: "interior (S \ T) = interior S \ interior T" ``` huffman@44522 ` 592` ``` by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1 ``` huffman@44519 ` 593` ``` Int_lower2 interior_maximal interior_subset open_Int open_interior) ``` huffman@44519 ` 594` huffman@44519 ` 595` ```lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" ``` huffman@44519 ` 596` ``` using open_contains_ball_eq [where S="interior S"] ``` huffman@44519 ` 597` ``` by (simp add: open_subset_interior) ``` himmelma@33175 ` 598` himmelma@33175 ` 599` ```lemma interior_limit_point [intro]: ``` himmelma@33175 ` 600` ``` fixes x :: "'a::perfect_space" ``` himmelma@33175 ` 601` ``` assumes x: "x \ interior S" shows "x islimpt S" ``` huffman@44072 ` 602` ``` using x islimpt_UNIV [of x] ``` huffman@44072 ` 603` ``` unfolding interior_def islimpt_def ``` huffman@44072 ` 604` ``` apply (clarsimp, rename_tac T T') ``` huffman@44072 ` 605` ``` apply (drule_tac x="T \ T'" in spec) ``` huffman@44072 ` 606` ``` apply (auto simp add: open_Int) ``` huffman@44072 ` 607` ``` done ``` himmelma@33175 ` 608` himmelma@33175 ` 609` ```lemma interior_closed_Un_empty_interior: ``` himmelma@33175 ` 610` ``` assumes cS: "closed S" and iT: "interior T = {}" ``` huffman@44519 ` 611` ``` shows "interior (S \ T) = interior S" ``` himmelma@33175 ` 612` ```proof ``` huffman@44519 ` 613` ``` show "interior S \ interior (S \ T)" ``` huffman@44522 ` 614` ``` by (rule interior_mono, rule Un_upper1) ``` himmelma@33175 ` 615` ```next ``` himmelma@33175 ` 616` ``` show "interior (S \ T) \ interior S" ``` himmelma@33175 ` 617` ``` proof ``` himmelma@33175 ` 618` ``` fix x assume "x \ interior (S \ T)" ``` huffman@44519 ` 619` ``` then obtain R where "open R" "x \ R" "R \ S \ T" .. ``` himmelma@33175 ` 620` ``` show "x \ interior S" ``` himmelma@33175 ` 621` ``` proof (rule ccontr) ``` himmelma@33175 ` 622` ``` assume "x \ interior S" ``` himmelma@33175 ` 623` ``` with `x \ R` `open R` obtain y where "y \ R - S" ``` huffman@44519 ` 624` ``` unfolding interior_def by fast ``` himmelma@33175 ` 625` ``` from `open R` `closed S` have "open (R - S)" by (rule open_Diff) ``` himmelma@33175 ` 626` ``` from `R \ S \ T` have "R - S \ T" by fast ``` himmelma@33175 ` 627` ``` from `y \ R - S` `open (R - S)` `R - S \ T` `interior T = {}` ``` himmelma@33175 ` 628` ``` show "False" unfolding interior_def by fast ``` himmelma@33175 ` 629` ``` qed ``` himmelma@33175 ` 630` ``` qed ``` himmelma@33175 ` 631` ```qed ``` himmelma@33175 ` 632` huffman@44365 ` 633` ```lemma interior_Times: "interior (A \ B) = interior A \ interior B" ``` huffman@44365 ` 634` ```proof (rule interior_unique) ``` huffman@44365 ` 635` ``` show "interior A \ interior B \ A \ B" ``` huffman@44365 ` 636` ``` by (intro Sigma_mono interior_subset) ``` huffman@44365 ` 637` ``` show "open (interior A \ interior B)" ``` huffman@44365 ` 638` ``` by (intro open_Times open_interior) ``` huffman@44519 ` 639` ``` fix T assume "T \ A \ B" and "open T" thus "T \ interior A \ interior B" ``` huffman@44519 ` 640` ``` proof (safe) ``` huffman@44519 ` 641` ``` fix x y assume "(x, y) \ T" ``` huffman@44519 ` 642` ``` then obtain C D where "open C" "open D" "C \ D \ T" "x \ C" "y \ D" ``` huffman@44519 ` 643` ``` using `open T` unfolding open_prod_def by fast ``` huffman@44519 ` 644` ``` hence "open C" "open D" "C \ A" "D \ B" "x \ C" "y \ D" ``` huffman@44519 ` 645` ``` using `T \ A \ B` by auto ``` huffman@44519 ` 646` ``` thus "x \ interior A" and "y \ interior B" ``` huffman@44519 ` 647` ``` by (auto intro: interiorI) ``` huffman@44519 ` 648` ``` qed ``` huffman@44365 ` 649` ```qed ``` huffman@44365 ` 650` himmelma@33175 ` 651` huffman@44210 ` 652` ```subsection {* Closure of a Set *} ``` himmelma@33175 ` 653` himmelma@33175 ` 654` ```definition "closure S = S \ {x | x. x islimpt S}" ``` himmelma@33175 ` 655` huffman@44518 ` 656` ```lemma interior_closure: "interior S = - (closure (- S))" ``` huffman@44518 ` 657` ``` unfolding interior_def closure_def islimpt_def by auto ``` huffman@44518 ` 658` huffman@34105 ` 659` ```lemma closure_interior: "closure S = - interior (- S)" ``` huffman@44518 ` 660` ``` unfolding interior_closure by simp ``` himmelma@33175 ` 661` himmelma@33175 ` 662` ```lemma closed_closure[simp, intro]: "closed (closure S)" ``` huffman@44518 ` 663` ``` unfolding closure_interior by (simp add: closed_Compl) ``` huffman@44518 ` 664` huffman@44518 ` 665` ```lemma closure_subset: "S \ closure S" ``` huffman@44518 ` 666` ``` unfolding closure_def by simp ``` himmelma@33175 ` 667` himmelma@33175 ` 668` ```lemma closure_hull: "closure S = closed hull S" ``` huffman@44519 ` 669` ``` unfolding hull_def closure_interior interior_def by auto ``` himmelma@33175 ` 670` himmelma@33175 ` 671` ```lemma closure_eq: "closure S = S \ closed S" ``` huffman@44519 ` 672` ``` unfolding closure_hull using closed_Inter by (rule hull_eq) ``` huffman@44519 ` 673` huffman@44519 ` 674` ```lemma closure_closed [simp]: "closed S \ closure S = S" ``` huffman@44519 ` 675` ``` unfolding closure_eq . ``` huffman@44519 ` 676` huffman@44519 ` 677` ```lemma closure_closure [simp]: "closure (closure S) = closure S" ``` huffman@44518 ` 678` ``` unfolding closure_hull by (rule hull_hull) ``` himmelma@33175 ` 679` huffman@44522 ` 680` ```lemma closure_mono: "S \ T \ closure S \ closure T" ``` huffman@44518 ` 681` ``` unfolding closure_hull by (rule hull_mono) ``` himmelma@33175 ` 682` huffman@44519 ` 683` ```lemma closure_minimal: "S \ T \ closed T \ closure S \ T" ``` huffman@44518 ` 684` ``` unfolding closure_hull by (rule hull_minimal) ``` himmelma@33175 ` 685` huffman@44519 ` 686` ```lemma closure_unique: ``` huffman@44519 ` 687` ``` assumes "S \ T" and "closed T" ``` huffman@44519 ` 688` ``` assumes "\T'. S \ T' \ closed T' \ T \ T'" ``` huffman@44519 ` 689` ``` shows "closure S = T" ``` huffman@44519 ` 690` ``` using assms unfolding closure_hull by (rule hull_unique) ``` huffman@44519 ` 691` huffman@44519 ` 692` ```lemma closure_empty [simp]: "closure {} = {}" ``` huffman@44518 ` 693` ``` using closed_empty by (rule closure_closed) ``` himmelma@33175 ` 694` huffman@44522 ` 695` ```lemma closure_UNIV [simp]: "closure UNIV = UNIV" ``` huffman@44518 ` 696` ``` using closed_UNIV by (rule closure_closed) ``` huffman@44518 ` 697` huffman@44518 ` 698` ```lemma closure_union [simp]: "closure (S \ T) = closure S \ closure T" ``` huffman@44518 ` 699` ``` unfolding closure_interior by simp ``` himmelma@33175 ` 700` himmelma@33175 ` 701` ```lemma closure_eq_empty: "closure S = {} \ S = {}" ``` himmelma@33175 ` 702` ``` using closure_empty closure_subset[of S] ``` himmelma@33175 ` 703` ``` by blast ``` himmelma@33175 ` 704` himmelma@33175 ` 705` ```lemma closure_subset_eq: "closure S \ S \ closed S" ``` himmelma@33175 ` 706` ``` using closure_eq[of S] closure_subset[of S] ``` himmelma@33175 ` 707` ``` by simp ``` himmelma@33175 ` 708` himmelma@33175 ` 709` ```lemma open_inter_closure_eq_empty: ``` himmelma@33175 ` 710` ``` "open S \ (S \ closure T) = {} \ S \ T = {}" ``` huffman@34105 ` 711` ``` using open_subset_interior[of S "- T"] ``` huffman@34105 ` 712` ``` using interior_subset[of "- T"] ``` himmelma@33175 ` 713` ``` unfolding closure_interior ``` himmelma@33175 ` 714` ``` by auto ``` himmelma@33175 ` 715` himmelma@33175 ` 716` ```lemma open_inter_closure_subset: ``` himmelma@33175 ` 717` ``` "open S \ (S \ (closure T)) \ closure(S \ T)" ``` himmelma@33175 ` 718` ```proof ``` himmelma@33175 ` 719` ``` fix x ``` himmelma@33175 ` 720` ``` assume as: "open S" "x \ S \ closure T" ``` himmelma@33175 ` 721` ``` { assume *:"x islimpt T" ``` himmelma@33175 ` 722` ``` have "x islimpt (S \ T)" ``` himmelma@33175 ` 723` ``` proof (rule islimptI) ``` himmelma@33175 ` 724` ``` fix A ``` himmelma@33175 ` 725` ``` assume "x \ A" "open A" ``` himmelma@33175 ` 726` ``` with as have "x \ A \ S" "open (A \ S)" ``` himmelma@33175 ` 727` ``` by (simp_all add: open_Int) ``` himmelma@33175 ` 728` ``` with * obtain y where "y \ T" "y \ A \ S" "y \ x" ``` himmelma@33175 ` 729` ``` by (rule islimptE) ``` himmelma@33175 ` 730` ``` hence "y \ S \ T" "y \ A \ y \ x" ``` himmelma@33175 ` 731` ``` by simp_all ``` himmelma@33175 ` 732` ``` thus "\y\(S \ T). y \ A \ y \ x" .. ``` himmelma@33175 ` 733` ``` qed ``` himmelma@33175 ` 734` ``` } ``` himmelma@33175 ` 735` ``` then show "x \ closure (S \ T)" using as ``` himmelma@33175 ` 736` ``` unfolding closure_def ``` himmelma@33175 ` 737` ``` by blast ``` himmelma@33175 ` 738` ```qed ``` himmelma@33175 ` 739` huffman@44519 ` 740` ```lemma closure_complement: "closure (- S) = - interior S" ``` huffman@44518 ` 741` ``` unfolding closure_interior by simp ``` himmelma@33175 ` 742` huffman@44519 ` 743` ```lemma interior_complement: "interior (- S) = - closure S" ``` huffman@44518 ` 744` ``` unfolding closure_interior by simp ``` himmelma@33175 ` 745` huffman@44365 ` 746` ```lemma closure_Times: "closure (A \ B) = closure A \ closure B" ``` huffman@44519 ` 747` ```proof (rule closure_unique) ``` huffman@44365 ` 748` ``` show "A \ B \ closure A \ closure B" ``` huffman@44365 ` 749` ``` by (intro Sigma_mono closure_subset) ``` huffman@44365 ` 750` ``` show "closed (closure A \ closure B)" ``` huffman@44365 ` 751` ``` by (intro closed_Times closed_closure) ``` huffman@44519 ` 752` ``` fix T assume "A \ B \ T" and "closed T" thus "closure A \ closure B \ T" ``` huffman@44365 ` 753` ``` apply (simp add: closed_def open_prod_def, clarify) ``` huffman@44365 ` 754` ``` apply (rule ccontr) ``` huffman@44365 ` 755` ``` apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D) ``` huffman@44365 ` 756` ``` apply (simp add: closure_interior interior_def) ``` huffman@44365 ` 757` ``` apply (drule_tac x=C in spec) ``` huffman@44365 ` 758` ``` apply (drule_tac x=D in spec) ``` huffman@44365 ` 759` ``` apply auto ``` huffman@44365 ` 760` ``` done ``` huffman@44365 ` 761` ```qed ``` huffman@44365 ` 762` huffman@44210 ` 763` huffman@44210 ` 764` ```subsection {* Frontier (aka boundary) *} ``` himmelma@33175 ` 765` himmelma@33175 ` 766` ```definition "frontier S = closure S - interior S" ``` himmelma@33175 ` 767` himmelma@33175 ` 768` ```lemma frontier_closed: "closed(frontier S)" ``` himmelma@33175 ` 769` ``` by (simp add: frontier_def closed_Diff) ``` himmelma@33175 ` 770` huffman@34105 ` 771` ```lemma frontier_closures: "frontier S = (closure S) \ (closure(- S))" ``` himmelma@33175 ` 772` ``` by (auto simp add: frontier_def interior_closure) ``` himmelma@33175 ` 773` himmelma@33175 ` 774` ```lemma frontier_straddle: ``` himmelma@33175 ` 775` ``` fixes a :: "'a::metric_space" ``` himmelma@33175 ` 776` ``` shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" (is "?lhs \ ?rhs") ``` himmelma@33175 ` 777` ```proof ``` himmelma@33175 ` 778` ``` assume "?lhs" ``` himmelma@33175 ` 779` ``` { fix e::real ``` himmelma@33175 ` 780` ``` assume "e > 0" ``` himmelma@33175 ` 781` ``` let ?rhse = "(\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e)" ``` himmelma@33175 ` 782` ``` { assume "a\S" ``` himmelma@33175 ` 783` ``` have "\x\S. dist a x < e" using `e>0` `a\S` by(rule_tac x=a in bexI) auto ``` himmelma@33175 ` 784` ``` moreover have "\x. x \ S \ dist a x < e" using `?lhs` `a\S` ``` himmelma@33175 ` 785` ``` unfolding frontier_closures closure_def islimpt_def using `e>0` ``` himmelma@33175 ` 786` ``` by (auto, erule_tac x="ball a e" in allE, auto) ``` himmelma@33175 ` 787` ``` ultimately have ?rhse by auto ``` himmelma@33175 ` 788` ``` } ``` himmelma@33175 ` 789` ``` moreover ``` himmelma@33175 ` 790` ``` { assume "a\S" ``` himmelma@33175 ` 791` ``` hence ?rhse using `?lhs` ``` himmelma@33175 ` 792` ``` unfolding frontier_closures closure_def islimpt_def ``` himmelma@33175 ` 793` ``` using open_ball[of a e] `e > 0` ``` paulson@33324 ` 794` ``` by simp (metis centre_in_ball mem_ball open_ball) ``` himmelma@33175 ` 795` ``` } ``` himmelma@33175 ` 796` ``` ultimately have ?rhse by auto ``` himmelma@33175 ` 797` ``` } ``` himmelma@33175 ` 798` ``` thus ?rhs by auto ``` himmelma@33175 ` 799` ```next ``` himmelma@33175 ` 800` ``` assume ?rhs ``` himmelma@33175 ` 801` ``` moreover ``` himmelma@33175 ` 802` ``` { fix T assume "a\S" and ``` himmelma@33175 ` 803` ``` as:"\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e)" "a \ S" "a \ T" "open T" ``` himmelma@33175 ` 804` ``` from `open T` `a \ T` have "\e>0. ball a e \ T" unfolding open_contains_ball[of T] by auto ``` himmelma@33175 ` 805` ``` then obtain e where "e>0" "ball a e \ T" by auto ``` himmelma@33175 ` 806` ``` then obtain y where y:"y\S" "dist a y < e" using as(1) by auto ``` himmelma@33175 ` 807` ``` have "\y\S. y \ T \ y \ a" ``` himmelma@33175 ` 808` ``` using `dist a y < e` `ball a e \ T` unfolding ball_def using `y\S` `a\S` by auto ``` himmelma@33175 ` 809` ``` } ``` himmelma@33175 ` 810` ``` hence "a \ closure S" unfolding closure_def islimpt_def using `?rhs` by auto ``` himmelma@33175 ` 811` ``` moreover ``` himmelma@33175 ` 812` ``` { fix T assume "a \ T" "open T" "a\S" ``` himmelma@33175 ` 813` ``` then obtain e where "e>0" and balle: "ball a e \ T" unfolding open_contains_ball using `?rhs` by auto ``` himmelma@33175 ` 814` ``` obtain x where "x \ S" "dist a x < e" using `?rhs` using `e>0` by auto ``` huffman@34105 ` 815` ``` hence "\y\- S. y \ T \ y \ a" using balle `a\S` unfolding ball_def by (rule_tac x=x in bexI)auto ``` himmelma@33175 ` 816` ``` } ``` huffman@34105 ` 817` ``` hence "a islimpt (- S) \ a\S" unfolding islimpt_def by auto ``` huffman@34105 ` 818` ``` ultimately show ?lhs unfolding frontier_closures using closure_def[of "- S"] by auto ``` himmelma@33175 ` 819` ```qed ``` himmelma@33175 ` 820` himmelma@33175 ` 821` ```lemma frontier_subset_closed: "closed S \ frontier S \ S" ``` himmelma@33175 ` 822` ``` by (metis frontier_def closure_closed Diff_subset) ``` himmelma@33175 ` 823` hoelzl@34964 ` 824` ```lemma frontier_empty[simp]: "frontier {} = {}" ``` huffman@36362 ` 825` ``` by (simp add: frontier_def) ``` himmelma@33175 ` 826` himmelma@33175 ` 827` ```lemma frontier_subset_eq: "frontier S \ S \ closed S" ``` himmelma@33175 ` 828` ```proof- ``` himmelma@33175 ` 829` ``` { assume "frontier S \ S" ``` himmelma@33175 ` 830` ``` hence "closure S \ S" using interior_subset unfolding frontier_def by auto ``` himmelma@33175 ` 831` ``` hence "closed S" using closure_subset_eq by auto ``` himmelma@33175 ` 832` ``` } ``` huffman@36362 ` 833` ``` thus ?thesis using frontier_subset_closed[of S] .. ``` himmelma@33175 ` 834` ```qed ``` himmelma@33175 ` 835` huffman@34105 ` 836` ```lemma frontier_complement: "frontier(- S) = frontier S" ``` himmelma@33175 ` 837` ``` by (auto simp add: frontier_def closure_complement interior_complement) ``` himmelma@33175 ` 838` himmelma@33175 ` 839` ```lemma frontier_disjoint_eq: "frontier S \ S = {} \ open S" ``` huffman@34105 ` 840` ``` using frontier_complement frontier_subset_eq[of "- S"] ``` huffman@34105 ` 841` ``` unfolding open_closed by auto ``` himmelma@33175 ` 842` huffman@44210 ` 843` huffman@44081 ` 844` ```subsection {* Filters and the ``eventually true'' quantifier *} ``` huffman@44081 ` 845` himmelma@33175 ` 846` ```definition ``` huffman@44081 ` 847` ``` at_infinity :: "'a::real_normed_vector filter" where ``` huffman@44081 ` 848` ``` "at_infinity = Abs_filter (\P. \r. \x. r \ norm x \ P x)" ``` himmelma@33175 ` 849` himmelma@33175 ` 850` ```definition ``` huffman@44081 ` 851` ``` indirection :: "'a::real_normed_vector \ 'a \ 'a filter" ``` huffman@44081 ` 852` ``` (infixr "indirection" 70) where ``` himmelma@33175 ` 853` ``` "a indirection v = (at a) within {b. \c\0. b - a = scaleR c v}" ``` himmelma@33175 ` 854` huffman@44081 ` 855` ```text{* Prove That They are all filters. *} ``` himmelma@33175 ` 856` huffman@36358 ` 857` ```lemma eventually_at_infinity: ``` huffman@36358 ` 858` ``` "eventually P at_infinity \ (\b. \x. norm x >= b \ P x)" ``` himmelma@33175 ` 859` ```unfolding at_infinity_def ``` huffman@44081 ` 860` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@36358 ` 861` ``` fix P Q :: "'a \ bool" ``` huffman@36358 ` 862` ``` assume "\r. \x. r \ norm x \ P x" and "\s. \x. s \ norm x \ Q x" ``` huffman@36358 ` 863` ``` then obtain r s where ``` huffman@36358 ` 864` ``` "\x. r \ norm x \ P x" and "\x. s \ norm x \ Q x" by auto ``` huffman@36358 ` 865` ``` then have "\x. max r s \ norm x \ P x \ Q x" by simp ``` huffman@36358 ` 866` ``` then show "\r. \x. r \ norm x \ P x \ Q x" .. ``` huffman@36358 ` 867` ```qed auto ``` himmelma@33175 ` 868` huffman@36437 ` 869` ```text {* Identify Trivial limits, where we can't approach arbitrarily closely. *} ``` himmelma@33175 ` 870` himmelma@33175 ` 871` ```lemma trivial_limit_within: ``` himmelma@33175 ` 872` ``` shows "trivial_limit (at a within S) \ \ a islimpt S" ``` himmelma@33175 ` 873` ```proof ``` himmelma@33175 ` 874` ``` assume "trivial_limit (at a within S)" ``` himmelma@33175 ` 875` ``` thus "\ a islimpt S" ``` himmelma@33175 ` 876` ``` unfolding trivial_limit_def ``` huffman@36358 ` 877` ``` unfolding eventually_within eventually_at_topological ``` himmelma@33175 ` 878` ``` unfolding islimpt_def ``` nipkow@39302 ` 879` ``` apply (clarsimp simp add: set_eq_iff) ``` himmelma@33175 ` 880` ``` apply (rename_tac T, rule_tac x=T in exI) ``` huffman@36358 ` 881` ``` apply (clarsimp, drule_tac x=y in bspec, simp_all) ``` himmelma@33175 ` 882` ``` done ``` himmelma@33175 ` 883` ```next ``` himmelma@33175 ` 884` ``` assume "\ a islimpt S" ``` himmelma@33175 ` 885` ``` thus "trivial_limit (at a within S)" ``` himmelma@33175 ` 886` ``` unfolding trivial_limit_def ``` huffman@36358 ` 887` ``` unfolding eventually_within eventually_at_topological ``` himmelma@33175 ` 888` ``` unfolding islimpt_def ``` huffman@36358 ` 889` ``` apply clarsimp ``` huffman@36358 ` 890` ``` apply (rule_tac x=T in exI) ``` huffman@36358 ` 891` ``` apply auto ``` himmelma@33175 ` 892` ``` done ``` himmelma@33175 ` 893` ```qed ``` himmelma@33175 ` 894` himmelma@33175 ` 895` ```lemma trivial_limit_at_iff: "trivial_limit (at a) \ \ a islimpt UNIV" ``` himmelma@33175 ` 896` ``` using trivial_limit_within [of a UNIV] ``` himmelma@33175 ` 897` ``` by (simp add: within_UNIV) ``` himmelma@33175 ` 898` himmelma@33175 ` 899` ```lemma trivial_limit_at: ``` himmelma@33175 ` 900` ``` fixes a :: "'a::perfect_space" ``` himmelma@33175 ` 901` ``` shows "\ trivial_limit (at a)" ``` huffman@44571 ` 902` ``` by (rule at_neq_bot) ``` himmelma@33175 ` 903` himmelma@33175 ` 904` ```lemma trivial_limit_at_infinity: ``` huffman@44081 ` 905` ``` "\ trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)" ``` huffman@36358 ` 906` ``` unfolding trivial_limit_def eventually_at_infinity ``` huffman@36358 ` 907` ``` apply clarsimp ``` huffman@44072 ` 908` ``` apply (subgoal_tac "\x::'a. x \ 0", clarify) ``` huffman@44072 ` 909` ``` apply (rule_tac x="scaleR (b / norm x) x" in exI, simp) ``` huffman@44072 ` 910` ``` apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def]) ``` huffman@44072 ` 911` ``` apply (drule_tac x=UNIV in spec, simp) ``` himmelma@33175 ` 912` ``` done ``` himmelma@33175 ` 913` huffman@36437 ` 914` ```text {* Some property holds "sufficiently close" to the limit point. *} ``` himmelma@33175 ` 915` himmelma@33175 ` 916` ```lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *) ``` himmelma@33175 ` 917` ``` "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" ``` himmelma@33175 ` 918` ```unfolding eventually_at dist_nz by auto ``` himmelma@33175 ` 919` himmelma@33175 ` 920` ```lemma eventually_within: "eventually P (at a within S) \ ``` himmelma@33175 ` 921` ``` (\d>0. \x\S. 0 < dist x a \ dist x a < d \ P x)" ``` himmelma@33175 ` 922` ```unfolding eventually_within eventually_at dist_nz by auto ``` himmelma@33175 ` 923` himmelma@33175 ` 924` ```lemma eventually_within_le: "eventually P (at a within S) \ ``` himmelma@33175 ` 925` ``` (\d>0. \x\S. 0 < dist x a \ dist x a <= d \ P x)" (is "?lhs = ?rhs") ``` himmelma@33175 ` 926` ```unfolding eventually_within ``` paulson@33324 ` 927` ```by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) ``` himmelma@33175 ` 928` himmelma@33175 ` 929` ```lemma eventually_happens: "eventually P net ==> trivial_limit net \ (\x. P x)" ``` huffman@36358 ` 930` ``` unfolding trivial_limit_def ``` huffman@36358 ` 931` ``` by (auto elim: eventually_rev_mp) ``` himmelma@33175 ` 932` himmelma@33175 ` 933` ```lemma trivial_limit_eventually: "trivial_limit net \ eventually P net" ``` huffman@36358 ` 934` ``` unfolding trivial_limit_def by (auto elim: eventually_rev_mp) ``` himmelma@33175 ` 935` himmelma@33175 ` 936` ```lemma trivial_limit_eq: "trivial_limit net \ (\P. eventually P net)" ``` huffman@44342 ` 937` ``` by (simp add: filter_eq_iff) ``` himmelma@33175 ` 938` himmelma@33175 ` 939` ```text{* Combining theorems for "eventually" *} ``` himmelma@33175 ` 940` himmelma@33175 ` 941` ```lemma eventually_rev_mono: ``` himmelma@33175 ` 942` ``` "eventually P net \ (\x. P x \ Q x) \ eventually Q net" ``` himmelma@33175 ` 943` ```using eventually_mono [of P Q] by fast ``` himmelma@33175 ` 944` himmelma@33175 ` 945` ```lemma not_eventually: "(\x. \ P x ) \ ~(trivial_limit net) ==> ~(eventually (\x. P x) net)" ``` himmelma@33175 ` 946` ``` by (simp add: eventually_False) ``` himmelma@33175 ` 947` huffman@44210 ` 948` huffman@36437 ` 949` ```subsection {* Limits *} ``` himmelma@33175 ` 950` huffman@44081 ` 951` ```text{* Notation Lim to avoid collition with lim defined in analysis *} ``` huffman@44081 ` 952` huffman@44081 ` 953` ```definition Lim :: "'a filter \ ('a \ 'b::t2_space) \ 'b" ``` huffman@44081 ` 954` ``` where "Lim A f = (THE l. (f ---> l) A)" ``` himmelma@33175 ` 955` himmelma@33175 ` 956` ```lemma Lim: ``` himmelma@33175 ` 957` ``` "(f ---> l) net \ ``` himmelma@33175 ` 958` ``` trivial_limit net \ ``` himmelma@33175 ` 959` ``` (\e>0. eventually (\x. dist (f x) l < e) net)" ``` himmelma@33175 ` 960` ``` unfolding tendsto_iff trivial_limit_eq by auto ``` himmelma@33175 ` 961` himmelma@33175 ` 962` ```text{* Show that they yield usual definitions in the various cases. *} ``` himmelma@33175 ` 963` himmelma@33175 ` 964` ```lemma Lim_within_le: "(f ---> l)(at a within S) \ ``` himmelma@33175 ` 965` ``` (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a <= d \ dist (f x) l < e)" ``` himmelma@33175 ` 966` ``` by (auto simp add: tendsto_iff eventually_within_le) ``` himmelma@33175 ` 967` himmelma@33175 ` 968` ```lemma Lim_within: "(f ---> l) (at a within S) \ ``` himmelma@33175 ` 969` ``` (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" ``` himmelma@33175 ` 970` ``` by (auto simp add: tendsto_iff eventually_within) ``` himmelma@33175 ` 971` himmelma@33175 ` 972` ```lemma Lim_at: "(f ---> l) (at a) \ ``` himmelma@33175 ` 973` ``` (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" ``` himmelma@33175 ` 974` ``` by (auto simp add: tendsto_iff eventually_at) ``` himmelma@33175 ` 975` himmelma@33175 ` 976` ```lemma Lim_at_iff_LIM: "(f ---> l) (at a) \ f -- a --> l" ``` himmelma@33175 ` 977` ``` unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff) ``` himmelma@33175 ` 978` himmelma@33175 ` 979` ```lemma Lim_at_infinity: ``` himmelma@33175 ` 980` ``` "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x >= b \ dist (f x) l < e)" ``` himmelma@33175 ` 981` ``` by (auto simp add: tendsto_iff eventually_at_infinity) ``` himmelma@33175 ` 982` himmelma@33175 ` 983` ```lemma Lim_sequentially: ``` himmelma@33175 ` 984` ``` "(S ---> l) sequentially \ ``` himmelma@33175 ` 985` ``` (\e>0. \N. \n\N. dist (S n) l < e)" ``` huffman@44210 ` 986` ``` by (rule LIMSEQ_def) (* FIXME: redundant *) ``` himmelma@33175 ` 987` himmelma@33175 ` 988` ```lemma Lim_eventually: "eventually (\x. f x = l) net \ (f ---> l) net" ``` himmelma@33175 ` 989` ``` by (rule topological_tendstoI, auto elim: eventually_rev_mono) ``` himmelma@33175 ` 990` himmelma@33175 ` 991` ```text{* The expected monotonicity property. *} ``` himmelma@33175 ` 992` himmelma@33175 ` 993` ```lemma Lim_within_empty: "(f ---> l) (net within {})" ``` himmelma@33175 ` 994` ``` unfolding tendsto_def Limits.eventually_within by simp ``` himmelma@33175 ` 995` himmelma@33175 ` 996` ```lemma Lim_within_subset: "(f ---> l) (net within S) \ T \ S \ (f ---> l) (net within T)" ``` himmelma@33175 ` 997` ``` unfolding tendsto_def Limits.eventually_within ``` himmelma@33175 ` 998` ``` by (auto elim!: eventually_elim1) ``` himmelma@33175 ` 999` himmelma@33175 ` 1000` ```lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)" ``` himmelma@33175 ` 1001` ``` shows "(f ---> l) (net within (S \ T))" ``` himmelma@33175 ` 1002` ``` using assms unfolding tendsto_def Limits.eventually_within ``` himmelma@33175 ` 1003` ``` apply clarify ``` himmelma@33175 ` 1004` ``` apply (drule spec, drule (1) mp, drule (1) mp) ``` himmelma@33175 ` 1005` ``` apply (drule spec, drule (1) mp, drule (1) mp) ``` himmelma@33175 ` 1006` ``` apply (auto elim: eventually_elim2) ``` himmelma@33175 ` 1007` ``` done ``` himmelma@33175 ` 1008` himmelma@33175 ` 1009` ```lemma Lim_Un_univ: ``` himmelma@33175 ` 1010` ``` "(f ---> l) (net within S) \ (f ---> l) (net within T) \ S \ T = UNIV ``` himmelma@33175 ` 1011` ``` ==> (f ---> l) net" ``` himmelma@33175 ` 1012` ``` by (metis Lim_Un within_UNIV) ``` himmelma@33175 ` 1013` himmelma@33175 ` 1014` ```text{* Interrelations between restricted and unrestricted limits. *} ``` himmelma@33175 ` 1015` himmelma@33175 ` 1016` ```lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)" ``` himmelma@33175 ` 1017` ``` (* FIXME: rename *) ``` himmelma@33175 ` 1018` ``` unfolding tendsto_def Limits.eventually_within ``` himmelma@33175 ` 1019` ``` apply (clarify, drule spec, drule (1) mp, drule (1) mp) ``` himmelma@33175 ` 1020` ``` by (auto elim!: eventually_elim1) ``` himmelma@33175 ` 1021` huffman@44210 ` 1022` ```lemma eventually_within_interior: ``` huffman@44210 ` 1023` ``` assumes "x \ interior S" ``` huffman@44210 ` 1024` ``` shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") ``` huffman@44210 ` 1025` ```proof- ``` huffman@44519 ` 1026` ``` from assms obtain T where T: "open T" "x \ T" "T \ S" .. ``` huffman@44210 ` 1027` ``` { assume "?lhs" ``` huffman@44210 ` 1028` ``` then obtain A where "open A" "x \ A" "\y\A. y \ x \ y \ S \ P y" ``` huffman@44210 ` 1029` ``` unfolding Limits.eventually_within Limits.eventually_at_topological ``` huffman@44210 ` 1030` ``` by auto ``` huffman@44210 ` 1031` ``` with T have "open (A \ T)" "x \ A \ T" "\y\(A \ T). y \ x \ P y" ``` huffman@44210 ` 1032` ``` by auto ``` huffman@44210 ` 1033` ``` then have "?rhs" ``` huffman@44210 ` 1034` ``` unfolding Limits.eventually_at_topological by auto ``` huffman@44210 ` 1035` ``` } moreover ``` huffman@44210 ` 1036` ``` { assume "?rhs" hence "?lhs" ``` huffman@44210 ` 1037` ``` unfolding Limits.eventually_within ``` huffman@44210 ` 1038` ``` by (auto elim: eventually_elim1) ``` huffman@44210 ` 1039` ``` } ultimately ``` huffman@44210 ` 1040` ``` show "?thesis" .. ``` huffman@44210 ` 1041` ```qed ``` huffman@44210 ` 1042` huffman@44210 ` 1043` ```lemma at_within_interior: ``` huffman@44210 ` 1044` ``` "x \ interior S \ at x within S = at x" ``` huffman@44210 ` 1045` ``` by (simp add: filter_eq_iff eventually_within_interior) ``` huffman@44210 ` 1046` huffman@44210 ` 1047` ```lemma at_within_open: ``` huffman@44210 ` 1048` ``` "\x \ S; open S\ \ at x within S = at x" ``` huffman@44210 ` 1049` ``` by (simp only: at_within_interior interior_open) ``` huffman@44210 ` 1050` himmelma@33175 ` 1051` ```lemma Lim_within_open: ``` himmelma@33175 ` 1052` ``` fixes f :: "'a::topological_space \ 'b::topological_space" ``` himmelma@33175 ` 1053` ``` assumes"a \ S" "open S" ``` huffman@44210 ` 1054` ``` shows "(f ---> l)(at a within S) \ (f ---> l)(at a)" ``` huffman@44210 ` 1055` ``` using assms by (simp only: at_within_open) ``` himmelma@33175 ` 1056` hoelzl@43338 ` 1057` ```lemma Lim_within_LIMSEQ: ``` huffman@44584 ` 1058` ``` fixes a :: "'a::metric_space" ``` hoelzl@43338 ` 1059` ``` assumes "\S. (\n. S n \ a \ S n \ T) \ S ----> a \ (\n. X (S n)) ----> L" ``` hoelzl@43338 ` 1060` ``` shows "(X ---> L) (at a within T)" ``` huffman@44584 ` 1061` ``` using assms unfolding tendsto_def [where l=L] ``` huffman@44584 ` 1062` ``` by (simp add: sequentially_imp_eventually_within) ``` hoelzl@43338 ` 1063` hoelzl@43338 ` 1064` ```lemma Lim_right_bound: ``` hoelzl@43338 ` 1065` ``` fixes f :: "real \ real" ``` hoelzl@43338 ` 1066` ``` assumes mono: "\a b. a \ I \ b \ I \ x < a \ a \ b \ f a \ f b" ``` hoelzl@43338 ` 1067` ``` assumes bnd: "\a. a \ I \ x < a \ K \ f a" ``` hoelzl@43338 ` 1068` ``` shows "(f ---> Inf (f ` ({x<..} \ I))) (at x within ({x<..} \ I))" ``` hoelzl@43338 ` 1069` ```proof cases ``` hoelzl@43338 ` 1070` ``` assume "{x<..} \ I = {}" then show ?thesis by (simp add: Lim_within_empty) ``` hoelzl@43338 ` 1071` ```next ``` hoelzl@43338 ` 1072` ``` assume [simp]: "{x<..} \ I \ {}" ``` hoelzl@43338 ` 1073` ``` show ?thesis ``` hoelzl@43338 ` 1074` ``` proof (rule Lim_within_LIMSEQ, safe) ``` hoelzl@43338 ` 1075` ``` fix S assume S: "\n. S n \ x \ S n \ {x <..} \ I" "S ----> x" ``` hoelzl@43338 ` 1076` ``` ``` hoelzl@43338 ` 1077` ``` show "(\n. f (S n)) ----> Inf (f ` ({x<..} \ I))" ``` hoelzl@43338 ` 1078` ``` proof (rule LIMSEQ_I, rule ccontr) ``` hoelzl@43338 ` 1079` ``` fix r :: real assume "0 < r" ``` hoelzl@43338 ` 1080` ``` with Inf_close[of "f ` ({x<..} \ I)" r] ``` hoelzl@43338 ` 1081` ``` obtain y where y: "x < y" "y \ I" "f y < Inf (f ` ({x <..} \ I)) + r" by auto ``` hoelzl@43338 ` 1082` ``` from `x < y` have "0 < y - x" by auto ``` hoelzl@43338 ` 1083` ``` from S(2)[THEN LIMSEQ_D, OF this] ``` hoelzl@43338 ` 1084` ``` obtain N where N: "\n. N \ n \ \S n - x\ < y - x" by auto ``` hoelzl@43338 ` 1085` ``` ``` hoelzl@43338 ` 1086` ``` assume "\ (\N. \n\N. norm (f (S n) - Inf (f ` ({x<..} \ I))) < r)" ``` hoelzl@43338 ` 1087` ``` moreover have "\n. Inf (f ` ({x<..} \ I)) \ f (S n)" ``` hoelzl@43338 ` 1088` ``` using S bnd by (intro Inf_lower[where z=K]) auto ``` hoelzl@43338 ` 1089` ``` ultimately obtain n where n: "N \ n" "r + Inf (f ` ({x<..} \ I)) \ f (S n)" ``` hoelzl@43338 ` 1090` ``` by (auto simp: not_less field_simps) ``` hoelzl@43338 ` 1091` ``` with N[OF n(1)] mono[OF _ `y \ I`, of "S n"] S(1)[THEN spec, of n] y ``` hoelzl@43338 ` 1092` ``` show False by auto ``` hoelzl@43338 ` 1093` ``` qed ``` hoelzl@43338 ` 1094` ``` qed ``` hoelzl@43338 ` 1095` ```qed ``` hoelzl@43338 ` 1096` himmelma@33175 ` 1097` ```text{* Another limit point characterization. *} ``` himmelma@33175 ` 1098` himmelma@33175 ` 1099` ```lemma islimpt_sequential: ``` huffman@36667 ` 1100` ``` fixes x :: "'a::metric_space" ``` himmelma@33175 ` 1101` ``` shows "x islimpt S \ (\f. (\n::nat. f n \ S -{x}) \ (f ---> x) sequentially)" ``` himmelma@33175 ` 1102` ``` (is "?lhs = ?rhs") ``` himmelma@33175 ` 1103` ```proof ``` himmelma@33175 ` 1104` ``` assume ?lhs ``` himmelma@33175 ` 1105` ``` then obtain f where f:"\y. y>0 \ f y \ S \ f y \ x \ dist (f y) x < y" ``` huffman@44584 ` 1106` ``` unfolding islimpt_approachable ``` huffman@44584 ` 1107` ``` using choice[of "\e y. e>0 \ y\S \ y\x \ dist y x < e"] by auto ``` huffman@44584 ` 1108` ``` let ?I = "\n. inverse (real (Suc n))" ``` huffman@44584 ` 1109` ``` have "\n. f (?I n) \ S - {x}" using f by simp ``` huffman@44584 ` 1110` ``` moreover have "(\n. f (?I n)) ----> x" ``` huffman@44584 ` 1111` ``` proof (rule metric_tendsto_imp_tendsto) ``` huffman@44584 ` 1112` ``` show "?I ----> 0" ``` huffman@44584 ` 1113` ``` by (rule LIMSEQ_inverse_real_of_nat) ``` huffman@44584 ` 1114` ``` show "eventually (\n. dist (f (?I n)) x \ dist (?I n) 0) sequentially" ``` huffman@44584 ` 1115` ``` by (simp add: norm_conv_dist [symmetric] less_imp_le f) ``` huffman@44584 ` 1116` ``` qed ``` huffman@44584 ` 1117` ``` ultimately show ?rhs by fast ``` himmelma@33175 ` 1118` ```next ``` himmelma@33175 ` 1119` ``` assume ?rhs ``` himmelma@33175 ` 1120` ``` then obtain f::"nat\'a" where f:"(\n. f n \ S - {x})" "(\e>0. \N. \n\N. dist (f n) x < e)" unfolding Lim_sequentially by auto ``` himmelma@33175 ` 1121` ``` { fix e::real assume "e>0" ``` himmelma@33175 ` 1122` ``` then obtain N where "dist (f N) x < e" using f(2) by auto ``` himmelma@33175 ` 1123` ``` moreover have "f N\S" "f N \ x" using f(1) by auto ``` himmelma@33175 ` 1124` ``` ultimately have "\x'\S. x' \ x \ dist x' x < e" by auto ``` himmelma@33175 ` 1125` ``` } ``` himmelma@33175 ` 1126` ``` thus ?lhs unfolding islimpt_approachable by auto ``` himmelma@33175 ` 1127` ```qed ``` himmelma@33175 ` 1128` huffman@44125 ` 1129` ```lemma Lim_inv: (* TODO: delete *) ``` huffman@44081 ` 1130` ``` fixes f :: "'a \ real" and A :: "'a filter" ``` huffman@44081 ` 1131` ``` assumes "(f ---> l) A" and "l \ 0" ``` huffman@44081 ` 1132` ``` shows "((inverse o f) ---> inverse l) A" ``` huffman@36437 ` 1133` ``` unfolding o_def using assms by (rule tendsto_inverse) ``` huffman@36437 ` 1134` himmelma@33175 ` 1135` ```lemma Lim_null: ``` himmelma@33175 ` 1136` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` huffman@44125 ` 1137` ``` shows "(f ---> l) net \ ((\x. f(x) - l) ---> 0) net" ``` himmelma@33175 ` 1138` ``` by (simp add: Lim dist_norm) ``` himmelma@33175 ` 1139` himmelma@33175 ` 1140` ```lemma Lim_null_comparison: ``` himmelma@33175 ` 1141` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` himmelma@33175 ` 1142` ``` assumes "eventually (\x. norm (f x) \ g x) net" "(g ---> 0) net" ``` himmelma@33175 ` 1143` ``` shows "(f ---> 0) net" ``` huffman@44252 ` 1144` ```proof (rule metric_tendsto_imp_tendsto) ``` huffman@44252 ` 1145` ``` show "(g ---> 0) net" by fact ``` huffman@44252 ` 1146` ``` show "eventually (\x. dist (f x) 0 \ dist (g x) 0) net" ``` huffman@44252 ` 1147` ``` using assms(1) by (rule eventually_elim1, simp add: dist_norm) ``` himmelma@33175 ` 1148` ```qed ``` himmelma@33175 ` 1149` himmelma@33175 ` 1150` ```lemma Lim_transform_bound: ``` himmelma@33175 ` 1151` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` himmelma@33175 ` 1152` ``` fixes g :: "'a \ 'c::real_normed_vector" ``` himmelma@33175 ` 1153` ``` assumes "eventually (\n. norm(f n) <= norm(g n)) net" "(g ---> 0) net" ``` himmelma@33175 ` 1154` ``` shows "(f ---> 0) net" ``` huffman@44252 ` 1155` ``` using assms(1) tendsto_norm_zero [OF assms(2)] ``` huffman@44252 ` 1156` ``` by (rule Lim_null_comparison) ``` himmelma@33175 ` 1157` himmelma@33175 ` 1158` ```text{* Deducing things about the limit from the elements. *} ``` himmelma@33175 ` 1159` himmelma@33175 ` 1160` ```lemma Lim_in_closed_set: ``` himmelma@33175 ` 1161` ``` assumes "closed S" "eventually (\x. f(x) \ S) net" "\(trivial_limit net)" "(f ---> l) net" ``` himmelma@33175 ` 1162` ``` shows "l \ S" ``` himmelma@33175 ` 1163` ```proof (rule ccontr) ``` himmelma@33175 ` 1164` ``` assume "l \ S" ``` himmelma@33175 ` 1165` ``` with `closed S` have "open (- S)" "l \ - S" ``` himmelma@33175 ` 1166` ``` by (simp_all add: open_Compl) ``` himmelma@33175 ` 1167` ``` with assms(4) have "eventually (\x. f x \ - S) net" ``` himmelma@33175 ` 1168` ``` by (rule topological_tendstoD) ``` himmelma@33175 ` 1169` ``` with assms(2) have "eventually (\x. False) net" ``` himmelma@33175 ` 1170` ``` by (rule eventually_elim2) simp ``` himmelma@33175 ` 1171` ``` with assms(3) show "False" ``` himmelma@33175 ` 1172` ``` by (simp add: eventually_False) ``` himmelma@33175 ` 1173` ```qed ``` himmelma@33175 ` 1174` himmelma@33175 ` 1175` ```text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *} ``` himmelma@33175 ` 1176` himmelma@33175 ` 1177` ```lemma Lim_dist_ubound: ``` himmelma@33175 ` 1178` ``` assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. dist a (f x) <= e) net" ``` himmelma@33175 ` 1179` ``` shows "dist a l <= e" ``` huffman@44252 ` 1180` ```proof- ``` huffman@44252 ` 1181` ``` have "dist a l \ {..e}" ``` huffman@44252 ` 1182` ``` proof (rule Lim_in_closed_set) ``` huffman@44252 ` 1183` ``` show "closed {..e}" by simp ``` huffman@44252 ` 1184` ``` show "eventually (\x. dist a (f x) \ {..e}) net" by (simp add: assms) ``` huffman@44252 ` 1185` ``` show "\ trivial_limit net" by fact ``` huffman@44252 ` 1186` ``` show "((\x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms) ``` huffman@44252 ` 1187` ``` qed ``` huffman@44252 ` 1188` ``` thus ?thesis by simp ``` himmelma@33175 ` 1189` ```qed ``` himmelma@33175 ` 1190` himmelma@33175 ` 1191` ```lemma Lim_norm_ubound: ``` himmelma@33175 ` 1192` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` himmelma@33175 ` 1193` ``` assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. norm(f x) <= e) net" ``` himmelma@33175 ` 1194` ``` shows "norm(l) <= e" ``` huffman@44252 ` 1195` ```proof- ``` huffman@44252 ` 1196` ``` have "norm l \ {..e}" ``` huffman@44252 ` 1197` ``` proof (rule Lim_in_closed_set) ``` huffman@44252 ` 1198` ``` show "closed {..e}" by simp ``` huffman@44252 ` 1199` ``` show "eventually (\x. norm (f x) \ {..e}) net" by (simp add: assms) ``` huffman@44252 ` 1200` ``` show "\ trivial_limit net" by fact ``` huffman@44252 ` 1201` ``` show "((\x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms) ``` huffman@44252 ` 1202` ``` qed ``` huffman@44252 ` 1203` ``` thus ?thesis by simp ``` himmelma@33175 ` 1204` ```qed ``` himmelma@33175 ` 1205` himmelma@33175 ` 1206` ```lemma Lim_norm_lbound: ``` himmelma@33175 ` 1207` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` himmelma@33175 ` 1208` ``` assumes "\ (trivial_limit net)" "(f ---> l) net" "eventually (\x. e <= norm(f x)) net" ``` himmelma@33175 ` 1209` ``` shows "e \ norm l" ``` huffman@44252 ` 1210` ```proof- ``` huffman@44252 ` 1211` ``` have "norm l \ {e..}" ``` huffman@44252 ` 1212` ``` proof (rule Lim_in_closed_set) ``` huffman@44252 ` 1213` ``` show "closed {e..}" by simp ``` huffman@44252 ` 1214` ``` show "eventually (\x. norm (f x) \ {e..}) net" by (simp add: assms) ``` huffman@44252 ` 1215` ``` show "\ trivial_limit net" by fact ``` huffman@44252 ` 1216` ``` show "((\x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms) ``` huffman@44252 ` 1217` ``` qed ``` huffman@44252 ` 1218` ``` thus ?thesis by simp ``` himmelma@33175 ` 1219` ```qed ``` himmelma@33175 ` 1220` himmelma@33175 ` 1221` ```text{* Uniqueness of the limit, when nontrivial. *} ``` himmelma@33175 ` 1222` himmelma@33175 ` 1223` ```lemma tendsto_Lim: ``` himmelma@33175 ` 1224` ``` fixes f :: "'a \ 'b::t2_space" ``` himmelma@33175 ` 1225` ``` shows "~(trivial_limit net) \ (f ---> l) net ==> Lim net f = l" ``` hoelzl@41970 ` 1226` ``` unfolding Lim_def using tendsto_unique[of net f] by auto ``` himmelma@33175 ` 1227` himmelma@33175 ` 1228` ```text{* Limit under bilinear function *} ``` himmelma@33175 ` 1229` himmelma@33175 ` 1230` ```lemma Lim_bilinear: ``` himmelma@33175 ` 1231` ``` assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h" ``` himmelma@33175 ` 1232` ``` shows "((\x. h (f x) (g x)) ---> (h l m)) net" ``` himmelma@33175 ` 1233` ```using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net` ``` himmelma@33175 ` 1234` ```by (rule bounded_bilinear.tendsto) ``` himmelma@33175 ` 1235` himmelma@33175 ` 1236` ```text{* These are special for limits out of the same vector space. *} ``` himmelma@33175 ` 1237` himmelma@33175 ` 1238` ```lemma Lim_within_id: "(id ---> a) (at a within s)" ``` himmelma@33175 ` 1239` ``` unfolding tendsto_def Limits.eventually_within eventually_at_topological ``` himmelma@33175 ` 1240` ``` by auto ``` himmelma@33175 ` 1241` himmelma@33175 ` 1242` ```lemma Lim_at_id: "(id ---> a) (at a)" ``` himmelma@33175 ` 1243` ```apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id) ``` himmelma@33175 ` 1244` himmelma@33175 ` 1245` ```lemma Lim_at_zero: ``` himmelma@33175 ` 1246` ``` fixes a :: "'a::real_normed_vector" ``` himmelma@33175 ` 1247` ``` fixes l :: "'b::topological_space" ``` himmelma@33175 ` 1248` ``` shows "(f ---> l) (at a) \ ((\x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs") ``` huffman@44252 ` 1249` ``` using LIM_offset_zero LIM_offset_zero_cancel .. ``` himmelma@33175 ` 1250` huffman@44081 ` 1251` ```text{* It's also sometimes useful to extract the limit point from the filter. *} ``` himmelma@33175 ` 1252` himmelma@33175 ` 1253` ```definition ``` huffman@44081 ` 1254` ``` netlimit :: "'a::t2_space filter \ 'a" where ``` himmelma@33175 ` 1255` ``` "netlimit net = (SOME a. ((\x. x) ---> a) net)" ``` himmelma@33175 ` 1256` himmelma@33175 ` 1257` ```lemma netlimit_within: ``` himmelma@33175 ` 1258` ``` assumes "\ trivial_limit (at a within S)" ``` himmelma@33175 ` 1259` ``` shows "netlimit (at a within S) = a" ``` himmelma@33175 ` 1260` ```unfolding netlimit_def ``` himmelma@33175 ` 1261` ```apply (rule some_equality) ``` himmelma@33175 ` 1262` ```apply (rule Lim_at_within) ``` huffman@44568 ` 1263` ```apply (rule tendsto_ident_at) ``` hoelzl@41970 ` 1264` ```apply (erule tendsto_unique [OF assms]) ``` himmelma@33175 ` 1265` ```apply (rule Lim_at_within) ``` huffman@44568 ` 1266` ```apply (rule tendsto_ident_at) ``` himmelma@33175 ` 1267` ```done ``` himmelma@33175 ` 1268` himmelma@33175 ` 1269` ```lemma netlimit_at: ``` huffman@44072 ` 1270` ``` fixes a :: "'a::{perfect_space,t2_space}" ``` himmelma@33175 ` 1271` ``` shows "netlimit (at a) = a" ``` himmelma@33175 ` 1272` ``` apply (subst within_UNIV[symmetric]) ``` himmelma@33175 ` 1273` ``` using netlimit_within[of a UNIV] ``` huffman@44584 ` 1274` ``` by (simp add: within_UNIV) ``` himmelma@33175 ` 1275` huffman@44210 ` 1276` ```lemma lim_within_interior: ``` huffman@44210 ` 1277` ``` "x \ interior S \ (f ---> l) (at x within S) \ (f ---> l) (at x)" ``` huffman@44210 ` 1278` ``` by (simp add: at_within_interior) ``` huffman@44210 ` 1279` huffman@44210 ` 1280` ```lemma netlimit_within_interior: ``` huffman@44210 ` 1281` ``` fixes x :: "'a::{t2_space,perfect_space}" ``` huffman@44210 ` 1282` ``` assumes "x \ interior S" ``` huffman@44210 ` 1283` ``` shows "netlimit (at x within S) = x" ``` huffman@44210 ` 1284` ```using assms by (simp add: at_within_interior netlimit_at) ``` huffman@44210 ` 1285` himmelma@33175 ` 1286` ```text{* Transformation of limit. *} ``` himmelma@33175 ` 1287` himmelma@33175 ` 1288` ```lemma Lim_transform: ``` himmelma@33175 ` 1289` ``` fixes f g :: "'a::type \ 'b::real_normed_vector" ``` himmelma@33175 ` 1290` ``` assumes "((\x. f x - g x) ---> 0) net" "(f ---> l) net" ``` himmelma@33175 ` 1291` ``` shows "(g ---> l) net" ``` huffman@44252 ` 1292` ``` using tendsto_diff [OF assms(2) assms(1)] by simp ``` himmelma@33175 ` 1293` himmelma@33175 ` 1294` ```lemma Lim_transform_eventually: ``` huffman@36667 ` 1295` ``` "eventually (\x. f x = g x) net \ (f ---> l) net \ (g ---> l) net" ``` himmelma@33175 ` 1296` ``` apply (rule topological_tendstoI) ``` himmelma@33175 ` 1297` ``` apply (drule (2) topological_tendstoD) ``` himmelma@33175 ` 1298` ``` apply (erule (1) eventually_elim2, simp) ``` himmelma@33175 ` 1299` ``` done ``` himmelma@33175 ` 1300` himmelma@33175 ` 1301` ```lemma Lim_transform_within: ``` huffman@36667 ` 1302` ``` assumes "0 < d" and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" ``` huffman@36667 ` 1303` ``` and "(f ---> l) (at x within S)" ``` huffman@36667 ` 1304` ``` shows "(g ---> l) (at x within S)" ``` huffman@36667 ` 1305` ```proof (rule Lim_transform_eventually) ``` huffman@36667 ` 1306` ``` show "eventually (\x. f x = g x) (at x within S)" ``` huffman@36667 ` 1307` ``` unfolding eventually_within ``` huffman@36667 ` 1308` ``` using assms(1,2) by auto ``` huffman@36667 ` 1309` ``` show "(f ---> l) (at x within S)" by fact ``` huffman@36667 ` 1310` ```qed ``` himmelma@33175 ` 1311` himmelma@33175 ` 1312` ```lemma Lim_transform_at: ``` huffman@36667 ` 1313` ``` assumes "0 < d" and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" ``` huffman@36667 ` 1314` ``` and "(f ---> l) (at x)" ``` huffman@36667 ` 1315` ``` shows "(g ---> l) (at x)" ``` huffman@36667 ` 1316` ```proof (rule Lim_transform_eventually) ``` huffman@36667 ` 1317` ``` show "eventually (\x. f x = g x) (at x)" ``` huffman@36667 ` 1318` ``` unfolding eventually_at ``` huffman@36667 ` 1319` ``` using assms(1,2) by auto ``` huffman@36667 ` 1320` ``` show "(f ---> l) (at x)" by fact ``` huffman@36667 ` 1321` ```qed ``` himmelma@33175 ` 1322` himmelma@33175 ` 1323` ```text{* Common case assuming being away from some crucial point like 0. *} ``` himmelma@33175 ` 1324` himmelma@33175 ` 1325` ```lemma Lim_transform_away_within: ``` huffman@36669 ` 1326` ``` fixes a b :: "'a::t1_space" ``` huffman@36667 ` 1327` ``` assumes "a \ b" and "\x\S. x \ a \ x \ b \ f x = g x" ``` himmelma@33175 ` 1328` ``` and "(f ---> l) (at a within S)" ``` himmelma@33175 ` 1329` ``` shows "(g ---> l) (at a within S)" ``` huffman@36669 ` 1330` ```proof (rule Lim_transform_eventually) ``` huffman@36669 ` 1331` ``` show "(f ---> l) (at a within S)" by fact ``` huffman@36669 ` 1332` ``` show "eventually (\x. f x = g x) (at a within S)" ``` huffman@36669 ` 1333` ``` unfolding Limits.eventually_within eventually_at_topological ``` huffman@36669 ` 1334` ``` by (rule exI [where x="- {b}"], simp add: open_Compl assms) ``` himmelma@33175 ` 1335` ```qed ``` himmelma@33175 ` 1336` himmelma@33175 ` 1337` ```lemma Lim_transform_away_at: ``` huffman@36669 ` 1338` ``` fixes a b :: "'a::t1_space" ``` himmelma@33175 ` 1339` ``` assumes ab: "a\b" and fg: "\x. x \ a \ x \ b \ f x = g x" ``` himmelma@33175 ` 1340` ``` and fl: "(f ---> l) (at a)" ``` himmelma@33175 ` 1341` ``` shows "(g ---> l) (at a)" ``` himmelma@33175 ` 1342` ``` using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl ``` himmelma@33175 ` 1343` ``` by (auto simp add: within_UNIV) ``` himmelma@33175 ` 1344` himmelma@33175 ` 1345` ```text{* Alternatively, within an open set. *} ``` himmelma@33175 ` 1346` himmelma@33175 ` 1347` ```lemma Lim_transform_within_open: ``` huffman@36667 ` 1348` ``` assumes "open S" and "a \ S" and "\x\S. x \ a \ f x = g x" ``` huffman@36667 ` 1349` ``` and "(f ---> l) (at a)" ``` himmelma@33175 ` 1350` ``` shows "(g ---> l) (at a)" ``` huffman@36667 ` 1351` ```proof (rule Lim_transform_eventually) ``` huffman@36667 ` 1352` ``` show "eventually (\x. f x = g x) (at a)" ``` huffman@36667 ` 1353` ``` unfolding eventually_at_topological ``` huffman@36667 ` 1354` ``` using assms(1,2,3) by auto ``` huffman@36667 ` 1355` ``` show "(f ---> l) (at a)" by fact ``` himmelma@33175 ` 1356` ```qed ``` himmelma@33175 ` 1357` himmelma@33175 ` 1358` ```text{* A congruence rule allowing us to transform limits assuming not at point. *} ``` himmelma@33175 ` 1359` himmelma@33175 ` 1360` ```(* FIXME: Only one congruence rule for tendsto can be used at a time! *) ``` himmelma@33175 ` 1361` huffman@36362 ` 1362` ```lemma Lim_cong_within(*[cong add]*): ``` hoelzl@43338 ` 1363` ``` assumes "a = b" "x = y" "S = T" ``` hoelzl@43338 ` 1364` ``` assumes "\x. x \ b \ x \ T \ f x = g x" ``` hoelzl@43338 ` 1365` ``` shows "(f ---> x) (at a within S) \ (g ---> y) (at b within T)" ``` huffman@36667 ` 1366` ``` unfolding tendsto_def Limits.eventually_within eventually_at_topological ``` huffman@36667 ` 1367` ``` using assms by simp ``` huffman@36667 ` 1368` huffman@36667 ` 1369` ```lemma Lim_cong_at(*[cong add]*): ``` hoelzl@43338 ` 1370` ``` assumes "a = b" "x = y" ``` huffman@36667 ` 1371` ``` assumes "\x. x \ a \ f x = g x" ``` hoelzl@43338 ` 1372` ``` shows "((\x. f x) ---> x) (at a) \ ((g ---> y) (at a))" ``` huffman@36667 ` 1373` ``` unfolding tendsto_def eventually_at_topological ``` huffman@36667 ` 1374` ``` using assms by simp ``` himmelma@33175 ` 1375` himmelma@33175 ` 1376` ```text{* Useful lemmas on closure and set of possible sequential limits.*} ``` himmelma@33175 ` 1377` himmelma@33175 ` 1378` ```lemma closure_sequential: ``` huffman@36667 ` 1379` ``` fixes l :: "'a::metric_space" ``` himmelma@33175 ` 1380` ``` shows "l \ closure S \ (\x. (\n. x n \ S) \ (x ---> l) sequentially)" (is "?lhs = ?rhs") ``` himmelma@33175 ` 1381` ```proof ``` himmelma@33175 ` 1382` ``` assume "?lhs" moreover ``` himmelma@33175 ` 1383` ``` { assume "l \ S" ``` huffman@44125 ` 1384` ``` hence "?rhs" using tendsto_const[of l sequentially] by auto ``` himmelma@33175 ` 1385` ``` } moreover ``` himmelma@33175 ` 1386` ``` { assume "l islimpt S" ``` himmelma@33175 ` 1387` ``` hence "?rhs" unfolding islimpt_sequential by auto ``` himmelma@33175 ` 1388` ``` } ultimately ``` himmelma@33175 ` 1389` ``` show "?rhs" unfolding closure_def by auto ``` himmelma@33175 ` 1390` ```next ``` himmelma@33175 ` 1391` ``` assume "?rhs" ``` himmelma@33175 ` 1392` ``` thus "?lhs" unfolding closure_def unfolding islimpt_sequential by auto ``` himmelma@33175 ` 1393` ```qed ``` himmelma@33175 ` 1394` himmelma@33175 ` 1395` ```lemma closed_sequential_limits: ``` himmelma@33175 ` 1396` ``` fixes S :: "'a::metric_space set" ``` himmelma@33175 ` 1397` ``` shows "closed S \ (\x l. (\n. x n \ S) \ (x ---> l) sequentially \ l \ S)" ``` himmelma@33175 ` 1398` ``` unfolding closed_limpt ``` himmelma@33175 ` 1399` ``` using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a] ``` himmelma@33175 ` 1400` ``` by metis ``` himmelma@33175 ` 1401` himmelma@33175 ` 1402` ```lemma closure_approachable: ``` himmelma@33175 ` 1403` ``` fixes S :: "'a::metric_space set" ``` himmelma@33175 ` 1404` ``` shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" ``` himmelma@33175 ` 1405` ``` apply (auto simp add: closure_def islimpt_approachable) ``` himmelma@33175 ` 1406` ``` by (metis dist_self) ``` himmelma@33175 ` 1407` himmelma@33175 ` 1408` ```lemma closed_approachable: ``` himmelma@33175 ` 1409` ``` fixes S :: "'a::metric_space set" ``` himmelma@33175 ` 1410` ``` shows "closed S ==> (\e>0. \y\S. dist y x < e) \ x \ S" ``` himmelma@33175 ` 1411` ``` by (metis closure_closed closure_approachable) ``` himmelma@33175 ` 1412` himmelma@33175 ` 1413` ```text{* Some other lemmas about sequences. *} ``` himmelma@33175 ` 1414` huffman@36441 ` 1415` ```lemma sequentially_offset: ``` huffman@36441 ` 1416` ``` assumes "eventually (\i. P i) sequentially" ``` huffman@36441 ` 1417` ``` shows "eventually (\i. P (i + k)) sequentially" ``` huffman@36441 ` 1418` ``` using assms unfolding eventually_sequentially by (metis trans_le_add1) ``` huffman@36441 ` 1419` himmelma@33175 ` 1420` ```lemma seq_offset: ``` huffman@36441 ` 1421` ``` assumes "(f ---> l) sequentially" ``` huffman@36441 ` 1422` ``` shows "((\i. f (i + k)) ---> l) sequentially" ``` huffman@44584 ` 1423` ``` using assms by (rule LIMSEQ_ignore_initial_segment) (* FIXME: redundant *) ``` himmelma@33175 ` 1424` himmelma@33175 ` 1425` ```lemma seq_offset_neg: ``` himmelma@33175 ` 1426` ``` "(f ---> l) sequentially ==> ((\i. f(i - k)) ---> l) sequentially" ``` himmelma@33175 ` 1427` ``` apply (rule topological_tendstoI) ``` himmelma@33175 ` 1428` ``` apply (drule (2) topological_tendstoD) ``` himmelma@33175 ` 1429` ``` apply (simp only: eventually_sequentially) ``` himmelma@33175 ` 1430` ``` apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k") ``` himmelma@33175 ` 1431` ``` apply metis ``` himmelma@33175 ` 1432` ``` by arith ``` himmelma@33175 ` 1433` himmelma@33175 ` 1434` ```lemma seq_offset_rev: ``` himmelma@33175 ` 1435` ``` "((\i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially" ``` huffman@44584 ` 1436` ``` by (rule LIMSEQ_offset) (* FIXME: redundant *) ``` himmelma@33175 ` 1437` himmelma@33175 ` 1438` ```lemma seq_harmonic: "((\n. inverse (real n)) ---> 0) sequentially" ``` huffman@44584 ` 1439` ``` using LIMSEQ_inverse_real_of_nat by (rule LIMSEQ_imp_Suc) ``` himmelma@33175 ` 1440` huffman@44210 ` 1441` ```subsection {* More properties of closed balls *} ``` himmelma@33175 ` 1442` himmelma@33175 ` 1443` ```lemma closed_cball: "closed (cball x e)" ``` himmelma@33175 ` 1444` ```unfolding cball_def closed_def ``` himmelma@33175 ` 1445` ```unfolding Collect_neg_eq [symmetric] not_le ``` himmelma@33175 ` 1446` ```apply (clarsimp simp add: open_dist, rename_tac y) ``` himmelma@33175 ` 1447` ```apply (rule_tac x="dist x y - e" in exI, clarsimp) ``` himmelma@33175 ` 1448` ```apply (rename_tac x') ``` himmelma@33175 ` 1449` ```apply (cut_tac x=x and y=x' and z=y in dist_triangle) ``` himmelma@33175 ` 1450` ```apply simp ``` himmelma@33175 ` 1451` ```done ``` himmelma@33175 ` 1452` himmelma@33175 ` 1453` ```lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" ``` himmelma@33175 ` 1454` ```proof- ``` himmelma@33175 ` 1455` ``` { fix x and e::real assume "x\S" "e>0" "ball x e \ S" ``` himmelma@33175 ` 1456` ``` hence "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) ``` himmelma@33175 ` 1457` ``` } moreover ``` himmelma@33175 ` 1458` ``` { fix x and e::real assume "x\S" "e>0" "cball x e \ S" ``` himmelma@33175 ` 1459` ``` hence "\d>0. ball x d \ S" unfolding subset_eq apply(rule_tac x="e/2" in exI) by auto ``` himmelma@33175 ` 1460` ``` } ultimately ``` himmelma@33175 ` 1461` ``` show ?thesis unfolding open_contains_ball by auto ``` himmelma@33175 ` 1462` ```qed ``` himmelma@33175 ` 1463` himmelma@33175 ` 1464` ```lemma open_contains_cball_eq: "open S ==> (\x. x \ S \ (\e>0. cball x e \ S))" ``` huffman@44170 ` 1465` ``` by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) ``` himmelma@33175 ` 1466` himmelma@33175 ` 1467` ```lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" ``` himmelma@33175 ` 1468` ``` apply (simp add: interior_def, safe) ``` himmelma@33175 ` 1469` ``` apply (force simp add: open_contains_cball) ``` himmelma@33175 ` 1470` ``` apply (rule_tac x="ball x e" in exI) ``` huffman@36362 ` 1471` ``` apply (simp add: subset_trans [OF ball_subset_cball]) ``` himmelma@33175 ` 1472` ``` done ``` himmelma@33175 ` 1473` himmelma@33175 ` 1474` ```lemma islimpt_ball: ``` himmelma@33175 ` 1475` ``` fixes x y :: "'a::{real_normed_vector,perfect_space}" ``` himmelma@33175 ` 1476` ``` shows "y islimpt ball x e \ 0 < e \ y \ cball x e" (is "?lhs = ?rhs") ``` himmelma@33175 ` 1477` ```proof ``` himmelma@33175 ` 1478` ``` assume "?lhs" ``` himmelma@33175 ` 1479` ``` { assume "e \ 0" ``` himmelma@33175 ` 1480` ``` hence *:"ball x e = {}" using ball_eq_empty[of x e] by auto ``` himmelma@33175 ` 1481` ``` have False using `?lhs` unfolding * using islimpt_EMPTY[of y] by auto ``` himmelma@33175 ` 1482` ``` } ``` himmelma@33175 ` 1483` ``` hence "e > 0" by (metis not_less) ``` himmelma@33175 ` 1484` ``` moreover ``` himmelma@33175 ` 1485` ``` have "y \ cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] `?lhs` unfolding closed_limpt by auto ``` himmelma@33175 ` 1486` ``` ultimately show "?rhs" by auto ``` himmelma@33175 ` 1487` ```next ``` himmelma@33175 ` 1488` ``` assume "?rhs" hence "e>0" by auto ``` himmelma@33175 ` 1489` ``` { fix d::real assume "d>0" ``` himmelma@33175 ` 1490` ``` have "\x'\ball x e. x' \ y \ dist x' y < d" ``` himmelma@33175 ` 1491` ``` proof(cases "d \ dist x y") ``` himmelma@33175 ` 1492` ``` case True thus "\x'\ball x e. x' \ y \ dist x' y < d" ``` himmelma@33175 ` 1493` ``` proof(cases "x=y") ``` himmelma@33175 ` 1494` ``` case True hence False using `d \ dist x y` `d>0` by auto ``` himmelma@33175 ` 1495` ``` thus "\x'\ball x e. x' \ y \ dist x' y < d" by auto ``` himmelma@33175 ` 1496` ``` next ``` himmelma@33175 ` 1497` ``` case False ``` himmelma@33175 ` 1498` himmelma@33175 ` 1499` ``` have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) ``` himmelma@33175 ` 1500` ``` = norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))" ``` himmelma@33175 ` 1501` ``` unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto ``` himmelma@33175 ` 1502` ``` also have "\ = \- 1 + d / (2 * norm (x - y))\ * norm (x - y)" ``` himmelma@33175 ` 1503` ``` using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"] ``` himmelma@33175 ` 1504` ``` unfolding scaleR_minus_left scaleR_one ``` himmelma@33175 ` 1505` ``` by (auto simp add: norm_minus_commute) ``` himmelma@33175 ` 1506` ``` also have "\ = \- norm (x - y) + d / 2\" ``` himmelma@33175 ` 1507` ``` unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]] ``` huffman@36778 ` 1508` ``` unfolding left_distrib using `x\y`[unfolded dist_nz, unfolded dist_norm] by auto ``` himmelma@33175 ` 1509` ``` also have "\ \ e - d/2" using `d \ dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm) ``` himmelma@33175 ` 1510` ``` finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \ ball x e" using `d>0` by auto ``` himmelma@33175 ` 1511` himmelma@33175 ` 1512` ``` moreover ``` himmelma@33175 ` 1513` himmelma@33175 ` 1514` ``` have "(d / (2*dist y x)) *\<^sub>R (y - x) \ 0" ``` himmelma@33175 ` 1515` ``` using `x\y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute) ``` himmelma@33175 ` 1516` ``` moreover ``` himmelma@33175 ` 1517` ``` have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel ``` himmelma@33175 ` 1518` ``` using `d>0` `x\y`[unfolded dist_nz] dist_commute[of x y] ``` himmelma@33175 ` 1519` ``` unfolding dist_norm by auto ``` himmelma@33175 ` 1520` ``` ultimately show "\x'\ball x e. x' \ y \ dist x' y < d" by (rule_tac x="y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) auto ``` himmelma@33175 ` 1521` ``` qed ``` himmelma@33175 ` 1522` ``` next ``` himmelma@33175 ` 1523` ``` case False hence "d > dist x y" by auto ``` himmelma@33175 ` 1524` ``` show "\x'\ball x e. x' \ y \ dist x' y < d" ``` himmelma@33175 ` 1525` ``` proof(cases "x=y") ``` himmelma@33175 ` 1526` ``` case True ``` himmelma@33175 ` 1527` ``` obtain z where **: "z \ y" "dist z y < min e d" ``` himmelma@33175 ` 1528` ``` using perfect_choose_dist[of "min e d" y] ``` himmelma@33175 ` 1529` ``` using `d > 0` `e>0` by auto ``` himmelma@33175 ` 1530` ``` show "\x'\ball x e. x' \ y \ dist x' y < d" ``` himmelma@33175 ` 1531` ``` unfolding `x = y` ``` himmelma@33175 ` 1532` ``` using `z \ y` ** ``` himmelma@33175 ` 1533` ``` by (rule_tac x=z in bexI, auto simp add: dist_commute) ``` himmelma@33175 ` 1534` ``` next ``` himmelma@33175 ` 1535` ``` case False thus "\x'\ball x e. x' \ y \ dist x' y < d" ``` himmelma@33175 ` 1536` ``` using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto) ``` himmelma@33175 ` 1537` ``` qed ``` himmelma@33175 ` 1538` ``` qed } ``` himmelma@33175 ` 1539` ``` thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto ``` himmelma@33175 ` 1540` ```qed ``` himmelma@33175 ` 1541` himmelma@33175 ` 1542` ```lemma closure_ball_lemma: ``` himmelma@33175 ` 1543` ``` fixes x y :: "'a::real_normed_vector" ``` himmelma@33175 ` 1544` ``` assumes "x \ y" shows "y islimpt ball x (dist x y)" ``` himmelma@33175 ` 1545` ```proof (rule islimptI) ``` himmelma@33175 ` 1546` ``` fix T assume "y \ T" "open T" ``` himmelma@33175 ` 1547` ``` then obtain r where "0 < r" "\z. dist z y < r \ z \ T" ``` himmelma@33175 ` 1548` ``` unfolding open_dist by fast ``` himmelma@33175 ` 1549` ``` (* choose point between x and y, within distance r of y. *) ``` himmelma@33175 ` 1550` ``` def k \ "min 1 (r / (2 * dist x y))" ``` himmelma@33175 ` 1551` ``` def z \ "y + scaleR k (x - y)" ``` himmelma@33175 ` 1552` ``` have z_def2: "z = x + scaleR (1 - k) (y - x)" ``` himmelma@33175 ` 1553` ``` unfolding z_def by (simp add: algebra_simps) ``` himmelma@33175 ` 1554` ``` have "dist z y < r" ``` himmelma@33175 ` 1555` ``` unfolding z_def k_def using `0 < r` ``` himmelma@33175 ` 1556` ``` by (simp add: dist_norm min_def) ``` himmelma@33175 ` 1557` ``` hence "z \ T" using `\z. dist z y < r \ z \ T` by simp ``` himmelma@33175 ` 1558` ``` have "dist x z < dist x y" ``` himmelma@33175 ` 1559` ``` unfolding z_def2 dist_norm ``` himmelma@33175 ` 1560` ``` apply (simp add: norm_minus_commute) ``` himmelma@33175 ` 1561` ``` apply (simp only: dist_norm [symmetric]) ``` himmelma@33175 ` 1562` ``` apply (subgoal_tac "\1 - k\ * dist x y < 1 * dist x y", simp) ``` himmelma@33175 ` 1563` ``` apply (rule mult_strict_right_mono) ``` himmelma@33175 ` 1564` ``` apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \ y`) ``` himmelma@33175 ` 1565` ``` apply (simp add: zero_less_dist_iff `x \ y`) ``` himmelma@33175 ` 1566` ``` done ``` himmelma@33175 ` 1567` ``` hence "z \ ball x (dist x y)" by simp ``` himmelma@33175 ` 1568` ``` have "z \ y" ``` himmelma@33175 ` 1569` ``` unfolding z_def k_def using `x \ y` `0 < r` ``` himmelma@33175 ` 1570` ``` by (simp add: min_def) ``` himmelma@33175 ` 1571` ``` show "\z\ball x (dist x y). z \ T \ z \ y" ``` himmelma@33175 ` 1572` ``` using `z \ ball x (dist x y)` `z \ T` `z \ y` ``` himmelma@33175 ` 1573` ``` by fast ``` himmelma@33175 ` 1574` ```qed ``` himmelma@33175 ` 1575` himmelma@33175 ` 1576` ```lemma closure_ball: ``` himmelma@33175 ` 1577` ``` fixes x :: "'a::real_normed_vector" ``` himmelma@33175 ` 1578` ``` shows "0 < e \ closure (ball x e) = cball x e" ``` himmelma@33175 ` 1579` ```apply (rule equalityI) ``` himmelma@33175 ` 1580` ```apply (rule closure_minimal) ``` himmelma@33175 ` 1581` ```apply (rule ball_subset_cball) ``` himmelma@33175 ` 1582` ```apply (rule closed_cball) ``` himmelma@33175 ` 1583` ```apply (rule subsetI, rename_tac y) ``` himmelma@33175 ` 1584` ```apply (simp add: le_less [where 'a=real]) ``` himmelma@33175 ` 1585` ```apply (erule disjE) ``` himmelma@33175 ` 1586` ```apply (rule subsetD [OF closure_subset], simp) ``` himmelma@33175 ` 1587` ```apply (simp add: closure_def) ``` himmelma@33175 ` 1588` ```apply clarify ``` himmelma@33175 ` 1589` ```apply (rule closure_ball_lemma) ``` himmelma@33175 ` 1590` ```apply (simp add: zero_less_dist_iff) ``` himmelma@33175 ` 1591` ```done ``` himmelma@33175 ` 1592` himmelma@33175 ` 1593` ```(* In a trivial vector space, this fails for e = 0. *) ``` himmelma@33175 ` 1594` ```lemma interior_cball: ``` himmelma@33175 ` 1595` ``` fixes x :: "'a::{real_normed_vector, perfect_space}" ``` himmelma@33175 ` 1596` ``` shows "interior (cball x e) = ball x e" ``` himmelma@33175 ` 1597` ```proof(cases "e\0") ``` himmelma@33175 ` 1598` ``` case False note cs = this ``` himmelma@33175 ` 1599` ``` from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover ``` himmelma@33175 ` 1600` ``` { fix y assume "y \ cball x e" ``` himmelma@33175 ` 1601` ``` hence False unfolding mem_cball using dist_nz[of x y] cs by auto } ``` himmelma@33175 ` 1602` ``` hence "cball x e = {}" by auto ``` himmelma@33175 ` 1603` ``` hence "interior (cball x e) = {}" using interior_empty by auto ``` himmelma@33175 ` 1604` ``` ultimately show ?thesis by blast ``` himmelma@33175 ` 1605` ```next ``` himmelma@33175 ` 1606` ``` case True note cs = this ``` himmelma@33175 ` 1607` ``` have "ball x e \ cball x e" using ball_subset_cball by auto moreover ``` himmelma@33175 ` 1608` ``` { fix S y assume as: "S \ cball x e" "open S" "y\S" ``` himmelma@33175 ` 1609` ``` then obtain d where "d>0" and d:"\x'. dist x' y < d \ x' \ S" unfolding open_dist by blast ``` himmelma@33175 ` 1610` himmelma@33175 ` 1611` ``` then obtain xa where xa_y: "xa \ y" and xa: "dist xa y < d" ``` himmelma@33175 ` 1612` ``` using perfect_choose_dist [of d] by auto ``` himmelma@33175 ` 1613` ``` have "xa\S" using d[THEN spec[where x=xa]] using xa by(auto simp add: dist_commute) ``` himmelma@33175 ` 1614` ``` hence xa_cball:"xa \ cball x e" using as(1) by auto ``` himmelma@33175 ` 1615` himmelma@33175 ` 1616` ``` hence "y \ ball x e" proof(cases "x = y") ``` himmelma@33175 ` 1617` ``` case True ``` himmelma@33175 ` 1618` ``` hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_commute) ``` himmelma@33175 ` 1619` ``` thus "y \ ball x e" using `x = y ` by simp ``` himmelma@33175 ` 1620` ``` next ``` himmelma@33175 ` 1621` ``` case False ``` himmelma@33175 ` 1622` ``` have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" unfolding dist_norm ``` himmelma@33175 ` 1623` ``` using `d>0` norm_ge_zero[of "y - x"] `x \ y` by auto ``` himmelma@33175 ` 1624` ``` hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \ cball x e" using d as(1)[unfolded subset_eq] by blast ``` himmelma@33175 ` 1625` ``` have "y - x \ 0" using `x \ y` by auto ``` himmelma@33175 ` 1626` ``` hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym] ``` himmelma@33175 ` 1627` ``` using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto ``` himmelma@33175 ` 1628` himmelma@33175 ` 1629` ``` have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x = norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)" ``` himmelma@33175 ` 1630` ``` by (auto simp add: dist_norm algebra_simps) ``` himmelma@33175 ` 1631` ``` also have "\ = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))" ``` himmelma@33175 ` 1632` ``` by (auto simp add: algebra_simps) ``` himmelma@33175 ` 1633` ``` also have "\ = \1 + d / (2 * norm (y - x))\ * norm (y - x)" ``` himmelma@33175 ` 1634` ``` using ** by auto ``` himmelma@33175 ` 1635` ``` also have "\ = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm) ``` himmelma@33175 ` 1636` ``` finally have "e \ dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute) ``` himmelma@33175 ` 1637` ``` thus "y \ ball x e" unfolding mem_ball using `d>0` by auto ``` himmelma@33175 ` 1638` ``` qed } ``` himmelma@33175 ` 1639` ``` hence "\S \ cball x e. open S \ S \ ball x e" by auto ``` himmelma@33175 ` 1640` ``` ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto ``` himmelma@33175 ` 1641` ```qed ``` himmelma@33175 ` 1642` himmelma@33175 ` 1643` ```lemma frontier_ball: ``` himmelma@33175 ` 1644` ``` fixes a :: "'a::real_normed_vector" ``` himmelma@33175 ` 1645` ``` shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}" ``` huffman@36362 ` 1646` ``` apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) ``` nipkow@39302 ` 1647` ``` apply (simp add: set_eq_iff) ``` himmelma@33175 ` 1648` ``` by arith ``` himmelma@33175 ` 1649` himmelma@33175 ` 1650` ```lemma frontier_cball: ``` himmelma@33175 ` 1651` ``` fixes a :: "'a::{real_normed_vector, perfect_space}" ``` himmelma@33175 ` 1652` ``` shows "frontier(cball a e) = {x. dist a x = e}" ``` huffman@36362 ` 1653` ``` apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) ``` nipkow@39302 ` 1654` ``` apply (simp add: set_eq_iff) ``` himmelma@33175 ` 1655` ``` by arith ``` himmelma@33175 ` 1656` himmelma@33175 ` 1657` ```lemma cball_eq_empty: "(cball x e = {}) \ e < 0" ``` nipkow@39302 ` 1658` ``` apply (simp add: set_eq_iff not_le) ``` himmelma@33175 ` 1659` ``` by (metis zero_le_dist dist_self order_less_le_trans) ``` himmelma@33175 ` 1660` ```lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty) ``` himmelma@33175 ` 1661` himmelma@33175 ` 1662` ```lemma cball_eq_sing: ``` huffman@44072 ` 1663` ``` fixes x :: "'a::{metric_space,perfect_space}" ``` himmelma@33175 ` 1664` ``` shows "(cball x e = {x}) \ e = 0" ``` himmelma@33175 ` 1665` ```proof (rule linorder_cases) ``` himmelma@33175 ` 1666` ``` assume e: "0 < e" ``` himmelma@33175 ` 1667` ``` obtain a where "a \ x" "dist a x < e" ``` himmelma@33175 ` 1668` ``` using perfect_choose_dist [OF e] by auto ``` himmelma@33175 ` 1669` ``` hence "a \ x" "dist x a \ e" by (auto simp add: dist_commute) ``` nipkow@39302 ` 1670` ``` with e show ?thesis by (auto simp add: set_eq_iff) ``` himmelma@33175 ` 1671` ```qed auto ``` himmelma@33175 ` 1672` himmelma@33175 ` 1673` ```lemma cball_sing: ``` himmelma@33175 ` 1674` ``` fixes x :: "'a::metric_space" ``` himmelma@33175 ` 1675` ``` shows "e = 0 ==> cball x e = {x}" ``` nipkow@39302 ` 1676` ``` by (auto simp add: set_eq_iff) ``` himmelma@33175 ` 1677` huffman@44210 ` 1678` huffman@44210 ` 1679` ```subsection {* Boundedness *} ``` himmelma@33175 ` 1680` himmelma@33175 ` 1681` ``` (* FIXME: This has to be unified with BSEQ!! *) ``` huffman@44207 ` 1682` ```definition (in metric_space) ``` huffman@44207 ` 1683` ``` bounded :: "'a set \ bool" where ``` himmelma@33175 ` 1684` ``` "bounded S \ (\x e. \y\S. dist x y \ e)" ``` himmelma@33175 ` 1685` himmelma@33175 ` 1686` ```lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" ``` himmelma@33175 ` 1687` ```unfolding bounded_def ``` himmelma@33175 ` 1688` ```apply safe ``` himmelma@33175 ` 1689` ```apply (rule_tac x="dist a x + e" in exI, clarify) ``` himmelma@33175 ` 1690` ```apply (drule (1) bspec) ``` himmelma@33175 ` 1691` ```apply (erule order_trans [OF dist_triangle add_left_mono]) ``` himmelma@33175 ` 1692` ```apply auto ``` himmelma@33175 ` 1693` ```done ``` himmelma@33175 ` 1694` himmelma@33175 ` 1695` ```lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" ``` himmelma@33175 ` 1696` ```unfolding bounded_any_center [where a=0] ``` himmelma@33175 ` 1697` ```by (simp add: dist_norm) ``` himmelma@33175 ` 1698` himmelma@33175 ` 1699` ```lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def) ``` himmelma@33175 ` 1700` ```lemma bounded_subset: "bounded T \ S \ T ==> bounded S" ``` himmelma@33175 ` 1701` ``` by (metis bounded_def subset_eq) ``` himmelma@33175 ` 1702` himmelma@33175 ` 1703` ```lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)" ``` himmelma@33175 ` 1704` ``` by (metis bounded_subset interior_subset) ``` himmelma@33175 ` 1705` himmelma@33175 ` 1706` ```lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)" ``` himmelma@33175 ` 1707` ```proof- ``` himmelma@33175 ` 1708` ``` from assms obtain x and a where a: "\y\S. dist x y \ a" unfolding bounded_def by auto ``` himmelma@33175 ` 1709` ``` { fix y assume "y \ closure S" ``` himmelma@33175 ` 1710` ``` then obtain f where f: "\n. f n \ S" "(f ---> y) sequentially" ``` himmelma@33175 ` 1711` ``` unfolding closure_sequential by auto ``` himmelma@33175 ` 1712` ``` have "\n. f n \ S \ dist x (f n) \ a" using a by simp ``` himmelma@33175 ` 1713` ``` hence "eventually (\n. dist x (f n) \ a) sequentially" ``` himmelma@33175 ` 1714` ``` by (rule eventually_mono, simp add: f(1)) ``` himmelma@33175 ` 1715` ``` have "dist x y \ a" ``` himmelma@33175 ` 1716` ``` apply (rule Lim_dist_ubound [of sequentially f]) ``` himmelma@33175 ` 1717` ``` apply (rule trivial_limit_sequentially) ``` himmelma@33175 ` 1718` ``` apply (rule f(2)) ``` himmelma@33175 ` 1719` ``` apply fact ``` himmelma@33175 ` 1720` ``` done ``` himmelma@33175 ` 1721` ``` } ``` himmelma@33175 ` 1722` ``` thus ?thesis unfolding bounded_def by auto ``` himmelma@33175 ` 1723` ```qed ``` himmelma@33175 ` 1724` himmelma@33175 ` 1725` ```lemma bounded_cball[simp,intro]: "bounded (cball x e)" ``` himmelma@33175 ` 1726` ``` apply (simp add: bounded_def) ``` himmelma@33175 ` 1727` ``` apply (rule_tac x=x in exI) ``` himmelma@33175 ` 1728` ``` apply (rule_tac x=e in exI) ``` himmelma@33175 ` 1729` ``` apply auto ``` himmelma@33175 ` 1730` ``` done ``` himmelma@33175 ` 1731` himmelma@33175 ` 1732` ```lemma bounded_ball[simp,intro]: "bounded(ball x e)" ``` himmelma@33175 ` 1733` ``` by (metis ball_subset_cball bounded_cball bounded_subset) ``` himmelma@33175 ` 1734` huffman@36362 ` 1735` ```lemma finite_imp_bounded[intro]: ``` huffman@36362 ` 1736` ``` fixes S :: "'a::metric_space set" assumes "finite S" shows "bounded S" ``` himmelma@33175 ` 1737` ```proof- ``` huffman@36362 ` 1738` ``` { fix a and F :: "'a set" assume as:"bounded F" ``` himmelma@33175 ` 1739` ``` then obtain x e where "\y\F. dist x y \ e" unfolding bounded_def by auto ``` himmelma@33175 ` 1740` ``` hence "\y\(insert a F). dist x y \ max e (dist x a)" by auto ``` himmelma@33175 ` 1741` ``` hence "bounded (insert a F)" unfolding bounded_def by (intro exI) ``` himmelma@33175 ` 1742` ``` } ``` himmelma@33175 ` 1743` ``` thus ?thesis using finite_induct[of S bounded] using bounded_empty assms by auto ``` himmelma@33175 ` 1744` ```qed ``` himmelma@33175 ` 1745` himmelma@33175 ` 1746` ```lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" ``` himmelma@33175 ` 1747` ``` apply (auto simp add: bounded_def) ``` himmelma@33175 ` 1748` ``` apply (rename_tac x y r s) ``` himmelma@33175 ` 1749` ``` apply (rule_tac x=x in exI) ``` himmelma@33175 ` 1750` ``` apply (rule_tac x="max r (dist x y + s)" in exI) ``` himmelma@33175 ` 1751` ``` apply (rule ballI, rename_tac z, safe) ``` himmelma@33175 ` 1752` ``` apply (drule (1) bspec, simp) ``` himmelma@33175 ` 1753` ``` apply (drule (1) bspec) ``` himmelma@33175 ` 1754` ``` apply (rule min_max.le_supI2) ``` himmelma@33175 ` 1755` ``` apply (erule order_trans [OF dist_triangle add_left_mono]) ``` himmelma@33175 ` 1756` ``` done ``` himmelma@33175 ` 1757` himmelma@33175 ` 1758` ```lemma bounded_Union[intro]: "finite F \ (\S\F. bounded S) \ bounded(\F)" ``` himmelma@33175 ` 1759` ``` by (induct rule: finite_induct[of F], auto) ``` himmelma@33175 ` 1760` himmelma@33175 ` 1761` ```lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x <= b)" ``` himmelma@33175 ` 1762` ``` apply (simp add: bounded_iff) ``` himmelma@33175 ` 1763` ``` apply (subgoal_tac "\x (y::real). 0 < 1 + abs y \ (x <= y \ x <= 1 + abs y)") ``` himmelma@33175 ` 1764` ``` by metis arith ``` himmelma@33175 ` 1765` himmelma@33175 ` 1766` ```lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" ``` himmelma@33175 ` 1767` ``` by (metis Int_lower1 Int_lower2 bounded_subset) ``` himmelma@33175 ` 1768` himmelma@33175 ` 1769` ```lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)" ``` himmelma@33175 ` 1770` ```apply (metis Diff_subset bounded_subset) ``` himmelma@33175 ` 1771` ```done ``` himmelma@33175 ` 1772` himmelma@33175 ` 1773` ```lemma bounded_insert[intro]:"bounded(insert x S) \ bounded S" ``` himmelma@33175 ` 1774` ``` by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI) ``` himmelma@33175 ` 1775` himmelma@33175 ` 1776` ```lemma not_bounded_UNIV[simp, intro]: ``` himmelma@33175 ` 1777` ``` "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" ``` himmelma@33175 ` 1778` ```proof(auto simp add: bounded_pos not_le) ``` himmelma@33175 ` 1779` ``` obtain x :: 'a where "x \ 0" ``` himmelma@33175 ` 1780` ``` using perfect_choose_dist [OF zero_less_one] by fast ``` himmelma@33175 ` 1781` ``` fix b::real assume b: "b >0" ``` himmelma@33175 ` 1782` ``` have b1: "b +1 \ 0" using b by simp ``` himmelma@33175 ` 1783` ``` with `x \ 0` have "b < norm (scaleR (b + 1) (sgn x))" ``` himmelma@33175 ` 1784` ``` by (simp add: norm_sgn) ``` himmelma@33175 ` 1785` ``` then show "\x::'a. b < norm x" .. ``` himmelma@33175 ` 1786` ```qed ``` himmelma@33175 ` 1787` himmelma@33175 ` 1788` ```lemma bounded_linear_image: ``` himmelma@33175 ` 1789` ``` assumes "bounded S" "bounded_linear f" ``` himmelma@33175 ` 1790` ``` shows "bounded(f ` S)" ``` himmelma@33175 ` 1791` ```proof- ``` himmelma@33175 ` 1792` ``` from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto ``` himmelma@33175 ` 1793` ``` from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) ``` himmelma@33175 ` 1794` ``` { fix x assume "x\S" ``` himmelma@33175 ` 1795` ``` hence "norm x \ b" using b by auto ``` himmelma@33175 ` 1796` ``` hence "norm (f x) \ B * b" using B(2) apply(erule_tac x=x in allE) ``` huffman@36778 ` 1797` ``` by (metis B(1) B(2) order_trans mult_le_cancel_left_pos) ``` himmelma@33175 ` 1798` ``` } ``` himmelma@33175 ` 1799` ``` thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI) ``` huffman@36778 ` 1800` ``` using b B mult_pos_pos [of b B] by (auto simp add: mult_commute) ``` himmelma@33175 ` 1801` ```qed ``` himmelma@33175 ` 1802` himmelma@33175 ` 1803` ```lemma bounded_scaling: ``` himmelma@33175 ` 1804` ``` fixes S :: "'a::real_normed_vector set" ``` himmelma@33175 ` 1805` ``` shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" ``` himmelma@33175 ` 1806` ``` apply (rule bounded_linear_image, assumption) ``` huffman@44282 ` 1807` ``` apply (rule bounded_linear_scaleR_right) ``` himmelma@33175 ` 1808` ``` done ``` himmelma@33175 ` 1809` himmelma@33175 ` 1810` ```lemma bounded_translation: ``` himmelma@33175 ` 1811` ``` fixes S :: "'a::real_normed_vector set" ``` himmelma@33175 ` 1812` ``` assumes "bounded S" shows "bounded ((\x. a + x) ` S)" ``` himmelma@33175 ` 1813` ```proof- ``` himmelma@33175 ` 1814` ``` from assms obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto ``` himmelma@33175 ` 1815` ``` { fix x assume "x\S" ``` himmelma@33175 ` 1816` ``` hence "norm (a + x) \ b + norm a" using norm_triangle_ineq[of a x] b by auto ``` himmelma@33175 ` 1817` ``` } ``` himmelma@33175 ` 1818` ``` thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"] ``` himmelma@33175 ` 1819` ``` by (auto intro!: add exI[of _ "b + norm a"]) ``` himmelma@33175 ` 1820` ```qed ``` himmelma@33175 ` 1821` himmelma@33175 ` 1822` himmelma@33175 ` 1823` ```text{* Some theorems on sups and infs using the notion "bounded". *} ``` himmelma@33175 ` 1824` himmelma@33175 ` 1825` ```lemma bounded_real: ``` himmelma@33175 ` 1826` ``` fixes S :: "real set" ``` himmelma@33175 ` 1827` ``` shows "bounded S \ (\a. \x\S. abs x <= a)" ``` himmelma@33175 ` 1828` ``` by (simp add: bounded_iff) ``` himmelma@33175 ` 1829` paulson@33270 ` 1830` ```lemma bounded_has_Sup: ``` paulson@33270 ` 1831` ``` fixes S :: "real set" ``` paulson@33270 ` 1832` ``` assumes "bounded S" "S \ {}" ``` paulson@33270 ` 1833` ``` shows "\x\S. x <= Sup S" and "\b. (\x\S. x <= b) \ Sup S <= b" ``` paulson@33270 ` 1834` ```proof ``` paulson@33270 ` 1835` ``` fix x assume "x\S" ``` paulson@33270 ` 1836` ``` thus "x \ Sup S" ``` paulson@33270 ` 1837` ``` by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real) ``` paulson@33270 ` 1838` ```next ``` paulson@33270 ` 1839` ``` show "\b. (\x\S. x \ b) \ Sup S \ b" using assms ``` paulson@33270 ` 1840` ``` by (metis SupInf.Sup_least) ``` paulson@33270 ` 1841` ```qed ``` paulson@33270 ` 1842` paulson@33270 ` 1843` ```lemma Sup_insert: ``` paulson@33270 ` 1844` ``` fixes S :: "real set" ``` paulson@33270 ` 1845` ``` shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" ``` paulson@33270 ` 1846` ```by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) ``` paulson@33270 ` 1847` paulson@33270 ` 1848` ```lemma Sup_insert_finite: ``` paulson@33270 ` 1849` ``` fixes S :: "real set" ``` paulson@33270 ` 1850` ``` shows "finite S \ Sup(insert x S) = (if S = {} then x else max x (Sup S))" ``` paulson@33270 ` 1851` ``` apply (rule Sup_insert) ``` paulson@33270 ` 1852` ``` apply (rule finite_imp_bounded) ``` paulson@33270 ` 1853` ``` by simp ``` paulson@33270 ` 1854` paulson@33270 ` 1855` ```lemma bounded_has_Inf: ``` paulson@33270 ` 1856` ``` fixes S :: "real set" ``` paulson@33270 ` 1857` ``` assumes "bounded S" "S \ {}" ``` paulson@33270 ` 1858` ``` shows "\x\S. x >= Inf S" and "\b. (\x\S. x >= b) \ Inf S >= b" ``` himmelma@33175 ` 1859` ```proof ``` himmelma@33175 ` 1860` ``` fix x assume "x\S" ``` himmelma@33175 ` 1861` ``` from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto ``` paulson@33270 ` 1862` ``` thus "x \ Inf S" using `x\S` ``` paulson@33270 ` 1863` ``` by (metis Inf_lower_EX abs_le_D2 minus_le_iff) ``` himmelma@33175 ` 1864` ```next ``` paulson@33270 ` 1865` ``` show "\b. (\x\S. x >= b) \ Inf S \ b" using assms ``` paulson@33270 ` 1866` ``` by (metis SupInf.Inf_greatest) ``` paulson@33270 ` 1867` ```qed ``` paulson@33270 ` 1868` paulson@33270 ` 1869` ```lemma Inf_insert: ``` paulson@33270 ` 1870` ``` fixes S :: "real set" ``` paulson@33270 ` 1871` ``` shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" ``` paulson@33270 ` 1872` ```by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) ``` paulson@33270 ` 1873` ```lemma Inf_insert_finite: ``` paulson@33270 ` 1874` ``` fixes S :: "real set" ``` paulson@33270 ` 1875` ``` shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" ``` paulson@33270 ` 1876` ``` by (rule Inf_insert, rule finite_imp_bounded, simp) ``` paulson@33270 ` 1877` himmelma@33175 ` 1878` ```(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *) ``` himmelma@33175 ` 1879` ```lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)" ``` himmelma@33175 ` 1880` ``` apply (frule isGlb_isLb) ``` himmelma@33175 ` 1881` ``` apply (frule_tac x = y in isGlb_isLb) ``` himmelma@33175 ` 1882` ``` apply (blast intro!: order_antisym dest!: isGlb_le_isLb) ``` himmelma@33175 ` 1883` ``` done ``` himmelma@33175 ` 1884` huffman@44210 ` 1885` huffman@36437 ` 1886` ```subsection {* Equivalent versions of compactness *} ``` huffman@36437 ` 1887` huffman@36437 ` 1888` ```subsubsection{* Sequential compactness *} ``` himmelma@33175 ` 1889` himmelma@33175 ` 1890` ```definition ``` himmelma@33175 ` 1891` ``` compact :: "'a::metric_space set \ bool" where (* TODO: generalize *) ``` himmelma@33175 ` 1892` ``` "compact S \ ``` himmelma@33175 ` 1893` ``` (\f. (\n. f n \ S) \ ``` himmelma@33175 ` 1894` ``` (\l\S. \r. subseq r \ ((f o r) ---> l) sequentially))" ``` himmelma@33175 ` 1895` huffman@44075 ` 1896` ```lemma compactI: ``` huffman@44075 ` 1897` ``` assumes "\f. \n. f n \ S \ \l\S. \r. subseq r \ ((f o r) ---> l) sequentially" ``` huffman@44075 ` 1898` ``` shows "compact S" ``` huffman@44075 ` 1899` ``` unfolding compact_def using assms by fast ``` huffman@44075 ` 1900` huffman@44075 ` 1901` ```lemma compactE: ``` huffman@44075 ` 1902` ``` assumes "compact S" "\n. f n \ S" ``` huffman@44075 ` 1903` ``` obtains l r where "l \ S" "subseq r" "((f \ r) ---> l) sequentially" ``` huffman@44075 ` 1904` ``` using assms unfolding compact_def by fast ``` huffman@44075 ` 1905` himmelma@33175 ` 1906` ```text {* ``` himmelma@33175 ` 1907` ``` A metric space (or topological vector space) is said to have the ``` himmelma@33175 ` 1908` ``` Heine-Borel property if every closed and bounded subset is compact. ``` himmelma@33175 ` 1909` ```*} ``` himmelma@33175 ` 1910` huffman@44207 ` 1911` ```class heine_borel = metric_space + ``` himmelma@33175 ` 1912` ``` assumes bounded_imp_convergent_subsequence: ``` himmelma@33175 ` 1913` ``` "bounded s \ \n. f n \ s ``` himmelma@33175 ` 1914` ``` \ \l r. subseq r \ ((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 1915` himmelma@33175 ` 1916` ```lemma bounded_closed_imp_compact: ``` himmelma@33175 ` 1917` ``` fixes s::"'a::heine_borel set" ``` himmelma@33175 ` 1918` ``` assumes "bounded s" and "closed s" shows "compact s" ``` himmelma@33175 ` 1919` ```proof (unfold compact_def, clarify) ``` himmelma@33175 ` 1920` ``` fix f :: "nat \ 'a" assume f: "\n. f n \ s" ``` himmelma@33175 ` 1921` ``` obtain l r where r: "subseq r" and l: "((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 1922` ``` using bounded_imp_convergent_subsequence [OF `bounded s` `\n. f n \ s`] by auto ``` himmelma@33175 ` 1923` ``` from f have fr: "\n. (f \ r) n \ s" by simp ``` himmelma@33175 ` 1924` ``` have "l \ s" using `closed s` fr l ``` himmelma@33175 ` 1925` ``` unfolding closed_sequential_limits by blast ``` himmelma@33175 ` 1926` ``` show "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 1927` ``` using `l \ s` r l by blast ``` himmelma@33175 ` 1928` ```qed ``` himmelma@33175 ` 1929` himmelma@33175 ` 1930` ```lemma subseq_bigger: assumes "subseq r" shows "n \ r n" ``` himmelma@33175 ` 1931` ```proof(induct n) ``` himmelma@33175 ` 1932` ``` show "0 \ r 0" by auto ``` himmelma@33175 ` 1933` ```next ``` himmelma@33175 ` 1934` ``` fix n assume "n \ r n" ``` himmelma@33175 ` 1935` ``` moreover have "r n < r (Suc n)" ``` himmelma@33175 ` 1936` ``` using assms [unfolded subseq_def] by auto ``` himmelma@33175 ` 1937` ``` ultimately show "Suc n \ r (Suc n)" by auto ``` himmelma@33175 ` 1938` ```qed ``` himmelma@33175 ` 1939` himmelma@33175 ` 1940` ```lemma eventually_subseq: ``` himmelma@33175 ` 1941` ``` assumes r: "subseq r" ``` himmelma@33175 ` 1942` ``` shows "eventually P sequentially \ eventually (\n. P (r n)) sequentially" ``` himmelma@33175 ` 1943` ```unfolding eventually_sequentially ``` himmelma@33175 ` 1944` ```by (metis subseq_bigger [OF r] le_trans) ``` himmelma@33175 ` 1945` himmelma@33175 ` 1946` ```lemma lim_subseq: ``` himmelma@33175 ` 1947` ``` "subseq r \ (s ---> l) sequentially \ ((s o r) ---> l) sequentially" ``` himmelma@33175 ` 1948` ```unfolding tendsto_def eventually_sequentially o_def ``` himmelma@33175 ` 1949` ```by (metis subseq_bigger le_trans) ``` himmelma@33175 ` 1950` himmelma@33175 ` 1951` ```lemma num_Axiom: "EX! g. g 0 = e \ (\n. g (Suc n) = f n (g n))" ``` himmelma@33175 ` 1952` ``` unfolding Ex1_def ``` himmelma@33175 ` 1953` ``` apply (rule_tac x="nat_rec e f" in exI) ``` himmelma@33175 ` 1954` ``` apply (rule conjI)+ ``` himmelma@33175 ` 1955` ```apply (rule def_nat_rec_0, simp) ``` himmelma@33175 ` 1956` ```apply (rule allI, rule def_nat_rec_Suc, simp) ``` himmelma@33175 ` 1957` ```apply (rule allI, rule impI, rule ext) ``` himmelma@33175 ` 1958` ```apply (erule conjE) ``` himmelma@33175 ` 1959` ```apply (induct_tac x) ``` huffman@36362 ` 1960` ```apply simp ``` himmelma@33175 ` 1961` ```apply (erule_tac x="n" in allE) ``` himmelma@33175 ` 1962` ```apply (simp) ``` himmelma@33175 ` 1963` ```done ``` himmelma@33175 ` 1964` himmelma@33175 ` 1965` ```lemma convergent_bounded_increasing: fixes s ::"nat\real" ``` himmelma@33175 ` 1966` ``` assumes "incseq s" and "\n. abs(s n) \ b" ``` himmelma@33175 ` 1967` ``` shows "\ l. \e::real>0. \ N. \n \ N. abs(s n - l) < e" ``` himmelma@33175 ` 1968` ```proof- ``` himmelma@33175 ` 1969` ``` have "isUb UNIV (range s) b" using assms(2) and abs_le_D1 unfolding isUb_def and setle_def by auto ``` himmelma@33175 ` 1970` ``` then obtain t where t:"isLub UNIV (range s) t" using reals_complete[of "range s" ] by auto ``` himmelma@33175 ` 1971` ``` { fix e::real assume "e>0" and as:"\N. \n\N. \ \s n - t\ < e" ``` himmelma@33175 ` 1972` ``` { fix n::nat ``` himmelma@33175 ` 1973` ``` obtain N where "N\n" and n:"\s N - t\ \ e" using as[THEN spec[where x=n]] by auto ``` himmelma@33175 ` 1974` ``` have "t \ s N" using isLub_isUb[OF t, unfolded isUb_def setle_def] by auto ``` himmelma@33175 ` 1975` ``` with n have "s N \ t - e" using `e>0` by auto ``` himmelma@33175 ` 1976` ``` hence "s n \ t - e" using assms(1)[unfolded incseq_def, THEN spec[where x=n], THEN spec[where x=N]] using `n\N` by auto } ``` himmelma@33175 ` 1977` ``` hence "isUb UNIV (range s) (t - e)" unfolding isUb_def and setle_def by auto ``` himmelma@33175 ` 1978` ``` hence False using isLub_le_isUb[OF t, of "t - e"] and `e>0` by auto } ``` himmelma@33175 ` 1979` ``` thus ?thesis by blast ``` himmelma@33175 ` 1980` ```qed ``` himmelma@33175 ` 1981` himmelma@33175 ` 1982` ```lemma convergent_bounded_monotone: fixes s::"nat \ real" ``` himmelma@33175 ` 1983` ``` assumes "\n. abs(s n) \ b" and "monoseq s" ``` himmelma@33175 ` 1984` ``` shows "\l. \e::real>0. \N. \n\N. abs(s n - l) < e" ``` himmelma@33175 ` 1985` ``` using convergent_bounded_increasing[of s b] assms using convergent_bounded_increasing[of "\n. - s n" b] ``` himmelma@33175 ` 1986` ``` unfolding monoseq_def incseq_def ``` himmelma@33175 ` 1987` ``` apply auto unfolding minus_add_distrib[THEN sym, unfolded diff_minus[THEN sym]] ``` himmelma@33175 ` 1988` ``` unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto ``` himmelma@33175 ` 1989` hoelzl@37489 ` 1990` ```(* TODO: merge this lemma with the ones above *) ``` hoelzl@37489 ` 1991` ```lemma bounded_increasing_convergent: fixes s::"nat \ real" ``` hoelzl@37489 ` 1992` ``` assumes "bounded {s n| n::nat. True}" "\n. (s n) \(s(Suc n))" ``` hoelzl@37489 ` 1993` ``` shows "\l. (s ---> l) sequentially" ``` hoelzl@37489 ` 1994` ```proof- ``` hoelzl@37489 ` 1995` ``` obtain a where a:"\n. \ (s n)\ \ a" using assms(1)[unfolded bounded_iff] by auto ``` hoelzl@37489 ` 1996` ``` { fix m::nat ``` hoelzl@37489 ` 1997` ``` have "\ n. n\m \ (s m) \ (s n)" ``` hoelzl@37489 ` 1998` ``` apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) ``` hoelzl@37489 ` 1999` ``` apply(case_tac "m \ na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq) } ``` hoelzl@37489 ` 2000` ``` hence "\m n. m \ n \ (s m) \ (s n)" by auto ``` hoelzl@37489 ` 2001` ``` then obtain l where "\e>0. \N. \n\N. \ (s n) - l\ < e" using convergent_bounded_monotone[OF a] ``` hoelzl@37489 ` 2002` ``` unfolding monoseq_def by auto ``` hoelzl@37489 ` 2003` ``` thus ?thesis unfolding Lim_sequentially apply(rule_tac x="l" in exI) ``` hoelzl@37489 ` 2004` ``` unfolding dist_norm by auto ``` hoelzl@37489 ` 2005` ```qed ``` hoelzl@37489 ` 2006` himmelma@33175 ` 2007` ```lemma compact_real_lemma: ``` himmelma@33175 ` 2008` ``` assumes "\n::nat. abs(s n) \ b" ``` himmelma@33175 ` 2009` ``` shows "\(l::real) r. subseq r \ ((s \ r) ---> l) sequentially" ``` himmelma@33175 ` 2010` ```proof- ``` himmelma@33175 ` 2011` ``` obtain r where r:"subseq r" "monoseq (\n. s (r n))" ``` himmelma@33175 ` 2012` ``` using seq_monosub[of s] by auto ``` himmelma@33175 ` 2013` ``` thus ?thesis using convergent_bounded_monotone[of "\n. s (r n)" b] and assms ``` himmelma@33175 ` 2014` ``` unfolding tendsto_iff dist_norm eventually_sequentially by auto ``` himmelma@33175 ` 2015` ```qed ``` himmelma@33175 ` 2016` himmelma@33175 ` 2017` ```instance real :: heine_borel ``` himmelma@33175 ` 2018` ```proof ``` himmelma@33175 ` 2019` ``` fix s :: "real set" and f :: "nat \ real" ``` himmelma@33175 ` 2020` ``` assume s: "bounded s" and f: "\n. f n \ s" ``` himmelma@33175 ` 2021` ``` then obtain b where b: "\n. abs (f n) \ b" ``` himmelma@33175 ` 2022` ``` unfolding bounded_iff by auto ``` himmelma@33175 ` 2023` ``` obtain l :: real and r :: "nat \ nat" where ``` himmelma@33175 ` 2024` ``` r: "subseq r" and l: "((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 2025` ``` using compact_real_lemma [OF b] by auto ``` himmelma@33175 ` 2026` ``` thus "\l r. subseq r \ ((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 2027` ``` by auto ``` himmelma@33175 ` 2028` ```qed ``` himmelma@33175 ` 2029` huffman@44138 ` 2030` ```lemma bounded_component: "bounded s \ bounded ((\x. x \$\$ i) ` s)" ``` huffman@44138 ` 2031` ``` apply (erule bounded_linear_image) ``` huffman@44138 ` 2032` ``` apply (rule bounded_linear_euclidean_component) ``` huffman@44138 ` 2033` ``` done ``` himmelma@33175 ` 2034` himmelma@33175 ` 2035` ```lemma compact_lemma: ``` hoelzl@37489 ` 2036` ``` fixes f :: "nat \ 'a::euclidean_space" ``` himmelma@33175 ` 2037` ``` assumes "bounded s" and "\n. f n \ s" ``` hoelzl@37489 ` 2038` ``` shows "\d. \l::'a. \ r. subseq r \ ``` hoelzl@37489 ` 2039` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)" ``` himmelma@33175 ` 2040` ```proof ``` hoelzl@37489 ` 2041` ``` fix d'::"nat set" def d \ "d' \ {..{..l::'a. \r. subseq r \ ``` hoelzl@37489 ` 2044` ``` (\e>0. eventually (\n. \i\d. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)" ``` himmelma@33175 ` 2045` ``` proof(induct d) case empty thus ?case unfolding subseq_def by auto ``` hoelzl@37489 ` 2046` ``` next case (insert k d) have k[intro]:"kx. x \$\$ k) ` s)" using `bounded s` by (rule bounded_component) ``` hoelzl@37489 ` 2048` ``` obtain l1::"'a" and r1 where r1:"subseq r1" and ``` hoelzl@37489 ` 2049` ``` lr1:"\e>0. eventually (\n. \i\d. dist (f (r1 n) \$\$ i) (l1 \$\$ i) < e) sequentially" ``` hoelzl@37489 ` 2050` ``` using insert(3) using insert(4) by auto ``` hoelzl@37489 ` 2051` ``` have f': "\n. f (r1 n) \$\$ k \ (\x. x \$\$ k) ` s" using `\n. f n \ s` by simp ``` hoelzl@37489 ` 2052` ``` obtain l2 r2 where r2:"subseq r2" and lr2:"((\i. f (r1 (r2 i)) \$\$ k) ---> l2) sequentially" ``` himmelma@33175 ` 2053` ``` using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto ``` himmelma@33175 ` 2054` ``` def r \ "r1 \ r2" have r:"subseq r" ``` himmelma@33175 ` 2055` ``` using r1 and r2 unfolding r_def o_def subseq_def by auto ``` himmelma@33175 ` 2056` ``` moreover ``` hoelzl@37489 ` 2057` ``` def l \ "(\\ i. if i = k then l2 else l1\$\$i)::'a" ``` himmelma@33175 ` 2058` ``` { fix e::real assume "e>0" ``` hoelzl@37489 ` 2059` ``` from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) \$\$ i) (l1 \$\$ i) < e) sequentially" by blast ``` hoelzl@37489 ` 2060` ``` from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) \$\$ k) l2 < e) sequentially" by (rule tendstoD) ``` hoelzl@37489 ` 2061` ``` from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) \$\$ i) (l1 \$\$ i) < e) sequentially" ``` himmelma@33175 ` 2062` ``` by (rule eventually_subseq) ``` hoelzl@37489 ` 2063` ``` have "eventually (\n. \i\(insert k d). dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially" ``` hoelzl@37489 ` 2064` ``` using N1' N2 apply(rule eventually_elim2) unfolding l_def r_def o_def ``` hoelzl@37489 ` 2065` ``` using insert.prems by auto ``` himmelma@33175 ` 2066` ``` } ``` himmelma@33175 ` 2067` ``` ultimately show ?case by auto ``` himmelma@33175 ` 2068` ``` qed ``` hoelzl@37489 ` 2069` ``` thus "\l::'a. \r. subseq r \ ``` hoelzl@37489 ` 2070` ``` (\e>0. eventually (\n. \i\d'. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)" ``` hoelzl@37489 ` 2071` ``` apply safe apply(rule_tac x=l in exI,rule_tac x=r in exI) apply safe ``` hoelzl@37489 ` 2072` ``` apply(erule_tac x=e in allE) unfolding d_def eventually_sequentially apply safe ``` hoelzl@37489 ` 2073` ``` apply(rule_tac x=N in exI) apply safe apply(erule_tac x=n in allE,safe) ``` hoelzl@37489 ` 2074` ``` apply(erule_tac x=i in ballE) ``` hoelzl@37489 ` 2075` ``` proof- fix i and r::"nat=>nat" and n::nat and e::real and l::'a ``` hoelzl@37489 ` 2076` ``` assume "i\d'" "i \ d' \ {..0" ``` hoelzl@37489 ` 2077` ``` hence *:"i\DIM('a)" by auto ``` hoelzl@37489 ` 2078` ``` thus "dist (f (r n) \$\$ i) (l \$\$ i) < e" using e by auto ``` hoelzl@37489 ` 2079` ``` qed ``` hoelzl@37489 ` 2080` ```qed ``` hoelzl@37489 ` 2081` hoelzl@37489 ` 2082` ```instance euclidean_space \ heine_borel ``` himmelma@33175 ` 2083` ```proof ``` hoelzl@37489 ` 2084` ``` fix s :: "'a set" and f :: "nat \ 'a" ``` himmelma@33175 ` 2085` ``` assume s: "bounded s" and f: "\n. f n \ s" ``` hoelzl@37489 ` 2086` ``` then obtain l::'a and r where r: "subseq r" ``` hoelzl@37489 ` 2087` ``` and l: "\e>0. eventually (\n. \i\UNIV. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially" ``` himmelma@33175 ` 2088` ``` using compact_lemma [OF s f] by blast ``` hoelzl@37489 ` 2089` ``` let ?d = "{..0" ``` himmelma@33175 ` 2091` ``` hence "0 < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 2092` ``` using DIM_positive using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto ``` hoelzl@37489 ` 2093` ``` with l have "eventually (\n. \i. dist (f (r n) \$\$ i) (l \$\$ i) < e / (real_of_nat (card ?d))) sequentially" ``` himmelma@33175 ` 2094` ``` by simp ``` himmelma@33175 ` 2095` ``` moreover ``` hoelzl@37489 ` 2096` ``` { fix n assume n: "\i. dist (f (r n) \$\$ i) (l \$\$ i) < e / (real_of_nat (card ?d))" ``` hoelzl@37489 ` 2097` ``` have "dist (f (r n)) l \ (\i\?d. dist (f (r n) \$\$ i) (l \$\$ i))" ``` hoelzl@37489 ` 2098` ``` apply(subst euclidean_dist_l2) using zero_le_dist by (rule setL2_le_setsum) ``` himmelma@33175 ` 2099` ``` also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" ``` hoelzl@37489 ` 2100` ``` apply(rule setsum_strict_mono) using n by auto ``` hoelzl@37489 ` 2101` ``` finally have "dist (f (r n)) l < e" unfolding setsum_constant ``` hoelzl@37489 ` 2102` ``` using DIM_positive[where 'a='a] by auto ``` himmelma@33175 ` 2103` ``` } ``` himmelma@33175 ` 2104` ``` ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" ``` himmelma@33175 ` 2105` ``` by (rule eventually_elim1) ``` himmelma@33175 ` 2106` ``` } ``` himmelma@33175 ` 2107` ``` hence *:"((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp ``` himmelma@33175 ` 2108` ``` with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto ``` himmelma@33175 ` 2109` ```qed ``` himmelma@33175 ` 2110` himmelma@33175 ` 2111` ```lemma bounded_fst: "bounded s \ bounded (fst ` s)" ``` himmelma@33175 ` 2112` ```unfolding bounded_def ``` himmelma@33175 ` 2113` ```apply clarify ``` himmelma@33175 ` 2114` ```apply (rule_tac x="a" in exI) ``` himmelma@33175 ` 2115` ```apply (rule_tac x="e" in exI) ``` himmelma@33175 ` 2116` ```apply clarsimp ``` himmelma@33175 ` 2117` ```apply (drule (1) bspec) ``` himmelma@33175 ` 2118` ```apply (simp add: dist_Pair_Pair) ``` himmelma@33175 ` 2119` ```apply (erule order_trans [OF real_sqrt_sum_squares_ge1]) ``` himmelma@33175 ` 2120` ```done ``` himmelma@33175 ` 2121` himmelma@33175 ` 2122` ```lemma bounded_snd: "bounded s \ bounded (snd ` s)" ``` himmelma@33175 ` 2123` ```unfolding bounded_def ``` himmelma@33175 ` 2124` ```apply clarify ``` himmelma@33175 ` 2125` ```apply (rule_tac x="b" in exI) ``` himmelma@33175 ` 2126` ```apply (rule_tac x="e" in exI) ``` himmelma@33175 ` 2127` ```apply clarsimp ``` himmelma@33175 ` 2128` ```apply (drule (1) bspec) ``` himmelma@33175 ` 2129` ```apply (simp add: dist_Pair_Pair) ``` himmelma@33175 ` 2130` ```apply (erule order_trans [OF real_sqrt_sum_squares_ge2]) ``` himmelma@33175 ` 2131` ```done ``` himmelma@33175 ` 2132` haftmann@37678 ` 2133` ```instance prod :: (heine_borel, heine_borel) heine_borel ``` himmelma@33175 ` 2134` ```proof ``` himmelma@33175 ` 2135` ``` fix s :: "('a * 'b) set" and f :: "nat \ 'a * 'b" ``` himmelma@33175 ` 2136` ``` assume s: "bounded s" and f: "\n. f n \ s" ``` himmelma@33175 ` 2137` ``` from s have s1: "bounded (fst ` s)" by (rule bounded_fst) ``` himmelma@33175 ` 2138` ``` from f have f1: "\n. fst (f n) \ fst ` s" by simp ``` himmelma@33175 ` 2139` ``` obtain l1 r1 where r1: "subseq r1" ``` himmelma@33175 ` 2140` ``` and l1: "((\n. fst (f (r1 n))) ---> l1) sequentially" ``` himmelma@33175 ` 2141` ``` using bounded_imp_convergent_subsequence [OF s1 f1] ``` himmelma@33175 ` 2142` ``` unfolding o_def by fast ``` himmelma@33175 ` 2143` ``` from s have s2: "bounded (snd ` s)" by (rule bounded_snd) ``` himmelma@33175 ` 2144` ``` from f have f2: "\n. snd (f (r1 n)) \ snd ` s" by simp ``` himmelma@33175 ` 2145` ``` obtain l2 r2 where r2: "subseq r2" ``` himmelma@33175 ` 2146` ``` and l2: "((\n. snd (f (r1 (r2 n)))) ---> l2) sequentially" ``` himmelma@33175 ` 2147` ``` using bounded_imp_convergent_subsequence [OF s2 f2] ``` himmelma@33175 ` 2148` ``` unfolding o_def by fast ``` himmelma@33175 ` 2149` ``` have l1': "((\n. fst (f (r1 (r2 n)))) ---> l1) sequentially" ``` himmelma@33175 ` 2150` ``` using lim_subseq [OF r2 l1] unfolding o_def . ``` himmelma@33175 ` 2151` ``` have l: "((f \ (r1 \ r2)) ---> (l1, l2)) sequentially" ``` himmelma@33175 ` 2152` ``` using tendsto_Pair [OF l1' l2] unfolding o_def by simp ``` himmelma@33175 ` 2153` ``` have r: "subseq (r1 \ r2)" ``` himmelma@33175 ` 2154` ``` using r1 r2 unfolding subseq_def by simp ``` himmelma@33175 ` 2155` ``` show "\l r. subseq r \ ((f \ r) ---> l) sequentially" ``` himmelma@33175 ` 2156` ``` using l r by fast ``` himmelma@33175 ` 2157` ```qed ``` himmelma@33175 ` 2158` huffman@36437 ` 2159` ```subsubsection{* Completeness *} ``` himmelma@33175 ` 2160` himmelma@33175 ` 2161` ```lemma cauchy_def: ``` himmelma@33175 ` 2162` ``` "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N --> dist(s m)(s n) < e)" ``` himmelma@33175 ` 2163` ```unfolding Cauchy_def by blast ``` himmelma@33175 ` 2164` himmelma@33175 ` 2165` ```definition ``` himmelma@33175 ` 2166` ``` complete :: "'a::metric_space set \ bool" where ``` himmelma@33175 ` 2167` ``` "complete s \ (\f. (\n. f n \ s) \ Cauchy f ``` himmelma@33175 ` 2168` ``` --> (\l \ s. (f ---> l) sequentially))" ``` himmelma@33175 ` 2169` himmelma@33175 ` 2170` ```lemma cauchy: "Cauchy s \ (\e>0.\ N::nat. \n\N. dist(s n)(s N) < e)" (is "?lhs = ?rhs") ``` himmelma@33175 ` 2171` ```proof- ``` himmelma@33175 ` 2172` ``` { assume ?rhs ``` himmelma@33175 ` 2173` ``` { fix e::real ``` himmelma@33175 ` 2174` ``` assume "e>0" ``` himmelma@33175 ` 2175` ``` with `?rhs` obtain N where N:"\n\N. dist (s n) (s N) < e/2" ``` himmelma@33175 ` 2176` ``` by (erule_tac x="e/2" in allE) auto ``` himmelma@33175 ` 2177` ``` { fix n m ``` himmelma@33175 ` 2178` ``` assume nm:"N \ m \ N \ n" ``` himmelma@33175 ` 2179` ``` hence "dist (s m) (s n) < e" using N ``` himmelma@33175 ` 2180` ``` using dist_triangle_half_l[of "s m" "s N" "e" "s n"] ``` himmelma@33175 ` 2181` ``` by blast ``` himmelma@33175 ` 2182` ``` } ``` himmelma@33175 ` 2183` ``` hence "\N. \m n. N \ m \ N \ n \ dist (s m) (s n) < e" ``` himmelma@33175 ` 2184` ``` by blast ``` himmelma@33175 ` 2185` ``` } ``` himmelma@33175 ` 2186` ``` hence ?lhs ``` himmelma@33175 ` 2187` ``` unfolding cauchy_def ``` himmelma@33175 ` 2188` ``` by blast ``` himmelma@33175 ` 2189` ``` } ``` himmelma@33175 ` 2190` ``` thus ?thesis ``` himmelma@33175 ` 2191` ``` unfolding cauchy_def ``` himmelma@33175 ` 2192` ``` using dist_triangle_half_l ``` himmelma@33175 ` 2193` ``` by blast ``` himmelma@33175 ` 2194` ```qed ``` himmelma@33175 ` 2195` himmelma@33175 ` 2196` ```lemma convergent_imp_cauchy: ``` himmelma@33175 ` 2197` ``` "(s ---> l) sequentially ==> Cauchy s" ``` himmelma@33175 ` 2198` ```proof(simp only: cauchy_def, rule, rule) ``` himmelma@33175 ` 2199` ``` fix e::real assume "e>0" "(s ---> l) sequentially" ``` himmelma@33175 ` 2200` ``` then obtain N::nat where N:"\n\N. dist (s n) l < e/2" unfolding Lim_sequentially by(erule_tac x="e/2" in allE) auto ``` himmelma@33175 ` 2201` ``` thus "\N. \m n. N \ m \ N \ n \ dist (s m) (s n) < e" using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto ``` himmelma@33175 ` 2202` ```qed ``` himmelma@33175 ` 2203` huffman@34104 ` 2204` ```lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" ``` himmelma@33175 ` 2205` ```proof- ``` himmelma@33175 ` 2206` ``` from assms obtain N::nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto ``` himmelma@33175 ` 2207` ``` hence N:"\n. N \ n \ dist (s N) (s n) < 1" by auto ``` himmelma@33175 ` 2208` ``` moreover ``` himmelma@33175 ` 2209` ``` have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto ``` himmelma@33175 ` 2210` ``` then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" ``` himmelma@33175 ` 2211` ``` unfolding bounded_any_center [where a="s N"] by auto ``` himmelma@33175 ` 2212` ``` ultimately show "?thesis" ``` himmelma@33175 ` 2213` ``` unfolding bounded_any_center [where a="s N"] ``` himmelma@33175 ` 2214` ``` apply(rule_tac x="max a 1" in exI) apply auto ``` huffman@34104 ` 2215` ``` apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto ``` himmelma@33175 ` 2216` ```qed ``` himmelma@33175 ` 2217` himmelma@33175 ` 2218` ```lemma compact_imp_complete: assumes "compact s" shows "complete s" ``` himmelma@33175 ` 2219` ```proof- ``` himmelma@33175 ` 2220` ``` { fix f assume as: "(\n::nat. f n \ s)" "Cauchy f" ``` himmelma@33175 ` 2221` ``` from as(1) obtain l r where lr: "l\s" "subseq r" "((f \ r) ---> l) sequentially" using assms unfolding compact_def by blast ``` himmelma@33175 ` 2222` himmelma@33175 ` 2223` ``` note lr' = subseq_bigger [OF lr(2)] ``` himmelma@33175 ` 2224` himmelma@33175 ` 2225` ``` { fix e::real assume "e>0" ``` himmelma@33175 ` 2226` ``` from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto ``` himmelma@33175 ` 2227` ``` from lr(3)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" using `e>0` by auto ``` himmelma@33175 ` 2228` ``` { fix n::nat assume n:"n \ max N M" ``` himmelma@33175 ` 2229` ``` have "dist ((f \ r) n) l < e/2" using n M by auto ``` himmelma@33175 ` 2230` ``` moreover have "r n \ N" using lr'[of n] n by auto ``` himmelma@33175 ` 2231` ``` hence "dist (f n) ((f \ r) n) < e / 2" using N using n by auto ``` himmelma@33175 ` 2232` ``` ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) } ``` himmelma@33175 ` 2233` ``` hence "\N. \n\N. dist (f n) l < e" by blast } ``` himmelma@33175 ` 2234` ``` hence "\l\s. (f ---> l) sequentially" using `l\s` unfolding Lim_sequentially by auto } ``` himmelma@33175 ` 2235` ``` thus ?thesis unfolding complete_def by auto ``` himmelma@33175 ` 2236` ```qed ``` himmelma@33175 ` 2237` himmelma@33175 ` 2238` ```instance heine_borel < complete_space ``` himmelma@33175 ` 2239` ```proof ``` himmelma@33175 ` 2240` ``` fix f :: "nat \ 'a" assume "Cauchy f" ``` huffman@34104 ` 2241` ``` hence "bounded (range f)" ``` huffman@34104 ` 2242` ``` by (rule cauchy_imp_bounded) ``` himmelma@33175 ` 2243` ``` hence "compact (closure (range f))" ``` himmelma@33175 ` 2244` ``` using bounded_closed_imp_compact [of "closure (range f)"] by auto ``` himmelma@33175 ` 2245` ``` hence "complete (closure (range f))" ``` huffman@34104 ` 2246` ``` by (rule compact_imp_complete) ``` himmelma@33175 ` 2247` ``` moreover have "\n. f n \ closure (range f)" ``` himmelma@33175 ` 2248` ``` using closure_subset [of "range f"] by auto ``` himmelma@33175 ` 2249` ``` ultimately have "\l\closure (range f). (f ---> l) sequentially" ``` himmelma@33175 ` 2250` ``` using `Cauchy f` unfolding complete_def by auto ``` himmelma@33175 ` 2251` ``` then show "convergent f" ``` huffman@36660 ` 2252` ``` unfolding convergent_def by auto ``` himmelma@33175 ` 2253` ```qed ``` himmelma@33175 ` 2254` himmelma@33175 ` 2255` ```lemma complete_univ: "complete (UNIV :: 'a::complete_space set)" ``` himmelma@33175 ` 2256` ```proof(simp add: complete_def, rule, rule) ``` himmelma@33175 ` 2257` ``` fix f :: "nat \ 'a" assume "Cauchy f" ``` himmelma@33175 ` 2258` ``` hence "convergent f" by (rule Cauchy_convergent) ```