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