src/HOL/Limits.thy
 author huffman Mon Aug 08 19:26:53 2011 -0700 (2011-08-08) changeset 44081 730f7cced3a6 parent 44079 bcc60791b7b9 child 44194 0639898074ae permissions -rw-r--r--
rename type 'a net to 'a filter, following standard mathematical terminology
 huffman@31349 ` 1` ```(* Title : Limits.thy ``` huffman@31349 ` 2` ``` Author : Brian Huffman ``` huffman@31349 ` 3` ```*) ``` huffman@31349 ` 4` huffman@31349 ` 5` ```header {* Filters and Limits *} ``` huffman@31349 ` 6` huffman@31349 ` 7` ```theory Limits ``` huffman@36822 ` 8` ```imports RealVector ``` huffman@31349 ` 9` ```begin ``` huffman@31349 ` 10` huffman@44081 ` 11` ```subsection {* Filters *} ``` huffman@31392 ` 12` huffman@31392 ` 13` ```text {* ``` huffman@44081 ` 14` ``` This definition also allows non-proper filters. ``` huffman@31392 ` 15` ```*} ``` huffman@31392 ` 16` huffman@36358 ` 17` ```locale is_filter = ``` huffman@44081 ` 18` ``` fixes F :: "('a \ bool) \ bool" ``` huffman@44081 ` 19` ``` assumes True: "F (\x. True)" ``` huffman@44081 ` 20` ``` assumes conj: "F (\x. P x) \ F (\x. Q x) \ F (\x. P x \ Q x)" ``` huffman@44081 ` 21` ``` assumes mono: "\x. P x \ Q x \ F (\x. P x) \ F (\x. Q x)" ``` huffman@36358 ` 22` huffman@44081 ` 23` ```typedef (open) 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}" ``` huffman@31392 ` 24` ```proof ``` huffman@44081 ` 25` ``` show "(\x. True) \ ?filter" by (auto intro: is_filter.intro) ``` huffman@31392 ` 26` ```qed ``` huffman@31349 ` 27` huffman@44081 ` 28` ```lemma is_filter_Rep_filter: "is_filter (Rep_filter A)" ``` huffman@44081 ` 29` ``` using Rep_filter [of A] by simp ``` huffman@31392 ` 30` huffman@44081 ` 31` ```lemma Abs_filter_inverse': ``` huffman@44081 ` 32` ``` assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" ``` huffman@44081 ` 33` ``` using assms by (simp add: Abs_filter_inverse) ``` huffman@31392 ` 34` huffman@31392 ` 35` huffman@31392 ` 36` ```subsection {* Eventually *} ``` huffman@31349 ` 37` huffman@44081 ` 38` ```definition eventually :: "('a \ bool) \ 'a filter \ bool" ``` huffman@44081 ` 39` ``` where "eventually P A \ Rep_filter A P" ``` huffman@36358 ` 40` huffman@44081 ` 41` ```lemma eventually_Abs_filter: ``` huffman@44081 ` 42` ``` assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" ``` huffman@44081 ` 43` ``` unfolding eventually_def using assms by (simp add: Abs_filter_inverse) ``` huffman@31349 ` 44` huffman@44081 ` 45` ```lemma filter_eq_iff: ``` huffman@44081 ` 46` ``` shows "A = B \ (\P. eventually P A = eventually P B)" ``` huffman@44081 ` 47` ``` unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. ``` huffman@36360 ` 48` huffman@44081 ` 49` ```lemma eventually_True [simp]: "eventually (\x. True) A" ``` huffman@44081 ` 50` ``` unfolding eventually_def ``` huffman@44081 ` 51` ``` by (rule is_filter.True [OF is_filter_Rep_filter]) ``` huffman@31349 ` 52` huffman@44081 ` 53` ```lemma always_eventually: "\x. P x \ eventually P A" ``` huffman@36630 ` 54` ```proof - ``` huffman@36630 ` 55` ``` assume "\x. P x" hence "P = (\x. True)" by (simp add: ext) ``` huffman@44081 ` 56` ``` thus "eventually P A" by simp ``` huffman@36630 ` 57` ```qed ``` huffman@36630 ` 58` huffman@31349 ` 59` ```lemma eventually_mono: ``` huffman@44081 ` 60` ``` "(\x. P x \ Q x) \ eventually P A \ eventually Q A" ``` huffman@44081 ` 61` ``` unfolding eventually_def ``` huffman@44081 ` 62` ``` by (rule is_filter.mono [OF is_filter_Rep_filter]) ``` huffman@31349 ` 63` huffman@31349 ` 64` ```lemma eventually_conj: ``` huffman@44081 ` 65` ``` assumes P: "eventually (\x. P x) A" ``` huffman@44081 ` 66` ``` assumes Q: "eventually (\x. Q x) A" ``` huffman@44081 ` 67` ``` shows "eventually (\x. P x \ Q x) A" ``` huffman@44081 ` 68` ``` using assms unfolding eventually_def ``` huffman@44081 ` 69` ``` by (rule is_filter.conj [OF is_filter_Rep_filter]) ``` huffman@31349 ` 70` huffman@31349 ` 71` ```lemma eventually_mp: ``` huffman@44081 ` 72` ``` assumes "eventually (\x. P x \ Q x) A" ``` huffman@44081 ` 73` ``` assumes "eventually (\x. P x) A" ``` huffman@44081 ` 74` ``` shows "eventually (\x. Q x) A" ``` huffman@31349 ` 75` ```proof (rule eventually_mono) ``` huffman@31349 ` 76` ``` show "\x. (P x \ Q x) \ P x \ Q x" by simp ``` huffman@44081 ` 77` ``` show "eventually (\x. (P x \ Q x) \ P x) A" ``` huffman@31349 ` 78` ``` using assms by (rule eventually_conj) ``` huffman@31349 ` 79` ```qed ``` huffman@31349 ` 80` huffman@31349 ` 81` ```lemma eventually_rev_mp: ``` huffman@44081 ` 82` ``` assumes "eventually (\x. P x) A" ``` huffman@44081 ` 83` ``` assumes "eventually (\x. P x \ Q x) A" ``` huffman@44081 ` 84` ``` shows "eventually (\x. Q x) A" ``` huffman@31349 ` 85` ```using assms(2) assms(1) by (rule eventually_mp) ``` huffman@31349 ` 86` huffman@31349 ` 87` ```lemma eventually_conj_iff: ``` huffman@44081 ` 88` ``` "eventually (\x. P x \ Q x) A \ eventually P A \ eventually Q A" ``` huffman@44081 ` 89` ``` by (auto intro: eventually_conj elim: eventually_rev_mp) ``` huffman@31349 ` 90` huffman@31349 ` 91` ```lemma eventually_elim1: ``` huffman@44081 ` 92` ``` assumes "eventually (\i. P i) A" ``` huffman@31349 ` 93` ``` assumes "\i. P i \ Q i" ``` huffman@44081 ` 94` ``` shows "eventually (\i. Q i) A" ``` huffman@44081 ` 95` ``` using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 96` huffman@31349 ` 97` ```lemma eventually_elim2: ``` huffman@44081 ` 98` ``` assumes "eventually (\i. P i) A" ``` huffman@44081 ` 99` ``` assumes "eventually (\i. Q i) A" ``` huffman@31349 ` 100` ``` assumes "\i. P i \ Q i \ R i" ``` huffman@44081 ` 101` ``` shows "eventually (\i. R i) A" ``` huffman@44081 ` 102` ``` using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 103` huffman@36360 ` 104` ```subsection {* Finer-than relation *} ``` huffman@36360 ` 105` huffman@44081 ` 106` ```text {* @{term "A \ B"} means that filter @{term A} is finer than ``` huffman@44081 ` 107` ```filter @{term B}. *} ``` huffman@36360 ` 108` huffman@44081 ` 109` ```instantiation filter :: (type) complete_lattice ``` huffman@36360 ` 110` ```begin ``` huffman@36360 ` 111` huffman@44081 ` 112` ```definition le_filter_def: ``` huffman@44081 ` 113` ``` "A \ B \ (\P. eventually P B \ eventually P A)" ``` huffman@36360 ` 114` huffman@36360 ` 115` ```definition ``` huffman@44081 ` 116` ``` "(A :: 'a filter) < B \ A \ B \ \ B \ A" ``` huffman@36360 ` 117` huffman@36360 ` 118` ```definition ``` huffman@44081 ` 119` ``` "top = Abs_filter (\P. \x. P x)" ``` huffman@36630 ` 120` huffman@36630 ` 121` ```definition ``` huffman@44081 ` 122` ``` "bot = Abs_filter (\P. True)" ``` huffman@36360 ` 123` huffman@36630 ` 124` ```definition ``` huffman@44081 ` 125` ``` "sup A B = Abs_filter (\P. eventually P A \ eventually P B)" ``` huffman@36630 ` 126` huffman@36630 ` 127` ```definition ``` huffman@44081 ` 128` ``` "inf A B = Abs_filter ``` huffman@44081 ` 129` ``` (\P. \Q R. eventually Q A \ eventually R B \ (\x. Q x \ R x \ P x))" ``` huffman@36630 ` 130` huffman@36630 ` 131` ```definition ``` huffman@44081 ` 132` ``` "Sup S = Abs_filter (\P. \A\S. eventually P A)" ``` huffman@36630 ` 133` huffman@36630 ` 134` ```definition ``` huffman@44081 ` 135` ``` "Inf S = Sup {A::'a filter. \B\S. A \ B}" ``` huffman@36630 ` 136` huffman@36630 ` 137` ```lemma eventually_top [simp]: "eventually P top \ (\x. P x)" ``` huffman@44081 ` 138` ``` unfolding top_filter_def ``` huffman@44081 ` 139` ``` by (rule eventually_Abs_filter, rule is_filter.intro, auto) ``` huffman@36630 ` 140` huffman@36629 ` 141` ```lemma eventually_bot [simp]: "eventually P bot" ``` huffman@44081 ` 142` ``` unfolding bot_filter_def ``` huffman@44081 ` 143` ``` by (subst eventually_Abs_filter, rule is_filter.intro, auto) ``` huffman@36360 ` 144` huffman@36630 ` 145` ```lemma eventually_sup: ``` huffman@44081 ` 146` ``` "eventually P (sup A B) \ eventually P A \ eventually P B" ``` huffman@44081 ` 147` ``` unfolding sup_filter_def ``` huffman@44081 ` 148` ``` by (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 149` ``` (auto elim!: eventually_rev_mp) ``` huffman@36630 ` 150` huffman@36630 ` 151` ```lemma eventually_inf: ``` huffman@44081 ` 152` ``` "eventually P (inf A B) \ ``` huffman@44081 ` 153` ``` (\Q R. eventually Q A \ eventually R B \ (\x. Q x \ R x \ P x))" ``` huffman@44081 ` 154` ``` unfolding inf_filter_def ``` huffman@44081 ` 155` ``` apply (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 156` ``` apply (fast intro: eventually_True) ``` huffman@44081 ` 157` ``` apply clarify ``` huffman@44081 ` 158` ``` apply (intro exI conjI) ``` huffman@44081 ` 159` ``` apply (erule (1) eventually_conj) ``` huffman@44081 ` 160` ``` apply (erule (1) eventually_conj) ``` huffman@44081 ` 161` ``` apply simp ``` huffman@44081 ` 162` ``` apply auto ``` huffman@44081 ` 163` ``` done ``` huffman@36630 ` 164` huffman@36630 ` 165` ```lemma eventually_Sup: ``` huffman@44081 ` 166` ``` "eventually P (Sup S) \ (\A\S. eventually P A)" ``` huffman@44081 ` 167` ``` unfolding Sup_filter_def ``` huffman@44081 ` 168` ``` apply (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 169` ``` apply (auto intro: eventually_conj elim!: eventually_rev_mp) ``` huffman@44081 ` 170` ``` done ``` huffman@36630 ` 171` huffman@36360 ` 172` ```instance proof ``` huffman@44081 ` 173` ``` fix A B :: "'a filter" show "A < B \ A \ B \ \ B \ A" ``` huffman@44081 ` 174` ``` by (rule less_filter_def) ``` huffman@36360 ` 175` ```next ``` huffman@44081 ` 176` ``` fix A :: "'a filter" show "A \ A" ``` huffman@44081 ` 177` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 178` ```next ``` huffman@44081 ` 179` ``` fix A B C :: "'a filter" assume "A \ B" and "B \ C" thus "A \ C" ``` huffman@44081 ` 180` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 181` ```next ``` huffman@44081 ` 182` ``` fix A B :: "'a filter" assume "A \ B" and "B \ A" thus "A = B" ``` huffman@44081 ` 183` ``` unfolding le_filter_def filter_eq_iff by fast ``` huffman@36360 ` 184` ```next ``` huffman@44081 ` 185` ``` fix A :: "'a filter" show "A \ top" ``` huffman@44081 ` 186` ``` unfolding le_filter_def eventually_top by (simp add: always_eventually) ``` huffman@36630 ` 187` ```next ``` huffman@44081 ` 188` ``` fix A :: "'a filter" show "bot \ A" ``` huffman@44081 ` 189` ``` unfolding le_filter_def by simp ``` huffman@36630 ` 190` ```next ``` huffman@44081 ` 191` ``` fix A B :: "'a filter" show "A \ sup A B" and "B \ sup A B" ``` huffman@44081 ` 192` ``` unfolding le_filter_def eventually_sup by simp_all ``` huffman@36630 ` 193` ```next ``` huffman@44081 ` 194` ``` fix A B C :: "'a filter" assume "A \ C" and "B \ C" thus "sup A B \ C" ``` huffman@44081 ` 195` ``` unfolding le_filter_def eventually_sup by simp ``` huffman@36630 ` 196` ```next ``` huffman@44081 ` 197` ``` fix A B :: "'a filter" show "inf A B \ A" and "inf A B \ B" ``` huffman@44081 ` 198` ``` unfolding le_filter_def eventually_inf by (auto intro: eventually_True) ``` huffman@36630 ` 199` ```next ``` huffman@44081 ` 200` ``` fix A B C :: "'a filter" assume "A \ B" and "A \ C" thus "A \ inf B C" ``` huffman@44081 ` 201` ``` unfolding le_filter_def eventually_inf ``` huffman@36630 ` 202` ``` by (auto elim!: eventually_mono intro: eventually_conj) ``` huffman@36630 ` 203` ```next ``` huffman@44081 ` 204` ``` fix A :: "'a filter" and S assume "A \ S" thus "A \ Sup S" ``` huffman@44081 ` 205` ``` unfolding le_filter_def eventually_Sup by simp ``` huffman@36630 ` 206` ```next ``` huffman@44081 ` 207` ``` fix S and B :: "'a filter" assume "\A. A \ S \ A \ B" thus "Sup S \ B" ``` huffman@44081 ` 208` ``` unfolding le_filter_def eventually_Sup by simp ``` huffman@36630 ` 209` ```next ``` huffman@44081 ` 210` ``` fix C :: "'a filter" and S assume "C \ S" thus "Inf S \ C" ``` huffman@44081 ` 211` ``` unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp ``` huffman@36630 ` 212` ```next ``` huffman@44081 ` 213` ``` fix S and A :: "'a filter" assume "\B. B \ S \ A \ B" thus "A \ Inf S" ``` huffman@44081 ` 214` ``` unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp ``` huffman@36360 ` 215` ```qed ``` huffman@36360 ` 216` huffman@36360 ` 217` ```end ``` huffman@36360 ` 218` huffman@44081 ` 219` ```lemma filter_leD: ``` huffman@44081 ` 220` ``` "A \ B \ eventually P B \ eventually P A" ``` huffman@44081 ` 221` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 222` huffman@44081 ` 223` ```lemma filter_leI: ``` huffman@44081 ` 224` ``` "(\P. eventually P B \ eventually P A) \ A \ B" ``` huffman@44081 ` 225` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 226` huffman@36360 ` 227` ```lemma eventually_False: ``` huffman@44081 ` 228` ``` "eventually (\x. False) A \ A = bot" ``` huffman@44081 ` 229` ``` unfolding filter_eq_iff by (auto elim: eventually_rev_mp) ``` huffman@36360 ` 230` huffman@44081 ` 231` ```subsection {* Map function for filters *} ``` huffman@36654 ` 232` huffman@44081 ` 233` ```definition filtermap :: "('a \ 'b) \ 'a filter \ 'b filter" ``` huffman@44081 ` 234` ``` where "filtermap f A = Abs_filter (\P. eventually (\x. P (f x)) A)" ``` huffman@36654 ` 235` huffman@44081 ` 236` ```lemma eventually_filtermap: ``` huffman@44081 ` 237` ``` "eventually P (filtermap f A) = eventually (\x. P (f x)) A" ``` huffman@44081 ` 238` ``` unfolding filtermap_def ``` huffman@44081 ` 239` ``` apply (rule eventually_Abs_filter) ``` huffman@44081 ` 240` ``` apply (rule is_filter.intro) ``` huffman@44081 ` 241` ``` apply (auto elim!: eventually_rev_mp) ``` huffman@44081 ` 242` ``` done ``` huffman@36654 ` 243` huffman@44081 ` 244` ```lemma filtermap_ident: "filtermap (\x. x) A = A" ``` huffman@44081 ` 245` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 246` huffman@44081 ` 247` ```lemma filtermap_filtermap: ``` huffman@44081 ` 248` ``` "filtermap f (filtermap g A) = filtermap (\x. f (g x)) A" ``` huffman@44081 ` 249` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 250` huffman@44081 ` 251` ```lemma filtermap_mono: "A \ B \ filtermap f A \ filtermap f B" ``` huffman@44081 ` 252` ``` unfolding le_filter_def eventually_filtermap by simp ``` huffman@44081 ` 253` huffman@44081 ` 254` ```lemma filtermap_bot [simp]: "filtermap f bot = bot" ``` huffman@44081 ` 255` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 256` huffman@36654 ` 257` huffman@36662 ` 258` ```subsection {* Sequentially *} ``` huffman@31392 ` 259` huffman@44081 ` 260` ```definition sequentially :: "nat filter" ``` huffman@44081 ` 261` ``` where "sequentially = Abs_filter (\P. \k. \n\k. P n)" ``` huffman@31392 ` 262` huffman@36662 ` 263` ```lemma eventually_sequentially: ``` huffman@36662 ` 264` ``` "eventually P sequentially \ (\N. \n\N. P n)" ``` huffman@36662 ` 265` ```unfolding sequentially_def ``` huffman@44081 ` 266` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@36662 ` 267` ``` fix P Q :: "nat \ bool" ``` huffman@36662 ` 268` ``` assume "\i. \n\i. P n" and "\j. \n\j. Q n" ``` huffman@36662 ` 269` ``` then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto ``` huffman@36662 ` 270` ``` then have "\n\max i j. P n \ Q n" by simp ``` huffman@36662 ` 271` ``` then show "\k. \n\k. P n \ Q n" .. ``` huffman@36662 ` 272` ```qed auto ``` huffman@36662 ` 273` huffman@36662 ` 274` ```lemma sequentially_bot [simp]: "sequentially \ bot" ``` huffman@44081 ` 275` ``` unfolding filter_eq_iff eventually_sequentially by auto ``` huffman@36662 ` 276` huffman@36662 ` 277` ```lemma eventually_False_sequentially [simp]: ``` huffman@36662 ` 278` ``` "\ eventually (\n. False) sequentially" ``` huffman@44081 ` 279` ``` by (simp add: eventually_False) ``` huffman@36662 ` 280` huffman@36662 ` 281` ```lemma le_sequentially: ``` huffman@44081 ` 282` ``` "A \ sequentially \ (\N. eventually (\n. N \ n) A)" ``` huffman@44081 ` 283` ``` unfolding le_filter_def eventually_sequentially ``` huffman@44081 ` 284` ``` by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) ``` huffman@36662 ` 285` huffman@36662 ` 286` huffman@44081 ` 287` ```definition trivial_limit :: "'a filter \ bool" ``` huffman@44081 ` 288` ``` where "trivial_limit A \ eventually (\x. False) A" ``` hoelzl@41970 ` 289` huffman@44081 ` 290` ```lemma trivial_limit_sequentially [intro]: "\ trivial_limit sequentially" ``` hoelzl@41970 ` 291` ``` by (auto simp add: trivial_limit_def eventually_sequentially) ``` hoelzl@41970 ` 292` huffman@44081 ` 293` ```subsection {* Standard filters *} ``` huffman@36662 ` 294` huffman@44081 ` 295` ```definition within :: "'a filter \ 'a set \ 'a filter" (infixr "within" 70) ``` huffman@44081 ` 296` ``` where "A within S = Abs_filter (\P. eventually (\x. x \ S \ P x) A)" ``` huffman@31392 ` 297` huffman@44081 ` 298` ```definition nhds :: "'a::topological_space \ 'a filter" ``` huffman@44081 ` 299` ``` where "nhds a = Abs_filter (\P. \S. open S \ a \ S \ (\x\S. P x))" ``` huffman@36654 ` 300` huffman@44081 ` 301` ```definition at :: "'a::topological_space \ 'a filter" ``` huffman@44081 ` 302` ``` where "at a = nhds a within - {a}" ``` huffman@31447 ` 303` huffman@31392 ` 304` ```lemma eventually_within: ``` huffman@44081 ` 305` ``` "eventually P (A within S) = eventually (\x. x \ S \ P x) A" ``` huffman@44081 ` 306` ``` unfolding within_def ``` huffman@44081 ` 307` ``` by (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 308` ``` (auto elim!: eventually_rev_mp) ``` huffman@31392 ` 309` huffman@44081 ` 310` ```lemma within_UNIV: "A within UNIV = A" ``` huffman@44081 ` 311` ``` unfolding filter_eq_iff eventually_within by simp ``` huffman@36360 ` 312` huffman@36654 ` 313` ```lemma eventually_nhds: ``` huffman@36654 ` 314` ``` "eventually P (nhds a) \ (\S. open S \ a \ S \ (\x\S. P x))" ``` huffman@36654 ` 315` ```unfolding nhds_def ``` huffman@44081 ` 316` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@36654 ` 317` ``` have "open UNIV \ a \ UNIV \ (\x\UNIV. True)" by simp ``` huffman@36654 ` 318` ``` thus "\S. open S \ a \ S \ (\x\S. True)" by - rule ``` huffman@36358 ` 319` ```next ``` huffman@36358 ` 320` ``` fix P Q ``` huffman@36654 ` 321` ``` assume "\S. open S \ a \ S \ (\x\S. P x)" ``` huffman@36654 ` 322` ``` and "\T. open T \ a \ T \ (\x\T. Q x)" ``` huffman@36358 ` 323` ``` then obtain S T where ``` huffman@36654 ` 324` ``` "open S \ a \ S \ (\x\S. P x)" ``` huffman@36654 ` 325` ``` "open T \ a \ T \ (\x\T. Q x)" by auto ``` huffman@36654 ` 326` ``` hence "open (S \ T) \ a \ S \ T \ (\x\(S \ T). P x \ Q x)" ``` huffman@36358 ` 327` ``` by (simp add: open_Int) ``` huffman@36654 ` 328` ``` thus "\S. open S \ a \ S \ (\x\S. P x \ Q x)" by - rule ``` huffman@36358 ` 329` ```qed auto ``` huffman@31447 ` 330` huffman@36656 ` 331` ```lemma eventually_nhds_metric: ``` huffman@36656 ` 332` ``` "eventually P (nhds a) \ (\d>0. \x. dist x a < d \ P x)" ``` huffman@36656 ` 333` ```unfolding eventually_nhds open_dist ``` huffman@31447 ` 334` ```apply safe ``` huffman@31447 ` 335` ```apply fast ``` huffman@31492 ` 336` ```apply (rule_tac x="{x. dist x a < d}" in exI, simp) ``` huffman@31447 ` 337` ```apply clarsimp ``` huffman@31447 ` 338` ```apply (rule_tac x="d - dist x a" in exI, clarsimp) ``` huffman@31447 ` 339` ```apply (simp only: less_diff_eq) ``` huffman@31447 ` 340` ```apply (erule le_less_trans [OF dist_triangle]) ``` huffman@31447 ` 341` ```done ``` huffman@31447 ` 342` huffman@36656 ` 343` ```lemma eventually_at_topological: ``` huffman@36656 ` 344` ``` "eventually P (at a) \ (\S. open S \ a \ S \ (\x\S. x \ a \ P x))" ``` huffman@36656 ` 345` ```unfolding at_def eventually_within eventually_nhds by simp ``` huffman@36656 ` 346` huffman@36656 ` 347` ```lemma eventually_at: ``` huffman@36656 ` 348` ``` fixes a :: "'a::metric_space" ``` huffman@36656 ` 349` ``` shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" ``` huffman@36656 ` 350` ```unfolding at_def eventually_within eventually_nhds_metric by auto ``` huffman@36656 ` 351` huffman@31392 ` 352` huffman@31355 ` 353` ```subsection {* Boundedness *} ``` huffman@31355 ` 354` huffman@44081 ` 355` ```definition Bfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44081 ` 356` ``` where "Bfun f A = (\K>0. eventually (\x. norm (f x) \ K) A)" ``` huffman@31355 ` 357` huffman@31487 ` 358` ```lemma BfunI: ``` huffman@44081 ` 359` ``` assumes K: "eventually (\x. norm (f x) \ K) A" shows "Bfun f A" ``` huffman@31355 ` 360` ```unfolding Bfun_def ``` huffman@31355 ` 361` ```proof (intro exI conjI allI) ``` huffman@31355 ` 362` ``` show "0 < max K 1" by simp ``` huffman@31355 ` 363` ```next ``` huffman@44081 ` 364` ``` show "eventually (\x. norm (f x) \ max K 1) A" ``` huffman@31355 ` 365` ``` using K by (rule eventually_elim1, simp) ``` huffman@31355 ` 366` ```qed ``` huffman@31355 ` 367` huffman@31355 ` 368` ```lemma BfunE: ``` huffman@44081 ` 369` ``` assumes "Bfun f A" ``` huffman@44081 ` 370` ``` obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) A" ``` huffman@31355 ` 371` ```using assms unfolding Bfun_def by fast ``` huffman@31355 ` 372` huffman@31355 ` 373` huffman@31349 ` 374` ```subsection {* Convergence to Zero *} ``` huffman@31349 ` 375` huffman@44081 ` 376` ```definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44081 ` 377` ``` where "Zfun f A = (\r>0. eventually (\x. norm (f x) < r) A)" ``` huffman@31349 ` 378` huffman@31349 ` 379` ```lemma ZfunI: ``` huffman@44081 ` 380` ``` "(\r. 0 < r \ eventually (\x. norm (f x) < r) A) \ Zfun f A" ``` huffman@44081 ` 381` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 382` huffman@31349 ` 383` ```lemma ZfunD: ``` huffman@44081 ` 384` ``` "\Zfun f A; 0 < r\ \ eventually (\x. norm (f x) < r) A" ``` huffman@44081 ` 385` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 386` huffman@31355 ` 387` ```lemma Zfun_ssubst: ``` huffman@44081 ` 388` ``` "eventually (\x. f x = g x) A \ Zfun g A \ Zfun f A" ``` huffman@44081 ` 389` ``` unfolding Zfun_def by (auto elim!: eventually_rev_mp) ``` huffman@31355 ` 390` huffman@44081 ` 391` ```lemma Zfun_zero: "Zfun (\x. 0) A" ``` huffman@44081 ` 392` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 393` huffman@44081 ` 394` ```lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) A = Zfun (\x. f x) A" ``` huffman@44081 ` 395` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 396` huffman@31349 ` 397` ```lemma Zfun_imp_Zfun: ``` huffman@44081 ` 398` ``` assumes f: "Zfun f A" ``` huffman@44081 ` 399` ``` assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) A" ``` huffman@44081 ` 400` ``` shows "Zfun (\x. g x) A" ``` huffman@31349 ` 401` ```proof (cases) ``` huffman@31349 ` 402` ``` assume K: "0 < K" ``` huffman@31349 ` 403` ``` show ?thesis ``` huffman@31349 ` 404` ``` proof (rule ZfunI) ``` huffman@31349 ` 405` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 406` ``` hence "0 < r / K" ``` huffman@31349 ` 407` ``` using K by (rule divide_pos_pos) ``` huffman@44081 ` 408` ``` then have "eventually (\x. norm (f x) < r / K) A" ``` huffman@31487 ` 409` ``` using ZfunD [OF f] by fast ``` huffman@44081 ` 410` ``` with g show "eventually (\x. norm (g x) < r) A" ``` huffman@31355 ` 411` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 412` ``` fix x ``` huffman@31487 ` 413` ``` assume *: "norm (g x) \ norm (f x) * K" ``` huffman@31487 ` 414` ``` assume "norm (f x) < r / K" ``` huffman@31487 ` 415` ``` hence "norm (f x) * K < r" ``` huffman@31349 ` 416` ``` by (simp add: pos_less_divide_eq K) ``` huffman@31487 ` 417` ``` thus "norm (g x) < r" ``` huffman@31355 ` 418` ``` by (simp add: order_le_less_trans [OF *]) ``` huffman@31349 ` 419` ``` qed ``` huffman@31349 ` 420` ``` qed ``` huffman@31349 ` 421` ```next ``` huffman@31349 ` 422` ``` assume "\ 0 < K" ``` huffman@31349 ` 423` ``` hence K: "K \ 0" by (simp only: not_less) ``` huffman@31355 ` 424` ``` show ?thesis ``` huffman@31355 ` 425` ``` proof (rule ZfunI) ``` huffman@31355 ` 426` ``` fix r :: real ``` huffman@31355 ` 427` ``` assume "0 < r" ``` huffman@44081 ` 428` ``` from g show "eventually (\x. norm (g x) < r) A" ``` huffman@31355 ` 429` ``` proof (rule eventually_elim1) ``` huffman@31487 ` 430` ``` fix x ``` huffman@31487 ` 431` ``` assume "norm (g x) \ norm (f x) * K" ``` huffman@31487 ` 432` ``` also have "\ \ norm (f x) * 0" ``` huffman@31355 ` 433` ``` using K norm_ge_zero by (rule mult_left_mono) ``` huffman@31487 ` 434` ``` finally show "norm (g x) < r" ``` huffman@31355 ` 435` ``` using `0 < r` by simp ``` huffman@31355 ` 436` ``` qed ``` huffman@31355 ` 437` ``` qed ``` huffman@31349 ` 438` ```qed ``` huffman@31349 ` 439` huffman@44081 ` 440` ```lemma Zfun_le: "\Zfun g A; \x. norm (f x) \ norm (g x)\ \ Zfun f A" ``` huffman@44081 ` 441` ``` by (erule_tac K="1" in Zfun_imp_Zfun, simp) ``` huffman@31349 ` 442` huffman@31349 ` 443` ```lemma Zfun_add: ``` huffman@44081 ` 444` ``` assumes f: "Zfun f A" and g: "Zfun g A" ``` huffman@44081 ` 445` ``` shows "Zfun (\x. f x + g x) A" ``` huffman@31349 ` 446` ```proof (rule ZfunI) ``` huffman@31349 ` 447` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 448` ``` hence r: "0 < r / 2" by simp ``` huffman@44081 ` 449` ``` have "eventually (\x. norm (f x) < r/2) A" ``` huffman@31487 ` 450` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 451` ``` moreover ``` huffman@44081 ` 452` ``` have "eventually (\x. norm (g x) < r/2) A" ``` huffman@31487 ` 453` ``` using g r by (rule ZfunD) ``` huffman@31349 ` 454` ``` ultimately ``` huffman@44081 ` 455` ``` show "eventually (\x. norm (f x + g x) < r) A" ``` huffman@31349 ` 456` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 457` ``` fix x ``` huffman@31487 ` 458` ``` assume *: "norm (f x) < r/2" "norm (g x) < r/2" ``` huffman@31487 ` 459` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@31349 ` 460` ``` by (rule norm_triangle_ineq) ``` huffman@31349 ` 461` ``` also have "\ < r/2 + r/2" ``` huffman@31349 ` 462` ``` using * by (rule add_strict_mono) ``` huffman@31487 ` 463` ``` finally show "norm (f x + g x) < r" ``` huffman@31349 ` 464` ``` by simp ``` huffman@31349 ` 465` ``` qed ``` huffman@31349 ` 466` ```qed ``` huffman@31349 ` 467` huffman@44081 ` 468` ```lemma Zfun_minus: "Zfun f A \ Zfun (\x. - f x) A" ``` huffman@44081 ` 469` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 470` huffman@44081 ` 471` ```lemma Zfun_diff: "\Zfun f A; Zfun g A\ \ Zfun (\x. f x - g x) A" ``` huffman@44081 ` 472` ``` by (simp only: diff_minus Zfun_add Zfun_minus) ``` huffman@31349 ` 473` huffman@31349 ` 474` ```lemma (in bounded_linear) Zfun: ``` huffman@44081 ` 475` ``` assumes g: "Zfun g A" ``` huffman@44081 ` 476` ``` shows "Zfun (\x. f (g x)) A" ``` huffman@31349 ` 477` ```proof - ``` huffman@31349 ` 478` ``` obtain K where "\x. norm (f x) \ norm x * K" ``` huffman@31349 ` 479` ``` using bounded by fast ``` huffman@44081 ` 480` ``` then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) A" ``` huffman@31355 ` 481` ``` by simp ``` huffman@31487 ` 482` ``` with g show ?thesis ``` huffman@31349 ` 483` ``` by (rule Zfun_imp_Zfun) ``` huffman@31349 ` 484` ```qed ``` huffman@31349 ` 485` huffman@31349 ` 486` ```lemma (in bounded_bilinear) Zfun: ``` huffman@44081 ` 487` ``` assumes f: "Zfun f A" ``` huffman@44081 ` 488` ``` assumes g: "Zfun g A" ``` huffman@44081 ` 489` ``` shows "Zfun (\x. f x ** g x) A" ``` huffman@31349 ` 490` ```proof (rule ZfunI) ``` huffman@31349 ` 491` ``` fix r::real assume r: "0 < r" ``` huffman@31349 ` 492` ``` obtain K where K: "0 < K" ``` huffman@31349 ` 493` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31349 ` 494` ``` using pos_bounded by fast ``` huffman@31349 ` 495` ``` from K have K': "0 < inverse K" ``` huffman@31349 ` 496` ``` by (rule positive_imp_inverse_positive) ``` huffman@44081 ` 497` ``` have "eventually (\x. norm (f x) < r) A" ``` huffman@31487 ` 498` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 499` ``` moreover ``` huffman@44081 ` 500` ``` have "eventually (\x. norm (g x) < inverse K) A" ``` huffman@31487 ` 501` ``` using g K' by (rule ZfunD) ``` huffman@31349 ` 502` ``` ultimately ``` huffman@44081 ` 503` ``` show "eventually (\x. norm (f x ** g x) < r) A" ``` huffman@31349 ` 504` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 505` ``` fix x ``` huffman@31487 ` 506` ``` assume *: "norm (f x) < r" "norm (g x) < inverse K" ``` huffman@31487 ` 507` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31349 ` 508` ``` by (rule norm_le) ``` huffman@31487 ` 509` ``` also have "norm (f x) * norm (g x) * K < r * inverse K * K" ``` huffman@31349 ` 510` ``` by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K) ``` huffman@31349 ` 511` ``` also from K have "r * inverse K * K = r" ``` huffman@31349 ` 512` ``` by simp ``` huffman@31487 ` 513` ``` finally show "norm (f x ** g x) < r" . ``` huffman@31349 ` 514` ``` qed ``` huffman@31349 ` 515` ```qed ``` huffman@31349 ` 516` huffman@31349 ` 517` ```lemma (in bounded_bilinear) Zfun_left: ``` huffman@44081 ` 518` ``` "Zfun f A \ Zfun (\x. f x ** a) A" ``` huffman@44081 ` 519` ``` by (rule bounded_linear_left [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 520` huffman@31349 ` 521` ```lemma (in bounded_bilinear) Zfun_right: ``` huffman@44081 ` 522` ``` "Zfun f A \ Zfun (\x. a ** f x) A" ``` huffman@44081 ` 523` ``` by (rule bounded_linear_right [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 524` huffman@31349 ` 525` ```lemmas Zfun_mult = mult.Zfun ``` huffman@31349 ` 526` ```lemmas Zfun_mult_right = mult.Zfun_right ``` huffman@31349 ` 527` ```lemmas Zfun_mult_left = mult.Zfun_left ``` huffman@31349 ` 528` huffman@31349 ` 529` wenzelm@31902 ` 530` ```subsection {* Limits *} ``` huffman@31349 ` 531` huffman@44081 ` 532` ```definition tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a filter \ bool" ``` haftmann@37767 ` 533` ``` (infixr "--->" 55) where ``` huffman@44081 ` 534` ``` "(f ---> l) A \ (\S. open S \ l \ S \ eventually (\x. f x \ S) A)" ``` huffman@31349 ` 535` wenzelm@31902 ` 536` ```ML {* ``` wenzelm@31902 ` 537` ```structure Tendsto_Intros = Named_Thms ``` wenzelm@31902 ` 538` ```( ``` wenzelm@31902 ` 539` ``` val name = "tendsto_intros" ``` wenzelm@31902 ` 540` ``` val description = "introduction rules for tendsto" ``` wenzelm@31902 ` 541` ```) ``` huffman@31565 ` 542` ```*} ``` huffman@31565 ` 543` wenzelm@31902 ` 544` ```setup Tendsto_Intros.setup ``` huffman@31565 ` 545` huffman@44081 ` 546` ```lemma tendsto_mono: "A \ A' \ (f ---> l) A' \ (f ---> l) A" ``` huffman@44081 ` 547` ``` unfolding tendsto_def le_filter_def by fast ``` huffman@36656 ` 548` huffman@31488 ` 549` ```lemma topological_tendstoI: ``` huffman@44081 ` 550` ``` "(\S. open S \ l \ S \ eventually (\x. f x \ S) A) ``` huffman@44081 ` 551` ``` \ (f ---> l) A" ``` huffman@31349 ` 552` ``` unfolding tendsto_def by auto ``` huffman@31349 ` 553` huffman@31488 ` 554` ```lemma topological_tendstoD: ``` huffman@44081 ` 555` ``` "(f ---> l) A \ open S \ l \ S \ eventually (\x. f x \ S) A" ``` huffman@31488 ` 556` ``` unfolding tendsto_def by auto ``` huffman@31488 ` 557` huffman@31488 ` 558` ```lemma tendstoI: ``` huffman@44081 ` 559` ``` assumes "\e. 0 < e \ eventually (\x. dist (f x) l < e) A" ``` huffman@44081 ` 560` ``` shows "(f ---> l) A" ``` huffman@44081 ` 561` ``` apply (rule topological_tendstoI) ``` huffman@44081 ` 562` ``` apply (simp add: open_dist) ``` huffman@44081 ` 563` ``` apply (drule (1) bspec, clarify) ``` huffman@44081 ` 564` ``` apply (drule assms) ``` huffman@44081 ` 565` ``` apply (erule eventually_elim1, simp) ``` huffman@44081 ` 566` ``` done ``` huffman@31488 ` 567` huffman@31349 ` 568` ```lemma tendstoD: ``` huffman@44081 ` 569` ``` "(f ---> l) A \ 0 < e \ eventually (\x. dist (f x) l < e) A" ``` huffman@44081 ` 570` ``` apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) ``` huffman@44081 ` 571` ``` apply (clarsimp simp add: open_dist) ``` huffman@44081 ` 572` ``` apply (rule_tac x="e - dist x l" in exI, clarsimp) ``` huffman@44081 ` 573` ``` apply (simp only: less_diff_eq) ``` huffman@44081 ` 574` ``` apply (erule le_less_trans [OF dist_triangle]) ``` huffman@44081 ` 575` ``` apply simp ``` huffman@44081 ` 576` ``` apply simp ``` huffman@44081 ` 577` ``` done ``` huffman@31488 ` 578` huffman@31488 ` 579` ```lemma tendsto_iff: ``` huffman@44081 ` 580` ``` "(f ---> l) A \ (\e>0. eventually (\x. dist (f x) l < e) A)" ``` huffman@44081 ` 581` ``` using tendstoI tendstoD by fast ``` huffman@31349 ` 582` huffman@44081 ` 583` ```lemma tendsto_Zfun_iff: "(f ---> a) A = Zfun (\x. f x - a) A" ``` huffman@44081 ` 584` ``` by (simp only: tendsto_iff Zfun_def dist_norm) ``` huffman@31349 ` 585` huffman@31565 ` 586` ```lemma tendsto_ident_at [tendsto_intros]: "((\x. x) ---> a) (at a)" ``` huffman@44081 ` 587` ``` unfolding tendsto_def eventually_at_topological by auto ``` huffman@31565 ` 588` huffman@31565 ` 589` ```lemma tendsto_ident_at_within [tendsto_intros]: ``` huffman@36655 ` 590` ``` "((\x. x) ---> a) (at a within S)" ``` huffman@44081 ` 591` ``` unfolding tendsto_def eventually_within eventually_at_topological by auto ``` huffman@31565 ` 592` huffman@44081 ` 593` ```lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) A" ``` huffman@44081 ` 594` ``` by (simp add: tendsto_def) ``` huffman@31349 ` 595` huffman@36662 ` 596` ```lemma tendsto_const_iff: ``` huffman@36662 ` 597` ``` fixes k l :: "'a::metric_space" ``` huffman@44081 ` 598` ``` assumes "A \ bot" shows "((\n. k) ---> l) A \ k = l" ``` huffman@44081 ` 599` ``` apply (safe intro!: tendsto_const) ``` huffman@44081 ` 600` ``` apply (rule ccontr) ``` huffman@44081 ` 601` ``` apply (drule_tac e="dist k l" in tendstoD) ``` huffman@44081 ` 602` ``` apply (simp add: zero_less_dist_iff) ``` huffman@44081 ` 603` ``` apply (simp add: eventually_False assms) ``` huffman@44081 ` 604` ``` done ``` huffman@36662 ` 605` huffman@31565 ` 606` ```lemma tendsto_dist [tendsto_intros]: ``` huffman@44081 ` 607` ``` assumes f: "(f ---> l) A" and g: "(g ---> m) A" ``` huffman@44081 ` 608` ``` shows "((\x. dist (f x) (g x)) ---> dist l m) A" ``` huffman@31565 ` 609` ```proof (rule tendstoI) ``` huffman@31565 ` 610` ``` fix e :: real assume "0 < e" ``` huffman@31565 ` 611` ``` hence e2: "0 < e/2" by simp ``` huffman@31565 ` 612` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` huffman@44081 ` 613` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) A" ``` huffman@31565 ` 614` ``` proof (rule eventually_elim2) ``` huffman@31565 ` 615` ``` fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" ``` huffman@31565 ` 616` ``` then show "dist (dist (f x) (g x)) (dist l m) < e" ``` huffman@31565 ` 617` ``` unfolding dist_real_def ``` huffman@31565 ` 618` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` huffman@31565 ` 619` ``` using dist_triangle2 [of "g x" "l" "m"] ``` huffman@31565 ` 620` ``` using dist_triangle3 [of "l" "m" "f x"] ``` huffman@31565 ` 621` ``` using dist_triangle [of "f x" "m" "g x"] ``` huffman@31565 ` 622` ``` by arith ``` huffman@31565 ` 623` ``` qed ``` huffman@31565 ` 624` ```qed ``` huffman@31565 ` 625` huffman@36662 ` 626` ```lemma norm_conv_dist: "norm x = dist x 0" ``` huffman@44081 ` 627` ``` unfolding dist_norm by simp ``` huffman@36662 ` 628` huffman@31565 ` 629` ```lemma tendsto_norm [tendsto_intros]: ``` huffman@44081 ` 630` ``` "(f ---> a) A \ ((\x. norm (f x)) ---> norm a) A" ``` huffman@44081 ` 631` ``` unfolding norm_conv_dist by (intro tendsto_intros) ``` huffman@36662 ` 632` huffman@36662 ` 633` ```lemma tendsto_norm_zero: ``` huffman@44081 ` 634` ``` "(f ---> 0) A \ ((\x. norm (f x)) ---> 0) A" ``` huffman@44081 ` 635` ``` by (drule tendsto_norm, simp) ``` huffman@36662 ` 636` huffman@36662 ` 637` ```lemma tendsto_norm_zero_cancel: ``` huffman@44081 ` 638` ``` "((\x. norm (f x)) ---> 0) A \ (f ---> 0) A" ``` huffman@44081 ` 639` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@36662 ` 640` huffman@36662 ` 641` ```lemma tendsto_norm_zero_iff: ``` huffman@44081 ` 642` ``` "((\x. norm (f x)) ---> 0) A \ (f ---> 0) A" ``` huffman@44081 ` 643` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@31349 ` 644` huffman@31565 ` 645` ```lemma tendsto_add [tendsto_intros]: ``` huffman@31349 ` 646` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44081 ` 647` ``` shows "\(f ---> a) A; (g ---> b) A\ \ ((\x. f x + g x) ---> a + b) A" ``` huffman@44081 ` 648` ``` by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) ``` huffman@31349 ` 649` huffman@31565 ` 650` ```lemma tendsto_minus [tendsto_intros]: ``` huffman@31349 ` 651` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44081 ` 652` ``` shows "(f ---> a) A \ ((\x. - f x) ---> - a) A" ``` huffman@44081 ` 653` ``` by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) ``` huffman@31349 ` 654` huffman@31349 ` 655` ```lemma tendsto_minus_cancel: ``` huffman@31349 ` 656` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44081 ` 657` ``` shows "((\x. - f x) ---> - a) A \ (f ---> a) A" ``` huffman@44081 ` 658` ``` by (drule tendsto_minus, simp) ``` huffman@31349 ` 659` huffman@31565 ` 660` ```lemma tendsto_diff [tendsto_intros]: ``` huffman@31349 ` 661` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44081 ` 662` ``` shows "\(f ---> a) A; (g ---> b) A\ \ ((\x. f x - g x) ---> a - b) A" ``` huffman@44081 ` 663` ``` by (simp add: diff_minus tendsto_add tendsto_minus) ``` huffman@31349 ` 664` huffman@31588 ` 665` ```lemma tendsto_setsum [tendsto_intros]: ``` huffman@31588 ` 666` ``` fixes f :: "'a \ 'b \ 'c::real_normed_vector" ``` huffman@44081 ` 667` ``` assumes "\i. i \ S \ (f i ---> a i) A" ``` huffman@44081 ` 668` ``` shows "((\x. \i\S. f i x) ---> (\i\S. a i)) A" ``` huffman@31588 ` 669` ```proof (cases "finite S") ``` huffman@31588 ` 670` ``` assume "finite S" thus ?thesis using assms ``` huffman@31588 ` 671` ``` proof (induct set: finite) ``` huffman@31588 ` 672` ``` case empty show ?case ``` huffman@31588 ` 673` ``` by (simp add: tendsto_const) ``` huffman@31588 ` 674` ``` next ``` huffman@31588 ` 675` ``` case (insert i F) thus ?case ``` huffman@31588 ` 676` ``` by (simp add: tendsto_add) ``` huffman@31588 ` 677` ``` qed ``` huffman@31588 ` 678` ```next ``` huffman@31588 ` 679` ``` assume "\ finite S" thus ?thesis ``` huffman@31588 ` 680` ``` by (simp add: tendsto_const) ``` huffman@31588 ` 681` ```qed ``` huffman@31588 ` 682` huffman@31565 ` 683` ```lemma (in bounded_linear) tendsto [tendsto_intros]: ``` huffman@44081 ` 684` ``` "(g ---> a) A \ ((\x. f (g x)) ---> f a) A" ``` huffman@44081 ` 685` ``` by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) ``` huffman@31349 ` 686` huffman@31565 ` 687` ```lemma (in bounded_bilinear) tendsto [tendsto_intros]: ``` huffman@44081 ` 688` ``` "\(f ---> a) A; (g ---> b) A\ \ ((\x. f x ** g x) ---> a ** b) A" ``` huffman@44081 ` 689` ``` by (simp only: tendsto_Zfun_iff prod_diff_prod ``` huffman@44081 ` 690` ``` Zfun_add Zfun Zfun_left Zfun_right) ``` huffman@31349 ` 691` huffman@31355 ` 692` huffman@31355 ` 693` ```subsection {* Continuity of Inverse *} ``` huffman@31355 ` 694` huffman@31355 ` 695` ```lemma (in bounded_bilinear) Zfun_prod_Bfun: ``` huffman@44081 ` 696` ``` assumes f: "Zfun f A" ``` huffman@44081 ` 697` ``` assumes g: "Bfun g A" ``` huffman@44081 ` 698` ``` shows "Zfun (\x. f x ** g x) A" ``` huffman@31355 ` 699` ```proof - ``` huffman@31355 ` 700` ``` obtain K where K: "0 \ K" ``` huffman@31355 ` 701` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31355 ` 702` ``` using nonneg_bounded by fast ``` huffman@31355 ` 703` ``` obtain B where B: "0 < B" ``` huffman@44081 ` 704` ``` and norm_g: "eventually (\x. norm (g x) \ B) A" ``` huffman@31487 ` 705` ``` using g by (rule BfunE) ``` huffman@44081 ` 706` ``` have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) A" ``` huffman@31487 ` 707` ``` using norm_g proof (rule eventually_elim1) ``` huffman@31487 ` 708` ``` fix x ``` huffman@31487 ` 709` ``` assume *: "norm (g x) \ B" ``` huffman@31487 ` 710` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31355 ` 711` ``` by (rule norm_le) ``` huffman@31487 ` 712` ``` also have "\ \ norm (f x) * B * K" ``` huffman@31487 ` 713` ``` by (intro mult_mono' order_refl norm_g norm_ge_zero ``` huffman@31355 ` 714` ``` mult_nonneg_nonneg K *) ``` huffman@31487 ` 715` ``` also have "\ = norm (f x) * (B * K)" ``` huffman@31355 ` 716` ``` by (rule mult_assoc) ``` huffman@31487 ` 717` ``` finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . ``` huffman@31355 ` 718` ``` qed ``` huffman@31487 ` 719` ``` with f show ?thesis ``` huffman@31487 ` 720` ``` by (rule Zfun_imp_Zfun) ``` huffman@31355 ` 721` ```qed ``` huffman@31355 ` 722` huffman@31355 ` 723` ```lemma (in bounded_bilinear) flip: ``` huffman@31355 ` 724` ``` "bounded_bilinear (\x y. y ** x)" ``` huffman@44081 ` 725` ``` apply default ``` huffman@44081 ` 726` ``` apply (rule add_right) ``` huffman@44081 ` 727` ``` apply (rule add_left) ``` huffman@44081 ` 728` ``` apply (rule scaleR_right) ``` huffman@44081 ` 729` ``` apply (rule scaleR_left) ``` huffman@44081 ` 730` ``` apply (subst mult_commute) ``` huffman@44081 ` 731` ``` using bounded by fast ``` huffman@31355 ` 732` huffman@31355 ` 733` ```lemma (in bounded_bilinear) Bfun_prod_Zfun: ``` huffman@44081 ` 734` ``` assumes f: "Bfun f A" ``` huffman@44081 ` 735` ``` assumes g: "Zfun g A" ``` huffman@44081 ` 736` ``` shows "Zfun (\x. f x ** g x) A" ``` huffman@44081 ` 737` ``` using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) ``` huffman@31355 ` 738` huffman@31355 ` 739` ```lemma Bfun_inverse_lemma: ``` huffman@31355 ` 740` ``` fixes x :: "'a::real_normed_div_algebra" ``` huffman@31355 ` 741` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` huffman@44081 ` 742` ``` apply (subst nonzero_norm_inverse, clarsimp) ``` huffman@44081 ` 743` ``` apply (erule (1) le_imp_inverse_le) ``` huffman@44081 ` 744` ``` done ``` huffman@31355 ` 745` huffman@31355 ` 746` ```lemma Bfun_inverse: ``` huffman@31355 ` 747` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44081 ` 748` ``` assumes f: "(f ---> a) A" ``` huffman@31355 ` 749` ``` assumes a: "a \ 0" ``` huffman@44081 ` 750` ``` shows "Bfun (\x. inverse (f x)) A" ``` huffman@31355 ` 751` ```proof - ``` huffman@31355 ` 752` ``` from a have "0 < norm a" by simp ``` huffman@31355 ` 753` ``` hence "\r>0. r < norm a" by (rule dense) ``` huffman@31355 ` 754` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" by fast ``` huffman@44081 ` 755` ``` have "eventually (\x. dist (f x) a < r) A" ``` huffman@31487 ` 756` ``` using tendstoD [OF f r1] by fast ``` huffman@44081 ` 757` ``` hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) A" ``` huffman@31355 ` 758` ``` proof (rule eventually_elim1) ``` huffman@31487 ` 759` ``` fix x ``` huffman@31487 ` 760` ``` assume "dist (f x) a < r" ``` huffman@31487 ` 761` ``` hence 1: "norm (f x - a) < r" ``` huffman@31355 ` 762` ``` by (simp add: dist_norm) ``` huffman@31487 ` 763` ``` hence 2: "f x \ 0" using r2 by auto ``` huffman@31487 ` 764` ``` hence "norm (inverse (f x)) = inverse (norm (f x))" ``` huffman@31355 ` 765` ``` by (rule nonzero_norm_inverse) ``` huffman@31355 ` 766` ``` also have "\ \ inverse (norm a - r)" ``` huffman@31355 ` 767` ``` proof (rule le_imp_inverse_le) ``` huffman@31355 ` 768` ``` show "0 < norm a - r" using r2 by simp ``` huffman@31355 ` 769` ``` next ``` huffman@31487 ` 770` ``` have "norm a - norm (f x) \ norm (a - f x)" ``` huffman@31355 ` 771` ``` by (rule norm_triangle_ineq2) ``` huffman@31487 ` 772` ``` also have "\ = norm (f x - a)" ``` huffman@31355 ` 773` ``` by (rule norm_minus_commute) ``` huffman@31355 ` 774` ``` also have "\ < r" using 1 . ``` huffman@31487 ` 775` ``` finally show "norm a - r \ norm (f x)" by simp ``` huffman@31355 ` 776` ``` qed ``` huffman@31487 ` 777` ``` finally show "norm (inverse (f x)) \ inverse (norm a - r)" . ``` huffman@31355 ` 778` ``` qed ``` huffman@31355 ` 779` ``` thus ?thesis by (rule BfunI) ``` huffman@31355 ` 780` ```qed ``` huffman@31355 ` 781` huffman@31355 ` 782` ```lemma tendsto_inverse_lemma: ``` huffman@31355 ` 783` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44081 ` 784` ``` shows "\(f ---> a) A; a \ 0; eventually (\x. f x \ 0) A\ ``` huffman@44081 ` 785` ``` \ ((\x. inverse (f x)) ---> inverse a) A" ``` huffman@44081 ` 786` ``` apply (subst tendsto_Zfun_iff) ``` huffman@44081 ` 787` ``` apply (rule Zfun_ssubst) ``` huffman@44081 ` 788` ``` apply (erule eventually_elim1) ``` huffman@44081 ` 789` ``` apply (erule (1) inverse_diff_inverse) ``` huffman@44081 ` 790` ``` apply (rule Zfun_minus) ``` huffman@44081 ` 791` ``` apply (rule Zfun_mult_left) ``` huffman@44081 ` 792` ``` apply (rule mult.Bfun_prod_Zfun) ``` huffman@44081 ` 793` ``` apply (erule (1) Bfun_inverse) ``` huffman@44081 ` 794` ``` apply (simp add: tendsto_Zfun_iff) ``` huffman@44081 ` 795` ``` done ``` huffman@31355 ` 796` huffman@31565 ` 797` ```lemma tendsto_inverse [tendsto_intros]: ``` huffman@31355 ` 798` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44081 ` 799` ``` assumes f: "(f ---> a) A" ``` huffman@31355 ` 800` ``` assumes a: "a \ 0" ``` huffman@44081 ` 801` ``` shows "((\x. inverse (f x)) ---> inverse a) A" ``` huffman@31355 ` 802` ```proof - ``` huffman@31355 ` 803` ``` from a have "0 < norm a" by simp ``` huffman@44081 ` 804` ``` with f have "eventually (\x. dist (f x) a < norm a) A" ``` huffman@31355 ` 805` ``` by (rule tendstoD) ``` huffman@44081 ` 806` ``` then have "eventually (\x. f x \ 0) A" ``` huffman@31355 ` 807` ``` unfolding dist_norm by (auto elim!: eventually_elim1) ``` huffman@31487 ` 808` ``` with f a show ?thesis ``` huffman@31355 ` 809` ``` by (rule tendsto_inverse_lemma) ``` huffman@31355 ` 810` ```qed ``` huffman@31355 ` 811` huffman@31565 ` 812` ```lemma tendsto_divide [tendsto_intros]: ``` huffman@31355 ` 813` ``` fixes a b :: "'a::real_normed_field" ``` huffman@44081 ` 814` ``` shows "\(f ---> a) A; (g ---> b) A; b \ 0\ ``` huffman@44081 ` 815` ``` \ ((\x. f x / g x) ---> a / b) A" ``` huffman@44081 ` 816` ``` by (simp add: mult.tendsto tendsto_inverse divide_inverse) ``` huffman@31355 ` 817` hoelzl@41970 ` 818` ```lemma tendsto_unique: ``` hoelzl@41970 ` 819` ``` fixes f :: "'a \ 'b::t2_space" ``` huffman@44081 ` 820` ``` assumes "\ trivial_limit A" "(f ---> l) A" "(f ---> l') A" ``` hoelzl@41970 ` 821` ``` shows "l = l'" ``` hoelzl@41970 ` 822` ```proof (rule ccontr) ``` hoelzl@41970 ` 823` ``` assume "l \ l'" ``` hoelzl@41970 ` 824` ``` obtain U V where "open U" "open V" "l \ U" "l' \ V" "U \ V = {}" ``` hoelzl@41970 ` 825` ``` using hausdorff [OF `l \ l'`] by fast ``` huffman@44081 ` 826` ``` have "eventually (\x. f x \ U) A" ``` huffman@44081 ` 827` ``` using `(f ---> l) A` `open U` `l \ U` by (rule topological_tendstoD) ``` hoelzl@41970 ` 828` ``` moreover ``` huffman@44081 ` 829` ``` have "eventually (\x. f x \ V) A" ``` huffman@44081 ` 830` ``` using `(f ---> l') A` `open V` `l' \ V` by (rule topological_tendstoD) ``` hoelzl@41970 ` 831` ``` ultimately ``` huffman@44081 ` 832` ``` have "eventually (\x. False) A" ``` hoelzl@41970 ` 833` ``` proof (rule eventually_elim2) ``` hoelzl@41970 ` 834` ``` fix x ``` hoelzl@41970 ` 835` ``` assume "f x \ U" "f x \ V" ``` hoelzl@41970 ` 836` ``` hence "f x \ U \ V" by simp ``` hoelzl@41970 ` 837` ``` with `U \ V = {}` show "False" by simp ``` hoelzl@41970 ` 838` ``` qed ``` huffman@44081 ` 839` ``` with `\ trivial_limit A` show "False" ``` hoelzl@41970 ` 840` ``` by (simp add: trivial_limit_def) ``` hoelzl@41970 ` 841` ```qed ``` hoelzl@41970 ` 842` huffman@31349 ` 843` ```end ```