src/HOL/Limits.thy
 author huffman Sun Apr 25 11:58:39 2010 -0700 (2010-04-25) changeset 36358 246493d61204 parent 31902 862ae16a799d child 36360 9d8f7efd9289 permissions -rw-r--r--
define nets directly as filters, instead of as filter bases
 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@31349 ` 8` ```imports RealVector RComplete ``` huffman@31349 ` 9` ```begin ``` huffman@31349 ` 10` huffman@31392 ` 11` ```subsection {* Nets *} ``` huffman@31392 ` 12` huffman@31392 ` 13` ```text {* ``` huffman@36358 ` 14` ``` A net is now defined simply as a filter. ``` 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@31392 ` 48` ```lemma eventually_True [simp]: "eventually (\x. True) net" ``` huffman@36358 ` 49` ```unfolding eventually_def ``` huffman@36358 ` 50` ```by (rule is_filter.True [OF is_filter_Rep_net]) ``` huffman@31349 ` 51` huffman@31349 ` 52` ```lemma eventually_mono: ``` huffman@31392 ` 53` ``` "(\x. P x \ Q x) \ eventually P net \ eventually Q net" ``` huffman@36358 ` 54` ```unfolding eventually_def ``` huffman@36358 ` 55` ```by (rule is_filter.mono [OF is_filter_Rep_net]) ``` huffman@31349 ` 56` huffman@31349 ` 57` ```lemma eventually_conj: ``` huffman@31392 ` 58` ``` assumes P: "eventually (\x. P x) net" ``` huffman@31392 ` 59` ``` assumes Q: "eventually (\x. Q x) net" ``` huffman@31392 ` 60` ``` shows "eventually (\x. P x \ Q x) net" ``` huffman@36358 ` 61` ```using assms unfolding eventually_def ``` huffman@36358 ` 62` ```by (rule is_filter.conj [OF is_filter_Rep_net]) ``` huffman@31349 ` 63` huffman@31349 ` 64` ```lemma eventually_mp: ``` huffman@31392 ` 65` ``` assumes "eventually (\x. P x \ Q x) net" ``` huffman@31392 ` 66` ``` assumes "eventually (\x. P x) net" ``` huffman@31392 ` 67` ``` shows "eventually (\x. Q x) net" ``` huffman@31349 ` 68` ```proof (rule eventually_mono) ``` huffman@31349 ` 69` ``` show "\x. (P x \ Q x) \ P x \ Q x" by simp ``` huffman@31392 ` 70` ``` show "eventually (\x. (P x \ Q x) \ P x) net" ``` huffman@31349 ` 71` ``` using assms by (rule eventually_conj) ``` huffman@31349 ` 72` ```qed ``` huffman@31349 ` 73` huffman@31349 ` 74` ```lemma eventually_rev_mp: ``` huffman@31392 ` 75` ``` assumes "eventually (\x. P x) net" ``` huffman@31392 ` 76` ``` assumes "eventually (\x. P x \ Q x) net" ``` huffman@31392 ` 77` ``` shows "eventually (\x. Q x) net" ``` huffman@31349 ` 78` ```using assms(2) assms(1) by (rule eventually_mp) ``` huffman@31349 ` 79` huffman@31349 ` 80` ```lemma eventually_conj_iff: ``` huffman@31349 ` 81` ``` "eventually (\x. P x \ Q x) net \ eventually P net \ eventually Q net" ``` huffman@31349 ` 82` ```by (auto intro: eventually_conj elim: eventually_rev_mp) ``` huffman@31349 ` 83` huffman@31349 ` 84` ```lemma eventually_elim1: ``` huffman@31392 ` 85` ``` assumes "eventually (\i. P i) net" ``` huffman@31349 ` 86` ``` assumes "\i. P i \ Q i" ``` huffman@31392 ` 87` ``` shows "eventually (\i. Q i) net" ``` huffman@31349 ` 88` ```using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 89` huffman@31349 ` 90` ```lemma eventually_elim2: ``` huffman@31392 ` 91` ``` assumes "eventually (\i. P i) net" ``` huffman@31392 ` 92` ``` assumes "eventually (\i. Q i) net" ``` huffman@31349 ` 93` ``` assumes "\i. P i \ Q i \ R i" ``` huffman@31392 ` 94` ``` shows "eventually (\i. R i) net" ``` huffman@31349 ` 95` ```using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 96` huffman@31349 ` 97` huffman@31392 ` 98` ```subsection {* Standard Nets *} ``` huffman@31392 ` 99` huffman@31392 ` 100` ```definition ``` huffman@36358 ` 101` ``` sequentially :: "nat net" ``` huffman@36358 ` 102` ```where [code del]: ``` huffman@36358 ` 103` ``` "sequentially = Abs_net (\P. \k. \n\k. P n)" ``` huffman@31392 ` 104` huffman@31392 ` 105` ```definition ``` huffman@36358 ` 106` ``` within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) ``` huffman@36358 ` 107` ```where [code del]: ``` huffman@36358 ` 108` ``` "net within S = Abs_net (\P. eventually (\x. x \ S \ P x) net)" ``` huffman@31392 ` 109` huffman@36358 ` 110` ```definition ``` huffman@36358 ` 111` ``` at :: "'a::topological_space \ 'a net" ``` huffman@36358 ` 112` ```where [code del]: ``` huffman@36358 ` 113` ``` "at a = Abs_net (\P. \S. open S \ a \ S \ (\x\S. x \ a \ P x))" ``` huffman@31447 ` 114` huffman@31392 ` 115` ```lemma eventually_sequentially: ``` huffman@31392 ` 116` ``` "eventually P sequentially \ (\N. \n\N. P n)" ``` huffman@36358 ` 117` ```unfolding sequentially_def ``` huffman@36358 ` 118` ```proof (rule eventually_Abs_net, rule is_filter.intro) ``` huffman@36358 ` 119` ``` fix P Q :: "nat \ bool" ``` huffman@36358 ` 120` ``` assume "\i. \n\i. P n" and "\j. \n\j. Q n" ``` huffman@36358 ` 121` ``` then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto ``` huffman@36358 ` 122` ``` then have "\n\max i j. P n \ Q n" by simp ``` huffman@36358 ` 123` ``` then show "\k. \n\k. P n \ Q n" .. ``` huffman@36358 ` 124` ```qed auto ``` huffman@31392 ` 125` huffman@31392 ` 126` ```lemma eventually_within: ``` huffman@31392 ` 127` ``` "eventually P (net within S) = eventually (\x. x \ S \ P x) net" ``` huffman@36358 ` 128` ```unfolding within_def ``` huffman@36358 ` 129` ```by (rule eventually_Abs_net, rule is_filter.intro) ``` huffman@36358 ` 130` ``` (auto elim!: eventually_rev_mp) ``` huffman@31392 ` 131` huffman@31447 ` 132` ```lemma eventually_at_topological: ``` huffman@31492 ` 133` ``` "eventually P (at a) \ (\S. open S \ a \ S \ (\x\S. x \ a \ P x))" ``` huffman@36358 ` 134` ```unfolding at_def ``` huffman@36358 ` 135` ```proof (rule eventually_Abs_net, rule is_filter.intro) ``` huffman@36358 ` 136` ``` have "open UNIV \ a \ UNIV \ (\x\UNIV. x \ a \ True)" by simp ``` huffman@36358 ` 137` ``` thus "\S. open S \ a \ S \ (\x\S. x \ a \ True)" by - rule ``` huffman@36358 ` 138` ```next ``` huffman@36358 ` 139` ``` fix P Q ``` huffman@36358 ` 140` ``` assume "\S. open S \ a \ S \ (\x\S. x \ a \ P x)" ``` huffman@36358 ` 141` ``` and "\T. open T \ a \ T \ (\x\T. x \ a \ Q x)" ``` huffman@36358 ` 142` ``` then obtain S T where ``` huffman@36358 ` 143` ``` "open S \ a \ S \ (\x\S. x \ a \ P x)" ``` huffman@36358 ` 144` ``` "open T \ a \ T \ (\x\T. x \ a \ Q x)" by auto ``` huffman@36358 ` 145` ``` hence "open (S \ T) \ a \ S \ T \ (\x\(S \ T). x \ a \ P x \ Q x)" ``` huffman@36358 ` 146` ``` by (simp add: open_Int) ``` huffman@36358 ` 147` ``` thus "\S. open S \ a \ S \ (\x\S. x \ a \ P x \ Q x)" by - rule ``` huffman@36358 ` 148` ```qed auto ``` huffman@31447 ` 149` huffman@31447 ` 150` ```lemma eventually_at: ``` huffman@31447 ` 151` ``` fixes a :: "'a::metric_space" ``` huffman@31447 ` 152` ``` shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" ``` huffman@31492 ` 153` ```unfolding eventually_at_topological open_dist ``` huffman@31447 ` 154` ```apply safe ``` huffman@31447 ` 155` ```apply fast ``` huffman@31492 ` 156` ```apply (rule_tac x="{x. dist x a < d}" in exI, simp) ``` huffman@31447 ` 157` ```apply clarsimp ``` huffman@31447 ` 158` ```apply (rule_tac x="d - dist x a" in exI, clarsimp) ``` huffman@31447 ` 159` ```apply (simp only: less_diff_eq) ``` huffman@31447 ` 160` ```apply (erule le_less_trans [OF dist_triangle]) ``` huffman@31447 ` 161` ```done ``` huffman@31447 ` 162` huffman@31392 ` 163` huffman@31355 ` 164` ```subsection {* Boundedness *} ``` huffman@31355 ` 165` huffman@31355 ` 166` ```definition ``` huffman@31392 ` 167` ``` Bfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where ``` huffman@31487 ` 168` ``` [code del]: "Bfun f net = (\K>0. eventually (\x. norm (f x) \ K) net)" ``` huffman@31355 ` 169` huffman@31487 ` 170` ```lemma BfunI: ``` huffman@31487 ` 171` ``` assumes K: "eventually (\x. norm (f x) \ K) net" shows "Bfun f net" ``` huffman@31355 ` 172` ```unfolding Bfun_def ``` huffman@31355 ` 173` ```proof (intro exI conjI allI) ``` huffman@31355 ` 174` ``` show "0 < max K 1" by simp ``` huffman@31355 ` 175` ```next ``` huffman@31487 ` 176` ``` show "eventually (\x. norm (f x) \ max K 1) net" ``` huffman@31355 ` 177` ``` using K by (rule eventually_elim1, simp) ``` huffman@31355 ` 178` ```qed ``` huffman@31355 ` 179` huffman@31355 ` 180` ```lemma BfunE: ``` huffman@31487 ` 181` ``` assumes "Bfun f net" ``` huffman@31487 ` 182` ``` obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) net" ``` huffman@31355 ` 183` ```using assms unfolding Bfun_def by fast ``` huffman@31355 ` 184` huffman@31355 ` 185` huffman@31349 ` 186` ```subsection {* Convergence to Zero *} ``` huffman@31349 ` 187` huffman@31349 ` 188` ```definition ``` huffman@31392 ` 189` ``` Zfun :: "('a \ 'b::real_normed_vector) \ 'a net \ bool" where ``` huffman@31487 ` 190` ``` [code del]: "Zfun f net = (\r>0. eventually (\x. norm (f x) < r) net)" ``` huffman@31349 ` 191` huffman@31349 ` 192` ```lemma ZfunI: ``` huffman@31487 ` 193` ``` "(\r. 0 < r \ eventually (\x. norm (f x) < r) net) \ Zfun f net" ``` huffman@31349 ` 194` ```unfolding Zfun_def by simp ``` huffman@31349 ` 195` huffman@31349 ` 196` ```lemma ZfunD: ``` huffman@31487 ` 197` ``` "\Zfun f net; 0 < r\ \ eventually (\x. norm (f x) < r) net" ``` huffman@31349 ` 198` ```unfolding Zfun_def by simp ``` huffman@31349 ` 199` huffman@31355 ` 200` ```lemma Zfun_ssubst: ``` huffman@31487 ` 201` ``` "eventually (\x. f x = g x) net \ Zfun g net \ Zfun f net" ``` huffman@31355 ` 202` ```unfolding Zfun_def by (auto elim!: eventually_rev_mp) ``` huffman@31355 ` 203` huffman@31487 ` 204` ```lemma Zfun_zero: "Zfun (\x. 0) net" ``` huffman@31349 ` 205` ```unfolding Zfun_def by simp ``` huffman@31349 ` 206` huffman@31487 ` 207` ```lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) net = Zfun (\x. f x) net" ``` huffman@31349 ` 208` ```unfolding Zfun_def by simp ``` huffman@31349 ` 209` huffman@31349 ` 210` ```lemma Zfun_imp_Zfun: ``` huffman@31487 ` 211` ``` assumes f: "Zfun f net" ``` huffman@31487 ` 212` ``` assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) net" ``` huffman@31487 ` 213` ``` shows "Zfun (\x. g x) net" ``` huffman@31349 ` 214` ```proof (cases) ``` huffman@31349 ` 215` ``` assume K: "0 < K" ``` huffman@31349 ` 216` ``` show ?thesis ``` huffman@31349 ` 217` ``` proof (rule ZfunI) ``` huffman@31349 ` 218` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 219` ``` hence "0 < r / K" ``` huffman@31349 ` 220` ``` using K by (rule divide_pos_pos) ``` huffman@31487 ` 221` ``` then have "eventually (\x. norm (f x) < r / K) net" ``` huffman@31487 ` 222` ``` using ZfunD [OF f] by fast ``` huffman@31487 ` 223` ``` with g show "eventually (\x. norm (g x) < r) net" ``` huffman@31355 ` 224` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 225` ``` fix x ``` huffman@31487 ` 226` ``` assume *: "norm (g x) \ norm (f x) * K" ``` huffman@31487 ` 227` ``` assume "norm (f x) < r / K" ``` huffman@31487 ` 228` ``` hence "norm (f x) * K < r" ``` huffman@31349 ` 229` ``` by (simp add: pos_less_divide_eq K) ``` huffman@31487 ` 230` ``` thus "norm (g x) < r" ``` huffman@31355 ` 231` ``` by (simp add: order_le_less_trans [OF *]) ``` huffman@31349 ` 232` ``` qed ``` huffman@31349 ` 233` ``` qed ``` huffman@31349 ` 234` ```next ``` huffman@31349 ` 235` ``` assume "\ 0 < K" ``` huffman@31349 ` 236` ``` hence K: "K \ 0" by (simp only: not_less) ``` huffman@31355 ` 237` ``` show ?thesis ``` huffman@31355 ` 238` ``` proof (rule ZfunI) ``` huffman@31355 ` 239` ``` fix r :: real ``` huffman@31355 ` 240` ``` assume "0 < r" ``` huffman@31487 ` 241` ``` from g show "eventually (\x. norm (g x) < r) net" ``` huffman@31355 ` 242` ``` proof (rule eventually_elim1) ``` huffman@31487 ` 243` ``` fix x ``` huffman@31487 ` 244` ``` assume "norm (g x) \ norm (f x) * K" ``` huffman@31487 ` 245` ``` also have "\ \ norm (f x) * 0" ``` huffman@31355 ` 246` ``` using K norm_ge_zero by (rule mult_left_mono) ``` huffman@31487 ` 247` ``` finally show "norm (g x) < r" ``` huffman@31355 ` 248` ``` using `0 < r` by simp ``` huffman@31355 ` 249` ``` qed ``` huffman@31355 ` 250` ``` qed ``` huffman@31349 ` 251` ```qed ``` huffman@31349 ` 252` huffman@31487 ` 253` ```lemma Zfun_le: "\Zfun g net; \x. norm (f x) \ norm (g x)\ \ Zfun f net" ``` huffman@31349 ` 254` ```by (erule_tac K="1" in Zfun_imp_Zfun, simp) ``` huffman@31349 ` 255` huffman@31349 ` 256` ```lemma Zfun_add: ``` huffman@31487 ` 257` ``` assumes f: "Zfun f net" and g: "Zfun g net" ``` huffman@31487 ` 258` ``` shows "Zfun (\x. f x + g x) net" ``` huffman@31349 ` 259` ```proof (rule ZfunI) ``` huffman@31349 ` 260` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 261` ``` hence r: "0 < r / 2" by simp ``` huffman@31487 ` 262` ``` have "eventually (\x. norm (f x) < r/2) net" ``` huffman@31487 ` 263` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 264` ``` moreover ``` huffman@31487 ` 265` ``` have "eventually (\x. norm (g x) < r/2) net" ``` huffman@31487 ` 266` ``` using g r by (rule ZfunD) ``` huffman@31349 ` 267` ``` ultimately ``` huffman@31487 ` 268` ``` show "eventually (\x. norm (f x + g x) < r) net" ``` huffman@31349 ` 269` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 270` ``` fix x ``` huffman@31487 ` 271` ``` assume *: "norm (f x) < r/2" "norm (g x) < r/2" ``` huffman@31487 ` 272` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@31349 ` 273` ``` by (rule norm_triangle_ineq) ``` huffman@31349 ` 274` ``` also have "\ < r/2 + r/2" ``` huffman@31349 ` 275` ``` using * by (rule add_strict_mono) ``` huffman@31487 ` 276` ``` finally show "norm (f x + g x) < r" ``` huffman@31349 ` 277` ``` by simp ``` huffman@31349 ` 278` ``` qed ``` huffman@31349 ` 279` ```qed ``` huffman@31349 ` 280` huffman@31487 ` 281` ```lemma Zfun_minus: "Zfun f net \ Zfun (\x. - f x) net" ``` huffman@31349 ` 282` ```unfolding Zfun_def by simp ``` huffman@31349 ` 283` huffman@31487 ` 284` ```lemma Zfun_diff: "\Zfun f net; Zfun g net\ \ Zfun (\x. f x - g x) net" ``` huffman@31349 ` 285` ```by (simp only: diff_minus Zfun_add Zfun_minus) ``` huffman@31349 ` 286` huffman@31349 ` 287` ```lemma (in bounded_linear) Zfun: ``` huffman@31487 ` 288` ``` assumes g: "Zfun g net" ``` huffman@31487 ` 289` ``` shows "Zfun (\x. f (g x)) net" ``` huffman@31349 ` 290` ```proof - ``` huffman@31349 ` 291` ``` obtain K where "\x. norm (f x) \ norm x * K" ``` huffman@31349 ` 292` ``` using bounded by fast ``` huffman@31487 ` 293` ``` then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) net" ``` huffman@31355 ` 294` ``` by simp ``` huffman@31487 ` 295` ``` with g show ?thesis ``` huffman@31349 ` 296` ``` by (rule Zfun_imp_Zfun) ``` huffman@31349 ` 297` ```qed ``` huffman@31349 ` 298` huffman@31349 ` 299` ```lemma (in bounded_bilinear) Zfun: ``` huffman@31487 ` 300` ``` assumes f: "Zfun f net" ``` huffman@31487 ` 301` ``` assumes g: "Zfun g net" ``` huffman@31487 ` 302` ``` shows "Zfun (\x. f x ** g x) net" ``` huffman@31349 ` 303` ```proof (rule ZfunI) ``` huffman@31349 ` 304` ``` fix r::real assume r: "0 < r" ``` huffman@31349 ` 305` ``` obtain K where K: "0 < K" ``` huffman@31349 ` 306` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31349 ` 307` ``` using pos_bounded by fast ``` huffman@31349 ` 308` ``` from K have K': "0 < inverse K" ``` huffman@31349 ` 309` ``` by (rule positive_imp_inverse_positive) ``` huffman@31487 ` 310` ``` have "eventually (\x. norm (f x) < r) net" ``` huffman@31487 ` 311` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 312` ``` moreover ``` huffman@31487 ` 313` ``` have "eventually (\x. norm (g x) < inverse K) net" ``` huffman@31487 ` 314` ``` using g K' by (rule ZfunD) ``` huffman@31349 ` 315` ``` ultimately ``` huffman@31487 ` 316` ``` show "eventually (\x. norm (f x ** g x) < r) net" ``` huffman@31349 ` 317` ``` proof (rule eventually_elim2) ``` huffman@31487 ` 318` ``` fix x ``` huffman@31487 ` 319` ``` assume *: "norm (f x) < r" "norm (g x) < inverse K" ``` huffman@31487 ` 320` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31349 ` 321` ``` by (rule norm_le) ``` huffman@31487 ` 322` ``` also have "norm (f x) * norm (g x) * K < r * inverse K * K" ``` huffman@31349 ` 323` ``` by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero * K) ``` huffman@31349 ` 324` ``` also from K have "r * inverse K * K = r" ``` huffman@31349 ` 325` ``` by simp ``` huffman@31487 ` 326` ``` finally show "norm (f x ** g x) < r" . ``` huffman@31349 ` 327` ``` qed ``` huffman@31349 ` 328` ```qed ``` huffman@31349 ` 329` huffman@31349 ` 330` ```lemma (in bounded_bilinear) Zfun_left: ``` huffman@31487 ` 331` ``` "Zfun f net \ Zfun (\x. f x ** a) net" ``` huffman@31349 ` 332` ```by (rule bounded_linear_left [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 333` huffman@31349 ` 334` ```lemma (in bounded_bilinear) Zfun_right: ``` huffman@31487 ` 335` ``` "Zfun f net \ Zfun (\x. a ** f x) net" ``` huffman@31349 ` 336` ```by (rule bounded_linear_right [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 337` huffman@31349 ` 338` ```lemmas Zfun_mult = mult.Zfun ``` huffman@31349 ` 339` ```lemmas Zfun_mult_right = mult.Zfun_right ``` huffman@31349 ` 340` ```lemmas Zfun_mult_left = mult.Zfun_left ``` huffman@31349 ` 341` huffman@31349 ` 342` wenzelm@31902 ` 343` ```subsection {* Limits *} ``` huffman@31349 ` 344` huffman@31349 ` 345` ```definition ``` huffman@31488 ` 346` ``` tendsto :: "('a \ 'b::topological_space) \ 'b \ 'a net \ bool" ``` huffman@31488 ` 347` ``` (infixr "--->" 55) ``` huffman@31488 ` 348` ```where [code del]: ``` huffman@31492 ` 349` ``` "(f ---> l) net \ (\S. open S \ l \ S \ eventually (\x. f x \ S) net)" ``` huffman@31349 ` 350` wenzelm@31902 ` 351` ```ML {* ``` wenzelm@31902 ` 352` ```structure Tendsto_Intros = Named_Thms ``` wenzelm@31902 ` 353` ```( ``` wenzelm@31902 ` 354` ``` val name = "tendsto_intros" ``` wenzelm@31902 ` 355` ``` val description = "introduction rules for tendsto" ``` wenzelm@31902 ` 356` ```) ``` huffman@31565 ` 357` ```*} ``` huffman@31565 ` 358` wenzelm@31902 ` 359` ```setup Tendsto_Intros.setup ``` huffman@31565 ` 360` huffman@31488 ` 361` ```lemma topological_tendstoI: ``` huffman@31492 ` 362` ``` "(\S. open S \ l \ S \ eventually (\x. f x \ S) net) ``` huffman@31487 ` 363` ``` \ (f ---> l) net" ``` huffman@31349 ` 364` ``` unfolding tendsto_def by auto ``` huffman@31349 ` 365` huffman@31488 ` 366` ```lemma topological_tendstoD: ``` huffman@31492 ` 367` ``` "(f ---> l) net \ open S \ l \ S \ eventually (\x. f x \ S) net" ``` huffman@31488 ` 368` ``` unfolding tendsto_def by auto ``` huffman@31488 ` 369` huffman@31488 ` 370` ```lemma tendstoI: ``` huffman@31488 ` 371` ``` assumes "\e. 0 < e \ eventually (\x. dist (f x) l < e) net" ``` huffman@31488 ` 372` ``` shows "(f ---> l) net" ``` huffman@31488 ` 373` ```apply (rule topological_tendstoI) ``` huffman@31492 ` 374` ```apply (simp add: open_dist) ``` huffman@31488 ` 375` ```apply (drule (1) bspec, clarify) ``` huffman@31488 ` 376` ```apply (drule assms) ``` huffman@31488 ` 377` ```apply (erule eventually_elim1, simp) ``` huffman@31488 ` 378` ```done ``` huffman@31488 ` 379` huffman@31349 ` 380` ```lemma tendstoD: ``` huffman@31487 ` 381` ``` "(f ---> l) net \ 0 < e \ eventually (\x. dist (f x) l < e) net" ``` huffman@31488 ` 382` ```apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) ``` huffman@31492 ` 383` ```apply (clarsimp simp add: open_dist) ``` huffman@31488 ` 384` ```apply (rule_tac x="e - dist x l" in exI, clarsimp) ``` huffman@31488 ` 385` ```apply (simp only: less_diff_eq) ``` huffman@31488 ` 386` ```apply (erule le_less_trans [OF dist_triangle]) ``` huffman@31488 ` 387` ```apply simp ``` huffman@31488 ` 388` ```apply simp ``` huffman@31488 ` 389` ```done ``` huffman@31488 ` 390` huffman@31488 ` 391` ```lemma tendsto_iff: ``` huffman@31488 ` 392` ``` "(f ---> l) net \ (\e>0. eventually (\x. dist (f x) l < e) net)" ``` huffman@31488 ` 393` ```using tendstoI tendstoD by fast ``` huffman@31349 ` 394` huffman@31487 ` 395` ```lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\x. f x - a) net" ``` huffman@31488 ` 396` ```by (simp only: tendsto_iff Zfun_def dist_norm) ``` huffman@31349 ` 397` huffman@31565 ` 398` ```lemma tendsto_ident_at [tendsto_intros]: "((\x. x) ---> a) (at a)" ``` huffman@31565 ` 399` ```unfolding tendsto_def eventually_at_topological by auto ``` huffman@31565 ` 400` huffman@31565 ` 401` ```lemma tendsto_ident_at_within [tendsto_intros]: ``` huffman@31565 ` 402` ``` "a \ S \ ((\x. x) ---> a) (at a within S)" ``` huffman@31565 ` 403` ```unfolding tendsto_def eventually_within eventually_at_topological by auto ``` huffman@31565 ` 404` huffman@31565 ` 405` ```lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) net" ``` huffman@31349 ` 406` ```by (simp add: tendsto_def) ``` huffman@31349 ` 407` huffman@31565 ` 408` ```lemma tendsto_dist [tendsto_intros]: ``` huffman@31565 ` 409` ``` assumes f: "(f ---> l) net" and g: "(g ---> m) net" ``` huffman@31565 ` 410` ``` shows "((\x. dist (f x) (g x)) ---> dist l m) net" ``` huffman@31565 ` 411` ```proof (rule tendstoI) ``` huffman@31565 ` 412` ``` fix e :: real assume "0 < e" ``` huffman@31565 ` 413` ``` hence e2: "0 < e/2" by simp ``` huffman@31565 ` 414` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` huffman@31565 ` 415` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) net" ``` huffman@31565 ` 416` ``` proof (rule eventually_elim2) ``` huffman@31565 ` 417` ``` fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2" ``` huffman@31565 ` 418` ``` then show "dist (dist (f x) (g x)) (dist l m) < e" ``` huffman@31565 ` 419` ``` unfolding dist_real_def ``` huffman@31565 ` 420` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` huffman@31565 ` 421` ``` using dist_triangle2 [of "g x" "l" "m"] ``` huffman@31565 ` 422` ``` using dist_triangle3 [of "l" "m" "f x"] ``` huffman@31565 ` 423` ``` using dist_triangle [of "f x" "m" "g x"] ``` huffman@31565 ` 424` ``` by arith ``` huffman@31565 ` 425` ``` qed ``` huffman@31565 ` 426` ```qed ``` huffman@31565 ` 427` huffman@31565 ` 428` ```lemma tendsto_norm [tendsto_intros]: ``` huffman@31565 ` 429` ``` "(f ---> a) net \ ((\x. norm (f x)) ---> norm a) net" ``` huffman@31488 ` 430` ```apply (simp add: tendsto_iff dist_norm, safe) ``` huffman@31349 ` 431` ```apply (drule_tac x="e" in spec, safe) ``` huffman@31349 ` 432` ```apply (erule eventually_elim1) ``` huffman@31349 ` 433` ```apply (erule order_le_less_trans [OF norm_triangle_ineq3]) ``` huffman@31349 ` 434` ```done ``` huffman@31349 ` 435` huffman@31349 ` 436` ```lemma add_diff_add: ``` huffman@31349 ` 437` ``` fixes a b c d :: "'a::ab_group_add" ``` huffman@31349 ` 438` ``` shows "(a + c) - (b + d) = (a - b) + (c - d)" ``` huffman@31349 ` 439` ```by simp ``` huffman@31349 ` 440` huffman@31349 ` 441` ```lemma minus_diff_minus: ``` huffman@31349 ` 442` ``` fixes a b :: "'a::ab_group_add" ``` huffman@31349 ` 443` ``` shows "(- a) - (- b) = - (a - b)" ``` huffman@31349 ` 444` ```by simp ``` huffman@31349 ` 445` huffman@31565 ` 446` ```lemma tendsto_add [tendsto_intros]: ``` huffman@31349 ` 447` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@31487 ` 448` ``` shows "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x + g x) ---> a + b) net" ``` huffman@31349 ` 449` ```by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) ``` huffman@31349 ` 450` huffman@31565 ` 451` ```lemma tendsto_minus [tendsto_intros]: ``` huffman@31349 ` 452` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31487 ` 453` ``` shows "(f ---> a) net \ ((\x. - f x) ---> - a) net" ``` huffman@31349 ` 454` ```by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) ``` huffman@31349 ` 455` huffman@31349 ` 456` ```lemma tendsto_minus_cancel: ``` huffman@31349 ` 457` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31487 ` 458` ``` shows "((\x. - f x) ---> - a) net \ (f ---> a) net" ``` huffman@31349 ` 459` ```by (drule tendsto_minus, simp) ``` huffman@31349 ` 460` huffman@31565 ` 461` ```lemma tendsto_diff [tendsto_intros]: ``` huffman@31349 ` 462` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@31487 ` 463` ``` shows "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x - g x) ---> a - b) net" ``` huffman@31349 ` 464` ```by (simp add: diff_minus tendsto_add tendsto_minus) ``` huffman@31349 ` 465` huffman@31588 ` 466` ```lemma tendsto_setsum [tendsto_intros]: ``` huffman@31588 ` 467` ``` fixes f :: "'a \ 'b \ 'c::real_normed_vector" ``` huffman@31588 ` 468` ``` assumes "\i. i \ S \ (f i ---> a i) net" ``` huffman@31588 ` 469` ``` shows "((\x. \i\S. f i x) ---> (\i\S. a i)) net" ``` huffman@31588 ` 470` ```proof (cases "finite S") ``` huffman@31588 ` 471` ``` assume "finite S" thus ?thesis using assms ``` huffman@31588 ` 472` ``` proof (induct set: finite) ``` huffman@31588 ` 473` ``` case empty show ?case ``` huffman@31588 ` 474` ``` by (simp add: tendsto_const) ``` huffman@31588 ` 475` ``` next ``` huffman@31588 ` 476` ``` case (insert i F) thus ?case ``` huffman@31588 ` 477` ``` by (simp add: tendsto_add) ``` huffman@31588 ` 478` ``` qed ``` huffman@31588 ` 479` ```next ``` huffman@31588 ` 480` ``` assume "\ finite S" thus ?thesis ``` huffman@31588 ` 481` ``` by (simp add: tendsto_const) ``` huffman@31588 ` 482` ```qed ``` huffman@31588 ` 483` huffman@31565 ` 484` ```lemma (in bounded_linear) tendsto [tendsto_intros]: ``` huffman@31487 ` 485` ``` "(g ---> a) net \ ((\x. f (g x)) ---> f a) net" ``` huffman@31349 ` 486` ```by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) ``` huffman@31349 ` 487` huffman@31565 ` 488` ```lemma (in bounded_bilinear) tendsto [tendsto_intros]: ``` huffman@31487 ` 489` ``` "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x ** g x) ---> a ** b) net" ``` huffman@31349 ` 490` ```by (simp only: tendsto_Zfun_iff prod_diff_prod ``` huffman@31349 ` 491` ``` Zfun_add Zfun Zfun_left Zfun_right) ``` huffman@31349 ` 492` huffman@31355 ` 493` huffman@31355 ` 494` ```subsection {* Continuity of Inverse *} ``` huffman@31355 ` 495` huffman@31355 ` 496` ```lemma (in bounded_bilinear) Zfun_prod_Bfun: ``` huffman@31487 ` 497` ``` assumes f: "Zfun f net" ``` huffman@31487 ` 498` ``` assumes g: "Bfun g net" ``` huffman@31487 ` 499` ``` shows "Zfun (\x. f x ** g x) net" ``` huffman@31355 ` 500` ```proof - ``` huffman@31355 ` 501` ``` obtain K where K: "0 \ K" ``` huffman@31355 ` 502` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31355 ` 503` ``` using nonneg_bounded by fast ``` huffman@31355 ` 504` ``` obtain B where B: "0 < B" ``` huffman@31487 ` 505` ``` and norm_g: "eventually (\x. norm (g x) \ B) net" ``` huffman@31487 ` 506` ``` using g by (rule BfunE) ``` huffman@31487 ` 507` ``` have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) net" ``` huffman@31487 ` 508` ``` using norm_g proof (rule eventually_elim1) ``` huffman@31487 ` 509` ``` fix x ``` huffman@31487 ` 510` ``` assume *: "norm (g x) \ B" ``` huffman@31487 ` 511` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31355 ` 512` ``` by (rule norm_le) ``` huffman@31487 ` 513` ``` also have "\ \ norm (f x) * B * K" ``` huffman@31487 ` 514` ``` by (intro mult_mono' order_refl norm_g norm_ge_zero ``` huffman@31355 ` 515` ``` mult_nonneg_nonneg K *) ``` huffman@31487 ` 516` ``` also have "\ = norm (f x) * (B * K)" ``` huffman@31355 ` 517` ``` by (rule mult_assoc) ``` huffman@31487 ` 518` ``` finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . ``` huffman@31355 ` 519` ``` qed ``` huffman@31487 ` 520` ``` with f show ?thesis ``` huffman@31487 ` 521` ``` by (rule Zfun_imp_Zfun) ``` huffman@31355 ` 522` ```qed ``` huffman@31355 ` 523` huffman@31355 ` 524` ```lemma (in bounded_bilinear) flip: ``` huffman@31355 ` 525` ``` "bounded_bilinear (\x y. y ** x)" ``` huffman@31355 ` 526` ```apply default ``` huffman@31355 ` 527` ```apply (rule add_right) ``` huffman@31355 ` 528` ```apply (rule add_left) ``` huffman@31355 ` 529` ```apply (rule scaleR_right) ``` huffman@31355 ` 530` ```apply (rule scaleR_left) ``` huffman@31355 ` 531` ```apply (subst mult_commute) ``` huffman@31355 ` 532` ```using bounded by fast ``` huffman@31355 ` 533` huffman@31355 ` 534` ```lemma (in bounded_bilinear) Bfun_prod_Zfun: ``` huffman@31487 ` 535` ``` assumes f: "Bfun f net" ``` huffman@31487 ` 536` ``` assumes g: "Zfun g net" ``` huffman@31487 ` 537` ``` shows "Zfun (\x. f x ** g x) net" ``` huffman@31487 ` 538` ```using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) ``` huffman@31355 ` 539` huffman@31355 ` 540` ```lemma inverse_diff_inverse: ``` huffman@31355 ` 541` ``` "\(a::'a::division_ring) \ 0; b \ 0\ ``` huffman@31355 ` 542` ``` \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" ``` huffman@31355 ` 543` ```by (simp add: algebra_simps) ``` huffman@31355 ` 544` huffman@31355 ` 545` ```lemma Bfun_inverse_lemma: ``` huffman@31355 ` 546` ``` fixes x :: "'a::real_normed_div_algebra" ``` huffman@31355 ` 547` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` huffman@31355 ` 548` ```apply (subst nonzero_norm_inverse, clarsimp) ``` huffman@31355 ` 549` ```apply (erule (1) le_imp_inverse_le) ``` huffman@31355 ` 550` ```done ``` huffman@31355 ` 551` huffman@31355 ` 552` ```lemma Bfun_inverse: ``` huffman@31355 ` 553` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@31487 ` 554` ``` assumes f: "(f ---> a) net" ``` huffman@31355 ` 555` ``` assumes a: "a \ 0" ``` huffman@31487 ` 556` ``` shows "Bfun (\x. inverse (f x)) net" ``` huffman@31355 ` 557` ```proof - ``` huffman@31355 ` 558` ``` from a have "0 < norm a" by simp ``` huffman@31355 ` 559` ``` hence "\r>0. r < norm a" by (rule dense) ``` huffman@31355 ` 560` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" by fast ``` huffman@31487 ` 561` ``` have "eventually (\x. dist (f x) a < r) net" ``` huffman@31487 ` 562` ``` using tendstoD [OF f r1] by fast ``` huffman@31487 ` 563` ``` hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) net" ``` huffman@31355 ` 564` ``` proof (rule eventually_elim1) ``` huffman@31487 ` 565` ``` fix x ``` huffman@31487 ` 566` ``` assume "dist (f x) a < r" ``` huffman@31487 ` 567` ``` hence 1: "norm (f x - a) < r" ``` huffman@31355 ` 568` ``` by (simp add: dist_norm) ``` huffman@31487 ` 569` ``` hence 2: "f x \ 0" using r2 by auto ``` huffman@31487 ` 570` ``` hence "norm (inverse (f x)) = inverse (norm (f x))" ``` huffman@31355 ` 571` ``` by (rule nonzero_norm_inverse) ``` huffman@31355 ` 572` ``` also have "\ \ inverse (norm a - r)" ``` huffman@31355 ` 573` ``` proof (rule le_imp_inverse_le) ``` huffman@31355 ` 574` ``` show "0 < norm a - r" using r2 by simp ``` huffman@31355 ` 575` ``` next ``` huffman@31487 ` 576` ``` have "norm a - norm (f x) \ norm (a - f x)" ``` huffman@31355 ` 577` ``` by (rule norm_triangle_ineq2) ``` huffman@31487 ` 578` ``` also have "\ = norm (f x - a)" ``` huffman@31355 ` 579` ``` by (rule norm_minus_commute) ``` huffman@31355 ` 580` ``` also have "\ < r" using 1 . ``` huffman@31487 ` 581` ``` finally show "norm a - r \ norm (f x)" by simp ``` huffman@31355 ` 582` ``` qed ``` huffman@31487 ` 583` ``` finally show "norm (inverse (f x)) \ inverse (norm a - r)" . ``` huffman@31355 ` 584` ``` qed ``` huffman@31355 ` 585` ``` thus ?thesis by (rule BfunI) ``` huffman@31355 ` 586` ```qed ``` huffman@31355 ` 587` huffman@31355 ` 588` ```lemma tendsto_inverse_lemma: ``` huffman@31355 ` 589` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@31487 ` 590` ``` shows "\(f ---> a) net; a \ 0; eventually (\x. f x \ 0) net\ ``` huffman@31487 ` 591` ``` \ ((\x. inverse (f x)) ---> inverse a) net" ``` huffman@31355 ` 592` ```apply (subst tendsto_Zfun_iff) ``` huffman@31355 ` 593` ```apply (rule Zfun_ssubst) ``` huffman@31355 ` 594` ```apply (erule eventually_elim1) ``` huffman@31355 ` 595` ```apply (erule (1) inverse_diff_inverse) ``` huffman@31355 ` 596` ```apply (rule Zfun_minus) ``` huffman@31355 ` 597` ```apply (rule Zfun_mult_left) ``` huffman@31355 ` 598` ```apply (rule mult.Bfun_prod_Zfun) ``` huffman@31355 ` 599` ```apply (erule (1) Bfun_inverse) ``` huffman@31355 ` 600` ```apply (simp add: tendsto_Zfun_iff) ``` huffman@31355 ` 601` ```done ``` huffman@31355 ` 602` huffman@31565 ` 603` ```lemma tendsto_inverse [tendsto_intros]: ``` huffman@31355 ` 604` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@31487 ` 605` ``` assumes f: "(f ---> a) net" ``` huffman@31355 ` 606` ``` assumes a: "a \ 0" ``` huffman@31487 ` 607` ``` shows "((\x. inverse (f x)) ---> inverse a) net" ``` huffman@31355 ` 608` ```proof - ``` huffman@31355 ` 609` ``` from a have "0 < norm a" by simp ``` huffman@31487 ` 610` ``` with f have "eventually (\x. dist (f x) a < norm a) net" ``` huffman@31355 ` 611` ``` by (rule tendstoD) ``` huffman@31487 ` 612` ``` then have "eventually (\x. f x \ 0) net" ``` huffman@31355 ` 613` ``` unfolding dist_norm by (auto elim!: eventually_elim1) ``` huffman@31487 ` 614` ``` with f a show ?thesis ``` huffman@31355 ` 615` ``` by (rule tendsto_inverse_lemma) ``` huffman@31355 ` 616` ```qed ``` huffman@31355 ` 617` huffman@31565 ` 618` ```lemma tendsto_divide [tendsto_intros]: ``` huffman@31355 ` 619` ``` fixes a b :: "'a::real_normed_field" ``` huffman@31487 ` 620` ``` shows "\(f ---> a) net; (g ---> b) net; b \ 0\ ``` huffman@31487 ` 621` ``` \ ((\x. f x / g x) ---> a / b) net" ``` huffman@31355 ` 622` ```by (simp add: mult.tendsto tendsto_inverse divide_inverse) ``` huffman@31355 ` 623` huffman@31349 ` 624` ```end ```