src/HOL/Limits.thy
 author hoelzl Tue Nov 27 19:31:11 2012 +0100 (2012-11-27) changeset 50247 491c5c81c2e8 parent 49834 b27bbb021df1 child 50322 b06b95a5fda2 permissions -rw-r--r--
introduce filter_lim as a generatlization of tendsto
 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` wenzelm@49834 ` 23` ```typedef '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@44195 ` 28` ```lemma is_filter_Rep_filter: "is_filter (Rep_filter F)" ``` huffman@44195 ` 29` ``` using Rep_filter [of F] 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@44195 ` 39` ``` where "eventually P F \ Rep_filter F 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@44195 ` 46` ``` shows "F = F' \ (\P. eventually P F = eventually P F')" ``` huffman@44081 ` 47` ``` unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. ``` huffman@36360 ` 48` huffman@44195 ` 49` ```lemma eventually_True [simp]: "eventually (\x. True) F" ``` huffman@44081 ` 50` ``` unfolding eventually_def ``` huffman@44081 ` 51` ``` by (rule is_filter.True [OF is_filter_Rep_filter]) ``` huffman@31349 ` 52` huffman@44195 ` 53` ```lemma always_eventually: "\x. P x \ eventually P F" ``` huffman@36630 ` 54` ```proof - ``` huffman@36630 ` 55` ``` assume "\x. P x" hence "P = (\x. True)" by (simp add: ext) ``` huffman@44195 ` 56` ``` thus "eventually P F" by simp ``` huffman@36630 ` 57` ```qed ``` huffman@36630 ` 58` huffman@31349 ` 59` ```lemma eventually_mono: ``` huffman@44195 ` 60` ``` "(\x. P x \ Q x) \ eventually P F \ eventually Q F" ``` 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@44195 ` 65` ``` assumes P: "eventually (\x. P x) F" ``` huffman@44195 ` 66` ``` assumes Q: "eventually (\x. Q x) F" ``` huffman@44195 ` 67` ``` shows "eventually (\x. P x \ Q x) F" ``` 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@44195 ` 72` ``` assumes "eventually (\x. P x \ Q x) F" ``` huffman@44195 ` 73` ``` assumes "eventually (\x. P x) F" ``` huffman@44195 ` 74` ``` shows "eventually (\x. Q x) F" ``` huffman@31349 ` 75` ```proof (rule eventually_mono) ``` huffman@31349 ` 76` ``` show "\x. (P x \ Q x) \ P x \ Q x" by simp ``` huffman@44195 ` 77` ``` show "eventually (\x. (P x \ Q x) \ P x) F" ``` huffman@31349 ` 78` ``` using assms by (rule eventually_conj) ``` huffman@31349 ` 79` ```qed ``` huffman@31349 ` 80` huffman@31349 ` 81` ```lemma eventually_rev_mp: ``` huffman@44195 ` 82` ``` assumes "eventually (\x. P x) F" ``` huffman@44195 ` 83` ``` assumes "eventually (\x. P x \ Q x) F" ``` huffman@44195 ` 84` ``` shows "eventually (\x. Q x) F" ``` huffman@31349 ` 85` ```using assms(2) assms(1) by (rule eventually_mp) ``` huffman@31349 ` 86` huffman@31349 ` 87` ```lemma eventually_conj_iff: ``` huffman@44195 ` 88` ``` "eventually (\x. P x \ Q x) F \ eventually P F \ eventually Q F" ``` huffman@44081 ` 89` ``` by (auto intro: eventually_conj elim: eventually_rev_mp) ``` huffman@31349 ` 90` huffman@31349 ` 91` ```lemma eventually_elim1: ``` huffman@44195 ` 92` ``` assumes "eventually (\i. P i) F" ``` huffman@31349 ` 93` ``` assumes "\i. P i \ Q i" ``` huffman@44195 ` 94` ``` shows "eventually (\i. Q i) F" ``` huffman@44081 ` 95` ``` using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 96` huffman@31349 ` 97` ```lemma eventually_elim2: ``` huffman@44195 ` 98` ``` assumes "eventually (\i. P i) F" ``` huffman@44195 ` 99` ``` assumes "eventually (\i. Q i) F" ``` huffman@31349 ` 100` ``` assumes "\i. P i \ Q i \ R i" ``` huffman@44195 ` 101` ``` shows "eventually (\i. R i) F" ``` huffman@44081 ` 102` ``` using assms by (auto elim!: eventually_rev_mp) ``` huffman@31349 ` 103` noschinl@45892 ` 104` ```lemma eventually_subst: ``` noschinl@45892 ` 105` ``` assumes "eventually (\n. P n = Q n) F" ``` noschinl@45892 ` 106` ``` shows "eventually P F = eventually Q F" (is "?L = ?R") ``` noschinl@45892 ` 107` ```proof - ``` noschinl@45892 ` 108` ``` from assms have "eventually (\x. P x \ Q x) F" ``` noschinl@45892 ` 109` ``` and "eventually (\x. Q x \ P x) F" ``` noschinl@45892 ` 110` ``` by (auto elim: eventually_elim1) ``` noschinl@45892 ` 111` ``` then show ?thesis by (auto elim: eventually_elim2) ``` noschinl@45892 ` 112` ```qed ``` noschinl@45892 ` 113` noschinl@46886 ` 114` ```ML {* ``` wenzelm@47432 ` 115` ``` fun eventually_elim_tac ctxt thms thm = ``` wenzelm@47432 ` 116` ``` let ``` noschinl@46886 ` 117` ``` val thy = Proof_Context.theory_of ctxt ``` noschinl@46886 ` 118` ``` val mp_thms = thms RL [@{thm eventually_rev_mp}] ``` noschinl@46886 ` 119` ``` val raw_elim_thm = ``` noschinl@46886 ` 120` ``` (@{thm allI} RS @{thm always_eventually}) ``` noschinl@46886 ` 121` ``` |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms ``` noschinl@46886 ` 122` ``` |> fold (fn _ => fn thm => @{thm impI} RS thm) thms ``` noschinl@46886 ` 123` ``` val cases_prop = prop_of (raw_elim_thm RS thm) ``` noschinl@46886 ` 124` ``` val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])]) ``` noschinl@46886 ` 125` ``` in ``` noschinl@46886 ` 126` ``` CASES cases (rtac raw_elim_thm 1) thm ``` noschinl@46886 ` 127` ``` end ``` noschinl@46886 ` 128` ```*} ``` noschinl@46886 ` 129` wenzelm@47432 ` 130` ```method_setup eventually_elim = {* ``` wenzelm@47432 ` 131` ``` Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt)) ``` wenzelm@47432 ` 132` ```*} "elimination of eventually quantifiers" ``` noschinl@45892 ` 133` noschinl@45892 ` 134` huffman@36360 ` 135` ```subsection {* Finer-than relation *} ``` huffman@36360 ` 136` huffman@44195 ` 137` ```text {* @{term "F \ F'"} means that filter @{term F} is finer than ``` huffman@44195 ` 138` ```filter @{term F'}. *} ``` huffman@36360 ` 139` huffman@44081 ` 140` ```instantiation filter :: (type) complete_lattice ``` huffman@36360 ` 141` ```begin ``` huffman@36360 ` 142` huffman@44081 ` 143` ```definition le_filter_def: ``` huffman@44195 ` 144` ``` "F \ F' \ (\P. eventually P F' \ eventually P F)" ``` huffman@36360 ` 145` huffman@36360 ` 146` ```definition ``` huffman@44195 ` 147` ``` "(F :: 'a filter) < F' \ F \ F' \ \ F' \ F" ``` huffman@36360 ` 148` huffman@36360 ` 149` ```definition ``` huffman@44081 ` 150` ``` "top = Abs_filter (\P. \x. P x)" ``` huffman@36630 ` 151` huffman@36630 ` 152` ```definition ``` huffman@44081 ` 153` ``` "bot = Abs_filter (\P. True)" ``` huffman@36360 ` 154` huffman@36630 ` 155` ```definition ``` huffman@44195 ` 156` ``` "sup F F' = Abs_filter (\P. eventually P F \ eventually P F')" ``` huffman@36630 ` 157` huffman@36630 ` 158` ```definition ``` huffman@44195 ` 159` ``` "inf F F' = Abs_filter ``` huffman@44195 ` 160` ``` (\P. \Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))" ``` huffman@36630 ` 161` huffman@36630 ` 162` ```definition ``` huffman@44195 ` 163` ``` "Sup S = Abs_filter (\P. \F\S. eventually P F)" ``` huffman@36630 ` 164` huffman@36630 ` 165` ```definition ``` huffman@44195 ` 166` ``` "Inf S = Sup {F::'a filter. \F'\S. F \ F'}" ``` huffman@36630 ` 167` huffman@36630 ` 168` ```lemma eventually_top [simp]: "eventually P top \ (\x. P x)" ``` huffman@44081 ` 169` ``` unfolding top_filter_def ``` huffman@44081 ` 170` ``` by (rule eventually_Abs_filter, rule is_filter.intro, auto) ``` huffman@36630 ` 171` huffman@36629 ` 172` ```lemma eventually_bot [simp]: "eventually P bot" ``` huffman@44081 ` 173` ``` unfolding bot_filter_def ``` huffman@44081 ` 174` ``` by (subst eventually_Abs_filter, rule is_filter.intro, auto) ``` huffman@36360 ` 175` huffman@36630 ` 176` ```lemma eventually_sup: ``` huffman@44195 ` 177` ``` "eventually P (sup F F') \ eventually P F \ eventually P F'" ``` huffman@44081 ` 178` ``` unfolding sup_filter_def ``` huffman@44081 ` 179` ``` by (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 180` ``` (auto elim!: eventually_rev_mp) ``` huffman@36630 ` 181` huffman@36630 ` 182` ```lemma eventually_inf: ``` huffman@44195 ` 183` ``` "eventually P (inf F F') \ ``` huffman@44195 ` 184` ``` (\Q R. eventually Q F \ eventually R F' \ (\x. Q x \ R x \ P x))" ``` huffman@44081 ` 185` ``` unfolding inf_filter_def ``` huffman@44081 ` 186` ``` apply (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 187` ``` apply (fast intro: eventually_True) ``` huffman@44081 ` 188` ``` apply clarify ``` huffman@44081 ` 189` ``` apply (intro exI conjI) ``` huffman@44081 ` 190` ``` apply (erule (1) eventually_conj) ``` huffman@44081 ` 191` ``` apply (erule (1) eventually_conj) ``` huffman@44081 ` 192` ``` apply simp ``` huffman@44081 ` 193` ``` apply auto ``` huffman@44081 ` 194` ``` done ``` huffman@36630 ` 195` huffman@36630 ` 196` ```lemma eventually_Sup: ``` huffman@44195 ` 197` ``` "eventually P (Sup S) \ (\F\S. eventually P F)" ``` huffman@44081 ` 198` ``` unfolding Sup_filter_def ``` huffman@44081 ` 199` ``` apply (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 200` ``` apply (auto intro: eventually_conj elim!: eventually_rev_mp) ``` huffman@44081 ` 201` ``` done ``` huffman@36630 ` 202` huffman@36360 ` 203` ```instance proof ``` huffman@44195 ` 204` ``` fix F F' F'' :: "'a filter" and S :: "'a filter set" ``` huffman@44195 ` 205` ``` { show "F < F' \ F \ F' \ \ F' \ F" ``` huffman@44195 ` 206` ``` by (rule less_filter_def) } ``` huffman@44195 ` 207` ``` { show "F \ F" ``` huffman@44195 ` 208` ``` unfolding le_filter_def by simp } ``` huffman@44195 ` 209` ``` { assume "F \ F'" and "F' \ F''" thus "F \ F''" ``` huffman@44195 ` 210` ``` unfolding le_filter_def by simp } ``` huffman@44195 ` 211` ``` { assume "F \ F'" and "F' \ F" thus "F = F'" ``` huffman@44195 ` 212` ``` unfolding le_filter_def filter_eq_iff by fast } ``` huffman@44195 ` 213` ``` { show "F \ top" ``` huffman@44195 ` 214` ``` unfolding le_filter_def eventually_top by (simp add: always_eventually) } ``` huffman@44195 ` 215` ``` { show "bot \ F" ``` huffman@44195 ` 216` ``` unfolding le_filter_def by simp } ``` huffman@44195 ` 217` ``` { show "F \ sup F F'" and "F' \ sup F F'" ``` huffman@44195 ` 218` ``` unfolding le_filter_def eventually_sup by simp_all } ``` huffman@44195 ` 219` ``` { assume "F \ F''" and "F' \ F''" thus "sup F F' \ F''" ``` huffman@44195 ` 220` ``` unfolding le_filter_def eventually_sup by simp } ``` huffman@44195 ` 221` ``` { show "inf F F' \ F" and "inf F F' \ F'" ``` huffman@44195 ` 222` ``` unfolding le_filter_def eventually_inf by (auto intro: eventually_True) } ``` huffman@44195 ` 223` ``` { assume "F \ F'" and "F \ F''" thus "F \ inf F' F''" ``` huffman@44081 ` 224` ``` unfolding le_filter_def eventually_inf ``` huffman@44195 ` 225` ``` by (auto elim!: eventually_mono intro: eventually_conj) } ``` huffman@44195 ` 226` ``` { assume "F \ S" thus "F \ Sup S" ``` huffman@44195 ` 227` ``` unfolding le_filter_def eventually_Sup by simp } ``` huffman@44195 ` 228` ``` { assume "\F. F \ S \ F \ F'" thus "Sup S \ F'" ``` huffman@44195 ` 229` ``` unfolding le_filter_def eventually_Sup by simp } ``` huffman@44195 ` 230` ``` { assume "F'' \ S" thus "Inf S \ F''" ``` huffman@44195 ` 231` ``` unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } ``` huffman@44195 ` 232` ``` { assume "\F'. F' \ S \ F \ F'" thus "F \ Inf S" ``` huffman@44195 ` 233` ``` unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp } ``` huffman@36360 ` 234` ```qed ``` huffman@36360 ` 235` huffman@36360 ` 236` ```end ``` huffman@36360 ` 237` huffman@44081 ` 238` ```lemma filter_leD: ``` huffman@44195 ` 239` ``` "F \ F' \ eventually P F' \ eventually P F" ``` huffman@44081 ` 240` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 241` huffman@44081 ` 242` ```lemma filter_leI: ``` huffman@44195 ` 243` ``` "(\P. eventually P F' \ eventually P F) \ F \ F'" ``` huffman@44081 ` 244` ``` unfolding le_filter_def by simp ``` huffman@36360 ` 245` huffman@36360 ` 246` ```lemma eventually_False: ``` huffman@44195 ` 247` ``` "eventually (\x. False) F \ F = bot" ``` huffman@44081 ` 248` ``` unfolding filter_eq_iff by (auto elim: eventually_rev_mp) ``` huffman@36360 ` 249` huffman@44342 ` 250` ```abbreviation (input) trivial_limit :: "'a filter \ bool" ``` huffman@44342 ` 251` ``` where "trivial_limit F \ F = bot" ``` huffman@44342 ` 252` huffman@44342 ` 253` ```lemma trivial_limit_def: "trivial_limit F \ eventually (\x. False) F" ``` huffman@44342 ` 254` ``` by (rule eventually_False [symmetric]) ``` huffman@44342 ` 255` huffman@44342 ` 256` huffman@44081 ` 257` ```subsection {* Map function for filters *} ``` huffman@36654 ` 258` huffman@44081 ` 259` ```definition filtermap :: "('a \ 'b) \ 'a filter \ 'b filter" ``` huffman@44195 ` 260` ``` where "filtermap f F = Abs_filter (\P. eventually (\x. P (f x)) F)" ``` huffman@36654 ` 261` huffman@44081 ` 262` ```lemma eventually_filtermap: ``` huffman@44195 ` 263` ``` "eventually P (filtermap f F) = eventually (\x. P (f x)) F" ``` huffman@44081 ` 264` ``` unfolding filtermap_def ``` huffman@44081 ` 265` ``` apply (rule eventually_Abs_filter) ``` huffman@44081 ` 266` ``` apply (rule is_filter.intro) ``` huffman@44081 ` 267` ``` apply (auto elim!: eventually_rev_mp) ``` huffman@44081 ` 268` ``` done ``` huffman@36654 ` 269` huffman@44195 ` 270` ```lemma filtermap_ident: "filtermap (\x. x) F = F" ``` huffman@44081 ` 271` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 272` huffman@44081 ` 273` ```lemma filtermap_filtermap: ``` huffman@44195 ` 274` ``` "filtermap f (filtermap g F) = filtermap (\x. f (g x)) F" ``` huffman@44081 ` 275` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 276` huffman@44195 ` 277` ```lemma filtermap_mono: "F \ F' \ filtermap f F \ filtermap f F'" ``` huffman@44081 ` 278` ``` unfolding le_filter_def eventually_filtermap by simp ``` huffman@44081 ` 279` huffman@44081 ` 280` ```lemma filtermap_bot [simp]: "filtermap f bot = bot" ``` huffman@44081 ` 281` ``` by (simp add: filter_eq_iff eventually_filtermap) ``` huffman@36654 ` 282` hoelzl@50247 ` 283` ```subsection {* Order filters *} ``` huffman@31392 ` 284` hoelzl@50247 ` 285` ```definition at_top :: "('a::order) filter" ``` hoelzl@50247 ` 286` ``` where "at_top = Abs_filter (\P. \k. \n\k. P n)" ``` huffman@31392 ` 287` hoelzl@50247 ` 288` ```lemma eventually_at_top_linorder: ``` hoelzl@50247 ` 289` ``` fixes P :: "'a::linorder \ bool" shows "eventually P at_top \ (\N. \n\N. P n)" ``` hoelzl@50247 ` 290` ``` unfolding at_top_def ``` huffman@44081 ` 291` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` hoelzl@50247 ` 292` ``` fix P Q :: "'a \ bool" ``` huffman@36662 ` 293` ``` assume "\i. \n\i. P n" and "\j. \n\j. Q n" ``` huffman@36662 ` 294` ``` then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto ``` huffman@36662 ` 295` ``` then have "\n\max i j. P n \ Q n" by simp ``` huffman@36662 ` 296` ``` then show "\k. \n\k. P n \ Q n" .. ``` huffman@36662 ` 297` ```qed auto ``` huffman@36662 ` 298` hoelzl@50247 ` 299` ```lemma eventually_at_top_dense: ``` hoelzl@50247 ` 300` ``` fixes P :: "'a::dense_linorder \ bool" shows "eventually P at_top \ (\N. \n>N. P n)" ``` hoelzl@50247 ` 301` ``` unfolding eventually_at_top_linorder ``` hoelzl@50247 ` 302` ```proof safe ``` hoelzl@50247 ` 303` ``` fix N assume "\n\N. P n" then show "\N. \n>N. P n" by (auto intro!: exI[of _ N]) ``` hoelzl@50247 ` 304` ```next ``` hoelzl@50247 ` 305` ``` fix N assume "\n>N. P n" ``` hoelzl@50247 ` 306` ``` moreover from gt_ex[of N] guess y .. ``` hoelzl@50247 ` 307` ``` ultimately show "\N. \n\N. P n" by (auto intro!: exI[of _ y]) ``` hoelzl@50247 ` 308` ```qed ``` hoelzl@50247 ` 309` hoelzl@50247 ` 310` ```definition at_bot :: "('a::order) filter" ``` hoelzl@50247 ` 311` ``` where "at_bot = Abs_filter (\P. \k. \n\k. P n)" ``` hoelzl@50247 ` 312` hoelzl@50247 ` 313` ```lemma eventually_at_bot_linorder: ``` hoelzl@50247 ` 314` ``` fixes P :: "'a::linorder \ bool" shows "eventually P at_bot \ (\N. \n\N. P n)" ``` hoelzl@50247 ` 315` ``` unfolding at_bot_def ``` hoelzl@50247 ` 316` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` hoelzl@50247 ` 317` ``` fix P Q :: "'a \ bool" ``` hoelzl@50247 ` 318` ``` assume "\i. \n\i. P n" and "\j. \n\j. Q n" ``` hoelzl@50247 ` 319` ``` then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto ``` hoelzl@50247 ` 320` ``` then have "\n\min i j. P n \ Q n" by simp ``` hoelzl@50247 ` 321` ``` then show "\k. \n\k. P n \ Q n" .. ``` hoelzl@50247 ` 322` ```qed auto ``` hoelzl@50247 ` 323` hoelzl@50247 ` 324` ```lemma eventually_at_bot_dense: ``` hoelzl@50247 ` 325` ``` fixes P :: "'a::dense_linorder \ bool" shows "eventually P at_bot \ (\N. \nn\N. P n" then show "\N. \nnN. \n\N. P n" by (auto intro!: exI[of _ y]) ``` hoelzl@50247 ` 333` ```qed ``` hoelzl@50247 ` 334` hoelzl@50247 ` 335` ```subsection {* Sequentially *} ``` hoelzl@50247 ` 336` hoelzl@50247 ` 337` ```abbreviation sequentially :: "nat filter" ``` hoelzl@50247 ` 338` ``` where "sequentially == at_top" ``` hoelzl@50247 ` 339` hoelzl@50247 ` 340` ```lemma sequentially_def: "sequentially = Abs_filter (\P. \k. \n\k. P n)" ``` hoelzl@50247 ` 341` ``` unfolding at_top_def by simp ``` hoelzl@50247 ` 342` hoelzl@50247 ` 343` ```lemma eventually_sequentially: ``` hoelzl@50247 ` 344` ``` "eventually P sequentially \ (\N. \n\N. P n)" ``` hoelzl@50247 ` 345` ``` by (rule eventually_at_top_linorder) ``` hoelzl@50247 ` 346` huffman@44342 ` 347` ```lemma sequentially_bot [simp, intro]: "sequentially \ bot" ``` huffman@44081 ` 348` ``` unfolding filter_eq_iff eventually_sequentially by auto ``` huffman@36662 ` 349` huffman@44342 ` 350` ```lemmas trivial_limit_sequentially = sequentially_bot ``` huffman@44342 ` 351` huffman@36662 ` 352` ```lemma eventually_False_sequentially [simp]: ``` huffman@36662 ` 353` ``` "\ eventually (\n. False) sequentially" ``` huffman@44081 ` 354` ``` by (simp add: eventually_False) ``` huffman@36662 ` 355` huffman@36662 ` 356` ```lemma le_sequentially: ``` huffman@44195 ` 357` ``` "F \ sequentially \ (\N. eventually (\n. N \ n) F)" ``` huffman@44081 ` 358` ``` unfolding le_filter_def eventually_sequentially ``` huffman@44081 ` 359` ``` by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) ``` huffman@36662 ` 360` noschinl@45892 ` 361` ```lemma eventually_sequentiallyI: ``` noschinl@45892 ` 362` ``` assumes "\x. c \ x \ P x" ``` noschinl@45892 ` 363` ``` shows "eventually P sequentially" ``` noschinl@45892 ` 364` ```using assms by (auto simp: eventually_sequentially) ``` noschinl@45892 ` 365` huffman@36662 ` 366` huffman@44081 ` 367` ```subsection {* Standard filters *} ``` huffman@36662 ` 368` huffman@44081 ` 369` ```definition within :: "'a filter \ 'a set \ 'a filter" (infixr "within" 70) ``` huffman@44195 ` 370` ``` where "F within S = Abs_filter (\P. eventually (\x. x \ S \ P x) F)" ``` huffman@31392 ` 371` huffman@44206 ` 372` ```definition (in topological_space) nhds :: "'a \ 'a filter" ``` huffman@44081 ` 373` ``` where "nhds a = Abs_filter (\P. \S. open S \ a \ S \ (\x\S. P x))" ``` huffman@36654 ` 374` huffman@44206 ` 375` ```definition (in topological_space) at :: "'a \ 'a filter" ``` huffman@44081 ` 376` ``` where "at a = nhds a within - {a}" ``` huffman@31447 ` 377` huffman@31392 ` 378` ```lemma eventually_within: ``` huffman@44195 ` 379` ``` "eventually P (F within S) = eventually (\x. x \ S \ P x) F" ``` huffman@44081 ` 380` ``` unfolding within_def ``` huffman@44081 ` 381` ``` by (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@44081 ` 382` ``` (auto elim!: eventually_rev_mp) ``` huffman@31392 ` 383` huffman@45031 ` 384` ```lemma within_UNIV [simp]: "F within UNIV = F" ``` huffman@45031 ` 385` ``` unfolding filter_eq_iff eventually_within by simp ``` huffman@45031 ` 386` huffman@45031 ` 387` ```lemma within_empty [simp]: "F within {} = bot" ``` huffman@44081 ` 388` ``` unfolding filter_eq_iff eventually_within by simp ``` huffman@36360 ` 389` hoelzl@50247 ` 390` ```lemma within_le: "F within S \ F" ``` hoelzl@50247 ` 391` ``` unfolding le_filter_def eventually_within by (auto elim: eventually_elim1) ``` hoelzl@50247 ` 392` huffman@36654 ` 393` ```lemma eventually_nhds: ``` huffman@36654 ` 394` ``` "eventually P (nhds a) \ (\S. open S \ a \ S \ (\x\S. P x))" ``` huffman@36654 ` 395` ```unfolding nhds_def ``` huffman@44081 ` 396` ```proof (rule eventually_Abs_filter, rule is_filter.intro) ``` huffman@36654 ` 397` ``` have "open UNIV \ a \ UNIV \ (\x\UNIV. True)" by simp ``` huffman@36654 ` 398` ``` thus "\S. open S \ a \ S \ (\x\S. True)" by - rule ``` huffman@36358 ` 399` ```next ``` huffman@36358 ` 400` ``` fix P Q ``` huffman@36654 ` 401` ``` assume "\S. open S \ a \ S \ (\x\S. P x)" ``` huffman@36654 ` 402` ``` and "\T. open T \ a \ T \ (\x\T. Q x)" ``` huffman@36358 ` 403` ``` then obtain S T where ``` huffman@36654 ` 404` ``` "open S \ a \ S \ (\x\S. P x)" ``` huffman@36654 ` 405` ``` "open T \ a \ T \ (\x\T. Q x)" by auto ``` huffman@36654 ` 406` ``` hence "open (S \ T) \ a \ S \ T \ (\x\(S \ T). P x \ Q x)" ``` huffman@36358 ` 407` ``` by (simp add: open_Int) ``` huffman@36654 ` 408` ``` thus "\S. open S \ a \ S \ (\x\S. P x \ Q x)" by - rule ``` huffman@36358 ` 409` ```qed auto ``` huffman@31447 ` 410` huffman@36656 ` 411` ```lemma eventually_nhds_metric: ``` huffman@36656 ` 412` ``` "eventually P (nhds a) \ (\d>0. \x. dist x a < d \ P x)" ``` huffman@36656 ` 413` ```unfolding eventually_nhds open_dist ``` huffman@31447 ` 414` ```apply safe ``` huffman@31447 ` 415` ```apply fast ``` huffman@31492 ` 416` ```apply (rule_tac x="{x. dist x a < d}" in exI, simp) ``` huffman@31447 ` 417` ```apply clarsimp ``` huffman@31447 ` 418` ```apply (rule_tac x="d - dist x a" in exI, clarsimp) ``` huffman@31447 ` 419` ```apply (simp only: less_diff_eq) ``` huffman@31447 ` 420` ```apply (erule le_less_trans [OF dist_triangle]) ``` huffman@31447 ` 421` ```done ``` huffman@31447 ` 422` huffman@44571 ` 423` ```lemma nhds_neq_bot [simp]: "nhds a \ bot" ``` huffman@44571 ` 424` ``` unfolding trivial_limit_def eventually_nhds by simp ``` huffman@44571 ` 425` huffman@36656 ` 426` ```lemma eventually_at_topological: ``` huffman@36656 ` 427` ``` "eventually P (at a) \ (\S. open S \ a \ S \ (\x\S. x \ a \ P x))" ``` huffman@36656 ` 428` ```unfolding at_def eventually_within eventually_nhds by simp ``` huffman@36656 ` 429` huffman@36656 ` 430` ```lemma eventually_at: ``` huffman@36656 ` 431` ``` fixes a :: "'a::metric_space" ``` huffman@36656 ` 432` ``` shows "eventually P (at a) \ (\d>0. \x. x \ a \ dist x a < d \ P x)" ``` huffman@36656 ` 433` ```unfolding at_def eventually_within eventually_nhds_metric by auto ``` huffman@36656 ` 434` huffman@44571 ` 435` ```lemma at_eq_bot_iff: "at a = bot \ open {a}" ``` huffman@44571 ` 436` ``` unfolding trivial_limit_def eventually_at_topological ``` huffman@44571 ` 437` ``` by (safe, case_tac "S = {a}", simp, fast, fast) ``` huffman@44571 ` 438` huffman@44571 ` 439` ```lemma at_neq_bot [simp]: "at (a::'a::perfect_space) \ bot" ``` huffman@44571 ` 440` ``` by (simp add: at_eq_bot_iff not_open_singleton) ``` huffman@44571 ` 441` huffman@31392 ` 442` huffman@31355 ` 443` ```subsection {* Boundedness *} ``` huffman@31355 ` 444` huffman@44081 ` 445` ```definition Bfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44195 ` 446` ``` where "Bfun f F = (\K>0. eventually (\x. norm (f x) \ K) F)" ``` huffman@31355 ` 447` huffman@31487 ` 448` ```lemma BfunI: ``` huffman@44195 ` 449` ``` assumes K: "eventually (\x. norm (f x) \ K) F" shows "Bfun f F" ``` huffman@31355 ` 450` ```unfolding Bfun_def ``` huffman@31355 ` 451` ```proof (intro exI conjI allI) ``` huffman@31355 ` 452` ``` show "0 < max K 1" by simp ``` huffman@31355 ` 453` ```next ``` huffman@44195 ` 454` ``` show "eventually (\x. norm (f x) \ max K 1) F" ``` huffman@31355 ` 455` ``` using K by (rule eventually_elim1, simp) ``` huffman@31355 ` 456` ```qed ``` huffman@31355 ` 457` huffman@31355 ` 458` ```lemma BfunE: ``` huffman@44195 ` 459` ``` assumes "Bfun f F" ``` huffman@44195 ` 460` ``` obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F" ``` huffman@31355 ` 461` ```using assms unfolding Bfun_def by fast ``` huffman@31355 ` 462` huffman@31355 ` 463` huffman@31349 ` 464` ```subsection {* Convergence to Zero *} ``` huffman@31349 ` 465` huffman@44081 ` 466` ```definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44195 ` 467` ``` where "Zfun f F = (\r>0. eventually (\x. norm (f x) < r) F)" ``` huffman@31349 ` 468` huffman@31349 ` 469` ```lemma ZfunI: ``` huffman@44195 ` 470` ``` "(\r. 0 < r \ eventually (\x. norm (f x) < r) F) \ Zfun f F" ``` huffman@44081 ` 471` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 472` huffman@31349 ` 473` ```lemma ZfunD: ``` huffman@44195 ` 474` ``` "\Zfun f F; 0 < r\ \ eventually (\x. norm (f x) < r) F" ``` huffman@44081 ` 475` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 476` huffman@31355 ` 477` ```lemma Zfun_ssubst: ``` huffman@44195 ` 478` ``` "eventually (\x. f x = g x) F \ Zfun g F \ Zfun f F" ``` huffman@44081 ` 479` ``` unfolding Zfun_def by (auto elim!: eventually_rev_mp) ``` huffman@31355 ` 480` huffman@44195 ` 481` ```lemma Zfun_zero: "Zfun (\x. 0) F" ``` huffman@44081 ` 482` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 483` huffman@44195 ` 484` ```lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) F = Zfun (\x. f x) F" ``` huffman@44081 ` 485` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 486` huffman@31349 ` 487` ```lemma Zfun_imp_Zfun: ``` huffman@44195 ` 488` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 489` ``` assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) F" ``` huffman@44195 ` 490` ``` shows "Zfun (\x. g x) F" ``` huffman@31349 ` 491` ```proof (cases) ``` huffman@31349 ` 492` ``` assume K: "0 < K" ``` huffman@31349 ` 493` ``` show ?thesis ``` huffman@31349 ` 494` ``` proof (rule ZfunI) ``` huffman@31349 ` 495` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 496` ``` hence "0 < r / K" ``` huffman@31349 ` 497` ``` using K by (rule divide_pos_pos) ``` huffman@44195 ` 498` ``` then have "eventually (\x. norm (f x) < r / K) F" ``` huffman@31487 ` 499` ``` using ZfunD [OF f] by fast ``` huffman@44195 ` 500` ``` with g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 501` ``` proof eventually_elim ``` noschinl@46887 ` 502` ``` case (elim x) ``` huffman@31487 ` 503` ``` hence "norm (f x) * K < r" ``` huffman@31349 ` 504` ``` by (simp add: pos_less_divide_eq K) ``` noschinl@46887 ` 505` ``` thus ?case ``` noschinl@46887 ` 506` ``` by (simp add: order_le_less_trans [OF elim(1)]) ``` huffman@31349 ` 507` ``` qed ``` huffman@31349 ` 508` ``` qed ``` huffman@31349 ` 509` ```next ``` huffman@31349 ` 510` ``` assume "\ 0 < K" ``` huffman@31349 ` 511` ``` hence K: "K \ 0" by (simp only: not_less) ``` huffman@31355 ` 512` ``` show ?thesis ``` huffman@31355 ` 513` ``` proof (rule ZfunI) ``` huffman@31355 ` 514` ``` fix r :: real ``` huffman@31355 ` 515` ``` assume "0 < r" ``` huffman@44195 ` 516` ``` from g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 517` ``` proof eventually_elim ``` noschinl@46887 ` 518` ``` case (elim x) ``` noschinl@46887 ` 519` ``` also have "norm (f x) * K \ norm (f x) * 0" ``` huffman@31355 ` 520` ``` using K norm_ge_zero by (rule mult_left_mono) ``` noschinl@46887 ` 521` ``` finally show ?case ``` huffman@31355 ` 522` ``` using `0 < r` by simp ``` huffman@31355 ` 523` ``` qed ``` huffman@31355 ` 524` ``` qed ``` huffman@31349 ` 525` ```qed ``` huffman@31349 ` 526` huffman@44195 ` 527` ```lemma Zfun_le: "\Zfun g F; \x. norm (f x) \ norm (g x)\ \ Zfun f F" ``` huffman@44081 ` 528` ``` by (erule_tac K="1" in Zfun_imp_Zfun, simp) ``` huffman@31349 ` 529` huffman@31349 ` 530` ```lemma Zfun_add: ``` huffman@44195 ` 531` ``` assumes f: "Zfun f F" and g: "Zfun g F" ``` huffman@44195 ` 532` ``` shows "Zfun (\x. f x + g x) F" ``` huffman@31349 ` 533` ```proof (rule ZfunI) ``` huffman@31349 ` 534` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 535` ``` hence r: "0 < r / 2" by simp ``` huffman@44195 ` 536` ``` have "eventually (\x. norm (f x) < r/2) F" ``` huffman@31487 ` 537` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 538` ``` moreover ``` huffman@44195 ` 539` ``` have "eventually (\x. norm (g x) < r/2) F" ``` huffman@31487 ` 540` ``` using g r by (rule ZfunD) ``` huffman@31349 ` 541` ``` ultimately ``` huffman@44195 ` 542` ``` show "eventually (\x. norm (f x + g x) < r) F" ``` noschinl@46887 ` 543` ``` proof eventually_elim ``` noschinl@46887 ` 544` ``` case (elim x) ``` huffman@31487 ` 545` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@31349 ` 546` ``` by (rule norm_triangle_ineq) ``` huffman@31349 ` 547` ``` also have "\ < r/2 + r/2" ``` noschinl@46887 ` 548` ``` using elim by (rule add_strict_mono) ``` noschinl@46887 ` 549` ``` finally show ?case ``` huffman@31349 ` 550` ``` by simp ``` huffman@31349 ` 551` ``` qed ``` huffman@31349 ` 552` ```qed ``` huffman@31349 ` 553` huffman@44195 ` 554` ```lemma Zfun_minus: "Zfun f F \ Zfun (\x. - f x) F" ``` huffman@44081 ` 555` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 556` huffman@44195 ` 557` ```lemma Zfun_diff: "\Zfun f F; Zfun g F\ \ Zfun (\x. f x - g x) F" ``` huffman@44081 ` 558` ``` by (simp only: diff_minus Zfun_add Zfun_minus) ``` huffman@31349 ` 559` huffman@31349 ` 560` ```lemma (in bounded_linear) Zfun: ``` huffman@44195 ` 561` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 562` ``` shows "Zfun (\x. f (g x)) F" ``` huffman@31349 ` 563` ```proof - ``` huffman@31349 ` 564` ``` obtain K where "\x. norm (f x) \ norm x * K" ``` huffman@31349 ` 565` ``` using bounded by fast ``` huffman@44195 ` 566` ``` then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F" ``` huffman@31355 ` 567` ``` by simp ``` huffman@31487 ` 568` ``` with g show ?thesis ``` huffman@31349 ` 569` ``` by (rule Zfun_imp_Zfun) ``` huffman@31349 ` 570` ```qed ``` huffman@31349 ` 571` huffman@31349 ` 572` ```lemma (in bounded_bilinear) Zfun: ``` huffman@44195 ` 573` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 574` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 575` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31349 ` 576` ```proof (rule ZfunI) ``` huffman@31349 ` 577` ``` fix r::real assume r: "0 < r" ``` huffman@31349 ` 578` ``` obtain K where K: "0 < K" ``` huffman@31349 ` 579` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31349 ` 580` ``` using pos_bounded by fast ``` huffman@31349 ` 581` ``` from K have K': "0 < inverse K" ``` huffman@31349 ` 582` ``` by (rule positive_imp_inverse_positive) ``` huffman@44195 ` 583` ``` have "eventually (\x. norm (f x) < r) F" ``` huffman@31487 ` 584` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 585` ``` moreover ``` huffman@44195 ` 586` ``` have "eventually (\x. norm (g x) < inverse K) F" ``` huffman@31487 ` 587` ``` using g K' by (rule ZfunD) ``` huffman@31349 ` 588` ``` ultimately ``` huffman@44195 ` 589` ``` show "eventually (\x. norm (f x ** g x) < r) F" ``` noschinl@46887 ` 590` ``` proof eventually_elim ``` noschinl@46887 ` 591` ``` case (elim x) ``` huffman@31487 ` 592` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31349 ` 593` ``` by (rule norm_le) ``` huffman@31487 ` 594` ``` also have "norm (f x) * norm (g x) * K < r * inverse K * K" ``` noschinl@46887 ` 595` ``` by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) ``` huffman@31349 ` 596` ``` also from K have "r * inverse K * K = r" ``` huffman@31349 ` 597` ``` by simp ``` noschinl@46887 ` 598` ``` finally show ?case . ``` huffman@31349 ` 599` ``` qed ``` huffman@31349 ` 600` ```qed ``` huffman@31349 ` 601` huffman@31349 ` 602` ```lemma (in bounded_bilinear) Zfun_left: ``` huffman@44195 ` 603` ``` "Zfun f F \ Zfun (\x. f x ** a) F" ``` huffman@44081 ` 604` ``` by (rule bounded_linear_left [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 605` huffman@31349 ` 606` ```lemma (in bounded_bilinear) Zfun_right: ``` huffman@44195 ` 607` ``` "Zfun f F \ Zfun (\x. a ** f x) F" ``` huffman@44081 ` 608` ``` by (rule bounded_linear_right [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 609` huffman@44282 ` 610` ```lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] ``` huffman@44282 ` 611` ```lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] ``` huffman@44282 ` 612` ```lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] ``` huffman@31349 ` 613` huffman@31349 ` 614` wenzelm@31902 ` 615` ```subsection {* Limits *} ``` huffman@31349 ` 616` hoelzl@50247 ` 617` ```definition filter_lim :: "('a \ 'b) \ 'b filter \ 'a filter \ bool" where ``` hoelzl@50247 ` 618` ``` "filter_lim f F2 F1 \ filtermap f F1 \ F2" ``` hoelzl@50247 ` 619` hoelzl@50247 ` 620` ```syntax ``` hoelzl@50247 ` 621` ``` "_LIM" :: "pttrns \ 'a \ 'b \ 'a \ bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10) ``` hoelzl@50247 ` 622` hoelzl@50247 ` 623` ```translations ``` hoelzl@50247 ` 624` ``` "LIM x F1. f :> F2" == "CONST filter_lim (%x. f) F2 F1" ``` hoelzl@50247 ` 625` hoelzl@50247 ` 626` ```lemma filter_limE: "(LIM x F1. f x :> F2) \ eventually P F2 \ eventually (\x. P (f x)) F1" ``` hoelzl@50247 ` 627` ``` by (auto simp: filter_lim_def eventually_filtermap le_filter_def) ``` hoelzl@50247 ` 628` hoelzl@50247 ` 629` ```lemma filter_limI: "(\P. eventually P F2 \ eventually (\x. P (f x)) F1) \ (LIM x F1. f x :> F2)" ``` hoelzl@50247 ` 630` ``` by (auto simp: filter_lim_def eventually_filtermap le_filter_def) ``` hoelzl@50247 ` 631` hoelzl@50247 ` 632` ```abbreviation (in topological_space) ``` huffman@44206 ` 633` ``` tendsto :: "('b \ 'a) \ 'a \ 'b filter \ bool" (infixr "--->" 55) where ``` hoelzl@50247 ` 634` ``` "(f ---> l) F \ filter_lim f (nhds l) F" ``` noschinl@45892 ` 635` wenzelm@31902 ` 636` ```ML {* ``` wenzelm@31902 ` 637` ```structure Tendsto_Intros = Named_Thms ``` wenzelm@31902 ` 638` ```( ``` wenzelm@45294 ` 639` ``` val name = @{binding tendsto_intros} ``` wenzelm@31902 ` 640` ``` val description = "introduction rules for tendsto" ``` wenzelm@31902 ` 641` ```) ``` huffman@31565 ` 642` ```*} ``` huffman@31565 ` 643` wenzelm@31902 ` 644` ```setup Tendsto_Intros.setup ``` huffman@31565 ` 645` hoelzl@50247 ` 646` ```lemma tendsto_def: "(f ---> l) F \ (\S. open S \ l \ S \ eventually (\x. f x \ S) F)" ``` hoelzl@50247 ` 647` ``` unfolding filter_lim_def ``` hoelzl@50247 ` 648` ```proof safe ``` hoelzl@50247 ` 649` ``` fix S assume "open S" "l \ S" "filtermap f F \ nhds l" ``` hoelzl@50247 ` 650` ``` then show "eventually (\x. f x \ S) F" ``` hoelzl@50247 ` 651` ``` unfolding eventually_nhds eventually_filtermap le_filter_def ``` hoelzl@50247 ` 652` ``` by (auto elim!: allE[of _ "\x. x \ S"] eventually_rev_mp) ``` hoelzl@50247 ` 653` ```qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def) ``` hoelzl@50247 ` 654` huffman@44195 ` 655` ```lemma tendsto_mono: "F \ F' \ (f ---> l) F' \ (f ---> l) F" ``` huffman@44081 ` 656` ``` unfolding tendsto_def le_filter_def by fast ``` huffman@36656 ` 657` huffman@31488 ` 658` ```lemma topological_tendstoI: ``` huffman@44195 ` 659` ``` "(\S. open S \ l \ S \ eventually (\x. f x \ S) F) ``` huffman@44195 ` 660` ``` \ (f ---> l) F" ``` huffman@31349 ` 661` ``` unfolding tendsto_def by auto ``` huffman@31349 ` 662` huffman@31488 ` 663` ```lemma topological_tendstoD: ``` huffman@44195 ` 664` ``` "(f ---> l) F \ open S \ l \ S \ eventually (\x. f x \ S) F" ``` huffman@31488 ` 665` ``` unfolding tendsto_def by auto ``` huffman@31488 ` 666` huffman@31488 ` 667` ```lemma tendstoI: ``` huffman@44195 ` 668` ``` assumes "\e. 0 < e \ eventually (\x. dist (f x) l < e) F" ``` huffman@44195 ` 669` ``` shows "(f ---> l) F" ``` huffman@44081 ` 670` ``` apply (rule topological_tendstoI) ``` huffman@44081 ` 671` ``` apply (simp add: open_dist) ``` huffman@44081 ` 672` ``` apply (drule (1) bspec, clarify) ``` huffman@44081 ` 673` ``` apply (drule assms) ``` huffman@44081 ` 674` ``` apply (erule eventually_elim1, simp) ``` huffman@44081 ` 675` ``` done ``` huffman@31488 ` 676` huffman@31349 ` 677` ```lemma tendstoD: ``` huffman@44195 ` 678` ``` "(f ---> l) F \ 0 < e \ eventually (\x. dist (f x) l < e) F" ``` huffman@44081 ` 679` ``` apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD) ``` huffman@44081 ` 680` ``` apply (clarsimp simp add: open_dist) ``` huffman@44081 ` 681` ``` apply (rule_tac x="e - dist x l" in exI, clarsimp) ``` huffman@44081 ` 682` ``` apply (simp only: less_diff_eq) ``` huffman@44081 ` 683` ``` apply (erule le_less_trans [OF dist_triangle]) ``` huffman@44081 ` 684` ``` apply simp ``` huffman@44081 ` 685` ``` apply simp ``` huffman@44081 ` 686` ``` done ``` huffman@31488 ` 687` huffman@31488 ` 688` ```lemma tendsto_iff: ``` huffman@44195 ` 689` ``` "(f ---> l) F \ (\e>0. eventually (\x. dist (f x) l < e) F)" ``` huffman@44081 ` 690` ``` using tendstoI tendstoD by fast ``` huffman@31349 ` 691` huffman@44195 ` 692` ```lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" ``` huffman@44081 ` 693` ``` by (simp only: tendsto_iff Zfun_def dist_norm) ``` huffman@31349 ` 694` huffman@45031 ` 695` ```lemma tendsto_bot [simp]: "(f ---> a) bot" ``` huffman@45031 ` 696` ``` unfolding tendsto_def by simp ``` huffman@45031 ` 697` huffman@31565 ` 698` ```lemma tendsto_ident_at [tendsto_intros]: "((\x. x) ---> a) (at a)" ``` huffman@44081 ` 699` ``` unfolding tendsto_def eventually_at_topological by auto ``` huffman@31565 ` 700` huffman@31565 ` 701` ```lemma tendsto_ident_at_within [tendsto_intros]: ``` huffman@36655 ` 702` ``` "((\x. x) ---> a) (at a within S)" ``` huffman@44081 ` 703` ``` unfolding tendsto_def eventually_within eventually_at_topological by auto ``` huffman@31565 ` 704` huffman@44195 ` 705` ```lemma tendsto_const [tendsto_intros]: "((\x. k) ---> k) F" ``` huffman@44081 ` 706` ``` by (simp add: tendsto_def) ``` huffman@31349 ` 707` huffman@44205 ` 708` ```lemma tendsto_unique: ``` huffman@44205 ` 709` ``` fixes f :: "'a \ 'b::t2_space" ``` huffman@44205 ` 710` ``` assumes "\ trivial_limit F" and "(f ---> a) F" and "(f ---> b) F" ``` huffman@44205 ` 711` ``` shows "a = b" ``` huffman@44205 ` 712` ```proof (rule ccontr) ``` huffman@44205 ` 713` ``` assume "a \ b" ``` huffman@44205 ` 714` ``` obtain U V where "open U" "open V" "a \ U" "b \ V" "U \ V = {}" ``` huffman@44205 ` 715` ``` using hausdorff [OF `a \ b`] by fast ``` huffman@44205 ` 716` ``` have "eventually (\x. f x \ U) F" ``` huffman@44205 ` 717` ``` using `(f ---> a) F` `open U` `a \ U` by (rule topological_tendstoD) ``` huffman@44205 ` 718` ``` moreover ``` huffman@44205 ` 719` ``` have "eventually (\x. f x \ V) F" ``` huffman@44205 ` 720` ``` using `(f ---> b) F` `open V` `b \ V` by (rule topological_tendstoD) ``` huffman@44205 ` 721` ``` ultimately ``` huffman@44205 ` 722` ``` have "eventually (\x. False) F" ``` noschinl@46887 ` 723` ``` proof eventually_elim ``` noschinl@46887 ` 724` ``` case (elim x) ``` huffman@44205 ` 725` ``` hence "f x \ U \ V" by simp ``` noschinl@46887 ` 726` ``` with `U \ V = {}` show ?case by simp ``` huffman@44205 ` 727` ``` qed ``` huffman@44205 ` 728` ``` with `\ trivial_limit F` show "False" ``` huffman@44205 ` 729` ``` by (simp add: trivial_limit_def) ``` huffman@44205 ` 730` ```qed ``` huffman@44205 ` 731` huffman@36662 ` 732` ```lemma tendsto_const_iff: ``` huffman@44205 ` 733` ``` fixes a b :: "'a::t2_space" ``` huffman@44205 ` 734` ``` assumes "\ trivial_limit F" shows "((\x. a) ---> b) F \ a = b" ``` huffman@44205 ` 735` ``` by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const]) ``` huffman@44205 ` 736` huffman@44218 ` 737` ```lemma tendsto_compose: ``` huffman@44218 ` 738` ``` assumes g: "(g ---> g l) (at l)" ``` huffman@44218 ` 739` ``` assumes f: "(f ---> l) F" ``` huffman@44218 ` 740` ``` shows "((\x. g (f x)) ---> g l) F" ``` huffman@44218 ` 741` ```proof (rule topological_tendstoI) ``` huffman@44218 ` 742` ``` fix B assume B: "open B" "g l \ B" ``` huffman@44218 ` 743` ``` obtain A where A: "open A" "l \ A" ``` huffman@44218 ` 744` ``` and gB: "\y. y \ A \ g y \ B" ``` huffman@44218 ` 745` ``` using topological_tendstoD [OF g B] B(2) ``` huffman@44218 ` 746` ``` unfolding eventually_at_topological by fast ``` huffman@44218 ` 747` ``` hence "\x. f x \ A \ g (f x) \ B" by simp ``` huffman@44218 ` 748` ``` from this topological_tendstoD [OF f A] ``` huffman@44218 ` 749` ``` show "eventually (\x. g (f x) \ B) F" ``` huffman@44218 ` 750` ``` by (rule eventually_mono) ``` huffman@44218 ` 751` ```qed ``` huffman@44218 ` 752` huffman@44253 ` 753` ```lemma tendsto_compose_eventually: ``` huffman@44253 ` 754` ``` assumes g: "(g ---> m) (at l)" ``` huffman@44253 ` 755` ``` assumes f: "(f ---> l) F" ``` huffman@44253 ` 756` ``` assumes inj: "eventually (\x. f x \ l) F" ``` huffman@44253 ` 757` ``` shows "((\x. g (f x)) ---> m) F" ``` huffman@44253 ` 758` ```proof (rule topological_tendstoI) ``` huffman@44253 ` 759` ``` fix B assume B: "open B" "m \ B" ``` huffman@44253 ` 760` ``` obtain A where A: "open A" "l \ A" ``` huffman@44253 ` 761` ``` and gB: "\y. y \ A \ y \ l \ g y \ B" ``` huffman@44253 ` 762` ``` using topological_tendstoD [OF g B] ``` huffman@44253 ` 763` ``` unfolding eventually_at_topological by fast ``` huffman@44253 ` 764` ``` show "eventually (\x. g (f x) \ B) F" ``` huffman@44253 ` 765` ``` using topological_tendstoD [OF f A] inj ``` huffman@44253 ` 766` ``` by (rule eventually_elim2) (simp add: gB) ``` huffman@44253 ` 767` ```qed ``` huffman@44253 ` 768` huffman@44251 ` 769` ```lemma metric_tendsto_imp_tendsto: ``` huffman@44251 ` 770` ``` assumes f: "(f ---> a) F" ``` huffman@44251 ` 771` ``` assumes le: "eventually (\x. dist (g x) b \ dist (f x) a) F" ``` huffman@44251 ` 772` ``` shows "(g ---> b) F" ``` huffman@44251 ` 773` ```proof (rule tendstoI) ``` huffman@44251 ` 774` ``` fix e :: real assume "0 < e" ``` huffman@44251 ` 775` ``` with f have "eventually (\x. dist (f x) a < e) F" by (rule tendstoD) ``` huffman@44251 ` 776` ``` with le show "eventually (\x. dist (g x) b < e) F" ``` huffman@44251 ` 777` ``` using le_less_trans by (rule eventually_elim2) ``` huffman@44251 ` 778` ```qed ``` huffman@44251 ` 779` huffman@44205 ` 780` ```subsubsection {* Distance and norms *} ``` huffman@36662 ` 781` huffman@31565 ` 782` ```lemma tendsto_dist [tendsto_intros]: ``` huffman@44195 ` 783` ``` assumes f: "(f ---> l) F" and g: "(g ---> m) F" ``` huffman@44195 ` 784` ``` shows "((\x. dist (f x) (g x)) ---> dist l m) F" ``` huffman@31565 ` 785` ```proof (rule tendstoI) ``` huffman@31565 ` 786` ``` fix e :: real assume "0 < e" ``` huffman@31565 ` 787` ``` hence e2: "0 < e/2" by simp ``` huffman@31565 ` 788` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` huffman@44195 ` 789` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F" ``` noschinl@46887 ` 790` ``` proof (eventually_elim) ``` noschinl@46887 ` 791` ``` case (elim x) ``` huffman@31565 ` 792` ``` then show "dist (dist (f x) (g x)) (dist l m) < e" ``` huffman@31565 ` 793` ``` unfolding dist_real_def ``` huffman@31565 ` 794` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` huffman@31565 ` 795` ``` using dist_triangle2 [of "g x" "l" "m"] ``` huffman@31565 ` 796` ``` using dist_triangle3 [of "l" "m" "f x"] ``` huffman@31565 ` 797` ``` using dist_triangle [of "f x" "m" "g x"] ``` huffman@31565 ` 798` ``` by arith ``` huffman@31565 ` 799` ``` qed ``` huffman@31565 ` 800` ```qed ``` huffman@31565 ` 801` huffman@36662 ` 802` ```lemma norm_conv_dist: "norm x = dist x 0" ``` huffman@44081 ` 803` ``` unfolding dist_norm by simp ``` huffman@36662 ` 804` huffman@31565 ` 805` ```lemma tendsto_norm [tendsto_intros]: ``` huffman@44195 ` 806` ``` "(f ---> a) F \ ((\x. norm (f x)) ---> norm a) F" ``` huffman@44081 ` 807` ``` unfolding norm_conv_dist by (intro tendsto_intros) ``` huffman@36662 ` 808` huffman@36662 ` 809` ```lemma tendsto_norm_zero: ``` huffman@44195 ` 810` ``` "(f ---> 0) F \ ((\x. norm (f x)) ---> 0) F" ``` huffman@44081 ` 811` ``` by (drule tendsto_norm, simp) ``` huffman@36662 ` 812` huffman@36662 ` 813` ```lemma tendsto_norm_zero_cancel: ``` huffman@44195 ` 814` ``` "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" ``` huffman@44081 ` 815` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@36662 ` 816` huffman@36662 ` 817` ```lemma tendsto_norm_zero_iff: ``` huffman@44195 ` 818` ``` "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" ``` huffman@44081 ` 819` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@31349 ` 820` huffman@44194 ` 821` ```lemma tendsto_rabs [tendsto_intros]: ``` huffman@44195 ` 822` ``` "(f ---> (l::real)) F \ ((\x. \f x\) ---> \l\) F" ``` huffman@44194 ` 823` ``` by (fold real_norm_def, rule tendsto_norm) ``` huffman@44194 ` 824` huffman@44194 ` 825` ```lemma tendsto_rabs_zero: ``` huffman@44195 ` 826` ``` "(f ---> (0::real)) F \ ((\x. \f x\) ---> 0) F" ``` huffman@44194 ` 827` ``` by (fold real_norm_def, rule tendsto_norm_zero) ``` huffman@44194 ` 828` huffman@44194 ` 829` ```lemma tendsto_rabs_zero_cancel: ``` huffman@44195 ` 830` ``` "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" ``` huffman@44194 ` 831` ``` by (fold real_norm_def, rule tendsto_norm_zero_cancel) ``` huffman@44194 ` 832` huffman@44194 ` 833` ```lemma tendsto_rabs_zero_iff: ``` huffman@44195 ` 834` ``` "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" ``` huffman@44194 ` 835` ``` by (fold real_norm_def, rule tendsto_norm_zero_iff) ``` huffman@44194 ` 836` huffman@44194 ` 837` ```subsubsection {* Addition and subtraction *} ``` huffman@44194 ` 838` huffman@31565 ` 839` ```lemma tendsto_add [tendsto_intros]: ``` huffman@31349 ` 840` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44195 ` 841` ``` shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x + g x) ---> a + b) F" ``` huffman@44081 ` 842` ``` by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) ``` huffman@31349 ` 843` huffman@44194 ` 844` ```lemma tendsto_add_zero: ``` huffman@44194 ` 845` ``` fixes f g :: "'a::type \ 'b::real_normed_vector" ``` huffman@44195 ` 846` ``` shows "\(f ---> 0) F; (g ---> 0) F\ \ ((\x. f x + g x) ---> 0) F" ``` huffman@44194 ` 847` ``` by (drule (1) tendsto_add, simp) ``` huffman@44194 ` 848` huffman@31565 ` 849` ```lemma tendsto_minus [tendsto_intros]: ``` huffman@31349 ` 850` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44195 ` 851` ``` shows "(f ---> a) F \ ((\x. - f x) ---> - a) F" ``` huffman@44081 ` 852` ``` by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) ``` huffman@31349 ` 853` huffman@31349 ` 854` ```lemma tendsto_minus_cancel: ``` huffman@31349 ` 855` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44195 ` 856` ``` shows "((\x. - f x) ---> - a) F \ (f ---> a) F" ``` huffman@44081 ` 857` ``` by (drule tendsto_minus, simp) ``` huffman@31349 ` 858` huffman@31565 ` 859` ```lemma tendsto_diff [tendsto_intros]: ``` huffman@31349 ` 860` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44195 ` 861` ``` shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x - g x) ---> a - b) F" ``` huffman@44081 ` 862` ``` by (simp add: diff_minus tendsto_add tendsto_minus) ``` huffman@31349 ` 863` huffman@31588 ` 864` ```lemma tendsto_setsum [tendsto_intros]: ``` huffman@31588 ` 865` ``` fixes f :: "'a \ 'b \ 'c::real_normed_vector" ``` huffman@44195 ` 866` ``` assumes "\i. i \ S \ (f i ---> a i) F" ``` huffman@44195 ` 867` ``` shows "((\x. \i\S. f i x) ---> (\i\S. a i)) F" ``` huffman@31588 ` 868` ```proof (cases "finite S") ``` huffman@31588 ` 869` ``` assume "finite S" thus ?thesis using assms ``` huffman@44194 ` 870` ``` by (induct, simp add: tendsto_const, simp add: tendsto_add) ``` huffman@31588 ` 871` ```next ``` huffman@31588 ` 872` ``` assume "\ finite S" thus ?thesis ``` huffman@31588 ` 873` ``` by (simp add: tendsto_const) ``` huffman@31588 ` 874` ```qed ``` huffman@31588 ` 875` noschinl@45892 ` 876` ```lemma real_tendsto_sandwich: ``` noschinl@45892 ` 877` ``` fixes f g h :: "'a \ real" ``` noschinl@45892 ` 878` ``` assumes ev: "eventually (\n. f n \ g n) net" "eventually (\n. g n \ h n) net" ``` noschinl@45892 ` 879` ``` assumes lim: "(f ---> c) net" "(h ---> c) net" ``` noschinl@45892 ` 880` ``` shows "(g ---> c) net" ``` noschinl@45892 ` 881` ```proof - ``` noschinl@45892 ` 882` ``` have "((\n. g n - f n) ---> 0) net" ``` noschinl@45892 ` 883` ``` proof (rule metric_tendsto_imp_tendsto) ``` noschinl@45892 ` 884` ``` show "eventually (\n. dist (g n - f n) 0 \ dist (h n - f n) 0) net" ``` noschinl@45892 ` 885` ``` using ev by (rule eventually_elim2) (simp add: dist_real_def) ``` noschinl@45892 ` 886` ``` show "((\n. h n - f n) ---> 0) net" ``` noschinl@45892 ` 887` ``` using tendsto_diff[OF lim(2,1)] by simp ``` noschinl@45892 ` 888` ``` qed ``` noschinl@45892 ` 889` ``` from tendsto_add[OF this lim(1)] show ?thesis by simp ``` noschinl@45892 ` 890` ```qed ``` noschinl@45892 ` 891` huffman@44194 ` 892` ```subsubsection {* Linear operators and multiplication *} ``` huffman@44194 ` 893` huffman@44282 ` 894` ```lemma (in bounded_linear) tendsto: ``` huffman@44195 ` 895` ``` "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" ``` huffman@44081 ` 896` ``` by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) ``` huffman@31349 ` 897` huffman@44194 ` 898` ```lemma (in bounded_linear) tendsto_zero: ``` huffman@44195 ` 899` ``` "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" ``` huffman@44194 ` 900` ``` by (drule tendsto, simp only: zero) ``` huffman@44194 ` 901` huffman@44282 ` 902` ```lemma (in bounded_bilinear) tendsto: ``` huffman@44195 ` 903` ``` "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x ** g x) ---> a ** b) F" ``` huffman@44081 ` 904` ``` by (simp only: tendsto_Zfun_iff prod_diff_prod ``` huffman@44081 ` 905` ``` Zfun_add Zfun Zfun_left Zfun_right) ``` huffman@31349 ` 906` huffman@44194 ` 907` ```lemma (in bounded_bilinear) tendsto_zero: ``` huffman@44195 ` 908` ``` assumes f: "(f ---> 0) F" ``` huffman@44195 ` 909` ``` assumes g: "(g ---> 0) F" ``` huffman@44195 ` 910` ``` shows "((\x. f x ** g x) ---> 0) F" ``` huffman@44194 ` 911` ``` using tendsto [OF f g] by (simp add: zero_left) ``` huffman@31355 ` 912` huffman@44194 ` 913` ```lemma (in bounded_bilinear) tendsto_left_zero: ``` huffman@44195 ` 914` ``` "(f ---> 0) F \ ((\x. f x ** c) ---> 0) F" ``` huffman@44194 ` 915` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) ``` huffman@44194 ` 916` huffman@44194 ` 917` ```lemma (in bounded_bilinear) tendsto_right_zero: ``` huffman@44195 ` 918` ``` "(f ---> 0) F \ ((\x. c ** f x) ---> 0) F" ``` huffman@44194 ` 919` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) ``` huffman@44194 ` 920` huffman@44282 ` 921` ```lemmas tendsto_of_real [tendsto_intros] = ``` huffman@44282 ` 922` ``` bounded_linear.tendsto [OF bounded_linear_of_real] ``` huffman@44282 ` 923` huffman@44282 ` 924` ```lemmas tendsto_scaleR [tendsto_intros] = ``` huffman@44282 ` 925` ``` bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] ``` huffman@44282 ` 926` huffman@44282 ` 927` ```lemmas tendsto_mult [tendsto_intros] = ``` huffman@44282 ` 928` ``` bounded_bilinear.tendsto [OF bounded_bilinear_mult] ``` huffman@44194 ` 929` huffman@44568 ` 930` ```lemmas tendsto_mult_zero = ``` huffman@44568 ` 931` ``` bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 932` huffman@44568 ` 933` ```lemmas tendsto_mult_left_zero = ``` huffman@44568 ` 934` ``` bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 935` huffman@44568 ` 936` ```lemmas tendsto_mult_right_zero = ``` huffman@44568 ` 937` ``` bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 938` huffman@44194 ` 939` ```lemma tendsto_power [tendsto_intros]: ``` huffman@44194 ` 940` ``` fixes f :: "'a \ 'b::{power,real_normed_algebra}" ``` huffman@44195 ` 941` ``` shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" ``` huffman@44194 ` 942` ``` by (induct n) (simp_all add: tendsto_const tendsto_mult) ``` huffman@44194 ` 943` huffman@44194 ` 944` ```lemma tendsto_setprod [tendsto_intros]: ``` huffman@44194 ` 945` ``` fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" ``` huffman@44195 ` 946` ``` assumes "\i. i \ S \ (f i ---> L i) F" ``` huffman@44195 ` 947` ``` shows "((\x. \i\S. f i x) ---> (\i\S. L i)) F" ``` huffman@44194 ` 948` ```proof (cases "finite S") ``` huffman@44194 ` 949` ``` assume "finite S" thus ?thesis using assms ``` huffman@44194 ` 950` ``` by (induct, simp add: tendsto_const, simp add: tendsto_mult) ``` huffman@44194 ` 951` ```next ``` huffman@44194 ` 952` ``` assume "\ finite S" thus ?thesis ``` huffman@44194 ` 953` ``` by (simp add: tendsto_const) ``` huffman@44194 ` 954` ```qed ``` huffman@44194 ` 955` huffman@44194 ` 956` ```subsubsection {* Inverse and division *} ``` huffman@31355 ` 957` huffman@31355 ` 958` ```lemma (in bounded_bilinear) Zfun_prod_Bfun: ``` huffman@44195 ` 959` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 960` ``` assumes g: "Bfun g F" ``` huffman@44195 ` 961` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31355 ` 962` ```proof - ``` huffman@31355 ` 963` ``` obtain K where K: "0 \ K" ``` huffman@31355 ` 964` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31355 ` 965` ``` using nonneg_bounded by fast ``` huffman@31355 ` 966` ``` obtain B where B: "0 < B" ``` huffman@44195 ` 967` ``` and norm_g: "eventually (\x. norm (g x) \ B) F" ``` huffman@31487 ` 968` ``` using g by (rule BfunE) ``` huffman@44195 ` 969` ``` have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) F" ``` noschinl@46887 ` 970` ``` using norm_g proof eventually_elim ``` noschinl@46887 ` 971` ``` case (elim x) ``` huffman@31487 ` 972` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31355 ` 973` ``` by (rule norm_le) ``` huffman@31487 ` 974` ``` also have "\ \ norm (f x) * B * K" ``` huffman@31487 ` 975` ``` by (intro mult_mono' order_refl norm_g norm_ge_zero ``` noschinl@46887 ` 976` ``` mult_nonneg_nonneg K elim) ``` huffman@31487 ` 977` ``` also have "\ = norm (f x) * (B * K)" ``` huffman@31355 ` 978` ``` by (rule mult_assoc) ``` huffman@31487 ` 979` ``` finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . ``` huffman@31355 ` 980` ``` qed ``` huffman@31487 ` 981` ``` with f show ?thesis ``` huffman@31487 ` 982` ``` by (rule Zfun_imp_Zfun) ``` huffman@31355 ` 983` ```qed ``` huffman@31355 ` 984` huffman@31355 ` 985` ```lemma (in bounded_bilinear) flip: ``` huffman@31355 ` 986` ``` "bounded_bilinear (\x y. y ** x)" ``` huffman@44081 ` 987` ``` apply default ``` huffman@44081 ` 988` ``` apply (rule add_right) ``` huffman@44081 ` 989` ``` apply (rule add_left) ``` huffman@44081 ` 990` ``` apply (rule scaleR_right) ``` huffman@44081 ` 991` ``` apply (rule scaleR_left) ``` huffman@44081 ` 992` ``` apply (subst mult_commute) ``` huffman@44081 ` 993` ``` using bounded by fast ``` huffman@31355 ` 994` huffman@31355 ` 995` ```lemma (in bounded_bilinear) Bfun_prod_Zfun: ``` huffman@44195 ` 996` ``` assumes f: "Bfun f F" ``` huffman@44195 ` 997` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 998` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@44081 ` 999` ``` using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) ``` huffman@31355 ` 1000` huffman@31355 ` 1001` ```lemma Bfun_inverse_lemma: ``` huffman@31355 ` 1002` ``` fixes x :: "'a::real_normed_div_algebra" ``` huffman@31355 ` 1003` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` huffman@44081 ` 1004` ``` apply (subst nonzero_norm_inverse, clarsimp) ``` huffman@44081 ` 1005` ``` apply (erule (1) le_imp_inverse_le) ``` huffman@44081 ` 1006` ``` done ``` huffman@31355 ` 1007` huffman@31355 ` 1008` ```lemma Bfun_inverse: ``` huffman@31355 ` 1009` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44195 ` 1010` ``` assumes f: "(f ---> a) F" ``` huffman@31355 ` 1011` ``` assumes a: "a \ 0" ``` huffman@44195 ` 1012` ``` shows "Bfun (\x. inverse (f x)) F" ``` huffman@31355 ` 1013` ```proof - ``` huffman@31355 ` 1014` ``` from a have "0 < norm a" by simp ``` huffman@31355 ` 1015` ``` hence "\r>0. r < norm a" by (rule dense) ``` huffman@31355 ` 1016` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" by fast ``` huffman@44195 ` 1017` ``` have "eventually (\x. dist (f x) a < r) F" ``` huffman@31487 ` 1018` ``` using tendstoD [OF f r1] by fast ``` huffman@44195 ` 1019` ``` hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F" ``` noschinl@46887 ` 1020` ``` proof eventually_elim ``` noschinl@46887 ` 1021` ``` case (elim x) ``` huffman@31487 ` 1022` ``` hence 1: "norm (f x - a) < r" ``` huffman@31355 ` 1023` ``` by (simp add: dist_norm) ``` huffman@31487 ` 1024` ``` hence 2: "f x \ 0" using r2 by auto ``` huffman@31487 ` 1025` ``` hence "norm (inverse (f x)) = inverse (norm (f x))" ``` huffman@31355 ` 1026` ``` by (rule nonzero_norm_inverse) ``` huffman@31355 ` 1027` ``` also have "\ \ inverse (norm a - r)" ``` huffman@31355 ` 1028` ``` proof (rule le_imp_inverse_le) ``` huffman@31355 ` 1029` ``` show "0 < norm a - r" using r2 by simp ``` huffman@31355 ` 1030` ``` next ``` huffman@31487 ` 1031` ``` have "norm a - norm (f x) \ norm (a - f x)" ``` huffman@31355 ` 1032` ``` by (rule norm_triangle_ineq2) ``` huffman@31487 ` 1033` ``` also have "\ = norm (f x - a)" ``` huffman@31355 ` 1034` ``` by (rule norm_minus_commute) ``` huffman@31355 ` 1035` ``` also have "\ < r" using 1 . ``` huffman@31487 ` 1036` ``` finally show "norm a - r \ norm (f x)" by simp ``` huffman@31355 ` 1037` ``` qed ``` huffman@31487 ` 1038` ``` finally show "norm (inverse (f x)) \ inverse (norm a - r)" . ``` huffman@31355 ` 1039` ``` qed ``` huffman@31355 ` 1040` ``` thus ?thesis by (rule BfunI) ``` huffman@31355 ` 1041` ```qed ``` huffman@31355 ` 1042` huffman@31565 ` 1043` ```lemma tendsto_inverse [tendsto_intros]: ``` huffman@31355 ` 1044` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44195 ` 1045` ``` assumes f: "(f ---> a) F" ``` huffman@31355 ` 1046` ``` assumes a: "a \ 0" ``` huffman@44195 ` 1047` ``` shows "((\x. inverse (f x)) ---> inverse a) F" ``` huffman@31355 ` 1048` ```proof - ``` huffman@31355 ` 1049` ``` from a have "0 < norm a" by simp ``` huffman@44195 ` 1050` ``` with f have "eventually (\x. dist (f x) a < norm a) F" ``` huffman@31355 ` 1051` ``` by (rule tendstoD) ``` huffman@44195 ` 1052` ``` then have "eventually (\x. f x \ 0) F" ``` huffman@31355 ` 1053` ``` unfolding dist_norm by (auto elim!: eventually_elim1) ``` huffman@44627 ` 1054` ``` with a have "eventually (\x. inverse (f x) - inverse a = ``` huffman@44627 ` 1055` ``` - (inverse (f x) * (f x - a) * inverse a)) F" ``` huffman@44627 ` 1056` ``` by (auto elim!: eventually_elim1 simp: inverse_diff_inverse) ``` huffman@44627 ` 1057` ``` moreover have "Zfun (\x. - (inverse (f x) * (f x - a) * inverse a)) F" ``` huffman@44627 ` 1058` ``` by (intro Zfun_minus Zfun_mult_left ``` huffman@44627 ` 1059` ``` bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] ``` huffman@44627 ` 1060` ``` Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) ``` huffman@44627 ` 1061` ``` ultimately show ?thesis ``` huffman@44627 ` 1062` ``` unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) ``` huffman@31355 ` 1063` ```qed ``` huffman@31355 ` 1064` huffman@31565 ` 1065` ```lemma tendsto_divide [tendsto_intros]: ``` huffman@31355 ` 1066` ``` fixes a b :: "'a::real_normed_field" ``` huffman@44195 ` 1067` ``` shows "\(f ---> a) F; (g ---> b) F; b \ 0\ ``` huffman@44195 ` 1068` ``` \ ((\x. f x / g x) ---> a / b) F" ``` huffman@44282 ` 1069` ``` by (simp add: tendsto_mult tendsto_inverse divide_inverse) ``` huffman@31355 ` 1070` huffman@44194 ` 1071` ```lemma tendsto_sgn [tendsto_intros]: ``` huffman@44194 ` 1072` ``` fixes l :: "'a::real_normed_vector" ``` huffman@44195 ` 1073` ``` shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" ``` huffman@44194 ` 1074` ``` unfolding sgn_div_norm by (simp add: tendsto_intros) ``` huffman@44194 ` 1075` hoelzl@50247 ` 1076` ```subsection {* Limits to @{const at_top} and @{const at_bot} *} ``` hoelzl@50247 ` 1077` hoelzl@50247 ` 1078` ```lemma filter_lim_at_top: ``` hoelzl@50247 ` 1079` ``` fixes f :: "'a \ ('b::dense_linorder)" ``` hoelzl@50247 ` 1080` ``` shows "(LIM x F. f x :> at_top) \ (\Z. eventually (\x. Z < f x) F)" ``` hoelzl@50247 ` 1081` ``` by (safe elim!: filter_limE intro!: filter_limI) ``` hoelzl@50247 ` 1082` ``` (auto simp: eventually_at_top_dense elim!: eventually_elim1) ``` hoelzl@50247 ` 1083` hoelzl@50247 ` 1084` ```lemma filter_lim_at_bot: ``` hoelzl@50247 ` 1085` ``` fixes f :: "'a \ ('b::dense_linorder)" ``` hoelzl@50247 ` 1086` ``` shows "(LIM x F. f x :> at_bot) \ (\Z. eventually (\x. f x < Z) F)" ``` hoelzl@50247 ` 1087` ``` by (safe elim!: filter_limE intro!: filter_limI) ``` hoelzl@50247 ` 1088` ``` (auto simp: eventually_at_bot_dense elim!: eventually_elim1) ``` hoelzl@50247 ` 1089` hoelzl@50247 ` 1090` ```lemma filter_lim_real_sequentially: "LIM x sequentially. real x :> at_top" ``` hoelzl@50247 ` 1091` ``` unfolding filter_lim_at_top ``` hoelzl@50247 ` 1092` ``` apply (intro allI) ``` hoelzl@50247 ` 1093` ``` apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI) ``` hoelzl@50247 ` 1094` ``` apply (auto simp: natceiling_le_eq) ``` hoelzl@50247 ` 1095` ``` done ``` hoelzl@50247 ` 1096` huffman@31349 ` 1097` ```end ```