src/HOL/Limits.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 65204 d23eded35a33 child 65680 378a2f11bec9 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
 wenzelm@52265 ` 1` ```(* Title: HOL/Limits.thy ``` hoelzl@51526 ` 2` ``` Author: Brian Huffman ``` hoelzl@51526 ` 3` ``` Author: Jacques D. Fleuriot, University of Cambridge ``` hoelzl@51526 ` 4` ``` Author: Lawrence C Paulson ``` hoelzl@51526 ` 5` ``` Author: Jeremy Avigad ``` huffman@31349 ` 6` ```*) ``` huffman@31349 ` 7` wenzelm@60758 ` 8` ```section \Limits on Real Vector Spaces\ ``` huffman@31349 ` 9` huffman@31349 ` 10` ```theory Limits ``` wenzelm@63546 ` 11` ``` imports Real_Vector_Spaces ``` huffman@31349 ` 12` ```begin ``` huffman@31349 ` 13` wenzelm@60758 ` 14` ```subsection \Filter going to infinity norm\ ``` hoelzl@51526 ` 15` wenzelm@63546 ` 16` ```definition at_infinity :: "'a::real_normed_vector filter" ``` wenzelm@63546 ` 17` ``` where "at_infinity = (INF r. principal {x. r \ norm x})" ``` hoelzl@50324 ` 18` hoelzl@57276 ` 19` ```lemma eventually_at_infinity: "eventually P at_infinity \ (\b. \x. b \ norm x \ P x)" ``` hoelzl@57276 ` 20` ``` unfolding at_infinity_def ``` hoelzl@57276 ` 21` ``` by (subst eventually_INF_base) ``` hoelzl@57276 ` 22` ``` (auto simp: subset_eq eventually_principal intro!: exI[of _ "max a b" for a b]) ``` huffman@31392 ` 23` lp15@62379 ` 24` ```corollary eventually_at_infinity_pos: ``` wenzelm@63546 ` 25` ``` "eventually p at_infinity \ (\b. 0 < b \ (\x. norm x \ b \ p x))" ``` wenzelm@63546 ` 26` ``` apply (simp add: eventually_at_infinity) ``` wenzelm@63546 ` 27` ``` apply auto ``` wenzelm@63546 ` 28` ``` apply (case_tac "b \ 0") ``` wenzelm@63546 ` 29` ``` using norm_ge_zero order_trans zero_less_one apply blast ``` wenzelm@63546 ` 30` ``` apply force ``` wenzelm@63546 ` 31` ``` done ``` wenzelm@63546 ` 32` wenzelm@63546 ` 33` ```lemma at_infinity_eq_at_top_bot: "(at_infinity :: real filter) = sup at_top at_bot" ``` hoelzl@57276 ` 34` ``` apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity ``` wenzelm@63546 ` 35` ``` eventually_at_top_linorder eventually_at_bot_linorder) ``` hoelzl@57276 ` 36` ``` apply safe ``` wenzelm@63546 ` 37` ``` apply (rule_tac x="b" in exI) ``` wenzelm@63546 ` 38` ``` apply simp ``` wenzelm@63546 ` 39` ``` apply (rule_tac x="- b" in exI) ``` wenzelm@63546 ` 40` ``` apply simp ``` wenzelm@63546 ` 41` ``` apply (rule_tac x="max (- Na) N" in exI) ``` wenzelm@63546 ` 42` ``` apply (auto simp: abs_real_def) ``` hoelzl@57276 ` 43` ``` done ``` hoelzl@50325 ` 44` hoelzl@57276 ` 45` ```lemma at_top_le_at_infinity: "at_top \ (at_infinity :: real filter)" ``` hoelzl@50325 ` 46` ``` unfolding at_infinity_eq_at_top_bot by simp ``` hoelzl@50325 ` 47` hoelzl@57276 ` 48` ```lemma at_bot_le_at_infinity: "at_bot \ (at_infinity :: real filter)" ``` hoelzl@50325 ` 49` ``` unfolding at_infinity_eq_at_top_bot by simp ``` hoelzl@50325 ` 50` wenzelm@63546 ` 51` ```lemma filterlim_at_top_imp_at_infinity: "filterlim f at_top F \ filterlim f at_infinity F" ``` wenzelm@63546 ` 52` ``` for f :: "_ \ real" ``` hoelzl@57275 ` 53` ``` by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) ``` hoelzl@57275 ` 54` wenzelm@63546 ` 55` ```lemma lim_infinity_imp_sequentially: "(f \ l) at_infinity \ ((\n. f(n)) \ l) sequentially" ``` wenzelm@63546 ` 56` ``` by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) ``` lp15@59613 ` 57` lp15@59613 ` 58` wenzelm@60758 ` 59` ```subsubsection \Boundedness\ ``` hoelzl@51531 ` 60` wenzelm@63546 ` 61` ```definition Bfun :: "('a \ 'b::metric_space) \ 'a filter \ bool" ``` wenzelm@63546 ` 62` ``` where Bfun_metric_def: "Bfun f F = (\y. \K>0. eventually (\x. dist (f x) y \ K) F)" ``` wenzelm@63546 ` 63` wenzelm@63546 ` 64` ```abbreviation Bseq :: "(nat \ 'a::metric_space) \ bool" ``` wenzelm@63546 ` 65` ``` where "Bseq X \ Bfun X sequentially" ``` hoelzl@51531 ` 66` hoelzl@51531 ` 67` ```lemma Bseq_conv_Bfun: "Bseq X \ Bfun X sequentially" .. ``` hoelzl@51531 ` 68` hoelzl@51531 ` 69` ```lemma Bseq_ignore_initial_segment: "Bseq X \ Bseq (\n. X (n + k))" ``` hoelzl@51531 ` 70` ``` unfolding Bfun_metric_def by (subst eventually_sequentially_seg) ``` hoelzl@51531 ` 71` hoelzl@51531 ` 72` ```lemma Bseq_offset: "Bseq (\n. X (n + k)) \ Bseq X" ``` hoelzl@51531 ` 73` ``` unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) ``` huffman@31355 ` 74` wenzelm@63546 ` 75` ```lemma Bfun_def: "Bfun f F \ (\K>0. eventually (\x. norm (f x) \ K) F)" ``` hoelzl@51474 ` 76` ``` unfolding Bfun_metric_def norm_conv_dist ``` hoelzl@51474 ` 77` ```proof safe ``` wenzelm@63546 ` 78` ``` fix y K ``` wenzelm@63546 ` 79` ``` assume K: "0 < K" and *: "eventually (\x. dist (f x) y \ K) F" ``` hoelzl@51474 ` 80` ``` moreover have "eventually (\x. dist (f x) 0 \ dist (f x) y + dist 0 y) F" ``` hoelzl@51474 ` 81` ``` by (intro always_eventually) (metis dist_commute dist_triangle) ``` hoelzl@51474 ` 82` ``` with * have "eventually (\x. dist (f x) 0 \ K + dist 0 y) F" ``` hoelzl@51474 ` 83` ``` by eventually_elim auto ``` wenzelm@60758 ` 84` ``` with \0 < K\ show "\K>0. eventually (\x. dist (f x) 0 \ K) F" ``` hoelzl@51474 ` 85` ``` by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto ``` lp15@62379 ` 86` ```qed (force simp del: norm_conv_dist [symmetric]) ``` huffman@31355 ` 87` huffman@31487 ` 88` ```lemma BfunI: ``` wenzelm@63546 ` 89` ``` assumes K: "eventually (\x. norm (f x) \ K) F" ``` wenzelm@63546 ` 90` ``` shows "Bfun f F" ``` wenzelm@63546 ` 91` ``` unfolding Bfun_def ``` huffman@31355 ` 92` ```proof (intro exI conjI allI) ``` huffman@31355 ` 93` ``` show "0 < max K 1" by simp ``` huffman@44195 ` 94` ``` show "eventually (\x. norm (f x) \ max K 1) F" ``` wenzelm@63546 ` 95` ``` using K by (rule eventually_mono) simp ``` huffman@31355 ` 96` ```qed ``` huffman@31355 ` 97` huffman@31355 ` 98` ```lemma BfunE: ``` huffman@44195 ` 99` ``` assumes "Bfun f F" ``` huffman@44195 ` 100` ``` obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F" ``` wenzelm@63546 ` 101` ``` using assms unfolding Bfun_def by blast ``` huffman@31355 ` 102` hoelzl@51531 ` 103` ```lemma Cauchy_Bseq: "Cauchy X \ Bseq X" ``` hoelzl@51531 ` 104` ``` unfolding Cauchy_def Bfun_metric_def eventually_sequentially ``` hoelzl@51531 ` 105` ``` apply (erule_tac x=1 in allE) ``` hoelzl@51531 ` 106` ``` apply simp ``` hoelzl@51531 ` 107` ``` apply safe ``` hoelzl@51531 ` 108` ``` apply (rule_tac x="X M" in exI) ``` hoelzl@51531 ` 109` ``` apply (rule_tac x=1 in exI) ``` hoelzl@51531 ` 110` ``` apply (erule_tac x=M in allE) ``` hoelzl@51531 ` 111` ``` apply simp ``` hoelzl@51531 ` 112` ``` apply (rule_tac x=M in exI) ``` hoelzl@51531 ` 113` ``` apply (auto simp: dist_commute) ``` hoelzl@51531 ` 114` ``` done ``` hoelzl@51531 ` 115` hoelzl@51531 ` 116` wenzelm@60758 ` 117` ```subsubsection \Bounded Sequences\ ``` hoelzl@51531 ` 118` hoelzl@51531 ` 119` ```lemma BseqI': "(\n. norm (X n) \ K) \ Bseq X" ``` hoelzl@51531 ` 120` ``` by (intro BfunI) (auto simp: eventually_sequentially) ``` hoelzl@51531 ` 121` hoelzl@51531 ` 122` ```lemma BseqI2': "\n\N. norm (X n) \ K \ Bseq X" ``` hoelzl@51531 ` 123` ``` by (intro BfunI) (auto simp: eventually_sequentially) ``` hoelzl@51531 ` 124` hoelzl@51531 ` 125` ```lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)" ``` hoelzl@51531 ` 126` ``` unfolding Bfun_def eventually_sequentially ``` hoelzl@51531 ` 127` ```proof safe ``` wenzelm@63546 ` 128` ``` fix N K ``` wenzelm@63546 ` 129` ``` assume "0 < K" "\n\N. norm (X n) \ K" ``` hoelzl@51531 ` 130` ``` then show "\K>0. \n. norm (X n) \ K" ``` haftmann@54863 ` 131` ``` by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) ``` hoelzl@51531 ` 132` ``` (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) ``` hoelzl@51531 ` 133` ```qed auto ``` hoelzl@51531 ` 134` wenzelm@63546 ` 135` ```lemma BseqE: "Bseq X \ (\K. 0 < K \ \n. norm (X n) \ K \ Q) \ Q" ``` wenzelm@63546 ` 136` ``` unfolding Bseq_def by auto ``` wenzelm@63546 ` 137` wenzelm@63546 ` 138` ```lemma BseqD: "Bseq X \ \K. 0 < K \ (\n. norm (X n) \ K)" ``` wenzelm@63546 ` 139` ``` by (simp add: Bseq_def) ``` wenzelm@63546 ` 140` wenzelm@63546 ` 141` ```lemma BseqI: "0 < K \ \n. norm (X n) \ K \ Bseq X" ``` wenzelm@63546 ` 142` ``` by (auto simp add: Bseq_def) ``` wenzelm@63546 ` 143` wenzelm@63546 ` 144` ```lemma Bseq_bdd_above: "Bseq X \ bdd_above (range X)" ``` wenzelm@63546 ` 145` ``` for X :: "nat \ real" ``` hoelzl@54263 ` 146` ```proof (elim BseqE, intro bdd_aboveI2) ``` wenzelm@63546 ` 147` ``` fix K n ``` wenzelm@63546 ` 148` ``` assume "0 < K" "\n. norm (X n) \ K" ``` wenzelm@63546 ` 149` ``` then show "X n \ K" ``` hoelzl@54263 ` 150` ``` by (auto elim!: allE[of _ n]) ``` hoelzl@54263 ` 151` ```qed ``` hoelzl@54263 ` 152` wenzelm@63546 ` 153` ```lemma Bseq_bdd_above': "Bseq X \ bdd_above (range (\n. norm (X n)))" ``` wenzelm@63546 ` 154` ``` for X :: "nat \ 'a :: real_normed_vector" ``` eberlm@61531 ` 155` ```proof (elim BseqE, intro bdd_aboveI2) ``` wenzelm@63546 ` 156` ``` fix K n ``` wenzelm@63546 ` 157` ``` assume "0 < K" "\n. norm (X n) \ K" ``` wenzelm@63546 ` 158` ``` then show "norm (X n) \ K" ``` eberlm@61531 ` 159` ``` by (auto elim!: allE[of _ n]) ``` eberlm@61531 ` 160` ```qed ``` eberlm@61531 ` 161` wenzelm@63546 ` 162` ```lemma Bseq_bdd_below: "Bseq X \ bdd_below (range X)" ``` wenzelm@63546 ` 163` ``` for X :: "nat \ real" ``` hoelzl@54263 ` 164` ```proof (elim BseqE, intro bdd_belowI2) ``` wenzelm@63546 ` 165` ``` fix K n ``` wenzelm@63546 ` 166` ``` assume "0 < K" "\n. norm (X n) \ K" ``` wenzelm@63546 ` 167` ``` then show "- K \ X n" ``` hoelzl@54263 ` 168` ``` by (auto elim!: allE[of _ n]) ``` hoelzl@54263 ` 169` ```qed ``` hoelzl@54263 ` 170` eberlm@61531 ` 171` ```lemma Bseq_eventually_mono: ``` eberlm@61531 ` 172` ``` assumes "eventually (\n. norm (f n) \ norm (g n)) sequentially" "Bseq g" ``` wenzelm@63546 ` 173` ``` shows "Bseq f" ``` eberlm@61531 ` 174` ```proof - ``` eberlm@61531 ` 175` ``` from assms(1) obtain N where N: "\n. n \ N \ norm (f n) \ norm (g n)" ``` eberlm@61531 ` 176` ``` by (auto simp: eventually_at_top_linorder) ``` wenzelm@63546 ` 177` ``` moreover from assms(2) obtain K where K: "\n. norm (g n) \ K" ``` wenzelm@63546 ` 178` ``` by (blast elim!: BseqE) ``` eberlm@61531 ` 179` ``` ultimately have "norm (f n) \ max K (Max {norm (f n) |n. n < N})" for n ``` eberlm@61531 ` 180` ``` apply (cases "n < N") ``` wenzelm@63546 ` 181` ``` subgoal by (rule max.coboundedI2, rule Max.coboundedI) auto ``` wenzelm@63546 ` 182` ``` subgoal by (rule max.coboundedI1) (force intro: order.trans[OF N K]) ``` eberlm@61531 ` 183` ``` done ``` wenzelm@63546 ` 184` ``` then show ?thesis by (blast intro: BseqI') ``` eberlm@61531 ` 185` ```qed ``` eberlm@61531 ` 186` wenzelm@63546 ` 187` ```lemma lemma_NBseq_def: "(\K > 0. \n. norm (X n) \ K) \ (\N. \n. norm (X n) \ real(Suc N))" ``` hoelzl@51531 ` 188` ```proof safe ``` hoelzl@51531 ` 189` ``` fix K :: real ``` hoelzl@51531 ` 190` ``` from reals_Archimedean2 obtain n :: nat where "K < real n" .. ``` hoelzl@51531 ` 191` ``` then have "K \ real (Suc n)" by auto ``` hoelzl@51531 ` 192` ``` moreover assume "\m. norm (X m) \ K" ``` hoelzl@51531 ` 193` ``` ultimately have "\m. norm (X m) \ real (Suc n)" ``` hoelzl@51531 ` 194` ``` by (blast intro: order_trans) ``` hoelzl@51531 ` 195` ``` then show "\N. \n. norm (X n) \ real (Suc N)" .. ``` lp15@61649 ` 196` ```next ``` lp15@61649 ` 197` ``` show "\N. \n. norm (X n) \ real (Suc N) \ \K>0. \n. norm (X n) \ K" ``` lp15@61649 ` 198` ``` using of_nat_0_less_iff by blast ``` lp15@61649 ` 199` ```qed ``` hoelzl@51531 ` 200` wenzelm@63546 ` 201` ```text \Alternative definition for \Bseq\.\ ``` wenzelm@63546 ` 202` ```lemma Bseq_iff: "Bseq X \ (\N. \n. norm (X n) \ real(Suc N))" ``` wenzelm@63546 ` 203` ``` by (simp add: Bseq_def) (simp add: lemma_NBseq_def) ``` wenzelm@63546 ` 204` wenzelm@63546 ` 205` ```lemma lemma_NBseq_def2: "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) < real(Suc N))" ``` wenzelm@63546 ` 206` ``` apply (subst lemma_NBseq_def) ``` wenzelm@63546 ` 207` ``` apply auto ``` wenzelm@63546 ` 208` ``` apply (rule_tac x = "Suc N" in exI) ``` wenzelm@63546 ` 209` ``` apply (rule_tac [2] x = N in exI) ``` wenzelm@63546 ` 210` ``` apply auto ``` wenzelm@63546 ` 211` ``` prefer 2 apply (blast intro: order_less_imp_le) ``` wenzelm@63546 ` 212` ``` apply (drule_tac x = n in spec) ``` wenzelm@63546 ` 213` ``` apply simp ``` wenzelm@63546 ` 214` ``` done ``` wenzelm@63546 ` 215` wenzelm@63546 ` 216` ```text \Yet another definition for Bseq.\ ``` wenzelm@63546 ` 217` ```lemma Bseq_iff1a: "Bseq X \ (\N. \n. norm (X n) < real (Suc N))" ``` wenzelm@63546 ` 218` ``` by (simp add: Bseq_def lemma_NBseq_def2) ``` wenzelm@63546 ` 219` wenzelm@63546 ` 220` ```subsubsection \A Few More Equivalence Theorems for Boundedness\ ``` wenzelm@63546 ` 221` wenzelm@63546 ` 222` ```text \Alternative formulation for boundedness.\ ``` wenzelm@63546 ` 223` ```lemma Bseq_iff2: "Bseq X \ (\k > 0. \x. \n. norm (X n + - x) \ k)" ``` wenzelm@63546 ` 224` ``` apply (unfold Bseq_def) ``` wenzelm@63546 ` 225` ``` apply safe ``` wenzelm@63546 ` 226` ``` apply (rule_tac [2] x = "k + norm x" in exI) ``` wenzelm@63546 ` 227` ``` apply (rule_tac x = K in exI) ``` wenzelm@63546 ` 228` ``` apply simp ``` wenzelm@63546 ` 229` ``` apply (rule exI [where x = 0]) ``` wenzelm@63546 ` 230` ``` apply auto ``` wenzelm@63546 ` 231` ``` apply (erule order_less_le_trans) ``` wenzelm@63546 ` 232` ``` apply simp ``` wenzelm@63546 ` 233` ``` apply (drule_tac x=n in spec) ``` wenzelm@63546 ` 234` ``` apply (drule order_trans [OF norm_triangle_ineq2]) ``` wenzelm@63546 ` 235` ``` apply simp ``` wenzelm@63546 ` 236` ``` done ``` wenzelm@63546 ` 237` wenzelm@63546 ` 238` ```text \Alternative formulation for boundedness.\ ``` wenzelm@63546 ` 239` ```lemma Bseq_iff3: "Bseq X \ (\k>0. \N. \n. norm (X n + - X N) \ k)" ``` wenzelm@63546 ` 240` ``` (is "?P \ ?Q") ``` haftmann@53602 ` 241` ```proof ``` haftmann@53602 ` 242` ``` assume ?P ``` wenzelm@63546 ` 243` ``` then obtain K where *: "0 < K" and **: "\n. norm (X n) \ K" ``` wenzelm@63546 ` 244` ``` by (auto simp add: Bseq_def) ``` haftmann@53602 ` 245` ``` from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp ``` haftmann@54230 ` 246` ``` from ** have "\n. norm (X n - X 0) \ K + norm (X 0)" ``` haftmann@54230 ` 247` ``` by (auto intro: order_trans norm_triangle_ineq4) ``` haftmann@54230 ` 248` ``` then have "\n. norm (X n + - X 0) \ K + norm (X 0)" ``` haftmann@54230 ` 249` ``` by simp ``` wenzelm@60758 ` 250` ``` with \0 < K + norm (X 0)\ show ?Q by blast ``` haftmann@53602 ` 251` ```next ``` wenzelm@63546 ` 252` ``` assume ?Q ``` wenzelm@63546 ` 253` ``` then show ?P by (auto simp add: Bseq_iff2) ``` haftmann@53602 ` 254` ```qed ``` hoelzl@51531 ` 255` wenzelm@63546 ` 256` ```lemma BseqI2: "\n. k \ f n \ f n \ K \ Bseq f" ``` wenzelm@63546 ` 257` ``` for k K :: real ``` wenzelm@63546 ` 258` ``` apply (simp add: Bseq_def) ``` wenzelm@63546 ` 259` ``` apply (rule_tac x = "(\k\ + \K\) + 1" in exI) ``` wenzelm@63546 ` 260` ``` apply auto ``` wenzelm@63546 ` 261` ``` apply (drule_tac x = n in spec) ``` wenzelm@63546 ` 262` ``` apply arith ``` wenzelm@63546 ` 263` ``` done ``` wenzelm@63546 ` 264` wenzelm@63546 ` 265` wenzelm@63546 ` 266` ```subsubsection \Upper Bounds and Lubs of Bounded Sequences\ ``` wenzelm@63546 ` 267` wenzelm@63546 ` 268` ```lemma Bseq_minus_iff: "Bseq (\n. - (X n) :: 'a::real_normed_vector) \ Bseq X" ``` hoelzl@51531 ` 269` ``` by (simp add: Bseq_def) ``` hoelzl@51531 ` 270` paulson@62087 ` 271` ```lemma Bseq_add: ``` wenzelm@63546 ` 272` ``` fixes f :: "nat \ 'a::real_normed_vector" ``` wenzelm@63546 ` 273` ``` assumes "Bseq f" ``` wenzelm@63546 ` 274` ``` shows "Bseq (\x. f x + c)" ``` eberlm@61531 ` 275` ```proof - ``` wenzelm@63546 ` 276` ``` from assms obtain K where K: "\x. norm (f x) \ K" ``` wenzelm@63546 ` 277` ``` unfolding Bseq_def by blast ``` eberlm@61531 ` 278` ``` { ``` eberlm@61531 ` 279` ``` fix x :: nat ``` eberlm@61531 ` 280` ``` have "norm (f x + c) \ norm (f x) + norm c" by (rule norm_triangle_ineq) ``` eberlm@61531 ` 281` ``` also have "norm (f x) \ K" by (rule K) ``` eberlm@61531 ` 282` ``` finally have "norm (f x + c) \ K + norm c" by simp ``` eberlm@61531 ` 283` ``` } ``` wenzelm@63546 ` 284` ``` then show ?thesis by (rule BseqI') ``` eberlm@61531 ` 285` ```qed ``` eberlm@61531 ` 286` wenzelm@63546 ` 287` ```lemma Bseq_add_iff: "Bseq (\x. f x + c) \ Bseq f" ``` wenzelm@63546 ` 288` ``` for f :: "nat \ 'a::real_normed_vector" ``` eberlm@61531 ` 289` ``` using Bseq_add[of f c] Bseq_add[of "\x. f x + c" "-c"] by auto ``` eberlm@61531 ` 290` paulson@62087 ` 291` ```lemma Bseq_mult: ``` wenzelm@63546 ` 292` ``` fixes f g :: "nat \ 'a::real_normed_field" ``` wenzelm@63546 ` 293` ``` assumes "Bseq f" and "Bseq g" ``` wenzelm@63546 ` 294` ``` shows "Bseq (\x. f x * g x)" ``` eberlm@61531 ` 295` ```proof - ``` wenzelm@63546 ` 296` ``` from assms obtain K1 K2 where K: "norm (f x) \ K1" "K1 > 0" "norm (g x) \ K2" "K2 > 0" ``` wenzelm@63546 ` 297` ``` for x ``` eberlm@61531 ` 298` ``` unfolding Bseq_def by blast ``` wenzelm@63546 ` 299` ``` then have "norm (f x * g x) \ K1 * K2" for x ``` wenzelm@63546 ` 300` ``` by (auto simp: norm_mult intro!: mult_mono) ``` wenzelm@63546 ` 301` ``` then show ?thesis by (rule BseqI') ``` eberlm@61531 ` 302` ```qed ``` eberlm@61531 ` 303` eberlm@61531 ` 304` ```lemma Bfun_const [simp]: "Bfun (\_. c) F" ``` eberlm@61531 ` 305` ``` unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"]) ``` eberlm@61531 ` 306` wenzelm@63546 ` 307` ```lemma Bseq_cmult_iff: ``` wenzelm@63546 ` 308` ``` fixes c :: "'a::real_normed_field" ``` wenzelm@63546 ` 309` ``` assumes "c \ 0" ``` wenzelm@63546 ` 310` ``` shows "Bseq (\x. c * f x) \ Bseq f" ``` eberlm@61531 ` 311` ```proof ``` wenzelm@63546 ` 312` ``` assume "Bseq (\x. c * f x)" ``` wenzelm@63546 ` 313` ``` with Bfun_const have "Bseq (\x. inverse c * (c * f x))" ``` wenzelm@63546 ` 314` ``` by (rule Bseq_mult) ``` wenzelm@63546 ` 315` ``` with \c \ 0\ show "Bseq f" ``` wenzelm@63546 ` 316` ``` by (simp add: divide_simps) ``` eberlm@61531 ` 317` ```qed (intro Bseq_mult Bfun_const) ``` eberlm@61531 ` 318` wenzelm@63546 ` 319` ```lemma Bseq_subseq: "Bseq f \ Bseq (\x. f (g x))" ``` wenzelm@63546 ` 320` ``` for f :: "nat \ 'a::real_normed_vector" ``` eberlm@61531 ` 321` ``` unfolding Bseq_def by auto ``` eberlm@61531 ` 322` wenzelm@63546 ` 323` ```lemma Bseq_Suc_iff: "Bseq (\n. f (Suc n)) \ Bseq f" ``` wenzelm@63546 ` 324` ``` for f :: "nat \ 'a::real_normed_vector" ``` eberlm@61531 ` 325` ``` using Bseq_offset[of f 1] by (auto intro: Bseq_subseq) ``` eberlm@61531 ` 326` eberlm@61531 ` 327` ```lemma increasing_Bseq_subseq_iff: ``` wenzelm@63546 ` 328` ``` assumes "\x y. x \ y \ norm (f x :: 'a::real_normed_vector) \ norm (f y)" "subseq g" ``` wenzelm@63546 ` 329` ``` shows "Bseq (\x. f (g x)) \ Bseq f" ``` eberlm@61531 ` 330` ```proof ``` eberlm@61531 ` 331` ``` assume "Bseq (\x. f (g x))" ``` wenzelm@63546 ` 332` ``` then obtain K where K: "\x. norm (f (g x)) \ K" ``` wenzelm@63546 ` 333` ``` unfolding Bseq_def by auto ``` eberlm@61531 ` 334` ``` { ``` eberlm@61531 ` 335` ``` fix x :: nat ``` eberlm@61531 ` 336` ``` from filterlim_subseq[OF assms(2)] obtain y where "g y \ x" ``` eberlm@61531 ` 337` ``` by (auto simp: filterlim_at_top eventually_at_top_linorder) ``` wenzelm@63546 ` 338` ``` then have "norm (f x) \ norm (f (g y))" ``` wenzelm@63546 ` 339` ``` using assms(1) by blast ``` eberlm@61531 ` 340` ``` also have "norm (f (g y)) \ K" by (rule K) ``` eberlm@61531 ` 341` ``` finally have "norm (f x) \ K" . ``` eberlm@61531 ` 342` ``` } ``` wenzelm@63546 ` 343` ``` then show "Bseq f" by (rule BseqI') ``` wenzelm@63546 ` 344` ```qed (use Bseq_subseq[of f g] in simp_all) ``` eberlm@61531 ` 345` eberlm@61531 ` 346` ```lemma nonneg_incseq_Bseq_subseq_iff: ``` wenzelm@63546 ` 347` ``` fixes f :: "nat \ real" ``` wenzelm@63546 ` 348` ``` and g :: "nat \ nat" ``` wenzelm@63546 ` 349` ``` assumes "\x. f x \ 0" "incseq f" "subseq g" ``` wenzelm@63546 ` 350` ``` shows "Bseq (\x. f (g x)) \ Bseq f" ``` eberlm@61531 ` 351` ``` using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def) ``` eberlm@61531 ` 352` wenzelm@63546 ` 353` ```lemma Bseq_eq_bounded: "range f \ {a..b} \ Bseq f" ``` wenzelm@63546 ` 354` ``` for a b :: real ``` hoelzl@51531 ` 355` ``` apply (simp add: subset_eq) ``` hoelzl@51531 ` 356` ``` apply (rule BseqI'[where K="max (norm a) (norm b)"]) ``` hoelzl@51531 ` 357` ``` apply (erule_tac x=n in allE) ``` hoelzl@51531 ` 358` ``` apply auto ``` hoelzl@51531 ` 359` ``` done ``` hoelzl@51531 ` 360` wenzelm@63546 ` 361` ```lemma incseq_bounded: "incseq X \ \i. X i \ B \ Bseq X" ``` wenzelm@63546 ` 362` ``` for B :: real ``` hoelzl@51531 ` 363` ``` by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) ``` hoelzl@51531 ` 364` wenzelm@63546 ` 365` ```lemma decseq_bounded: "decseq X \ \i. B \ X i \ Bseq X" ``` wenzelm@63546 ` 366` ``` for B :: real ``` hoelzl@51531 ` 367` ``` by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) ``` hoelzl@51531 ` 368` wenzelm@63546 ` 369` wenzelm@60758 ` 370` ```subsection \Bounded Monotonic Sequences\ ``` hoelzl@51531 ` 371` wenzelm@63546 ` 372` ```subsubsection \A Bounded and Monotonic Sequence Converges\ ``` hoelzl@51531 ` 373` hoelzl@51531 ` 374` ```(* TODO: delete *) ``` hoelzl@51531 ` 375` ```(* FIXME: one use in NSA/HSEQ.thy *) ``` wenzelm@63546 ` 376` ```lemma Bmonoseq_LIMSEQ: "\n. m \ n \ X n = X m \ \L. X \ L" ``` hoelzl@51531 ` 377` ``` apply (rule_tac x="X m" in exI) ``` hoelzl@51531 ` 378` ``` apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const]) ``` hoelzl@51531 ` 379` ``` unfolding eventually_sequentially ``` hoelzl@51531 ` 380` ``` apply blast ``` hoelzl@51531 ` 381` ``` done ``` hoelzl@51531 ` 382` wenzelm@63546 ` 383` wenzelm@60758 ` 384` ```subsection \Convergence to Zero\ ``` huffman@31349 ` 385` huffman@44081 ` 386` ```definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44195 ` 387` ``` where "Zfun f F = (\r>0. eventually (\x. norm (f x) < r) F)" ``` huffman@31349 ` 388` wenzelm@63546 ` 389` ```lemma ZfunI: "(\r. 0 < r \ eventually (\x. norm (f x) < r) F) \ Zfun f F" ``` wenzelm@63546 ` 390` ``` by (simp add: Zfun_def) ``` wenzelm@63546 ` 391` wenzelm@63546 ` 392` ```lemma ZfunD: "Zfun f F \ 0 < r \ eventually (\x. norm (f x) < r) F" ``` wenzelm@63546 ` 393` ``` by (simp add: Zfun_def) ``` wenzelm@63546 ` 394` wenzelm@63546 ` 395` ```lemma Zfun_ssubst: "eventually (\x. f x = g x) F \ Zfun g F \ Zfun f F" ``` huffman@44081 ` 396` ``` unfolding Zfun_def by (auto elim!: eventually_rev_mp) ``` huffman@31355 ` 397` huffman@44195 ` 398` ```lemma Zfun_zero: "Zfun (\x. 0) F" ``` huffman@44081 ` 399` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 400` huffman@44195 ` 401` ```lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) F = Zfun (\x. f x) F" ``` huffman@44081 ` 402` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 403` huffman@31349 ` 404` ```lemma Zfun_imp_Zfun: ``` huffman@44195 ` 405` ``` assumes f: "Zfun f F" ``` wenzelm@63546 ` 406` ``` and g: "eventually (\x. norm (g x) \ norm (f x) * K) F" ``` huffman@44195 ` 407` ``` shows "Zfun (\x. g x) F" ``` wenzelm@63546 ` 408` ```proof (cases "0 < K") ``` wenzelm@63546 ` 409` ``` case K: True ``` huffman@31349 ` 410` ``` show ?thesis ``` huffman@31349 ` 411` ``` proof (rule ZfunI) ``` wenzelm@63546 ` 412` ``` fix r :: real ``` wenzelm@63546 ` 413` ``` assume "0 < r" ``` wenzelm@63546 ` 414` ``` then have "0 < r / K" using K by simp ``` huffman@44195 ` 415` ``` then have "eventually (\x. norm (f x) < r / K) F" ``` lp15@61649 ` 416` ``` using ZfunD [OF f] by blast ``` huffman@44195 ` 417` ``` with g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 418` ``` proof eventually_elim ``` noschinl@46887 ` 419` ``` case (elim x) ``` wenzelm@63546 ` 420` ``` then have "norm (f x) * K < r" ``` huffman@31349 ` 421` ``` by (simp add: pos_less_divide_eq K) ``` wenzelm@63546 ` 422` ``` then show ?case ``` noschinl@46887 ` 423` ``` by (simp add: order_le_less_trans [OF elim(1)]) ``` huffman@31349 ` 424` ``` qed ``` huffman@31349 ` 425` ``` qed ``` huffman@31349 ` 426` ```next ``` wenzelm@63546 ` 427` ``` case False ``` wenzelm@63546 ` 428` ``` then have K: "K \ 0" by (simp only: not_less) ``` huffman@31355 ` 429` ``` show ?thesis ``` huffman@31355 ` 430` ``` proof (rule ZfunI) ``` huffman@31355 ` 431` ``` fix r :: real ``` huffman@31355 ` 432` ``` assume "0 < r" ``` huffman@44195 ` 433` ``` from g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 434` ``` proof eventually_elim ``` noschinl@46887 ` 435` ``` case (elim x) ``` noschinl@46887 ` 436` ``` also have "norm (f x) * K \ norm (f x) * 0" ``` huffman@31355 ` 437` ``` using K norm_ge_zero by (rule mult_left_mono) ``` noschinl@46887 ` 438` ``` finally show ?case ``` wenzelm@60758 ` 439` ``` using \0 < r\ by simp ``` huffman@31355 ` 440` ``` qed ``` huffman@31355 ` 441` ``` qed ``` huffman@31349 ` 442` ```qed ``` huffman@31349 ` 443` wenzelm@63546 ` 444` ```lemma Zfun_le: "Zfun g F \ \x. norm (f x) \ norm (g x) \ Zfun f F" ``` wenzelm@63546 ` 445` ``` by (erule Zfun_imp_Zfun [where K = 1]) simp ``` huffman@31349 ` 446` huffman@31349 ` 447` ```lemma Zfun_add: ``` wenzelm@63546 ` 448` ``` assumes f: "Zfun f F" ``` wenzelm@63546 ` 449` ``` and g: "Zfun g F" ``` huffman@44195 ` 450` ``` shows "Zfun (\x. f x + g x) F" ``` huffman@31349 ` 451` ```proof (rule ZfunI) ``` wenzelm@63546 ` 452` ``` fix r :: real ``` wenzelm@63546 ` 453` ``` assume "0 < r" ``` wenzelm@63546 ` 454` ``` then have r: "0 < r / 2" by simp ``` huffman@44195 ` 455` ``` have "eventually (\x. norm (f x) < r/2) F" ``` huffman@31487 ` 456` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 457` ``` moreover ``` huffman@44195 ` 458` ``` have "eventually (\x. norm (g x) < r/2) F" ``` huffman@31487 ` 459` ``` using g r by (rule ZfunD) ``` huffman@31349 ` 460` ``` ultimately ``` huffman@44195 ` 461` ``` show "eventually (\x. norm (f x + g x) < r) F" ``` noschinl@46887 ` 462` ``` proof eventually_elim ``` noschinl@46887 ` 463` ``` case (elim x) ``` huffman@31487 ` 464` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@31349 ` 465` ``` by (rule norm_triangle_ineq) ``` huffman@31349 ` 466` ``` also have "\ < r/2 + r/2" ``` noschinl@46887 ` 467` ``` using elim by (rule add_strict_mono) ``` noschinl@46887 ` 468` ``` finally show ?case ``` huffman@31349 ` 469` ``` by simp ``` huffman@31349 ` 470` ``` qed ``` huffman@31349 ` 471` ```qed ``` huffman@31349 ` 472` huffman@44195 ` 473` ```lemma Zfun_minus: "Zfun f F \ Zfun (\x. - f x) F" ``` huffman@44081 ` 474` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 475` wenzelm@63546 ` 476` ```lemma Zfun_diff: "Zfun f F \ Zfun g F \ Zfun (\x. f x - g x) F" ``` haftmann@54230 ` 477` ``` using Zfun_add [of f F "\x. - g x"] by (simp add: Zfun_minus) ``` huffman@31349 ` 478` huffman@31349 ` 479` ```lemma (in bounded_linear) Zfun: ``` huffman@44195 ` 480` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 481` ``` shows "Zfun (\x. f (g x)) F" ``` huffman@31349 ` 482` ```proof - ``` wenzelm@63546 ` 483` ``` obtain K where "norm (f x) \ norm x * K" for x ``` lp15@61649 ` 484` ``` using bounded by blast ``` huffman@44195 ` 485` ``` then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F" ``` huffman@31355 ` 486` ``` by simp ``` huffman@31487 ` 487` ``` with g show ?thesis ``` huffman@31349 ` 488` ``` by (rule Zfun_imp_Zfun) ``` huffman@31349 ` 489` ```qed ``` huffman@31349 ` 490` huffman@31349 ` 491` ```lemma (in bounded_bilinear) Zfun: ``` huffman@44195 ` 492` ``` assumes f: "Zfun f F" ``` wenzelm@63546 ` 493` ``` and g: "Zfun g F" ``` huffman@44195 ` 494` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31349 ` 495` ```proof (rule ZfunI) ``` wenzelm@63546 ` 496` ``` fix r :: real ``` wenzelm@63546 ` 497` ``` assume r: "0 < r" ``` huffman@31349 ` 498` ``` obtain K where K: "0 < K" ``` wenzelm@63546 ` 499` ``` and norm_le: "norm (x ** y) \ norm x * norm y * K" for x y ``` lp15@61649 ` 500` ``` using pos_bounded by blast ``` huffman@31349 ` 501` ``` from K have K': "0 < inverse K" ``` huffman@31349 ` 502` ``` by (rule positive_imp_inverse_positive) ``` huffman@44195 ` 503` ``` have "eventually (\x. norm (f x) < r) F" ``` huffman@31487 ` 504` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 505` ``` moreover ``` huffman@44195 ` 506` ``` have "eventually (\x. norm (g x) < inverse K) F" ``` huffman@31487 ` 507` ``` using g K' by (rule ZfunD) ``` huffman@31349 ` 508` ``` ultimately ``` huffman@44195 ` 509` ``` show "eventually (\x. norm (f x ** g x) < r) F" ``` noschinl@46887 ` 510` ``` proof eventually_elim ``` noschinl@46887 ` 511` ``` case (elim x) ``` huffman@31487 ` 512` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31349 ` 513` ``` by (rule norm_le) ``` huffman@31487 ` 514` ``` also have "norm (f x) * norm (g x) * K < r * inverse K * K" ``` noschinl@46887 ` 515` ``` by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) ``` huffman@31349 ` 516` ``` also from K have "r * inverse K * K = r" ``` huffman@31349 ` 517` ``` by simp ``` noschinl@46887 ` 518` ``` finally show ?case . ``` huffman@31349 ` 519` ``` qed ``` huffman@31349 ` 520` ```qed ``` huffman@31349 ` 521` wenzelm@63546 ` 522` ```lemma (in bounded_bilinear) Zfun_left: "Zfun f F \ Zfun (\x. f x ** a) F" ``` huffman@44081 ` 523` ``` by (rule bounded_linear_left [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 524` wenzelm@63546 ` 525` ```lemma (in bounded_bilinear) Zfun_right: "Zfun f F \ Zfun (\x. a ** f x) F" ``` huffman@44081 ` 526` ``` by (rule bounded_linear_right [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 527` huffman@44282 ` 528` ```lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] ``` huffman@44282 ` 529` ```lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] ``` huffman@44282 ` 530` ```lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] ``` huffman@31349 ` 531` wenzelm@61973 ` 532` ```lemma tendsto_Zfun_iff: "(f \ a) F = Zfun (\x. f x - a) F" ``` huffman@44081 ` 533` ``` by (simp only: tendsto_iff Zfun_def dist_norm) ``` huffman@31349 ` 534` wenzelm@63546 ` 535` ```lemma tendsto_0_le: ``` wenzelm@63546 ` 536` ``` "(f \ 0) F \ eventually (\x. norm (g x) \ norm (f x) * K) F \ (g \ 0) F" ``` lp15@56366 ` 537` ``` by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) ``` lp15@56366 ` 538` wenzelm@63546 ` 539` wenzelm@60758 ` 540` ```subsubsection \Distance and norms\ ``` huffman@36662 ` 541` hoelzl@51531 ` 542` ```lemma tendsto_dist [tendsto_intros]: ``` wenzelm@63546 ` 543` ``` fixes l m :: "'a::metric_space" ``` wenzelm@63546 ` 544` ``` assumes f: "(f \ l) F" ``` wenzelm@63546 ` 545` ``` and g: "(g \ m) F" ``` wenzelm@61973 ` 546` ``` shows "((\x. dist (f x) (g x)) \ dist l m) F" ``` hoelzl@51531 ` 547` ```proof (rule tendstoI) ``` wenzelm@63546 ` 548` ``` fix e :: real ``` wenzelm@63546 ` 549` ``` assume "0 < e" ``` wenzelm@63546 ` 550` ``` then have e2: "0 < e/2" by simp ``` hoelzl@51531 ` 551` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` hoelzl@51531 ` 552` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F" ``` hoelzl@51531 ` 553` ``` proof (eventually_elim) ``` hoelzl@51531 ` 554` ``` case (elim x) ``` hoelzl@51531 ` 555` ``` then show "dist (dist (f x) (g x)) (dist l m) < e" ``` hoelzl@51531 ` 556` ``` unfolding dist_real_def ``` hoelzl@51531 ` 557` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` wenzelm@63546 ` 558` ``` and dist_triangle2 [of "g x" "l" "m"] ``` wenzelm@63546 ` 559` ``` and dist_triangle3 [of "l" "m" "f x"] ``` wenzelm@63546 ` 560` ``` and dist_triangle [of "f x" "m" "g x"] ``` hoelzl@51531 ` 561` ``` by arith ``` hoelzl@51531 ` 562` ``` qed ``` hoelzl@51531 ` 563` ```qed ``` hoelzl@51531 ` 564` hoelzl@51531 ` 565` ```lemma continuous_dist[continuous_intros]: ``` hoelzl@51531 ` 566` ``` fixes f g :: "_ \ 'a :: metric_space" ``` hoelzl@51531 ` 567` ``` shows "continuous F f \ continuous F g \ continuous F (\x. dist (f x) (g x))" ``` hoelzl@51531 ` 568` ``` unfolding continuous_def by (rule tendsto_dist) ``` hoelzl@51531 ` 569` hoelzl@56371 ` 570` ```lemma continuous_on_dist[continuous_intros]: ``` hoelzl@51531 ` 571` ``` fixes f g :: "_ \ 'a :: metric_space" ``` hoelzl@51531 ` 572` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))" ``` hoelzl@51531 ` 573` ``` unfolding continuous_on_def by (auto intro: tendsto_dist) ``` hoelzl@51531 ` 574` wenzelm@63546 ` 575` ```lemma tendsto_norm [tendsto_intros]: "(f \ a) F \ ((\x. norm (f x)) \ norm a) F" ``` huffman@44081 ` 576` ``` unfolding norm_conv_dist by (intro tendsto_intros) ``` huffman@36662 ` 577` wenzelm@63546 ` 578` ```lemma continuous_norm [continuous_intros]: "continuous F f \ continuous F (\x. norm (f x))" ``` hoelzl@51478 ` 579` ``` unfolding continuous_def by (rule tendsto_norm) ``` hoelzl@51478 ` 580` hoelzl@56371 ` 581` ```lemma continuous_on_norm [continuous_intros]: ``` hoelzl@51478 ` 582` ``` "continuous_on s f \ continuous_on s (\x. norm (f x))" ``` hoelzl@51478 ` 583` ``` unfolding continuous_on_def by (auto intro: tendsto_norm) ``` hoelzl@51478 ` 584` wenzelm@63546 ` 585` ```lemma tendsto_norm_zero: "(f \ 0) F \ ((\x. norm (f x)) \ 0) F" ``` wenzelm@63546 ` 586` ``` by (drule tendsto_norm) simp ``` wenzelm@63546 ` 587` wenzelm@63546 ` 588` ```lemma tendsto_norm_zero_cancel: "((\x. norm (f x)) \ 0) F \ (f \ 0) F" ``` huffman@44081 ` 589` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@36662 ` 590` wenzelm@63546 ` 591` ```lemma tendsto_norm_zero_iff: "((\x. norm (f x)) \ 0) F \ (f \ 0) F" ``` huffman@44081 ` 592` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@31349 ` 593` wenzelm@63546 ` 594` ```lemma tendsto_rabs [tendsto_intros]: "(f \ l) F \ ((\x. \f x\) \ \l\) F" ``` wenzelm@63546 ` 595` ``` for l :: real ``` wenzelm@63546 ` 596` ``` by (fold real_norm_def) (rule tendsto_norm) ``` huffman@44194 ` 597` hoelzl@51478 ` 598` ```lemma continuous_rabs [continuous_intros]: ``` hoelzl@51478 ` 599` ``` "continuous F f \ continuous F (\x. \f x :: real\)" ``` hoelzl@51478 ` 600` ``` unfolding real_norm_def[symmetric] by (rule continuous_norm) ``` hoelzl@51478 ` 601` hoelzl@56371 ` 602` ```lemma continuous_on_rabs [continuous_intros]: ``` hoelzl@51478 ` 603` ``` "continuous_on s f \ continuous_on s (\x. \f x :: real\)" ``` hoelzl@51478 ` 604` ``` unfolding real_norm_def[symmetric] by (rule continuous_on_norm) ``` hoelzl@51478 ` 605` wenzelm@63546 ` 606` ```lemma tendsto_rabs_zero: "(f \ (0::real)) F \ ((\x. \f x\) \ 0) F" ``` wenzelm@63546 ` 607` ``` by (fold real_norm_def) (rule tendsto_norm_zero) ``` wenzelm@63546 ` 608` wenzelm@63546 ` 609` ```lemma tendsto_rabs_zero_cancel: "((\x. \f x\) \ (0::real)) F \ (f \ 0) F" ``` wenzelm@63546 ` 610` ``` by (fold real_norm_def) (rule tendsto_norm_zero_cancel) ``` wenzelm@63546 ` 611` wenzelm@63546 ` 612` ```lemma tendsto_rabs_zero_iff: "((\x. \f x\) \ (0::real)) F \ (f \ 0) F" ``` wenzelm@63546 ` 613` ``` by (fold real_norm_def) (rule tendsto_norm_zero_iff) ``` wenzelm@63546 ` 614` huffman@44194 ` 615` hoelzl@62368 ` 616` ```subsection \Topological Monoid\ ``` hoelzl@62368 ` 617` hoelzl@62368 ` 618` ```class topological_monoid_add = topological_space + monoid_add + ``` hoelzl@62368 ` 619` ``` assumes tendsto_add_Pair: "LIM x (nhds a \\<^sub>F nhds b). fst x + snd x :> nhds (a + b)" ``` hoelzl@62368 ` 620` hoelzl@62368 ` 621` ```class topological_comm_monoid_add = topological_monoid_add + comm_monoid_add ``` huffman@44194 ` 622` huffman@31565 ` 623` ```lemma tendsto_add [tendsto_intros]: ``` hoelzl@62368 ` 624` ``` fixes a b :: "'a::topological_monoid_add" ``` hoelzl@62368 ` 625` ``` shows "(f \ a) F \ (g \ b) F \ ((\x. f x + g x) \ a + b) F" ``` hoelzl@62368 ` 626` ``` using filterlim_compose[OF tendsto_add_Pair, of "\x. (f x, g x)" a b F] ``` hoelzl@62368 ` 627` ``` by (simp add: nhds_prod[symmetric] tendsto_Pair) ``` huffman@31349 ` 628` hoelzl@51478 ` 629` ```lemma continuous_add [continuous_intros]: ``` hoelzl@62368 ` 630` ``` fixes f g :: "_ \ 'b::topological_monoid_add" ``` hoelzl@51478 ` 631` ``` shows "continuous F f \ continuous F g \ continuous F (\x. f x + g x)" ``` hoelzl@51478 ` 632` ``` unfolding continuous_def by (rule tendsto_add) ``` hoelzl@51478 ` 633` hoelzl@56371 ` 634` ```lemma continuous_on_add [continuous_intros]: ``` hoelzl@62368 ` 635` ``` fixes f g :: "_ \ 'b::topological_monoid_add" ``` hoelzl@51478 ` 636` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)" ``` hoelzl@51478 ` 637` ``` unfolding continuous_on_def by (auto intro: tendsto_add) ``` hoelzl@51478 ` 638` huffman@44194 ` 639` ```lemma tendsto_add_zero: ``` hoelzl@62368 ` 640` ``` fixes f g :: "_ \ 'b::topological_monoid_add" ``` wenzelm@63546 ` 641` ``` shows "(f \ 0) F \ (g \ 0) F \ ((\x. f x + g x) \ 0) F" ``` wenzelm@63546 ` 642` ``` by (drule (1) tendsto_add) simp ``` huffman@44194 ` 643` nipkow@64267 ` 644` ```lemma tendsto_sum [tendsto_intros]: ``` hoelzl@62368 ` 645` ``` fixes f :: "'a \ 'b \ 'c::topological_comm_monoid_add" ``` wenzelm@63915 ` 646` ``` shows "(\i. i \ I \ (f i \ a i) F) \ ((\x. \i\I. f i x) \ (\i\I. a i)) F" ``` wenzelm@63915 ` 647` ``` by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add) ``` hoelzl@62368 ` 648` nipkow@64267 ` 649` ```lemma continuous_sum [continuous_intros]: ``` hoelzl@62368 ` 650` ``` fixes f :: "'a \ 'b::t2_space \ 'c::topological_comm_monoid_add" ``` lp15@63301 ` 651` ``` shows "(\i. i \ I \ continuous F (f i)) \ continuous F (\x. \i\I. f i x)" ``` nipkow@64267 ` 652` ``` unfolding continuous_def by (rule tendsto_sum) ``` nipkow@64267 ` 653` nipkow@64267 ` 654` ```lemma continuous_on_sum [continuous_intros]: ``` hoelzl@62368 ` 655` ``` fixes f :: "'a \ 'b::topological_space \ 'c::topological_comm_monoid_add" ``` lp15@63301 ` 656` ``` shows "(\i. i \ I \ continuous_on S (f i)) \ continuous_on S (\x. \i\I. f i x)" ``` nipkow@64267 ` 657` ``` unfolding continuous_on_def by (auto intro: tendsto_sum) ``` hoelzl@62368 ` 658` hoelzl@62369 ` 659` ```instance nat :: topological_comm_monoid_add ``` wenzelm@63546 ` 660` ``` by standard ``` wenzelm@63546 ` 661` ``` (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) ``` hoelzl@62369 ` 662` hoelzl@62369 ` 663` ```instance int :: topological_comm_monoid_add ``` wenzelm@63546 ` 664` ``` by standard ``` wenzelm@63546 ` 665` ``` (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal) ``` wenzelm@63546 ` 666` hoelzl@62369 ` 667` immler@63081 ` 668` ```subsubsection \Topological group\ ``` immler@63081 ` 669` immler@63081 ` 670` ```class topological_group_add = topological_monoid_add + group_add + ``` immler@63081 ` 671` ``` assumes tendsto_uminus_nhds: "(uminus \ - a) (nhds a)" ``` immler@63081 ` 672` ```begin ``` immler@63081 ` 673` wenzelm@63546 ` 674` ```lemma tendsto_minus [tendsto_intros]: "(f \ a) F \ ((\x. - f x) \ - a) F" ``` immler@63081 ` 675` ``` by (rule filterlim_compose[OF tendsto_uminus_nhds]) ``` immler@63081 ` 676` immler@63081 ` 677` ```end ``` immler@63081 ` 678` immler@63081 ` 679` ```class topological_ab_group_add = topological_group_add + ab_group_add ``` immler@63081 ` 680` immler@63081 ` 681` ```instance topological_ab_group_add < topological_comm_monoid_add .. ``` immler@63081 ` 682` wenzelm@63546 ` 683` ```lemma continuous_minus [continuous_intros]: "continuous F f \ continuous F (\x. - f x)" ``` wenzelm@63546 ` 684` ``` for f :: "'a::t2_space \ 'b::topological_group_add" ``` immler@63081 ` 685` ``` unfolding continuous_def by (rule tendsto_minus) ``` immler@63081 ` 686` wenzelm@63546 ` 687` ```lemma continuous_on_minus [continuous_intros]: "continuous_on s f \ continuous_on s (\x. - f x)" ``` wenzelm@63546 ` 688` ``` for f :: "_ \ 'b::topological_group_add" ``` immler@63081 ` 689` ``` unfolding continuous_on_def by (auto intro: tendsto_minus) ``` hoelzl@62368 ` 690` wenzelm@63546 ` 691` ```lemma tendsto_minus_cancel: "((\x. - f x) \ - a) F \ (f \ a) F" ``` wenzelm@63546 ` 692` ``` for a :: "'a::topological_group_add" ``` wenzelm@63546 ` 693` ``` by (drule tendsto_minus) simp ``` immler@63081 ` 694` immler@63081 ` 695` ```lemma tendsto_minus_cancel_left: ``` wenzelm@63546 ` 696` ``` "(f \ - (y::_::topological_group_add)) F \ ((\x. - f x) \ y) F" ``` immler@63081 ` 697` ``` using tendsto_minus_cancel[of f "- y" F] tendsto_minus[of f "- y" F] ``` immler@63081 ` 698` ``` by auto ``` immler@63081 ` 699` immler@63081 ` 700` ```lemma tendsto_diff [tendsto_intros]: ``` immler@63081 ` 701` ``` fixes a b :: "'a::topological_group_add" ``` wenzelm@63546 ` 702` ``` shows "(f \ a) F \ (g \ b) F \ ((\x. f x - g x) \ a - b) F" ``` immler@63081 ` 703` ``` using tendsto_add [of f a F "\x. - g x" "- b"] by (simp add: tendsto_minus) ``` immler@63081 ` 704` immler@63081 ` 705` ```lemma continuous_diff [continuous_intros]: ``` immler@63081 ` 706` ``` fixes f g :: "'a::t2_space \ 'b::topological_group_add" ``` immler@63081 ` 707` ``` shows "continuous F f \ continuous F g \ continuous F (\x. f x - g x)" ``` immler@63081 ` 708` ``` unfolding continuous_def by (rule tendsto_diff) ``` immler@63081 ` 709` immler@63081 ` 710` ```lemma continuous_on_diff [continuous_intros]: ``` immler@63081 ` 711` ``` fixes f g :: "_ \ 'b::topological_group_add" ``` immler@63081 ` 712` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" ``` immler@63081 ` 713` ``` unfolding continuous_on_def by (auto intro: tendsto_diff) ``` immler@63081 ` 714` immler@63081 ` 715` ```lemma continuous_on_op_minus: "continuous_on (s::'a::topological_group_add set) (op - x)" ``` immler@63081 ` 716` ``` by (rule continuous_intros | simp)+ ``` immler@63081 ` 717` immler@63081 ` 718` ```instance real_normed_vector < topological_ab_group_add ``` hoelzl@62368 ` 719` ```proof ``` wenzelm@63546 ` 720` ``` fix a b :: 'a ``` wenzelm@63546 ` 721` ``` show "((\x. fst x + snd x) \ a + b) (nhds a \\<^sub>F nhds b)" ``` hoelzl@62368 ` 722` ``` unfolding tendsto_Zfun_iff add_diff_add ``` hoelzl@62368 ` 723` ``` using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"] ``` hoelzl@62368 ` 724` ``` by (intro Zfun_add) ``` hoelzl@62368 ` 725` ``` (auto simp add: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst) ``` immler@63081 ` 726` ``` show "(uminus \ - a) (nhds a)" ``` immler@63081 ` 727` ``` unfolding tendsto_Zfun_iff minus_diff_minus ``` immler@63081 ` 728` ``` using filterlim_ident[of "nhds a"] ``` immler@63081 ` 729` ``` by (intro Zfun_minus) (simp add: tendsto_Zfun_iff) ``` hoelzl@62368 ` 730` ```qed ``` hoelzl@62368 ` 731` immler@65204 ` 732` ```lemmas real_tendsto_sandwich = tendsto_sandwich[where 'a=real] ``` hoelzl@50999 ` 733` wenzelm@63546 ` 734` wenzelm@60758 ` 735` ```subsubsection \Linear operators and multiplication\ ``` huffman@44194 ` 736` wenzelm@63546 ` 737` ```lemma linear_times: "linear (\x. c * x)" ``` wenzelm@63546 ` 738` ``` for c :: "'a::real_algebra" ``` lp15@61806 ` 739` ``` by (auto simp: linearI distrib_left) ``` lp15@61806 ` 740` wenzelm@63546 ` 741` ```lemma (in bounded_linear) tendsto: "(g \ a) F \ ((\x. f (g x)) \ f a) F" ``` huffman@44081 ` 742` ``` by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) ``` huffman@31349 ` 743` wenzelm@63546 ` 744` ```lemma (in bounded_linear) continuous: "continuous F g \ continuous F (\x. f (g x))" ``` hoelzl@51478 ` 745` ``` using tendsto[of g _ F] by (auto simp: continuous_def) ``` hoelzl@51478 ` 746` wenzelm@63546 ` 747` ```lemma (in bounded_linear) continuous_on: "continuous_on s g \ continuous_on s (\x. f (g x))" ``` hoelzl@51478 ` 748` ``` using tendsto[of g] by (auto simp: continuous_on_def) ``` hoelzl@51478 ` 749` wenzelm@63546 ` 750` ```lemma (in bounded_linear) tendsto_zero: "(g \ 0) F \ ((\x. f (g x)) \ 0) F" ``` wenzelm@63546 ` 751` ``` by (drule tendsto) (simp only: zero) ``` huffman@44194 ` 752` huffman@44282 ` 753` ```lemma (in bounded_bilinear) tendsto: ``` wenzelm@63546 ` 754` ``` "(f \ a) F \ (g \ b) F \ ((\x. f x ** g x) \ a ** b) F" ``` wenzelm@63546 ` 755` ``` by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) ``` huffman@31349 ` 756` hoelzl@51478 ` 757` ```lemma (in bounded_bilinear) continuous: ``` hoelzl@51478 ` 758` ``` "continuous F f \ continuous F g \ continuous F (\x. f x ** g x)" ``` hoelzl@51478 ` 759` ``` using tendsto[of f _ F g] by (auto simp: continuous_def) ``` hoelzl@51478 ` 760` hoelzl@51478 ` 761` ```lemma (in bounded_bilinear) continuous_on: ``` hoelzl@51478 ` 762` ``` "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x ** g x)" ``` hoelzl@51478 ` 763` ``` using tendsto[of f _ _ g] by (auto simp: continuous_on_def) ``` hoelzl@51478 ` 764` huffman@44194 ` 765` ```lemma (in bounded_bilinear) tendsto_zero: ``` wenzelm@61973 ` 766` ``` assumes f: "(f \ 0) F" ``` wenzelm@63546 ` 767` ``` and g: "(g \ 0) F" ``` wenzelm@61973 ` 768` ``` shows "((\x. f x ** g x) \ 0) F" ``` huffman@44194 ` 769` ``` using tendsto [OF f g] by (simp add: zero_left) ``` huffman@31355 ` 770` huffman@44194 ` 771` ```lemma (in bounded_bilinear) tendsto_left_zero: ``` wenzelm@61973 ` 772` ``` "(f \ 0) F \ ((\x. f x ** c) \ 0) F" ``` huffman@44194 ` 773` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) ``` huffman@44194 ` 774` huffman@44194 ` 775` ```lemma (in bounded_bilinear) tendsto_right_zero: ``` wenzelm@61973 ` 776` ``` "(f \ 0) F \ ((\x. c ** f x) \ 0) F" ``` huffman@44194 ` 777` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) ``` huffman@44194 ` 778` huffman@44282 ` 779` ```lemmas tendsto_of_real [tendsto_intros] = ``` huffman@44282 ` 780` ``` bounded_linear.tendsto [OF bounded_linear_of_real] ``` huffman@44282 ` 781` huffman@44282 ` 782` ```lemmas tendsto_scaleR [tendsto_intros] = ``` huffman@44282 ` 783` ``` bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] ``` huffman@44282 ` 784` huffman@44282 ` 785` ```lemmas tendsto_mult [tendsto_intros] = ``` huffman@44282 ` 786` ``` bounded_bilinear.tendsto [OF bounded_bilinear_mult] ``` huffman@44194 ` 787` wenzelm@63546 ` 788` ```lemma tendsto_mult_left: "(f \ l) F \ ((\x. c * (f x)) \ c * l) F" ``` wenzelm@63546 ` 789` ``` for c :: "'a::real_normed_algebra" ``` wenzelm@63546 ` 790` ``` by (rule tendsto_mult [OF tendsto_const]) ``` wenzelm@63546 ` 791` wenzelm@63546 ` 792` ```lemma tendsto_mult_right: "(f \ l) F \ ((\x. (f x) * c) \ l * c) F" ``` wenzelm@63546 ` 793` ``` for c :: "'a::real_normed_algebra" ``` wenzelm@63546 ` 794` ``` by (rule tendsto_mult [OF _ tendsto_const]) ``` lp15@61806 ` 795` hoelzl@51478 ` 796` ```lemmas continuous_of_real [continuous_intros] = ``` hoelzl@51478 ` 797` ``` bounded_linear.continuous [OF bounded_linear_of_real] ``` hoelzl@51478 ` 798` hoelzl@51478 ` 799` ```lemmas continuous_scaleR [continuous_intros] = ``` hoelzl@51478 ` 800` ``` bounded_bilinear.continuous [OF bounded_bilinear_scaleR] ``` hoelzl@51478 ` 801` hoelzl@51478 ` 802` ```lemmas continuous_mult [continuous_intros] = ``` hoelzl@51478 ` 803` ``` bounded_bilinear.continuous [OF bounded_bilinear_mult] ``` hoelzl@51478 ` 804` hoelzl@56371 ` 805` ```lemmas continuous_on_of_real [continuous_intros] = ``` hoelzl@51478 ` 806` ``` bounded_linear.continuous_on [OF bounded_linear_of_real] ``` hoelzl@51478 ` 807` hoelzl@56371 ` 808` ```lemmas continuous_on_scaleR [continuous_intros] = ``` hoelzl@51478 ` 809` ``` bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] ``` hoelzl@51478 ` 810` hoelzl@56371 ` 811` ```lemmas continuous_on_mult [continuous_intros] = ``` hoelzl@51478 ` 812` ``` bounded_bilinear.continuous_on [OF bounded_bilinear_mult] ``` hoelzl@51478 ` 813` huffman@44568 ` 814` ```lemmas tendsto_mult_zero = ``` huffman@44568 ` 815` ``` bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 816` huffman@44568 ` 817` ```lemmas tendsto_mult_left_zero = ``` huffman@44568 ` 818` ``` bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 819` huffman@44568 ` 820` ```lemmas tendsto_mult_right_zero = ``` huffman@44568 ` 821` ``` bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 822` wenzelm@63546 ` 823` ```lemma tendsto_power [tendsto_intros]: "(f \ a) F \ ((\x. f x ^ n) \ a ^ n) F" ``` wenzelm@63546 ` 824` ``` for f :: "'a \ 'b::{power,real_normed_algebra}" ``` hoelzl@58729 ` 825` ``` by (induct n) (simp_all add: tendsto_mult) ``` huffman@44194 ` 826` wenzelm@63546 ` 827` ```lemma continuous_power [continuous_intros]: "continuous F f \ continuous F (\x. (f x)^n)" ``` wenzelm@63546 ` 828` ``` for f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` hoelzl@51478 ` 829` ``` unfolding continuous_def by (rule tendsto_power) ``` hoelzl@51478 ` 830` hoelzl@56371 ` 831` ```lemma continuous_on_power [continuous_intros]: ``` hoelzl@51478 ` 832` ``` fixes f :: "_ \ 'b::{power,real_normed_algebra}" ``` hoelzl@51478 ` 833` ``` shows "continuous_on s f \ continuous_on s (\x. (f x)^n)" ``` hoelzl@51478 ` 834` ``` unfolding continuous_on_def by (auto intro: tendsto_power) ``` hoelzl@51478 ` 835` nipkow@64272 ` 836` ```lemma tendsto_prod [tendsto_intros]: ``` huffman@44194 ` 837` ``` fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" ``` wenzelm@63915 ` 838` ``` shows "(\i. i \ S \ (f i \ L i) F) \ ((\x. \i\S. f i x) \ (\i\S. L i)) F" ``` wenzelm@63915 ` 839` ``` by (induct S rule: infinite_finite_induct) (simp_all add: tendsto_mult) ``` huffman@44194 ` 840` nipkow@64272 ` 841` ```lemma continuous_prod [continuous_intros]: ``` hoelzl@51478 ` 842` ``` fixes f :: "'a \ 'b::t2_space \ 'c::{real_normed_algebra,comm_ring_1}" ``` hoelzl@51478 ` 843` ``` shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" ``` nipkow@64272 ` 844` ``` unfolding continuous_def by (rule tendsto_prod) ``` nipkow@64272 ` 845` nipkow@64272 ` 846` ```lemma continuous_on_prod [continuous_intros]: ``` hoelzl@51478 ` 847` ``` fixes f :: "'a \ _ \ 'c::{real_normed_algebra,comm_ring_1}" ``` hoelzl@51478 ` 848` ``` shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" ``` nipkow@64272 ` 849` ``` unfolding continuous_on_def by (auto intro: tendsto_prod) ``` hoelzl@51478 ` 850` eberlm@61531 ` 851` ```lemma tendsto_of_real_iff: ``` wenzelm@63546 ` 852` ``` "((\x. of_real (f x) :: 'a::real_normed_div_algebra) \ of_real c) F \ (f \ c) F" ``` eberlm@61531 ` 853` ``` unfolding tendsto_iff by simp ``` eberlm@61531 ` 854` eberlm@61531 ` 855` ```lemma tendsto_add_const_iff: ``` wenzelm@63546 ` 856` ``` "((\x. c + f x :: 'a::real_normed_vector) \ c + d) F \ (f \ d) F" ``` paulson@62087 ` 857` ``` using tendsto_add[OF tendsto_const[of c], of f d] ``` wenzelm@63546 ` 858` ``` and tendsto_add[OF tendsto_const[of "-c"], of "\x. c + f x" "c + d"] by auto ``` eberlm@61531 ` 859` eberlm@61531 ` 860` wenzelm@60758 ` 861` ```subsubsection \Inverse and division\ ``` huffman@31355 ` 862` huffman@31355 ` 863` ```lemma (in bounded_bilinear) Zfun_prod_Bfun: ``` huffman@44195 ` 864` ``` assumes f: "Zfun f F" ``` wenzelm@63546 ` 865` ``` and g: "Bfun g F" ``` huffman@44195 ` 866` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31355 ` 867` ```proof - ``` huffman@31355 ` 868` ``` obtain K where K: "0 \ K" ``` huffman@31355 ` 869` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` lp15@61649 ` 870` ``` using nonneg_bounded by blast ``` huffman@31355 ` 871` ``` obtain B where B: "0 < B" ``` huffman@44195 ` 872` ``` and norm_g: "eventually (\x. norm (g x) \ B) F" ``` huffman@31487 ` 873` ``` using g by (rule BfunE) ``` huffman@44195 ` 874` ``` have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) F" ``` noschinl@46887 ` 875` ``` using norm_g proof eventually_elim ``` noschinl@46887 ` 876` ``` case (elim x) ``` huffman@31487 ` 877` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31355 ` 878` ``` by (rule norm_le) ``` huffman@31487 ` 879` ``` also have "\ \ norm (f x) * B * K" ``` wenzelm@63546 ` 880` ``` by (intro mult_mono' order_refl norm_g norm_ge_zero mult_nonneg_nonneg K elim) ``` huffman@31487 ` 881` ``` also have "\ = norm (f x) * (B * K)" ``` haftmann@57512 ` 882` ``` by (rule mult.assoc) ``` huffman@31487 ` 883` ``` finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . ``` huffman@31355 ` 884` ``` qed ``` huffman@31487 ` 885` ``` with f show ?thesis ``` huffman@31487 ` 886` ``` by (rule Zfun_imp_Zfun) ``` huffman@31355 ` 887` ```qed ``` huffman@31355 ` 888` huffman@31355 ` 889` ```lemma (in bounded_bilinear) Bfun_prod_Zfun: ``` huffman@44195 ` 890` ``` assumes f: "Bfun f F" ``` wenzelm@63546 ` 891` ``` and g: "Zfun g F" ``` huffman@44195 ` 892` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@44081 ` 893` ``` using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) ``` huffman@31355 ` 894` huffman@31355 ` 895` ```lemma Bfun_inverse_lemma: ``` huffman@31355 ` 896` ``` fixes x :: "'a::real_normed_div_algebra" ``` wenzelm@63546 ` 897` ``` shows "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" ``` wenzelm@63546 ` 898` ``` apply (subst nonzero_norm_inverse) ``` wenzelm@63546 ` 899` ``` apply clarsimp ``` huffman@44081 ` 900` ``` apply (erule (1) le_imp_inverse_le) ``` huffman@44081 ` 901` ``` done ``` huffman@31355 ` 902` huffman@31355 ` 903` ```lemma Bfun_inverse: ``` huffman@31355 ` 904` ``` fixes a :: "'a::real_normed_div_algebra" ``` wenzelm@61973 ` 905` ``` assumes f: "(f \ a) F" ``` huffman@31355 ` 906` ``` assumes a: "a \ 0" ``` huffman@44195 ` 907` ``` shows "Bfun (\x. inverse (f x)) F" ``` huffman@31355 ` 908` ```proof - ``` huffman@31355 ` 909` ``` from a have "0 < norm a" by simp ``` wenzelm@63546 ` 910` ``` then have "\r>0. r < norm a" by (rule dense) ``` wenzelm@63546 ` 911` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" ``` wenzelm@63546 ` 912` ``` by blast ``` huffman@44195 ` 913` ``` have "eventually (\x. dist (f x) a < r) F" ``` lp15@61649 ` 914` ``` using tendstoD [OF f r1] by blast ``` wenzelm@63546 ` 915` ``` then have "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F" ``` noschinl@46887 ` 916` ``` proof eventually_elim ``` noschinl@46887 ` 917` ``` case (elim x) ``` wenzelm@63546 ` 918` ``` then have 1: "norm (f x - a) < r" ``` huffman@31355 ` 919` ``` by (simp add: dist_norm) ``` wenzelm@63546 ` 920` ``` then have 2: "f x \ 0" using r2 by auto ``` wenzelm@63546 ` 921` ``` then have "norm (inverse (f x)) = inverse (norm (f x))" ``` huffman@31355 ` 922` ``` by (rule nonzero_norm_inverse) ``` huffman@31355 ` 923` ``` also have "\ \ inverse (norm a - r)" ``` huffman@31355 ` 924` ``` proof (rule le_imp_inverse_le) ``` wenzelm@63546 ` 925` ``` show "0 < norm a - r" ``` wenzelm@63546 ` 926` ``` using r2 by simp ``` huffman@31487 ` 927` ``` have "norm a - norm (f x) \ norm (a - f x)" ``` huffman@31355 ` 928` ``` by (rule norm_triangle_ineq2) ``` huffman@31487 ` 929` ``` also have "\ = norm (f x - a)" ``` huffman@31355 ` 930` ``` by (rule norm_minus_commute) ``` huffman@31355 ` 931` ``` also have "\ < r" using 1 . ``` wenzelm@63546 ` 932` ``` finally show "norm a - r \ norm (f x)" ``` wenzelm@63546 ` 933` ``` by simp ``` huffman@31355 ` 934` ``` qed ``` huffman@31487 ` 935` ``` finally show "norm (inverse (f x)) \ inverse (norm a - r)" . ``` huffman@31355 ` 936` ``` qed ``` wenzelm@63546 ` 937` ``` then show ?thesis by (rule BfunI) ``` huffman@31355 ` 938` ```qed ``` huffman@31355 ` 939` huffman@31565 ` 940` ```lemma tendsto_inverse [tendsto_intros]: ``` huffman@31355 ` 941` ``` fixes a :: "'a::real_normed_div_algebra" ``` wenzelm@61973 ` 942` ``` assumes f: "(f \ a) F" ``` wenzelm@63546 ` 943` ``` and a: "a \ 0" ``` wenzelm@61973 ` 944` ``` shows "((\x. inverse (f x)) \ inverse a) F" ``` huffman@31355 ` 945` ```proof - ``` huffman@31355 ` 946` ``` from a have "0 < norm a" by simp ``` huffman@44195 ` 947` ``` with f have "eventually (\x. dist (f x) a < norm a) F" ``` huffman@31355 ` 948` ``` by (rule tendstoD) ``` huffman@44195 ` 949` ``` then have "eventually (\x. f x \ 0) F" ``` lp15@61810 ` 950` ``` unfolding dist_norm by (auto elim!: eventually_mono) ``` huffman@44627 ` 951` ``` with a have "eventually (\x. inverse (f x) - inverse a = ``` huffman@44627 ` 952` ``` - (inverse (f x) * (f x - a) * inverse a)) F" ``` lp15@61810 ` 953` ``` by (auto elim!: eventually_mono simp: inverse_diff_inverse) ``` huffman@44627 ` 954` ``` moreover have "Zfun (\x. - (inverse (f x) * (f x - a) * inverse a)) F" ``` huffman@44627 ` 955` ``` by (intro Zfun_minus Zfun_mult_left ``` huffman@44627 ` 956` ``` bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] ``` huffman@44627 ` 957` ``` Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) ``` huffman@44627 ` 958` ``` ultimately show ?thesis ``` huffman@44627 ` 959` ``` unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) ``` huffman@31355 ` 960` ```qed ``` huffman@31355 ` 961` hoelzl@51478 ` 962` ```lemma continuous_inverse: ``` hoelzl@51478 ` 963` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` wenzelm@63546 ` 964` ``` assumes "continuous F f" ``` wenzelm@63546 ` 965` ``` and "f (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 966` ``` shows "continuous F (\x. inverse (f x))" ``` hoelzl@51478 ` 967` ``` using assms unfolding continuous_def by (rule tendsto_inverse) ``` hoelzl@51478 ` 968` hoelzl@51478 ` 969` ```lemma continuous_at_within_inverse[continuous_intros]: ``` hoelzl@51478 ` 970` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` wenzelm@63546 ` 971` ``` assumes "continuous (at a within s) f" ``` wenzelm@63546 ` 972` ``` and "f a \ 0" ``` hoelzl@51478 ` 973` ``` shows "continuous (at a within s) (\x. inverse (f x))" ``` hoelzl@51478 ` 974` ``` using assms unfolding continuous_within by (rule tendsto_inverse) ``` hoelzl@51478 ` 975` hoelzl@51478 ` 976` ```lemma isCont_inverse[continuous_intros, simp]: ``` hoelzl@51478 ` 977` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` wenzelm@63546 ` 978` ``` assumes "isCont f a" ``` wenzelm@63546 ` 979` ``` and "f a \ 0" ``` hoelzl@51478 ` 980` ``` shows "isCont (\x. inverse (f x)) a" ``` hoelzl@51478 ` 981` ``` using assms unfolding continuous_at by (rule tendsto_inverse) ``` hoelzl@51478 ` 982` hoelzl@56371 ` 983` ```lemma continuous_on_inverse[continuous_intros]: ``` hoelzl@51478 ` 984` ``` fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" ``` wenzelm@63546 ` 985` ``` assumes "continuous_on s f" ``` wenzelm@63546 ` 986` ``` and "\x\s. f x \ 0" ``` hoelzl@51478 ` 987` ``` shows "continuous_on s (\x. inverse (f x))" ``` lp15@61649 ` 988` ``` using assms unfolding continuous_on_def by (blast intro: tendsto_inverse) ``` hoelzl@51478 ` 989` huffman@31565 ` 990` ```lemma tendsto_divide [tendsto_intros]: ``` huffman@31355 ` 991` ``` fixes a b :: "'a::real_normed_field" ``` wenzelm@63546 ` 992` ``` shows "(f \ a) F \ (g \ b) F \ b \ 0 \ ((\x. f x / g x) \ a / b) F" ``` huffman@44282 ` 993` ``` by (simp add: tendsto_mult tendsto_inverse divide_inverse) ``` huffman@31355 ` 994` hoelzl@51478 ` 995` ```lemma continuous_divide: ``` hoelzl@51478 ` 996` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` wenzelm@63546 ` 997` ``` assumes "continuous F f" ``` wenzelm@63546 ` 998` ``` and "continuous F g" ``` wenzelm@63546 ` 999` ``` and "g (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 1000` ``` shows "continuous F (\x. (f x) / (g x))" ``` hoelzl@51478 ` 1001` ``` using assms unfolding continuous_def by (rule tendsto_divide) ``` hoelzl@51478 ` 1002` hoelzl@51478 ` 1003` ```lemma continuous_at_within_divide[continuous_intros]: ``` hoelzl@51478 ` 1004` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` wenzelm@63546 ` 1005` ``` assumes "continuous (at a within s) f" "continuous (at a within s) g" ``` wenzelm@63546 ` 1006` ``` and "g a \ 0" ``` hoelzl@51478 ` 1007` ``` shows "continuous (at a within s) (\x. (f x) / (g x))" ``` hoelzl@51478 ` 1008` ``` using assms unfolding continuous_within by (rule tendsto_divide) ``` hoelzl@51478 ` 1009` hoelzl@51478 ` 1010` ```lemma isCont_divide[continuous_intros, simp]: ``` hoelzl@51478 ` 1011` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` hoelzl@51478 ` 1012` ``` assumes "isCont f a" "isCont g a" "g a \ 0" ``` hoelzl@51478 ` 1013` ``` shows "isCont (\x. (f x) / g x) a" ``` hoelzl@51478 ` 1014` ``` using assms unfolding continuous_at by (rule tendsto_divide) ``` hoelzl@51478 ` 1015` hoelzl@56371 ` 1016` ```lemma continuous_on_divide[continuous_intros]: ``` hoelzl@51478 ` 1017` ``` fixes f :: "'a::topological_space \ 'b::real_normed_field" ``` wenzelm@63546 ` 1018` ``` assumes "continuous_on s f" "continuous_on s g" ``` wenzelm@63546 ` 1019` ``` and "\x\s. g x \ 0" ``` hoelzl@51478 ` 1020` ``` shows "continuous_on s (\x. (f x) / (g x))" ``` lp15@61649 ` 1021` ``` using assms unfolding continuous_on_def by (blast intro: tendsto_divide) ``` hoelzl@51478 ` 1022` wenzelm@63546 ` 1023` ```lemma tendsto_sgn [tendsto_intros]: "(f \ l) F \ l \ 0 \ ((\x. sgn (f x)) \ sgn l) F" ``` wenzelm@63546 ` 1024` ``` for l :: "'a::real_normed_vector" ``` huffman@44194 ` 1025` ``` unfolding sgn_div_norm by (simp add: tendsto_intros) ``` huffman@44194 ` 1026` hoelzl@51478 ` 1027` ```lemma continuous_sgn: ``` hoelzl@51478 ` 1028` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` wenzelm@63546 ` 1029` ``` assumes "continuous F f" ``` wenzelm@63546 ` 1030` ``` and "f (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 1031` ``` shows "continuous F (\x. sgn (f x))" ``` hoelzl@51478 ` 1032` ``` using assms unfolding continuous_def by (rule tendsto_sgn) ``` hoelzl@51478 ` 1033` hoelzl@51478 ` 1034` ```lemma continuous_at_within_sgn[continuous_intros]: ``` hoelzl@51478 ` 1035` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` wenzelm@63546 ` 1036` ``` assumes "continuous (at a within s) f" ``` wenzelm@63546 ` 1037` ``` and "f a \ 0" ``` hoelzl@51478 ` 1038` ``` shows "continuous (at a within s) (\x. sgn (f x))" ``` hoelzl@51478 ` 1039` ``` using assms unfolding continuous_within by (rule tendsto_sgn) ``` hoelzl@51478 ` 1040` hoelzl@51478 ` 1041` ```lemma isCont_sgn[continuous_intros]: ``` hoelzl@51478 ` 1042` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` wenzelm@63546 ` 1043` ``` assumes "isCont f a" ``` wenzelm@63546 ` 1044` ``` and "f a \ 0" ``` hoelzl@51478 ` 1045` ``` shows "isCont (\x. sgn (f x)) a" ``` hoelzl@51478 ` 1046` ``` using assms unfolding continuous_at by (rule tendsto_sgn) ``` hoelzl@51478 ` 1047` hoelzl@56371 ` 1048` ```lemma continuous_on_sgn[continuous_intros]: ``` hoelzl@51478 ` 1049` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` wenzelm@63546 ` 1050` ``` assumes "continuous_on s f" ``` wenzelm@63546 ` 1051` ``` and "\x\s. f x \ 0" ``` hoelzl@51478 ` 1052` ``` shows "continuous_on s (\x. sgn (f x))" ``` lp15@61649 ` 1053` ``` using assms unfolding continuous_on_def by (blast intro: tendsto_sgn) ``` hoelzl@51478 ` 1054` hoelzl@50325 ` 1055` ```lemma filterlim_at_infinity: ``` wenzelm@61076 ` 1056` ``` fixes f :: "_ \ 'a::real_normed_vector" ``` hoelzl@50325 ` 1057` ``` assumes "0 \ c" ``` hoelzl@50325 ` 1058` ``` shows "(LIM x F. f x :> at_infinity) \ (\r>c. eventually (\x. r \ norm (f x)) F)" ``` hoelzl@50325 ` 1059` ``` unfolding filterlim_iff eventually_at_infinity ``` hoelzl@50325 ` 1060` ```proof safe ``` wenzelm@63546 ` 1061` ``` fix P :: "'a \ bool" ``` wenzelm@63546 ` 1062` ``` fix b ``` hoelzl@50325 ` 1063` ``` assume *: "\r>c. eventually (\x. r \ norm (f x)) F" ``` wenzelm@63546 ` 1064` ``` assume P: "\x. b \ norm x \ P x" ``` hoelzl@50325 ` 1065` ``` have "max b (c + 1) > c" by auto ``` hoelzl@50325 ` 1066` ``` with * have "eventually (\x. max b (c + 1) \ norm (f x)) F" ``` hoelzl@50325 ` 1067` ``` by auto ``` hoelzl@50325 ` 1068` ``` then show "eventually (\x. P (f x)) F" ``` hoelzl@50325 ` 1069` ``` proof eventually_elim ``` wenzelm@63546 ` 1070` ``` case (elim x) ``` hoelzl@50325 ` 1071` ``` with P show "P (f x)" by auto ``` hoelzl@50325 ` 1072` ``` qed ``` hoelzl@50325 ` 1073` ```qed force ``` hoelzl@50325 ` 1074` eberlm@61531 ` 1075` ```lemma not_tendsto_and_filterlim_at_infinity: ``` wenzelm@63546 ` 1076` ``` fixes c :: "'a::real_normed_vector" ``` eberlm@61531 ` 1077` ``` assumes "F \ bot" ``` wenzelm@63546 ` 1078` ``` and "(f \ c) F" ``` wenzelm@63546 ` 1079` ``` and "filterlim f at_infinity F" ``` wenzelm@63546 ` 1080` ``` shows False ``` eberlm@61531 ` 1081` ```proof - ``` paulson@62087 ` 1082` ``` from tendstoD[OF assms(2), of "1/2"] ``` wenzelm@63546 ` 1083` ``` have "eventually (\x. dist (f x) c < 1/2) F" ``` wenzelm@63546 ` 1084` ``` by simp ``` wenzelm@63546 ` 1085` ``` moreover ``` wenzelm@63546 ` 1086` ``` from filterlim_at_infinity[of "norm c" f F] assms(3) ``` wenzelm@63546 ` 1087` ``` have "eventually (\x. norm (f x) \ norm c + 1) F" by simp ``` eberlm@61531 ` 1088` ``` ultimately have "eventually (\x. False) F" ``` eberlm@61531 ` 1089` ``` proof eventually_elim ``` wenzelm@63546 ` 1090` ``` fix x ``` wenzelm@63546 ` 1091` ``` assume A: "dist (f x) c < 1/2" ``` wenzelm@63546 ` 1092` ``` assume "norm (f x) \ norm c + 1" ``` lp15@62379 ` 1093` ``` also have "norm (f x) = dist (f x) 0" by simp ``` wenzelm@63546 ` 1094` ``` also have "\ \ dist (f x) c + dist c 0" by (rule dist_triangle) ``` lp15@62379 ` 1095` ``` finally show False using A by simp ``` eberlm@61531 ` 1096` ``` qed ``` eberlm@61531 ` 1097` ``` with assms show False by simp ``` eberlm@61531 ` 1098` ```qed ``` eberlm@61531 ` 1099` eberlm@61531 ` 1100` ```lemma filterlim_at_infinity_imp_not_convergent: ``` eberlm@61531 ` 1101` ``` assumes "filterlim f at_infinity sequentially" ``` wenzelm@63546 ` 1102` ``` shows "\ convergent f" ``` eberlm@61531 ` 1103` ``` by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms]) ``` eberlm@61531 ` 1104` ``` (simp_all add: convergent_LIMSEQ_iff) ``` eberlm@61531 ` 1105` eberlm@61531 ` 1106` ```lemma filterlim_at_infinity_imp_eventually_ne: ``` eberlm@61531 ` 1107` ``` assumes "filterlim f at_infinity F" ``` wenzelm@63546 ` 1108` ``` shows "eventually (\z. f z \ c) F" ``` eberlm@61531 ` 1109` ```proof - ``` wenzelm@63546 ` 1110` ``` have "norm c + 1 > 0" ``` wenzelm@63546 ` 1111` ``` by (intro add_nonneg_pos) simp_all ``` eberlm@61531 ` 1112` ``` with filterlim_at_infinity[OF order.refl, of f F] assms ``` wenzelm@63546 ` 1113` ``` have "eventually (\z. norm (f z) \ norm c + 1) F" ``` wenzelm@63546 ` 1114` ``` by blast ``` wenzelm@63546 ` 1115` ``` then show ?thesis ``` wenzelm@63546 ` 1116` ``` by eventually_elim auto ``` eberlm@61531 ` 1117` ```qed ``` eberlm@61531 ` 1118` paulson@62087 ` 1119` ```lemma tendsto_of_nat [tendsto_intros]: ``` wenzelm@63546 ` 1120` ``` "filterlim (of_nat :: nat \ 'a::real_normed_algebra_1) at_infinity sequentially" ``` eberlm@61531 ` 1121` ```proof (subst filterlim_at_infinity[OF order.refl], intro allI impI) ``` wenzelm@63040 ` 1122` ``` fix r :: real ``` wenzelm@63040 ` 1123` ``` assume r: "r > 0" ``` wenzelm@63040 ` 1124` ``` define n where "n = nat \r\" ``` wenzelm@63546 ` 1125` ``` from r have n: "\m\n. of_nat m \ r" ``` wenzelm@63546 ` 1126` ``` unfolding n_def by linarith ``` eberlm@61531 ` 1127` ``` from eventually_ge_at_top[of n] show "eventually (\m. norm (of_nat m :: 'a) \ r) sequentially" ``` wenzelm@63546 ` 1128` ``` by eventually_elim (use n in simp_all) ``` eberlm@61531 ` 1129` ```qed ``` eberlm@61531 ` 1130` eberlm@61531 ` 1131` wenzelm@60758 ` 1132` ```subsection \Relate @{const at}, @{const at_left} and @{const at_right}\ ``` hoelzl@50347 ` 1133` wenzelm@60758 ` 1134` ```text \ ``` wenzelm@63546 ` 1135` ``` This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and ``` wenzelm@63546 ` 1136` ``` @{term "at_right x"} and also @{term "at_right 0"}. ``` wenzelm@60758 ` 1137` ```\ ``` hoelzl@50347 ` 1138` hoelzl@51471 ` 1139` ```lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real] ``` hoelzl@50323 ` 1140` wenzelm@63546 ` 1141` ```lemma filtermap_nhds_shift: "filtermap (\x. x - d) (nhds a) = nhds (a - d)" ``` wenzelm@63546 ` 1142` ``` for a d :: "'a::real_normed_vector" ``` hoelzl@60721 ` 1143` ``` by (rule filtermap_fun_inverse[where g="\x. x + d"]) ``` wenzelm@63546 ` 1144` ``` (auto intro!: tendsto_eq_intros filterlim_ident) ``` wenzelm@63546 ` 1145` wenzelm@63546 ` 1146` ```lemma filtermap_nhds_minus: "filtermap (\x. - x) (nhds a) = nhds (- a)" ``` wenzelm@63546 ` 1147` ``` for a :: "'a::real_normed_vector" ``` hoelzl@60721 ` 1148` ``` by (rule filtermap_fun_inverse[where g=uminus]) ``` wenzelm@63546 ` 1149` ``` (auto intro!: tendsto_eq_intros filterlim_ident) ``` wenzelm@63546 ` 1150` wenzelm@63546 ` 1151` ```lemma filtermap_at_shift: "filtermap (\x. x - d) (at a) = at (a - d)" ``` wenzelm@63546 ` 1152` ``` for a d :: "'a::real_normed_vector" ``` hoelzl@51641 ` 1153` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50347 ` 1154` wenzelm@63546 ` 1155` ```lemma filtermap_at_right_shift: "filtermap (\x. x - d) (at_right a) = at_right (a - d)" ``` wenzelm@63546 ` 1156` ``` for a d :: "real" ``` hoelzl@51641 ` 1157` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50323 ` 1158` wenzelm@63546 ` 1159` ```lemma at_right_to_0: "at_right a = filtermap (\x. x + a) (at_right 0)" ``` wenzelm@63546 ` 1160` ``` for a :: real ``` hoelzl@50347 ` 1161` ``` using filtermap_at_right_shift[of "-a" 0] by simp ``` hoelzl@50347 ` 1162` hoelzl@50347 ` 1163` ```lemma filterlim_at_right_to_0: ``` wenzelm@63546 ` 1164` ``` "filterlim f F (at_right a) \ filterlim (\x. f (x + a)) F (at_right 0)" ``` wenzelm@63546 ` 1165` ``` for a :: real ``` hoelzl@50347 ` 1166` ``` unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. ``` hoelzl@50347 ` 1167` hoelzl@50347 ` 1168` ```lemma eventually_at_right_to_0: ``` wenzelm@63546 ` 1169` ``` "eventually P (at_right a) \ eventually (\x. P (x + a)) (at_right 0)" ``` wenzelm@63546 ` 1170` ``` for a :: real ``` hoelzl@50347 ` 1171` ``` unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 1172` wenzelm@63546 ` 1173` ```lemma filtermap_at_minus: "filtermap (\x. - x) (at a) = at (- a)" ``` wenzelm@63546 ` 1174` ``` for a :: "'a::real_normed_vector" ``` hoelzl@51641 ` 1175` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 1176` wenzelm@63546 ` 1177` ```lemma at_left_minus: "at_left a = filtermap (\x. - x) (at_right (- a))" ``` wenzelm@63546 ` 1178` ``` for a :: real ``` hoelzl@51641 ` 1179` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50323 ` 1180` wenzelm@63546 ` 1181` ```lemma at_right_minus: "at_right a = filtermap (\x. - x) (at_left (- a))" ``` wenzelm@63546 ` 1182` ``` for a :: real ``` hoelzl@51641 ` 1183` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 1184` hoelzl@50347 ` 1185` ```lemma filterlim_at_left_to_right: ``` wenzelm@63546 ` 1186` ``` "filterlim f F (at_left a) \ filterlim (\x. f (- x)) F (at_right (-a))" ``` wenzelm@63546 ` 1187` ``` for a :: real ``` hoelzl@50347 ` 1188` ``` unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. ``` hoelzl@50347 ` 1189` hoelzl@50347 ` 1190` ```lemma eventually_at_left_to_right: ``` wenzelm@63546 ` 1191` ``` "eventually P (at_left a) \ eventually (\x. P (- x)) (at_right (-a))" ``` wenzelm@63546 ` 1192` ``` for a :: real ``` hoelzl@50347 ` 1193` ``` unfolding at_left_minus[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 1194` hoelzl@60721 ` 1195` ```lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top" ``` hoelzl@60721 ` 1196` ``` unfolding filterlim_at_top eventually_at_bot_dense ``` hoelzl@60721 ` 1197` ``` by (metis leI minus_less_iff order_less_asym) ``` hoelzl@60721 ` 1198` hoelzl@60721 ` 1199` ```lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" ``` hoelzl@60721 ` 1200` ``` unfolding filterlim_at_bot eventually_at_top_dense ``` hoelzl@60721 ` 1201` ``` by (metis leI less_minus_iff order_less_asym) ``` hoelzl@60721 ` 1202` hoelzl@50346 ` 1203` ```lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)" ``` hoelzl@60721 ` 1204` ``` by (rule filtermap_fun_inverse[symmetric, of uminus]) ``` hoelzl@60721 ` 1205` ``` (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot) ``` hoelzl@50346 ` 1206` hoelzl@50346 ` 1207` ```lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)" ``` hoelzl@50346 ` 1208` ``` unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident) ``` hoelzl@50346 ` 1209` hoelzl@50346 ` 1210` ```lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \ (LIM x at_bot. f (-x::real) :> F)" ``` hoelzl@50346 ` 1211` ``` unfolding filterlim_def at_top_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 1212` hoelzl@50346 ` 1213` ```lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \ (LIM x at_top. f (-x::real) :> F)" ``` hoelzl@50346 ` 1214` ``` unfolding filterlim_def at_bot_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 1215` hoelzl@50346 ` 1216` ```lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \ (LIM x F. - (f x) :: real :> at_bot)" ``` hoelzl@50346 ` 1217` ``` using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] ``` wenzelm@63546 ` 1218` ``` and filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\x. - f x" F] ``` hoelzl@50346 ` 1219` ``` by auto ``` hoelzl@50346 ` 1220` hoelzl@50346 ` 1221` ```lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \ (LIM x F. - (f x) :: real :> at_top)" ``` hoelzl@50346 ` 1222` ``` unfolding filterlim_uminus_at_top by simp ``` hoelzl@50323 ` 1223` hoelzl@50347 ` 1224` ```lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" ``` hoelzl@51641 ` 1225` ``` unfolding filterlim_at_top_gt[where c=0] eventually_at_filter ``` hoelzl@50347 ` 1226` ```proof safe ``` wenzelm@63546 ` 1227` ``` fix Z :: real ``` wenzelm@63546 ` 1228` ``` assume [arith]: "0 < Z" ``` hoelzl@50347 ` 1229` ``` then have "eventually (\x. x < inverse Z) (nhds 0)" ``` hoelzl@50347 ` 1230` ``` by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\inverse Z\"]) ``` hoelzl@51641 ` 1231` ``` then show "eventually (\x. x \ 0 \ x \ {0<..} \ Z \ inverse x) (nhds 0)" ``` lp15@61810 ` 1232` ``` by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps) ``` hoelzl@50347 ` 1233` ```qed ``` hoelzl@50347 ` 1234` hoelzl@50325 ` 1235` ```lemma tendsto_inverse_0: ``` wenzelm@61076 ` 1236` ``` fixes x :: "_ \ 'a::real_normed_div_algebra" ``` wenzelm@61973 ` 1237` ``` shows "(inverse \ (0::'a)) at_infinity" ``` hoelzl@50325 ` 1238` ``` unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity ``` hoelzl@50325 ` 1239` ```proof safe ``` wenzelm@63546 ` 1240` ``` fix r :: real ``` wenzelm@63546 ` 1241` ``` assume "0 < r" ``` hoelzl@50325 ` 1242` ``` show "\b. \x. b \ norm x \ norm (inverse x :: 'a) < r" ``` hoelzl@50325 ` 1243` ``` proof (intro exI[of _ "inverse (r / 2)"] allI impI) ``` hoelzl@50325 ` 1244` ``` fix x :: 'a ``` wenzelm@60758 ` 1245` ``` from \0 < r\ have "0 < inverse (r / 2)" by simp ``` hoelzl@50325 ` 1246` ``` also assume *: "inverse (r / 2) \ norm x" ``` hoelzl@50325 ` 1247` ``` finally show "norm (inverse x) < r" ``` wenzelm@63546 ` 1248` ``` using * \0 < r\ ``` wenzelm@63546 ` 1249` ``` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) ``` hoelzl@50325 ` 1250` ``` qed ``` hoelzl@50325 ` 1251` ```qed ``` hoelzl@50325 ` 1252` eberlm@61552 ` 1253` ```lemma tendsto_add_filterlim_at_infinity: ``` wenzelm@63546 ` 1254` ``` fixes c :: "'b::real_normed_vector" ``` wenzelm@63546 ` 1255` ``` and F :: "'a filter" ``` wenzelm@63546 ` 1256` ``` assumes "(f \ c) F" ``` wenzelm@63546 ` 1257` ``` and "filterlim g at_infinity F" ``` wenzelm@63546 ` 1258` ``` shows "filterlim (\x. f x + g x) at_infinity F" ``` eberlm@61552 ` 1259` ```proof (subst filterlim_at_infinity[OF order_refl], safe) ``` wenzelm@63546 ` 1260` ``` fix r :: real ``` wenzelm@63546 ` 1261` ``` assume r: "r > 0" ``` wenzelm@63546 ` 1262` ``` from assms(1) have "((\x. norm (f x)) \ norm c) F" ``` wenzelm@63546 ` 1263` ``` by (rule tendsto_norm) ``` wenzelm@63546 ` 1264` ``` then have "eventually (\x. norm (f x) < norm c + 1) F" ``` wenzelm@63546 ` 1265` ``` by (rule order_tendstoD) simp_all ``` wenzelm@63546 ` 1266` ``` moreover from r have "r + norm c + 1 > 0" ``` wenzelm@63546 ` 1267` ``` by (intro add_pos_nonneg) simp_all ``` eberlm@61552 ` 1268` ``` with assms(2) have "eventually (\x. norm (g x) \ r + norm c + 1) F" ``` wenzelm@63546 ` 1269` ``` unfolding filterlim_at_infinity[OF order_refl] ``` wenzelm@63546 ` 1270` ``` by (elim allE[of _ "r + norm c + 1"]) simp_all ``` eberlm@61552 ` 1271` ``` ultimately show "eventually (\x. norm (f x + g x) \ r) F" ``` eberlm@61552 ` 1272` ``` proof eventually_elim ``` wenzelm@63546 ` 1273` ``` fix x :: 'a ``` wenzelm@63546 ` 1274` ``` assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 \ norm (g x)" ``` wenzelm@63546 ` 1275` ``` from A B have "r \ norm (g x) - norm (f x)" ``` wenzelm@63546 ` 1276` ``` by simp ``` wenzelm@63546 ` 1277` ``` also have "norm (g x) - norm (f x) \ norm (g x + f x)" ``` wenzelm@63546 ` 1278` ``` by (rule norm_diff_ineq) ``` wenzelm@63546 ` 1279` ``` finally show "r \ norm (f x + g x)" ``` wenzelm@63546 ` 1280` ``` by (simp add: add_ac) ``` eberlm@61552 ` 1281` ``` qed ``` eberlm@61552 ` 1282` ```qed ``` eberlm@61552 ` 1283` eberlm@61552 ` 1284` ```lemma tendsto_add_filterlim_at_infinity': ``` wenzelm@63546 ` 1285` ``` fixes c :: "'b::real_normed_vector" ``` wenzelm@63546 ` 1286` ``` and F :: "'a filter" ``` eberlm@61552 ` 1287` ``` assumes "filterlim f at_infinity F" ``` wenzelm@63546 ` 1288` ``` and "(g \ c) F" ``` wenzelm@63546 ` 1289` ``` shows "filterlim (\x. f x + g x) at_infinity F" ``` eberlm@61552 ` 1290` ``` by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+ ``` eberlm@61552 ` 1291` hoelzl@60721 ` 1292` ```lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)" ``` hoelzl@60721 ` 1293` ``` unfolding filterlim_at ``` hoelzl@60721 ` 1294` ``` by (auto simp: eventually_at_top_dense) ``` hoelzl@60721 ` 1295` ``` (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) ``` hoelzl@60721 ` 1296` hoelzl@60721 ` 1297` ```lemma filterlim_inverse_at_top: ``` wenzelm@61973 ` 1298` ``` "(f \ (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" ``` hoelzl@60721 ` 1299` ``` by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) ``` lp15@61810 ` 1300` ``` (simp add: filterlim_def eventually_filtermap eventually_mono at_within_def le_principal) ``` hoelzl@60721 ` 1301` hoelzl@60721 ` 1302` ```lemma filterlim_inverse_at_bot_neg: ``` hoelzl@60721 ` 1303` ``` "LIM x (at_left (0::real)). inverse x :> at_bot" ``` hoelzl@60721 ` 1304` ``` by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) ``` hoelzl@60721 ` 1305` hoelzl@60721 ` 1306` ```lemma filterlim_inverse_at_bot: ``` wenzelm@61973 ` 1307` ``` "(f \ (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" ``` hoelzl@60721 ` 1308` ``` unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] ``` hoelzl@60721 ` 1309` ``` by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) ``` hoelzl@60721 ` 1310` hoelzl@50347 ` 1311` ```lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" ``` hoelzl@60721 ` 1312` ``` by (intro filtermap_fun_inverse[symmetric, where g=inverse]) ``` hoelzl@60721 ` 1313` ``` (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top) ``` hoelzl@50347 ` 1314` hoelzl@50347 ` 1315` ```lemma eventually_at_right_to_top: ``` hoelzl@50347 ` 1316` ``` "eventually P (at_right (0::real)) \ eventually (\x. P (inverse x)) at_top" ``` hoelzl@50347 ` 1317` ``` unfolding at_right_to_top eventually_filtermap .. ``` hoelzl@50347 ` 1318` hoelzl@50347 ` 1319` ```lemma filterlim_at_right_to_top: ``` hoelzl@50347 ` 1320` ``` "filterlim f F (at_right (0::real)) \ (LIM x at_top. f (inverse x) :> F)" ``` hoelzl@50347 ` 1321` ``` unfolding filterlim_def at_right_to_top filtermap_filtermap .. ``` hoelzl@50347 ` 1322` hoelzl@50347 ` 1323` ```lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" ``` hoelzl@50347 ` 1324` ``` unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. ``` hoelzl@50347 ` 1325` hoelzl@50347 ` 1326` ```lemma eventually_at_top_to_right: ``` hoelzl@50347 ` 1327` ``` "eventually P at_top \ eventually (\x. P (inverse x)) (at_right (0::real))" ``` hoelzl@50347 ` 1328` ``` unfolding at_top_to_right eventually_filtermap .. ``` hoelzl@50347 ` 1329` hoelzl@50347 ` 1330` ```lemma filterlim_at_top_to_right: ``` hoelzl@50347 ` 1331` ``` "filterlim f F at_top \ (LIM x (at_right (0::real)). f (inverse x) :> F)" ``` hoelzl@50347 ` 1332` ``` unfolding filterlim_def at_top_to_right filtermap_filtermap .. ``` hoelzl@50347 ` 1333` hoelzl@50325 ` 1334` ```lemma filterlim_inverse_at_infinity: ``` wenzelm@61076 ` 1335` ``` fixes x :: "_ \ 'a::{real_normed_div_algebra, division_ring}" ``` hoelzl@50325 ` 1336` ``` shows "filterlim inverse at_infinity (at (0::'a))" ``` hoelzl@50325 ` 1337` ``` unfolding filterlim_at_infinity[OF order_refl] ``` hoelzl@50325 ` 1338` ```proof safe ``` wenzelm@63546 ` 1339` ``` fix r :: real ``` wenzelm@63546 ` 1340` ``` assume "0 < r" ``` hoelzl@50325 ` 1341` ``` then show "eventually (\x::'a. r \ norm (inverse x)) (at 0)" ``` hoelzl@50325 ` 1342` ``` unfolding eventually_at norm_inverse ``` hoelzl@50325 ` 1343` ``` by (intro exI[of _ "inverse r"]) ``` hoelzl@50325 ` 1344` ``` (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) ``` hoelzl@50325 ` 1345` ```qed ``` hoelzl@50325 ` 1346` hoelzl@50325 ` 1347` ```lemma filterlim_inverse_at_iff: ``` wenzelm@61076 ` 1348` ``` fixes g :: "'a \ 'b::{real_normed_div_algebra, division_ring}" ``` hoelzl@50325 ` 1349` ``` shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" ``` hoelzl@50325 ` 1350` ``` unfolding filterlim_def filtermap_filtermap[symmetric] ``` hoelzl@50325 ` 1351` ```proof ``` hoelzl@50325 ` 1352` ``` assume "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1353` ``` then have "filtermap inverse (filtermap g F) \ filtermap inverse at_infinity" ``` hoelzl@50325 ` 1354` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1355` ``` also have "\ \ at 0" ``` hoelzl@51641 ` 1356` ``` using tendsto_inverse_0[where 'a='b] ``` hoelzl@51641 ` 1357` ``` by (auto intro!: exI[of _ 1] ``` wenzelm@63546 ` 1358` ``` simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity) ``` hoelzl@50325 ` 1359` ``` finally show "filtermap inverse (filtermap g F) \ at 0" . ``` hoelzl@50325 ` 1360` ```next ``` hoelzl@50325 ` 1361` ``` assume "filtermap inverse (filtermap g F) \ at 0" ``` hoelzl@50325 ` 1362` ``` then have "filtermap inverse (filtermap inverse (filtermap g F)) \ filtermap inverse (at 0)" ``` hoelzl@50325 ` 1363` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1364` ``` with filterlim_inverse_at_infinity show "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1365` ``` by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) ``` hoelzl@50325 ` 1366` ```qed ``` hoelzl@50325 ` 1367` eberlm@61531 ` 1368` ```lemma tendsto_mult_filterlim_at_infinity: ``` wenzelm@63546 ` 1369` ``` fixes c :: "'a::real_normed_field" ``` lp15@64394 ` 1370` ``` assumes "(f \ c) F" "c \ 0" ``` eberlm@61531 ` 1371` ``` assumes "filterlim g at_infinity F" ``` wenzelm@63546 ` 1372` ``` shows "filterlim (\x. f x * g x) at_infinity F" ``` eberlm@61531 ` 1373` ```proof - ``` wenzelm@61973 ` 1374` ``` have "((\x. inverse (f x) * inverse (g x)) \ inverse c * 0) F" ``` eberlm@61531 ` 1375` ``` by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0]) ``` wenzelm@63546 ` 1376` ``` then have "filterlim (\x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F" ``` wenzelm@63546 ` 1377` ``` unfolding filterlim_at ``` wenzelm@63546 ` 1378` ``` using assms ``` eberlm@61531 ` 1379` ``` by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj) ``` wenzelm@63546 ` 1380` ``` then show ?thesis ``` wenzelm@63546 ` 1381` ``` by (subst filterlim_inverse_at_iff[symmetric]) simp_all ``` lp15@64394 ` 1382` ```qed ``` eberlm@61531 ` 1383` wenzelm@61973 ` 1384` ```lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) \ 0) F" ``` hoelzl@51641 ` 1385` ``` by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) ``` hoelzl@50419 ` 1386` immler@63556 ` 1387` ```lemma real_tendsto_divide_at_top: ``` immler@63556 ` 1388` ``` fixes c::"real" ``` immler@63556 ` 1389` ``` assumes "(f \ c) F" ``` immler@63556 ` 1390` ``` assumes "filterlim g at_top F" ``` immler@63556 ` 1391` ``` shows "((\x. f x / g x) \ 0) F" ``` immler@63556 ` 1392` ``` by (auto simp: divide_inverse_commute ``` immler@63556 ` 1393` ``` intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms) ``` immler@63556 ` 1394` wenzelm@63546 ` 1395` ```lemma mult_nat_left_at_top: "c > 0 \ filterlim (\x. c * x) at_top sequentially" ``` wenzelm@63546 ` 1396` ``` for c :: nat ``` eberlm@61531 ` 1397` ``` by (rule filterlim_subseq) (auto simp: subseq_def) ``` lp15@59613 ` 1398` wenzelm@63546 ` 1399` ```lemma mult_nat_right_at_top: "c > 0 \ filterlim (\x. x * c) at_top sequentially" ``` wenzelm@63546 ` 1400` ``` for c :: nat ``` wenzelm@63546 ` 1401` ``` by (rule filterlim_subseq) (auto simp: subseq_def) ``` wenzelm@63546 ` 1402` wenzelm@63546 ` 1403` ```lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity" ``` lp15@59613 ` 1404` ```proof (rule antisym) ``` wenzelm@61973 ` 1405` ``` have "(inverse \ (0::'a)) at_infinity" ``` lp15@59613 ` 1406` ``` by (fact tendsto_inverse_0) ``` lp15@59613 ` 1407` ``` then show "filtermap inverse at_infinity \ at (0::'a)" ``` lp15@59613 ` 1408` ``` apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def) ``` wenzelm@63546 ` 1409` ``` apply (rule_tac x="1" in exI) ``` wenzelm@63546 ` 1410` ``` apply auto ``` lp15@59613 ` 1411` ``` done ``` lp15@59613 ` 1412` ```next ``` lp15@59613 ` 1413` ``` have "filtermap inverse (filtermap inverse (at (0::'a))) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1414` ``` using filterlim_inverse_at_infinity unfolding filterlim_def ``` lp15@59613 ` 1415` ``` by (rule filtermap_mono) ``` lp15@59613 ` 1416` ``` then show "at (0::'a) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1417` ``` by (simp add: filtermap_ident filtermap_filtermap) ``` lp15@59613 ` 1418` ```qed ``` lp15@59613 ` 1419` lp15@59613 ` 1420` ```lemma lim_at_infinity_0: ``` wenzelm@63546 ` 1421` ``` fixes l :: "'a::{real_normed_field,field}" ``` wenzelm@63546 ` 1422` ``` shows "(f \ l) at_infinity \ ((f \ inverse) \ l) (at (0::'a))" ``` wenzelm@63546 ` 1423` ``` by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) ``` lp15@59613 ` 1424` lp15@59613 ` 1425` ```lemma lim_zero_infinity: ``` wenzelm@63546 ` 1426` ``` fixes l :: "'a::{real_normed_field,field}" ``` wenzelm@61973 ` 1427` ``` shows "((\x. f(1 / x)) \ l) (at (0::'a)) \ (f \ l) at_infinity" ``` wenzelm@63546 ` 1428` ``` by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) ``` lp15@59613 ` 1429` lp15@59613 ` 1430` wenzelm@60758 ` 1431` ```text \ ``` wenzelm@63546 ` 1432` ``` We only show rules for multiplication and addition when the functions are either against a real ``` wenzelm@63546 ` 1433` ``` value or against infinity. Further rules are easy to derive by using @{thm ``` wenzelm@63546 ` 1434` ``` filterlim_uminus_at_top}. ``` wenzelm@60758 ` 1435` ```\ ``` hoelzl@50324 ` 1436` lp15@60141 ` 1437` ```lemma filterlim_tendsto_pos_mult_at_top: ``` wenzelm@63546 ` 1438` ``` assumes f: "(f \ c) F" ``` wenzelm@63546 ` 1439` ``` and c: "0 < c" ``` wenzelm@63546 ` 1440` ``` and g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1441` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1442` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1443` ```proof safe ``` wenzelm@63546 ` 1444` ``` fix Z :: real ``` wenzelm@63546 ` 1445` ``` assume "0 < Z" ``` wenzelm@60758 ` 1446` ``` from f \0 < c\ have "eventually (\x. c / 2 < f x) F" ``` lp15@61810 ` 1447` ``` by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_mono ``` wenzelm@63546 ` 1448` ``` simp: dist_real_def abs_real_def split: if_split_asm) ``` hoelzl@50346 ` 1449` ``` moreover from g have "eventually (\x. (Z / c * 2) \ g x) F" ``` hoelzl@50324 ` 1450` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1451` ``` ultimately show "eventually (\x. Z \ f x * g x) F" ``` hoelzl@50324 ` 1452` ``` proof eventually_elim ``` wenzelm@63546 ` 1453` ``` case (elim x) ``` wenzelm@60758 ` 1454` ``` with \0 < Z\ \0 < c\ have "c / 2 * (Z / c * 2) \ f x * g x" ``` hoelzl@50346 ` 1455` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` wenzelm@60758 ` 1456` ``` with \0 < c\ show "Z \ f x * g x" ``` hoelzl@50324 ` 1457` ``` by simp ``` hoelzl@50324 ` 1458` ``` qed ``` hoelzl@50324 ` 1459` ```qed ``` hoelzl@50324 ` 1460` lp15@60141 ` 1461` ```lemma filterlim_at_top_mult_at_top: ``` hoelzl@50324 ` 1462` ``` assumes f: "LIM x F. f x :> at_top" ``` wenzelm@63546 ` 1463` ``` and g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1464` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1465` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1466` ```proof safe ``` wenzelm@63546 ` 1467` ``` fix Z :: real ``` wenzelm@63546 ` 1468` ``` assume "0 < Z" ``` hoelzl@50346 ` 1469` ``` from f have "eventually (\x. 1 \ f x) F" ``` hoelzl@50324 ` 1470` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1471` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1472` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1473` ``` ultimately show "eventually (\x. Z \ f x * g x) F" ``` hoelzl@50324 ` 1474` ``` proof eventually_elim ``` wenzelm@63546 ` 1475` ``` case (elim x) ``` wenzelm@60758 ` 1476` ``` with \0 < Z\ have "1 * Z \ f x * g x" ``` hoelzl@50346 ` 1477` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` hoelzl@50346 ` 1478` ``` then show "Z \ f x * g x" ``` hoelzl@50324 ` 1479` ``` by simp ``` hoelzl@50324 ` 1480` ``` qed ``` hoelzl@50324 ` 1481` ```qed ``` hoelzl@50324 ` 1482` immler@63556 ` 1483` ```lemma filterlim_at_top_mult_tendsto_pos: ``` immler@63556 ` 1484` ``` assumes f: "(f \ c) F" ``` immler@63556 ` 1485` ``` and c: "0 < c" ``` immler@63556 ` 1486` ``` and g: "LIM x F. g x :> at_top" ``` immler@63556 ` 1487` ``` shows "LIM x F. (g x * f x:: real) :> at_top" ``` immler@63556 ` 1488` ``` by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g) ``` immler@63556 ` 1489` hoelzl@50419 ` 1490` ```lemma filterlim_tendsto_pos_mult_at_bot: ``` wenzelm@63546 ` 1491` ``` fixes c :: real ``` wenzelm@63546 ` 1492` ``` assumes "(f \ c) F" "0 < c" "filterlim g at_bot F" ``` hoelzl@50419 ` 1493` ``` shows "LIM x F. f x * g x :> at_bot" ``` hoelzl@50419 ` 1494` ``` using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) ``` hoelzl@50419 ` 1495` ``` unfolding filterlim_uminus_at_bot by simp ``` hoelzl@50419 ` 1496` hoelzl@60182 ` 1497` ```lemma filterlim_tendsto_neg_mult_at_bot: ``` wenzelm@63546 ` 1498` ``` fixes c :: real ``` wenzelm@63546 ` 1499` ``` assumes c: "(f \ c) F" "c < 0" and g: "filterlim g at_top F" ``` hoelzl@60182 ` 1500` ``` shows "LIM x F. f x * g x :> at_bot" ``` hoelzl@60182 ` 1501` ``` using c filterlim_tendsto_pos_mult_at_top[of "\x. - f x" "- c" F, OF _ _ g] ``` hoelzl@60182 ` 1502` ``` unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp ``` hoelzl@60182 ` 1503` hoelzl@56330 ` 1504` ```lemma filterlim_pow_at_top: ``` eberlm@63721 ` 1505` ``` fixes f :: "'a \ real" ``` wenzelm@63546 ` 1506` ``` assumes "0 < n" ``` wenzelm@63546 ` 1507` ``` and f: "LIM x F. f x :> at_top" ``` hoelzl@56330 ` 1508` ``` shows "LIM x F. (f x)^n :: real :> at_top" ``` wenzelm@63546 ` 1509` ``` using \0 < n\ ``` wenzelm@63546 ` 1510` ```proof (induct n) ``` wenzelm@63546 ` 1511` ``` case 0 ``` wenzelm@63546 ` 1512` ``` then show ?case by simp ``` wenzelm@63546 ` 1513` ```next ``` hoelzl@56330 ` 1514` ``` case (Suc n) with f show ?case ``` hoelzl@56330 ` 1515` ``` by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) ``` wenzelm@63546 ` 1516` ```qed ``` hoelzl@56330 ` 1517` hoelzl@56330 ` 1518` ```lemma filterlim_pow_at_bot_even: ``` hoelzl@56330 ` 1519` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1520` ``` shows "0 < n \ LIM x F. f x :> at_bot \ even n \ LIM x F. (f x)^n :> at_top" ``` hoelzl@56330 ` 1521` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_top) ``` hoelzl@56330 ` 1522` hoelzl@56330 ` 1523` ```lemma filterlim_pow_at_bot_odd: ``` hoelzl@56330 ` 1524` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1525` ``` shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" ``` hoelzl@56330 ` 1526` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) ``` hoelzl@56330 ` 1527` lp15@60141 ` 1528` ```lemma filterlim_tendsto_add_at_top: ``` wenzelm@61973 ` 1529` ``` assumes f: "(f \ c) F" ``` wenzelm@63546 ` 1530` ``` and g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1531` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1532` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1533` ```proof safe ``` wenzelm@63546 ` 1534` ``` fix Z :: real ``` wenzelm@63546 ` 1535` ``` assume "0 < Z" ``` hoelzl@50324 ` 1536` ``` from f have "eventually (\x. c - 1 < f x) F" ``` lp15@61810 ` 1537` ``` by (auto dest!: tendstoD[where e=1] elim!: eventually_mono simp: dist_real_def) ``` hoelzl@50346 ` 1538` ``` moreover from g have "eventually (\x. Z - (c - 1) \ g x) F" ``` hoelzl@50324 ` 1539` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1540` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1541` ``` by eventually_elim simp ``` hoelzl@50324 ` 1542` ```qed ``` hoelzl@50324 ` 1543` hoelzl@50347 ` 1544` ```lemma LIM_at_top_divide: ``` hoelzl@50347 ` 1545` ``` fixes f g :: "'a \ real" ``` wenzelm@61973 ` 1546` ``` assumes f: "(f \ a) F" "0 < a" ``` wenzelm@63546 ` 1547` ``` and g: "(g \ 0) F" "eventually (\x. 0 < g x) F" ``` hoelzl@50347 ` 1548` ``` shows "LIM x F. f x / g x :> at_top" ``` hoelzl@50347 ` 1549` ``` unfolding divide_inverse ``` hoelzl@50347 ` 1550` ``` by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) ``` hoelzl@50347 ` 1551` lp15@60141 ` 1552` ```lemma filterlim_at_top_add_at_top: ``` hoelzl@50324 ` 1553` ``` assumes f: "LIM x F. f x :> at_top" ``` wenzelm@63546 ` 1554` ``` and g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1555` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1556` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1557` ```proof safe ``` wenzelm@63546 ` 1558` ``` fix Z :: real ``` wenzelm@63546 ` 1559` ``` assume "0 < Z" ``` hoelzl@50346 ` 1560` ``` from f have "eventually (\x. 0 \ f x) F" ``` hoelzl@50324 ` 1561` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1562` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1563` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1564` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1565` ``` by eventually_elim simp ``` hoelzl@50324 ` 1566` ```qed ``` hoelzl@50324 ` 1567` hoelzl@50331 ` 1568` ```lemma tendsto_divide_0: ``` wenzelm@61076 ` 1569` ``` fixes f :: "_ \ 'a::{real_normed_div_algebra, division_ring}" ``` wenzelm@61973 ` 1570` ``` assumes f: "(f \ c) F" ``` wenzelm@63546 ` 1571` ``` and g: "LIM x F. g x :> at_infinity" ``` wenzelm@61973 ` 1572` ``` shows "((\x. f x / g x) \ 0) F" ``` wenzelm@63546 ` 1573` ``` using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] ``` wenzelm@63546 ` 1574` ``` by (simp add: divide_inverse) ``` hoelzl@50331 ` 1575` hoelzl@50331 ` 1576` ```lemma linear_plus_1_le_power: ``` hoelzl@50331 ` 1577` ``` fixes x :: real ``` hoelzl@50331 ` 1578` ``` assumes x: "0 \ x" ``` hoelzl@50331 ` 1579` ``` shows "real n * x + 1 \ (x + 1) ^ n" ``` hoelzl@50331 ` 1580` ```proof (induct n) ``` wenzelm@63546 ` 1581` ``` case 0 ``` wenzelm@63546 ` 1582` ``` then show ?case by simp ``` wenzelm@63546 ` 1583` ```next ``` hoelzl@50331 ` 1584` ``` case (Suc n) ``` wenzelm@63546 ` 1585` ``` from x have "real (Suc n) * x + 1 \ (x + 1) * (real n * x + 1)" ``` wenzelm@63546 ` 1586` ``` by (simp add: field_simps) ``` hoelzl@50331 ` 1587` ``` also have "\ \ (x + 1)^Suc n" ``` hoelzl@50331 ` 1588` ``` using Suc x by (simp add: mult_left_mono) ``` hoelzl@50331 ` 1589` ``` finally show ?case . ``` wenzelm@63546 ` 1590` ```qed ``` hoelzl@50331 ` 1591` hoelzl@50331 ` 1592` ```lemma filterlim_realpow_sequentially_gt1: ``` hoelzl@50331 ` 1593` ``` fixes x :: "'a :: real_normed_div_algebra" ``` hoelzl@50331 ` 1594` ``` assumes x[arith]: "1 < norm x" ``` hoelzl@50331 ` 1595` ``` shows "LIM n sequentially. x ^ n :> at_infinity" ``` hoelzl@50331 ` 1596` ```proof (intro filterlim_at_infinity[THEN iffD2] allI impI) ``` wenzelm@63546 ` 1597` ``` fix y :: real ``` wenzelm@63546 ` 1598` ``` assume "0 < y" ``` hoelzl@50331 ` 1599` ``` have "0 < norm x - 1" by simp ``` wenzelm@63546 ` 1600` ``` then obtain N :: nat where "y < real N * (norm x - 1)" ``` wenzelm@63546 ` 1601` ``` by (blast dest: reals_Archimedean3) ``` wenzelm@63546 ` 1602` ``` also have "\ \ real N * (norm x - 1) + 1" ``` wenzelm@63546 ` 1603` ``` by simp ``` wenzelm@63546 ` 1604` ``` also have "\ \ (norm x - 1 + 1) ^ N" ``` wenzelm@63546 ` 1605` ``` by (rule linear_plus_1_le_power) simp ``` wenzelm@63546 ` 1606` ``` also have "\ = norm x ^ N" ``` wenzelm@63546 ` 1607` ``` by simp ``` hoelzl@50331 ` 1608` ``` finally have "\n\N. y \ norm x ^ n" ``` hoelzl@50331 ` 1609` ``` by (metis order_less_le_trans power_increasing order_less_imp_le x) ``` hoelzl@50331 ` 1610` ``` then show "eventually (\n. y \ norm (x ^ n)) sequentially" ``` hoelzl@50331 ` 1611` ``` unfolding eventually_sequentially ``` hoelzl@50331 ` 1612` ``` by (auto simp: norm_power) ``` hoelzl@50331 ` 1613` ```qed simp ``` hoelzl@50331 ` 1614` hoelzl@51471 ` 1615` immler@63263 ` 1616` ```subsection \Floor and Ceiling\ ``` immler@63263 ` 1617` immler@63263 ` 1618` ```lemma eventually_floor_less: ``` wenzelm@63546 ` 1619` ``` fixes f :: "'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1620` ``` assumes f: "(f \ l) F" ``` wenzelm@63546 ` 1621` ``` and l: "l \ \" ``` immler@63263 ` 1622` ``` shows "\\<^sub>F x in F. of_int (floor l) < f x" ``` immler@63263 ` 1623` ``` by (intro order_tendstoD[OF f]) (metis Ints_of_int antisym_conv2 floor_correct l) ``` immler@63263 ` 1624` immler@63263 ` 1625` ```lemma eventually_less_ceiling: ``` wenzelm@63546 ` 1626` ``` fixes f :: "'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1627` ``` assumes f: "(f \ l) F" ``` wenzelm@63546 ` 1628` ``` and l: "l \ \" ``` immler@63263 ` 1629` ``` shows "\\<^sub>F x in F. f x < of_int (ceiling l)" ``` immler@63263 ` 1630` ``` by (intro order_tendstoD[OF f]) (metis Ints_of_int l le_of_int_ceiling less_le) ``` immler@63263 ` 1631` immler@63263 ` 1632` ```lemma eventually_floor_eq: ``` wenzelm@63546 ` 1633` ``` fixes f::"'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1634` ``` assumes f: "(f \ l) F" ``` wenzelm@63546 ` 1635` ``` and l: "l \ \" ``` immler@63263 ` 1636` ``` shows "\\<^sub>F x in F. floor (f x) = floor l" ``` immler@63263 ` 1637` ``` using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms] ``` immler@63263 ` 1638` ``` by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq) ``` immler@63263 ` 1639` immler@63263 ` 1640` ```lemma eventually_ceiling_eq: ``` wenzelm@63546 ` 1641` ``` fixes f::"'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1642` ``` assumes f: "(f \ l) F" ``` wenzelm@63546 ` 1643` ``` and l: "l \ \" ``` immler@63263 ` 1644` ``` shows "\\<^sub>F x in F. ceiling (f x) = ceiling l" ``` immler@63263 ` 1645` ``` using eventually_floor_less[OF assms] eventually_less_ceiling[OF assms] ``` immler@63263 ` 1646` ``` by eventually_elim (meson floor_less_iff less_ceiling_iff not_less_iff_gr_or_eq) ``` immler@63263 ` 1647` immler@63263 ` 1648` ```lemma tendsto_of_int_floor: ``` wenzelm@63546 ` 1649` ``` fixes f::"'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1650` ``` assumes "(f \ l) F" ``` wenzelm@63546 ` 1651` ``` and "l \ \" ``` wenzelm@63546 ` 1652` ``` shows "((\x. of_int (floor (f x)) :: 'c::{ring_1,topological_space}) \ of_int (floor l)) F" ``` immler@63263 ` 1653` ``` using eventually_floor_eq[OF assms] ``` immler@63263 ` 1654` ``` by (simp add: eventually_mono topological_tendstoI) ``` immler@63263 ` 1655` immler@63263 ` 1656` ```lemma tendsto_of_int_ceiling: ``` wenzelm@63546 ` 1657` ``` fixes f::"'a \ 'b::{order_topology,floor_ceiling}" ``` immler@63263 ` 1658` ``` assumes "(f \ l) F" ``` wenzelm@63546 ` 1659` ``` and "l \ \" ``` wenzelm@63546 ` 1660` ``` shows "((\x. of_int (ceiling (f x)):: 'c::{ring_1,topological_space}) \ of_int (ceiling l)) F" ``` immler@63263 ` 1661` ``` using eventually_ceiling_eq[OF assms] ``` immler@63263 ` 1662` ``` by (simp add: eventually_mono topological_tendstoI) ``` immler@63263 ` 1663` immler@63263 ` 1664` ```lemma continuous_on_of_int_floor: ``` immler@63263 ` 1665` ``` "continuous_on (UNIV - \::'a::{order_topology, floor_ceiling} set) ``` immler@63263 ` 1666` ``` (\x. of_int (floor x)::'b::{ring_1, topological_space})" ``` immler@63263 ` 1667` ``` unfolding continuous_on_def ``` immler@63263 ` 1668` ``` by (auto intro!: tendsto_of_int_floor) ``` immler@63263 ` 1669` immler@63263 ` 1670` ```lemma continuous_on_of_int_ceiling: ``` immler@63263 ` 1671` ``` "continuous_on (UNIV - \::'a::{order_topology, floor_ceiling} set) ``` immler@63263 ` 1672` ``` (\x. of_int (ceiling x)::'b::{ring_1, topological_space})" ``` immler@63263 ` 1673` ``` unfolding continuous_on_def ``` immler@63263 ` 1674` ``` by (auto intro!: tendsto_of_int_ceiling) ``` immler@63263 ` 1675` immler@63263 ` 1676` wenzelm@60758 ` 1677` ```subsection \Limits of Sequences\ ``` hoelzl@51526 ` 1678` hoelzl@62368 ` 1679` ```lemma [trans]: "X = Y \ Y \ z \ X \ z" ``` hoelzl@51526 ` 1680` ``` by simp ``` hoelzl@51526 ` 1681` hoelzl@51526 ` 1682` ```lemma LIMSEQ_iff: ``` hoelzl@51526 ` 1683` ``` fixes L :: "'a::real_normed_vector" ``` wenzelm@61969 ` 1684` ``` shows "(X \ L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" ``` lp15@60017 ` 1685` ```unfolding lim_sequentially dist_norm .. ``` hoelzl@51526 ` 1686` wenzelm@63546 ` 1687` ```lemma LIMSEQ_I: "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X \ L" ``` wenzelm@63546 ` 1688` ``` for L :: "'a::real_normed_vector" ``` wenzelm@63546 ` 1689` ``` by (simp add: LIMSEQ_iff) ``` wenzelm@63546 ` 1690` wenzelm@63546 ` 1691` ```lemma LIMSEQ_D: "X \ L \ 0 < r \ \no. \n\no. norm (X n - L) < r" ``` wenzelm@63546 ` 1692` ``` for L :: "'a::real_normed_vector" ``` wenzelm@63546 ` 1693` ``` by (simp add: LIMSEQ_iff) ``` wenzelm@63546 ` 1694` wenzelm@63546 ` 1695` ```lemma LIMSEQ_linear: "X \ x \ l > 0 \ (\ n. X (n * l)) \ x" ``` hoelzl@51526 ` 1696` ``` unfolding tendsto_def eventually_sequentially ``` haftmann@57512 ` 1697` ``` by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) ``` hoelzl@51526 ` 1698` lp15@65036 ` 1699` ```lemma norm_inverse_le_norm: "r \ norm x \ 0 < r \ norm (inverse x) \ inverse r" ``` wenzelm@63546 ` 1700` ``` for x :: "'a::real_normed_div_algebra" ``` wenzelm@63546 ` 1701` ``` apply (subst nonzero_norm_inverse, clarsimp) ``` wenzelm@63546 ` 1702` ``` apply (erule (1) le_imp_inverse_le) ``` wenzelm@63546 ` 1703` ``` done ``` wenzelm@63546 ` 1704` wenzelm@63546 ` 1705` ```lemma Bseq_inverse: "X \ a \ a \ 0 \ Bseq (\n. inverse (X n))" ``` wenzelm@63546 ` 1706` ``` for a :: "'a::real_normed_div_algebra" ``` hoelzl@51526 ` 1707` ``` by (rule Bfun_inverse) ``` hoelzl@51526 ` 1708` wenzelm@63546 ` 1709` wenzelm@63546 ` 1710` ```text \Transformation of limit.\ ``` wenzelm@63546 ` 1711` wenzelm@63546 ` 1712` ```lemma Lim_transform: "(g \ a) F \ ((\x. f x - g x) \ 0) F \ (f \ a) F" ``` wenzelm@63546 ` 1713` ``` for a b :: "'a::real_normed_vector" ``` lp15@60141 ` 1714` ``` using tendsto_add [of g a F "\x. f x - g x" 0] by simp ``` lp15@60141 ` 1715` wenzelm@63546 ` 1716` ```lemma Lim_transform2: "(f \ a) F \ ((\x. f x - g x) \ 0) F \ (g \ a) F" ``` wenzelm@63546 ` 1717` ``` for a b :: "'a::real_normed_vector" ``` lp15@60141 ` 1718` ``` by (erule Lim_transform) (simp add: tendsto_minus_cancel) ``` lp15@60141 ` 1719` wenzelm@63546 ` 1720` ```proposition Lim_transform_eq: "((\x. f x - g x) \ 0) F \ (f \ a) F \ (g \ a) F" ``` wenzelm@63546 ` 1721` ``` for a :: "'a::real_normed_vector" ``` wenzelm@63546 ` 1722` ``` using Lim_transform Lim_transform2 by blast ``` lp15@62379 ` 1723` lp15@60141 ` 1724` ```lemma Lim_transform_eventually: ``` wenzelm@61973 ` 1725` ``` "eventually (\x. f x = g x) net \ (f \ l) net \ (g \ l) net" ``` lp15@60141 ` 1726` ``` apply (rule topological_tendstoI) ``` lp15@60141 ` 1727` ``` apply (drule (2) topological_tendstoD) ``` wenzelm@63546 ` 1728` ``` apply (erule (1) eventually_elim2) ``` wenzelm@63546 ` 1729` ``` apply simp ``` lp15@60141 ` 1730` ``` done ``` lp15@60141 ` 1731` lp15@60141 ` 1732` ```lemma Lim_transform_within: ``` paulson@62087 ` 1733` ``` assumes "(f \ l) (at x within S)" ``` paulson@62087 ` 1734` ``` and "0 < d" ``` wenzelm@63546 ` 1735` ``` and "\x'. x'\S \ 0 < dist x' x \ dist x' x < d \ f x' = g x'" ``` wenzelm@61973 ` 1736` ``` shows "(g \ l) (at x within S)" ``` lp15@60141 ` 1737` ```proof (rule Lim_transform_eventually) ``` lp15@60141 ` 1738` ``` show "eventually (\x. f x = g x) (at x within S)" ``` paulson@62087 ` 1739` ``` using assms by (auto simp: eventually_at) ``` wenzelm@63546 ` 1740` ``` show "(f \ l) (at x within S)" ``` wenzelm@63546 ` 1741` ``` by fact ``` lp15@60141 ` 1742` ```qed ``` lp15@60141 ` 1743` wenzelm@63546 ` 1744` ```text \Common case assuming being away from some crucial point like 0.\ ``` lp15@60141 ` 1745` ```lemma Lim_transform_away_within: ``` lp15@60141 ` 1746` ``` fixes a b :: "'a::t1_space" ``` lp15@60141 ` 1747` ``` assumes "a \ b" ``` lp15@60141 ` 1748` ``` and "\x\S. x \ a \ x \ b \ f x = g x" ``` wenzelm@61973 ` 1749` ``` and "(f \ l) (at a within S)" ``` wenzelm@61973 ` 1750` ``` shows "(g \ l) (at a within S)" ``` lp15@60141 ` 1751` ```proof (rule Lim_transform_eventually) ``` wenzelm@63546 ` 1752` ``` show "(f \ l) (at a within S)" ``` wenzelm@63546 ` 1753` ``` by fact ``` lp15@60141 ` 1754` ``` show "eventually (\x. f x = g x) (at a within S)" ``` lp15@60141 ` 1755` ``` unfolding eventually_at_topological ``` wenzelm@63546 ` 1756` ``` by (rule exI [where x="- {b}"]) (simp add: open_Compl assms) ``` lp15@60141 ` 1757` ```qed ``` lp15@60141 ` 1758` lp15@60141 ` 1759` ```lemma Lim_transform_away_at: ``` lp15@60141 ` 1760` ``` fixes a b :: "'a::t1_space" ``` wenzelm@63546 ` 1761` ``` assumes ab: "a \ b" ``` lp15@60141 ` 1762` ``` and fg: "\x. x \ a \ x \ b \ f x = g x" ``` wenzelm@61973 ` 1763` ``` and fl: "(f \ l) (at a)" ``` wenzelm@61973 ` 1764` ``` shows "(g \ l) (at a)" ``` lp15@60141 ` 1765` ``` using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp ``` lp15@60141 ` 1766` wenzelm@63546 ` 1767` ```text \Alternatively, within an open set.\ ``` lp15@60141 ` 1768` ```lemma Lim_transform_within_open: ``` paulson@62087 ` 1769` ``` assumes "(f \ l) (at a within T)" ``` paulson@62087 ` 1770` ``` and "open s" and "a \ s" ``` wenzelm@63546 ` 1771` ``` and "\x. x\s \ x \ a \ f x = g x" ``` paulson@62087 ` 1772` ``` shows "(g \ l) (at a within T)" ``` lp15@60141 ` 1773` ```proof (rule Lim_transform_eventually) ``` paulson@62087 ` 1774` ``` show "eventually (\x. f x = g x) (at a within T)" ``` lp15@60141 ` 1775` ``` unfolding eventually_at_topological ``` paulson@62087 ` 1776` ``` using assms by auto ``` paulson@62087 ` 1777` ``` show "(f \ l) (at a within T)" by fact ``` lp15@60141 ` 1778` ```qed ``` lp15@60141 ` 1779` wenzelm@63546 ` 1780` wenzelm@63546 ` 1781` ```text \A congruence rule allowing us to transform limits assuming not at point.\ ``` lp15@60141 ` 1782` lp15@60141 ` 1783` ```(* FIXME: Only one congruence rule for tendsto can be used at a time! *) ``` lp15@60141 ` 1784` lp15@60141 ` 1785` ```lemma Lim_cong_within(*[cong add]*): ``` lp15@60141 ` 1786` ``` assumes "a = b" ``` lp15@60141 ` 1787` ``` and "x = y" ``` lp15@60141 ` 1788` ``` and "S = T" ``` lp15@60141 ` 1789` ``` and "\x. x \ b \ x \ T \ f x = g x" ``` wenzelm@61973 ` 1790` ``` shows "(f \ x) (at a within S) \ (g \ y) (at b within T)" ``` lp15@60141 ` 1791` ``` unfolding tendsto_def eventually_at_topological ``` lp15@60141 ` 1792` ``` using assms by simp ``` lp15@60141 ` 1793` lp15@60141 ` 1794` ```lemma Lim_cong_at(*[cong add]*): ``` lp15@60141 ` 1795` ``` assumes "a = b" "x = y" ``` lp15@60141 ` 1796` ``` and "\x. x \ a \ f x = g x" ``` wenzelm@61973 ` 1797` ``` shows "((\x. f x) \ x) (at a) \ ((g \ y) (at a))" ``` lp15@60141 ` 1798` ``` unfolding tendsto_def eventually_at_topological ``` lp15@60141 ` 1799` ``` using assms by simp ``` wenzelm@63546 ` 1800` wenzelm@63546 ` 1801` ```text \An unbounded sequence's inverse tends to 0.\ ``` lp15@65578 ` 1802` ```lemma LIMSEQ_inverse_zero: ``` lp15@65578 ` 1803` ``` assumes "\r::real. \N. \n\N. r < X n" ``` lp15@65578 ` 1804` ``` shows "(\n. inverse (X n)) \ 0" ``` hoelzl@51526 ` 1805` ``` apply (rule filterlim_compose[OF tendsto_inverse_0]) ``` hoelzl@51526 ` 1806` ``` apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) ``` lp15@65578 ` 1807` ``` apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le) ``` hoelzl@51526 ` 1808` ``` done ``` hoelzl@51526 ` 1809` wenzelm@63546 ` 1810` ```text \The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\ ``` wenzelm@63546 ` 1811` ```lemma LIMSEQ_inverse_real_of_nat: "(\n. inverse (real (Suc n))) \ 0" ``` hoelzl@51526 ` 1812` ``` by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc ``` wenzelm@63546 ` 1813` ``` filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity) ``` wenzelm@63546 ` 1814` wenzelm@63546 ` 1815` ```text \ ``` wenzelm@63546 ` 1816` ``` The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to ``` wenzelm@63546 ` 1817` ``` infinity is now easily proved. ``` wenzelm@63546 ` 1818` ```\ ``` wenzelm@63546 ` 1819` wenzelm@63546 ` 1820` ```lemma LIMSEQ_inverse_real_of_nat_add: "(\n. r + inverse (real (Suc n))) \ r" ``` hoelzl@51526 ` 1821` ``` using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto ``` hoelzl@51526 ` 1822` wenzelm@63546 ` 1823` ```lemma LIMSEQ_inverse_real_of_nat_add_minus: "(\n. r + -inverse (real (Suc n))) \ r" ``` hoelzl@51526 ` 1824` ``` using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] ``` hoelzl@51526 ` 1825` ``` by auto ``` hoelzl@51526 ` 1826` wenzelm@63546 ` 1827` ```lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: "(\n. r * (1 + - inverse (real (Suc n)))) \ r" ``` hoelzl@51526 ` 1828` ``` using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] ``` hoelzl@51526 ` 1829` ``` by auto ``` hoelzl@51526 ` 1830` wenzelm@61973 ` 1831` ```lemma lim_inverse_n: "((\n. inverse(of_nat n)) \ (0::'a::real_normed_field)) sequentially" ``` eberlm@61524 ` 1832` ``` using lim_1_over_n by (simp add: inverse_eq_divide) ``` eberlm@61524 ` 1833` wenzelm@61969 ` 1834` ```lemma LIMSEQ_Suc_n_over_n: "(\n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \ 1" ``` eberlm@61524 ` 1835` ```proof (rule Lim_transform_eventually) ``` eberlm@61524 ` 1836` ``` show "eventually (\n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially" ``` wenzelm@63546 ` 1837` ``` using eventually_gt_at_top[of "0::nat"] ``` wenzelm@63546 ` 1838` ``` by eventually_elim (simp add: field_simps) ``` wenzelm@61969 ` 1839` ``` have "(\n. 1 + inverse (of_nat n) :: 'a) \ 1 + 0" ``` eberlm@61524 ` 1840` ``` by (intro tendsto_add tendsto_const lim_inverse_n) ``` wenzelm@63546 ` 1841` ``` then show "(\n. 1 + inverse (of_nat n) :: 'a) \ 1" ``` wenzelm@63546 ` 1842` ``` by simp ``` eberlm@61524 ` 1843` ```qed ``` eberlm@61524 ` 1844` wenzelm@61969 ` 1845` ```lemma LIMSEQ_n_over_Suc_n: "(\n. of_nat n / of_nat (Suc n) :: 'a :: real_normed_field) \ 1" ``` eberlm@61524 ` 1846` ```proof (rule Lim_transform_eventually) ``` paulson@62087 ` 1847` ``` show "eventually (\n. inverse (of_nat (Suc n) / of_nat n :: 'a) = ``` wenzelm@63546 ` 1848` ``` of_nat n / of_nat (Suc n)) sequentially" ``` paulson@62087 ` 1849` ``` using eventually_gt_at_top[of "0::nat"] ``` eberlm@61524 ` 1850` ``` by eventually_elim (simp add: field_simps del: of_nat_Suc) ``` wenzelm@61969 ` 1851` ``` have "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \ inverse 1" ``` eberlm@61524 ` 1852` ``` by (intro tendsto_inverse LIMSEQ_Suc_n_over_n) simp_all ``` wenzelm@63546 ` 1853` ``` then show "(\n. inverse (of_nat (Suc n) / of_nat n :: 'a)) \ 1" ``` wenzelm@63546 ` 1854` ``` by simp ``` eberlm@61524 ` 1855` ```qed ``` eberlm@61524 ` 1856` wenzelm@63546 ` 1857` wenzelm@60758 ` 1858` ```subsection \Convergence on sequences\ ``` hoelzl@51526 ` 1859` eberlm@61531 ` 1860` ```lemma convergent_cong: ``` eberlm@61531 ` 1861` ``` assumes "eventually (\x. f x = g x) sequentially" ``` wenzelm@63546 ` 1862` ``` shows "convergent f \ convergent g" ``` wenzelm@63546 ` 1863` ``` unfolding convergent_def ``` wenzelm@63546 ` 1864` ``` by (subst filterlim_cong[OF refl refl assms]) (rule refl) ``` eberlm@61531 ` 1865` eberlm@61531 ` 1866` ```lemma convergent_Suc_iff: "convergent (\n. f (Suc n)) \ convergent f" ``` eberlm@61531 ` 1867` ``` by (auto simp: convergent_def LIMSEQ_Suc_iff) ``` eberlm@61531 ` 1868` eberlm@61531 ` 1869` ```lemma convergent_ignore_initial_segment: "convergent (\n. f (n + m)) = convergent f" ``` wenzelm@63546 ` 1870` ```proof (induct m arbitrary: f) ``` wenzelm@63546 ` 1871` ``` case 0 ``` wenzelm@63546 ` 1872` ``` then show ?case by simp ``` wenzelm@63546 ` 1873` ```next ``` eberlm@61531 ` 1874` ``` case (Suc m) ``` wenzelm@63546 ` 1875` ``` have "convergent (\n. f (n + Suc m)) \ convergent (\n. f (Suc n + m))" ``` wenzelm@63546 ` 1876` ``` by simp ``` wenzelm@63546 ` 1877` ``` also have "\ \ convergent (\n. f (n + m))" ``` wenzelm@63546 ` 1878` ``` by (rule convergent_Suc_iff) ``` wenzelm@63546 ` 1879` ``` also have "\ \ convergent f" ``` wenzelm@63546 ` 1880` ``` by (rule Suc) ``` eberlm@61531 ` 1881` ``` finally show ?case . ``` wenzelm@63546 ` 1882` ```qed ``` eberlm@61531 ` 1883` hoelzl@51526 ` 1884` ```lemma convergent_add: ``` hoelzl@51526 ` 1885` ``` fixes X Y :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1886` ``` assumes "convergent (\n. X n)" ``` wenzelm@63546 ` 1887` ``` and "convergent (\n. Y n)" ``` hoelzl@51526 ` 1888` ``` shows "convergent (\n. X n + Y n)" ``` lp15@61649 ` 1889` ``` using assms unfolding convergent_def by (blast intro: tendsto_add) ``` hoelzl@51526 ` 1890` nipkow@64267 ` 1891` ```lemma convergent_sum: ``` hoelzl@51526 ` 1892` ``` fixes X :: "'a \ nat \ 'b::real_normed_vector" ``` wenzelm@63915 ` 1893` ``` shows "(\i. i \ A \ convergent (\n. X i n)) \ convergent (\n. \i\A. X i n)" ``` wenzelm@63915 ` 1894` ``` by (induct A rule: infinite_finite_induct) (simp_all add: convergent_const convergent_add) ``` hoelzl@51526 ` 1895` hoelzl@51526 ` 1896` ```lemma (in bounded_linear) convergent: ``` hoelzl@51526 ` 1897` ``` assumes "convergent (\n. X n)" ``` hoelzl@51526 ` 1898` ``` shows "convergent (\n. f (X n))" ``` lp15@61649 ` 1899` ``` using assms unfolding convergent_def by (blast intro: tendsto) ``` hoelzl@51526 ` 1900` hoelzl@51526 ` 1901` ```lemma (in bounded_bilinear) convergent: ``` wenzelm@63546 ` 1902` ``` assumes "convergent (\n. X n)" ``` wenzelm@63546 ` 1903` ``` and "convergent (\n. Y n)" ``` hoelzl@51526 ` 1904` ``` shows "convergent (\n. X n ** Y n)" ``` lp15@61649 ` 1905` ``` using assms unfolding convergent_def by (blast intro: tendsto) ``` hoelzl@51526 ` 1906` wenzelm@63546 ` 1907` ```lemma convergent_minus_iff: "convergent X \ convergent (\n. - X n)" ``` wenzelm@63546 ` 1908` ``` for X :: "nat \ 'a::real_normed_vector" ``` wenzelm@63546 ` 1909` ``` apply (simp add: convergent_def) ``` wenzelm@63546 ` 1910` ``` apply (auto dest: tendsto_minus) ``` wenzelm@63546 ` 1911` ``` apply (drule tendsto_minus) ``` wenzelm@63546 ` 1912` ``` apply auto ``` wenzelm@63546 ` 1913` ``` done ``` hoelzl@51526 ` 1914` eberlm@61531 ` 1915` ```lemma convergent_diff: ``` eberlm@61531 ` 1916` ``` fixes X Y :: "nat \ 'a::real_normed_vector" ``` eberlm@61531 ` 1917` ``` assumes "convergent (\n. X n)" ``` eberlm@61531 ` 1918` ``` assumes "convergent (\n. Y n)" ``` eberlm@61531 ` 1919` ``` shows "convergent (\n. X n - Y n)" ``` lp15@61649 ` 1920` ``` using assms unfolding convergent_def by (blast intro: tendsto_diff) ``` eberlm@61531 ` 1921` eberlm@61531 ` 1922` ```lemma convergent_norm: ``` eberlm@61531 ` 1923` ``` assumes "convergent f" ``` wenzelm@63546 ` 1924` ``` shows "convergent (\n. norm (f n))" ``` eberlm@61531 ` 1925` ```proof - ``` wenzelm@63546 ` 1926` ``` from assms have "f \ lim f" ``` wenzelm@63546 ` 1927` ``` by (simp add: convergent_LIMSEQ_iff) ``` wenzelm@63546 ` 1928` ``` then have "(\n. norm (f n)) \ norm (lim f)" ``` wenzelm@63546 ` 1929` ``` by (rule tendsto_norm) ``` wenzelm@63546 ` 1930` ``` then show ?thesis ``` wenzelm@63546 ` 1931` ``` by (auto simp: convergent_def) ``` eberlm@61531 ` 1932` ```qed ``` eberlm@61531 ` 1933` paulson@62087 ` 1934` ```lemma convergent_of_real: ``` wenzelm@63546 ` 1935` ``` "convergent f \ convergent (\n. of_real (f n) :: 'a::real_normed_algebra_1)" ``` eberlm@61531 ` 1936` ``` unfolding convergent_def by (blast intro!: tendsto_of_real) ``` eberlm@61531 ` 1937` paulson@62087 ` 1938` ```lemma convergent_add_const_iff: ``` wenzelm@63546 ` 1939` ``` "convergent (\n. c + f n :: 'a::real_normed_vector) \ convergent f" ``` eberlm@61531 ` 1940` ```proof ``` eberlm@61531 ` 1941` ``` assume "convergent (\n. c + f n)" ``` wenzelm@63546 ` 1942` ``` from convergent_diff[OF this convergent_const[of c]] show "convergent f" ``` wenzelm@63546 ` 1943` ``` by simp ``` eberlm@61531 ` 1944` ```next ``` eberlm@61531 ` 1945` ``` assume "convergent f" ``` wenzelm@63546 ` 1946` ``` from convergent_add[OF convergent_const[of c] this] show "convergent (\n. c + f n)" ``` wenzelm@63546 ` 1947` ``` by simp ``` eberlm@61531 ` 1948` ```qed ``` eberlm@61531 ` 1949` paulson@62087 ` 1950` ```lemma convergent_add_const_right_iff: ``` wenzelm@63546 ` 1951` ``` "convergent (\n. f n + c :: 'a::real_normed_vector) \ convergent f" ``` eberlm@61531 ` 1952` ``` using convergent_add_const_iff[of c f] by (simp add: add_ac) ``` eberlm@61531 ` 1953` paulson@62087 ` 1954` ```lemma convergent_diff_const_right_iff: ``` wenzelm@63546 ` 1955` ``` "convergent (\n. f n - c :: 'a::real_normed_vector) \ convergent f" ``` eberlm@61531 ` 1956` ``` using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac) ``` eberlm@61531 ` 1957` eberlm@61531 ` 1958` ```lemma convergent_mult: ``` eberlm@61531 ` 1959` ``` fixes X Y :: "nat \ 'a::real_normed_field" ``` eberlm@61531 ` 1960` ``` assumes "convergent (\n. X n)" ``` wenzelm@63546 ` 1961` ``` and "convergent (\n. Y n)" ``` eberlm@61531 ` 1962` ``` shows "convergent (\n. X n * Y n)" ``` lp15@61649 ` 1963` ``` using assms unfolding convergent_def by (blast intro: tendsto_mult) ``` eberlm@61531 ` 1964` eberlm@61531 ` 1965` ```lemma convergent_mult_const_iff: ``` eberlm@61531 ` 1966` ``` assumes "c \ 0" ``` wenzelm@63546 ` 1967` ``` shows "convergent (\n. c * f n :: 'a::real_normed_field) \ convergent f" ``` eberlm@61531 ` 1968` ```proof ``` eberlm@61531 ` 1969` ``` assume "convergent (\n. c * f n)" ``` paulson@62087 ` 1970` ``` from assms convergent_mult[OF this convergent_const[of "inverse c"]] ``` eberlm@61531 ` 1971` ``` show "convergent f" by (simp add: field_simps) ``` eberlm@61531 ` 1972` ```next ``` eberlm@61531 ` 1973` ``` assume "convergent f" ``` wenzelm@63546 ` 1974` ``` from convergent_mult[OF convergent_const[of c] this] show "convergent (\n. c * f n)" ``` wenzelm@63546 ` 1975` ``` by simp ``` eberlm@61531 ` 1976` ```qed ``` eberlm@61531 ` 1977` eberlm@61531 ` 1978` ```lemma convergent_mult_const_right_iff: ``` wenzelm@63546 ` 1979` ``` fixes c :: "'a::real_normed_field" ``` eberlm@61531 ` 1980` ``` assumes "c \ 0" ``` wenzelm@63546 ` 1981` ``` shows "convergent (\n. f n * c) \ convergent f" ``` eberlm@61531 ` 1982` ``` using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac) ``` eberlm@61531 ` 1983` eberlm@61531 ` 1984` ```lemma convergent_imp_Bseq: "convergent f \ Bseq f" ``` eberlm@61531 ` 1985` ``` by (simp add: Cauchy_Bseq convergent_Cauchy) ``` eberlm@61531 ` 1986` hoelzl@51526 ` 1987` wenzelm@60758 ` 1988` ```text \A monotone sequence converges to its least upper bound.\ ``` hoelzl@51526 ` 1989` hoelzl@54263 ` 1990` ```lemma LIMSEQ_incseq_SUP: ``` wenzelm@63546 ` 1991` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder,linorder_topology}" ``` hoelzl@54263 ` 1992` ``` assumes u: "bdd_above (range X)" ``` wenzelm@63546 ` 1993` ``` and X: "incseq X" ``` wenzelm@61969 ` 1994` ``` shows "X \ (SUP i. X i)" ``` hoelzl@54263 ` 1995` ``` by (rule order_tendstoI) ``` wenzelm@63546 ` 1996` ``` (auto simp: eventually_sequentially u less_cSUP_iff ``` wenzelm@63546 ` 1997` ``` intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) ``` hoelzl@51526 ` 1998` hoelzl@54263 ` 1999` ```lemma LIMSEQ_decseq_INF: ``` hoelzl@54263 ` 2000` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" ``` hoelzl@54263 ` 2001` ``` assumes u: "bdd_below (range X)" ``` wenzelm@63546 ` 2002` ``` and X: "decseq X" ``` wenzelm@61969 ` 2003` ``` shows "X \ (INF i. X i)" ``` hoelzl@54263 ` 2004` ``` by (rule order_tendstoI) ``` wenzelm@63546 ` 2005` ``` (auto simp: eventually_sequentially u cINF_less_iff ``` wenzelm@63546 ` 2006` ``` intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) ``` wenzelm@63546 ` 2007` wenzelm@63546 ` 2008` ```text \Main monotonicity theorem.\ ``` wenzelm@63546 ` 2009` wenzelm@63546 ` 2010` ```lemma Bseq_monoseq_convergent: "Bseq X \ monoseq X \ convergent X" ``` wenzelm@63546 ` 2011` ``` for X :: "nat \ real" ``` wenzelm@63546 ` 2012` ``` by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP ``` wenzelm@63546 ` 2013` ``` dest: Bseq_bdd_above Bseq_bdd_below) ``` wenzelm@63546 ` 2014` wenzelm@63546 ` 2015` ```lemma Bseq_mono_convergent: "Bseq X \ (\m n. m \ n \ X m \ X n) \ convergent X" ``` wenzelm@63546 ` 2016` ``` for X :: "nat \ real" ``` hoelzl@54263 ` 2017` ``` by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) ``` hoelzl@51526 ` 2018` wenzelm@63546 ` 2019` ```lemma monoseq_imp_convergent_iff_Bseq: "monoseq f \ convergent f \ Bseq f" ``` wenzelm@63546 ` 2020` ``` for f :: "nat \ real" ``` eberlm@61531 ` 2021` ``` using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast ``` eberlm@61531 ` 2022` eberlm@61531 ` 2023` ```lemma Bseq_monoseq_convergent'_inc: ``` wenzelm@63546 ` 2024` ``` fixes f :: "nat \ real" ``` wenzelm@63546 ` 2025` ``` shows "Bseq (\n. f (n + M)) \ (\m n. M \ m \ m \ n \ f m \ f n) \ convergent f" ``` eberlm@61531 ` 2026` ``` by (subst convergent_ignore_initial_segment [symmetric, of _ M]) ``` eberlm@61531 ` 2027` ``` (auto intro!: Bseq_monoseq_convergent simp: monoseq_def) ``` eberlm@61531 ` 2028` eberlm@61531 ` 2029` ```lemma Bseq_monoseq_convergent'_dec: ``` wenzelm@63546 ` 2030` ``` fixes f :: "nat \ real" ``` wenzelm@63546 ` 2031` ``` shows "Bseq (\n. f (n + M)) \ (\m n. M \ m \ m \ n \ f m \ f n) \ convergent f" ``` eberlm@61531 ` 2032` ``` by (subst convergent_ignore_initial_segment [symmetric, of _ M]) ``` wenzelm@63546 ` 2033` ``` (auto intro!: Bseq_monoseq_convergent simp: monoseq_def) ``` wenzelm@63546 ` 2034` wenzelm@63546 ` 2035` ```lemma Cauchy_iff: "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" ``` wenzelm@63546 ` 2036` ``` for X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 2037` ``` unfolding Cauchy_def dist_norm .. ``` hoelzl@51526 ` 2038` wenzelm@63546 ` 2039` ```lemma CauchyI: "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" ``` wenzelm@63546 ` 2040` ``` for X :: "nat \ 'a::real_normed_vector" ``` wenzelm@63546 ` 2041` ``` by (simp add: Cauchy_iff) ``` wenzelm@63546 ` 2042` wenzelm@63546 ` 2043` ```lemma CauchyD: "Cauchy X \ 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e" ``` wenzelm@63546 ` 2044` ``` for X :: "nat \ 'a::real_normed_vector" ``` wenzelm@63546 ` 2045` ``` by (simp add: Cauchy_iff) ``` hoelzl@51526 ` 2046` hoelzl@51526 ` 2047` ```lemma incseq_convergent: ``` hoelzl@51526 ` 2048` ``` fixes X :: "nat \ real" ``` wenzelm@63546 ` 2049` ``` assumes "incseq X" ``` wenzelm@63546 ` 2050` ``` and "\i. X i \ B" ``` wenzelm@61969 ` 2051` ``` obtains L where "X \ L" "\i. X i \ L" ``` hoelzl@51526 ` 2052` ```proof atomize_elim ``` wenzelm@60758 ` 2053` ``` from incseq_bounded[OF assms] \incseq X\ Bseq_monoseq_convergent[of X] ``` wenzelm@61969 ` 2054` ``` obtain L where "X \ L" ``` hoelzl@51526 ` 2055` ``` by (auto simp: convergent_def monoseq_def incseq_def) ``` wenzelm@61969 ` 2056` ``` with \incseq X\ show "\L. X \ L \ (\i. X i \ L)" ``` hoelzl@51526 ` 2057` ``` by (auto intro!: exI[of _ L] incseq_le) ``` hoelzl@51526 ` 2058` ```qed ``` hoelzl@51526 ` 2059` hoelzl@51526 ` 2060` ```lemma decseq_convergent: ``` hoelzl@51526 ` 2061` ``` fixes X :: "nat \ real" ``` wenzelm@63546 ` 2062` ``` assumes "decseq X" ``` wenzelm@63546 ` 2063` ``` and "\i. B \ X i" ``` wenzelm@61969 ` 2064` ``` obtains L where "X \ L" "\i. L \ X i" ``` hoelzl@51526 ` 2065` ```proof atomize_elim ``` wenzelm@60758 ` 2066` ``` from decseq_bounded[OF assms] \decseq X\ Bseq_monoseq_convergent[of X] ``` wenzelm@61969 ` 2067` ``` obtain L where "X \ L" ``` hoelzl@51526 ` 2068` ``` by (auto simp: convergent_def monoseq_def decseq_def) ``` wenzelm@61969 ` 2069` ``` with \decseq X\ show "\L. X \ L \ (\i. L \ X i)" ``` hoelzl@51526 ` 2070` ``` by (auto intro!: exI[of _ L] decseq_le) ``` hoelzl@51526 ` 2071` ```qed ``` hoelzl@51526 ` 2072` wenzelm@63546 ` 2073` wenzelm@60758 ` 2074` ```subsection \Power Sequences\ ``` hoelzl@51526 ` 2075` wenzelm@63546 ` 2076` ```text \ ``` wenzelm@63546 ` 2077` ``` The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term ``` wenzelm@63546 ` 2078` ``` "x<1"}. Proof will use (NS) Cauchy equivalence for convergence and ``` wenzelm@63546 ` 2079` ``` also fact that bounded and monotonic sequence converges. ``` wenzelm@63546 ` 2080` ```\ ``` wenzelm@63546 ` 2081` wenzelm@63546 ` 2082` ```lemma Bseq_realpow: "0 \ x \ x \ 1 \ Bseq (\n. x ^ n)" ``` wenzelm@63546 ` 2083` ``` for x :: real ``` wenzelm@63546 ` 2084` ``` apply (simp add: Bseq_def) ``` wenzelm@63546 ` 2085` ``` apply (rule_tac x = 1 in exI) ``` wenzelm@63546 ` 2086` ``` apply (simp add: power_abs) ``` wenzelm@63546 ` 2087` ``` apply (auto dest: power_mono) ``` wenzelm@63546 ` 2088` ``` done ``` wenzelm@63546 ` 2089` wenzelm@63546 ` 2090` ```lemma monoseq_realpow: "0 \ x \ x \ 1 \ monoseq (\n. x ^ n)" ``` wenzelm@63546 ` 2091` ``` for x :: real ``` wenzelm@63546 ` 2092` ``` apply (clarify intro!: mono_SucI2) ``` wenzelm@63546 ` 2093` ``` apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing) ``` wenzelm@63546 ` 2094` ``` apply auto ``` wenzelm@63546 ` 2095` ``` done ``` wenzelm@63546 ` 2096` wenzelm@63546 ` 2097` ```lemma convergent_realpow: "0 \ x \ x \ 1 \ convergent (\n. x ^ n)" ``` wenzelm@63546 ` 2098` ``` for x :: real ``` wenzelm@63546 ` 2099` ``` by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) ``` wenzelm@63546 ` 2100` wenzelm@63546 ` 2101` ```lemma LIMSEQ_inverse_realpow_zero: "1 < x \ (\n. inverse (x ^ n)) \ 0" ``` wenzelm@63546 ` 2102` ``` for x :: real ``` hoelzl@51526 ` 2103` ``` by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 2104` hoelzl@51526 ` 2105` ```lemma LIMSEQ_realpow_zero: ``` wenzelm@63546 ` 2106` ``` fixes x :: real ``` wenzelm@63546 ` 2107` ``` assumes "0 \ x" "x < 1" ``` wenzelm@63546 ` 2108` ``` shows "(\n. x ^ n) \ 0" ``` wenzelm@63546 ` 2109` ```proof (cases "x = 0") ``` wenzelm@63546 ` 2110` ``` case False ``` wenzelm@63546 ` 2111` ``` with \0 \ x\ have x0: "0 < x" by simp ``` wenzelm@63546 ` 2112` ``` then have "1 < inverse x" ``` wenzelm@63546 ` 2113` ``` using \x < 1\ by (rule one_less_inverse) ``` wenzelm@63546 ` 2114` ``` then have "(\n. inverse (inverse x ^ n)) \ 0" ``` hoelzl@51526 ` 2115` ``` by (rule LIMSEQ_inverse_realpow_zero) ``` wenzelm@63546 ` 2116` ``` then show ?thesis by (simp add: power_inverse) ``` wenzelm@63546 ` 2117` ```next ``` wenzelm@63546 ` 2118` ``` case True ``` wenzelm@63546 ` 2119` ``` show ?thesis ``` wenzelm@63546 ` 2120` ``` by (rule LIMSEQ_imp_Suc) (simp add: True) ``` wenzelm@63546 ` 2121` ```qed ``` wenzelm@63546 ` 2122` wenzelm@63546 ` 2123` ```lemma LIMSEQ_power_zero: "norm x < 1 \ (\n. x ^ n) \ 0" ``` wenzelm@63546 ` 2124` ``` for x :: "'a::real_normed_algebra_1" ``` wenzelm@63546 ` 2125` ``` apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) ``` wenzelm@63546 ` 2126` ``` apply (simp only: tendsto_Zfun_iff, erule Zfun_le) ``` wenzelm@63546 ` 2127` ``` apply (simp add: power_abs norm_power_ineq) ``` wenzelm@63546 ` 2128` ``` done ``` hoelzl@51526 ` 2129` wenzelm@61969 ` 2130` ```lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) \ 0" ``` hoelzl@51526 ` 2131` ``` by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 2132` immler@63556 ` 2133` ```lemma ``` immler@63556 ` 2134` ``` tendsto_power_zero: ``` immler@63556 ` 2135` ``` fixes x::"'a::real_normed_algebra_1" ``` immler@63556 ` 2136` ``` assumes "filterlim f at_top F" ``` immler@63556 ` 2137` ``` assumes "norm x < 1" ``` immler@63556 ` 2138` ``` shows "((\y. x ^ (f y)) \ 0) F" ``` immler@63556 ` 2139` ```proof (rule tendstoI) ``` immler@63556 ` 2140` ``` fix e::real assume "0 < e" ``` immler@63556 ` 2141` ``` from tendstoD[OF LIMSEQ_power_zero[OF \norm x < 1\] \0 < e\] ``` immler@63556 ` 2142` ``` have "\\<^sub>F xa in sequentially. norm (x ^ xa) < e" ``` immler@63556 ` 2143` ``` by simp ``` immler@63556 ` 2144` ``` then obtain N where N: "norm (x ^ n) < e" if "n \ N" for n ``` immler@63556 ` 2145` ``` by (auto simp: eventually_sequentially) ``` immler@63556 ` 2146` ``` have "\\<^sub>F i in F. f i \ N" ``` immler@63556 ` 2147` ``` using \filterlim f sequentially F\ ``` immler@63556 ` 2148` ``` by (simp add: filterlim_at_top) ``` immler@63556 ` 2149` ``` then show "\\<^sub>F i in F. dist (x ^ f i) 0 < e" ``` immler@63556 ` 2150` ``` by (eventually_elim) (auto simp: N) ``` immler@63556 ` 2151` ```qed ``` immler@63556 ` 2152` wenzelm@63546 ` 2153` ```text \Limit of @{term "c^n"} for @{term"\c\ < 1"}.\ ``` hoelzl@51526 ` 2154` wenzelm@61969 ` 2155` ```lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) \ 0" ``` hoelzl@51526 ` 2156` ``` by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) ``` hoelzl@51526 ` 2157` wenzelm@61969 ` 2158` ```lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) \ 0" ``` hoelzl@51526 ` 2159` ``` by (rule LIMSEQ_power_zero) simp ``` hoelzl@51526 ` 2160` hoelzl@51526 ` 2161` wenzelm@60758 ` 2162` ```subsection \Limits of Functions\ ``` hoelzl@51526 ` 2163` wenzelm@63546 ` 2164` ```lemma LIM_eq: "f \a\ L = (\r>0. \s>0. \x. x \ a \ norm (x - a) < s \ norm (f x - L) < r)" ``` wenzelm@63546 ` 2165` ``` for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` wenzelm@63546 ` 2166` ``` by (simp add: LIM_def dist_norm) ``` hoelzl@51526 ` 2167` hoelzl@51526 ` 2168` ```lemma LIM_I: ``` wenzelm@63546 ` 2169` ``` "(\r. 0 < r \ \s>0. \x. x \ a \ norm (x - a) < s \ norm (f x - L) < r) \ f \a\ L" ``` wenzelm@63546 ` 2170` ``` for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` wenzelm@63546 ` 2171` ``` by (simp add: LIM_eq) ``` wenzelm@63546 ` 2172` wenzelm@63546 ` 2173` ```lemma LIM_D: "f \a\ L \ 0 < r \ \s>0.\x. x \ a \ norm (x - a) < s \ norm (f x - L) < r" ``` wenzelm@63546 ` 2174` ``` for a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` wenzelm@63546 ` 2175` ``` by (simp add: LIM_eq) ``` wenzelm@63546 ` 2176` wenzelm@63546 ` 2177` ```lemma LIM_offset: "f \a\ L \ (\x. f (x + k)) \(a - k)\ L" ``` wenzelm@63546 ` 2178` ``` for a :: "'a::real_normed_vector" ``` wenzelm@63546 ` 2179` ``` by (simp add: filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap) ``` wenzelm@63546 ` 2180` wenzelm@63546 ` 2181` ```lemma LIM_offset_zero: "f \a\ L \ (\h. f (a + h)) \0\ L" ``` wenzelm@63546 ` 2182` ``` for a :: "'a::real_normed_vector" ``` wenzelm@63546 ` 2183` ``` by (drule LIM_offset [where k = a]) (simp add: add.commute) ``` wenzelm@63546 ` 2184` wenzelm@63546 ` 2185` ```lemma LIM_offset_zero_cancel: "(\h. f (a + h)) \0\ L \ f \a\ L" ``` wenzelm@63546 ` 2186` ``` for a :: "'a::real_normed_vector" ``` wenzelm@63546 ` 2187` ``` by (drule LIM_offset [where k = "- a"]) simp ``` wenzelm@63546 ` 2188` wenzelm@63546 ` 2189` ```lemma LIM_offset_zero_iff: "f \a\ L \ (\h. f (a + h)) \0\ L" ``` wenzelm@63546 ` 2190` ``` for f :: "'a :: real_normed_vector \ _" ``` hoelzl@51642 ` 2191` ``` using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto ``` hoelzl@51642 ` 2192` wenzelm@63546 ` 2193` ```lemma LIM_zero: "(f \ l) F \ ((\x. f x - l) \ 0) F" ``` lp15@65578 ` 2194` ``` for f :: "'a \ 'b::real_normed_vector" ``` wenzelm@63546 ` 2195` ``` unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 2196` hoelzl@51526 ` 2197` ```lemma LIM_zero_cancel: ``` lp15@65578 ` 2198` ``` fixes f :: "'a \ 'b::real_normed_vector" ``` wenzelm@61973 ` 2199` ``` shows "((\x. f x - l) \ 0) F \ (f \ l) F" ``` hoelzl@51526 ` 2200` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 2201` wenzelm@63546 ` 2202` ```lemma LIM_zero_iff: "((\x. f x - l) \ 0) F = (f \ l) F" ``` lp15@65578 ` 2203` ``` for f :: "'a \ 'b::real_normed_vector" ``` wenzelm@63546 ` 2204` ``` unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 2205` hoelzl@51526 ` 2206` ```lemma LIM_imp_LIM: ``` hoelzl@51526 ` 2207` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 2208` ``` fixes g :: "'a::topological_space \ 'c::real_normed_vector" ``` wenzelm@61976 ` 2209` ``` assumes f: "f \a\ l" ``` wenzelm@63546 ` 2210` ``` and le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" ``` wenzelm@61976 ` 2211` ``` shows "g \a\ m" ``` wenzelm@63546 ` 2212` ``` by (rule metric_LIM_imp_LIM [OF f]) (simp add: dist_norm le) ``` hoelzl@51526 ` 2213` hoelzl@51526 ` 2214` ```lemma LIM_equal2: ``` hoelzl@51526 ` 2215` ``` fixes f g :: "'a::real_normed_vector \ 'b::topological_space" ``` wenzelm@63546 ` 2216` ``` assumes "0 < R" ``` wenzelm@63546 ` 2217` ``` and "\x. x \ a \ norm (x - a) < R \ f x = g x" ``` wenzelm@61976 ` 2218` ``` shows "g \a\ l \ f \a\ l" ``` wenzelm@63546 ` 2219` ``` by (rule metric_LIM_equal2 [OF assms]) (simp_all add: dist_norm) ``` hoelzl@51526 ` 2220` hoelzl@51526 ` 2221` ```lemma LIM_compose2: ``` hoelzl@51526 ` 2222` ``` fixes a :: "'a::real_normed_vector" ``` wenzelm@61976 ` 2223` ``` assumes f: "f \a\ b" ``` wenzelm@63546 ` 2224` ``` and g: "g \b\ c" ``` wenzelm@63546 ` 2225` ``` and inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" ``` wenzelm@61976 ` 2226` ``` shows "(\x. g (f x)) \a\ c" ``` wenzelm@63546 ` 2227` ``` by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) ``` hoelzl@51526 ` 2228` hoelzl@51526 ` 2229` ```lemma real_LIM_sandwich_zero: ``` hoelzl@51526 ` 2230` ``` fixes f g :: "'a::topological_space \ real" ``` wenzelm@61976 ` 2231` ``` assumes f: "f \a\ 0" ``` wenzelm@63546 ` 2232` ``` and 1: "\x. x \ a \ 0 \ g x" ``` wenzelm@63546 ` 2233` ``` and 2: "\x. x \ a \ g x \ f x" ``` wenzelm@61976 ` 2234` ``` shows "g \a\ 0" ``` hoelzl@51526 ` 2235` ```proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) ``` wenzelm@63546 ` 2236` ``` fix x ``` wenzelm@63546 ` 2237` ``` assume x: "x \ a" ``` wenzelm@63546 ` 2238` ``` with 1 have "norm (g x - 0) = g x" by simp ``` hoelzl@51526 ` 2239` ``` also have "g x \ f x" by (rule 2 [OF x]) ``` hoelzl@51526 ` 2240` ``` also have "f x \ \f x\" by (rule abs_ge_self) ``` hoelzl@51526 ` 2241` ``` also have "\f x\ = norm (f x - 0)" by simp ``` hoelzl@51526 ` 2242` ``` finally show "norm (g x - 0) \ norm (f x - 0)" . ``` hoelzl@51526 ` 2243` ```qed ``` hoelzl@51526 ` 2244` hoelzl@51526 ` 2245` wenzelm@60758 ` 2246` ```subsection \Continuity\ ``` hoelzl@51526 ` 2247` wenzelm@63546 ` 2248` ```lemma LIM_isCont_iff: "(f \a\ f a) = ((\h. f (a + h)) \0\ f a)" ``` wenzelm@63546 ` 2249` ``` for f :: "'a::real_normed_vector \ 'b::topological_space" ``` wenzelm@63546 ` 2250` ``` by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) ``` wenzelm@63546 ` 2251` wenzelm@63546 ` 2252` ```lemma isCont_iff: "isCont f x = (\h. f (x + h)) \0\ f x" ``` wenzelm@63546 ` 2253` ``` for f :: "'a::real_normed_vector \ 'b::topological_space" ``` wenzelm@63546 ` 2254` ``` by (simp add: isCont_def LIM_isCont_iff) ``` hoelzl@51526 ` 2255` hoelzl@51526 ` 2256` ```lemma isCont_LIM_compose2: ``` hoelzl@51526 ` 2257` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 2258` ``` assumes f [unfolded isCont_def]: "isCont f a" ``` wenzelm@63546 ` 2259` ``` and g: "g \f a\ l" ``` wenzelm@63546 ` 2260` ``` and inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" ``` wenzelm@61976 ` 2261` ``` shows "(\x. g (f x)) \a\ l" ``` wenzelm@63546 ` 2262` ``` by (rule LIM_compose2 [OF f g inj]) ``` wenzelm@63546 ` 2263` wenzelm@63546 ` 2264` ```lemma isCont_norm [simp]: "isCont f a \ isCont (\x. norm (f x)) a" ``` wenzelm@63546 ` 2265` ``` for f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 2266` ``` by (fact continuous_norm) ``` hoelzl@51526 ` 2267` wenzelm@63546 ` 2268` ```lemma isCont_rabs [simp]: "isCont f a \ isCont (\x. \f x\) a" ``` wenzelm@63546 ` 2269` ``` for f :: "'a::t2_space \ real" ``` hoelzl@51526 ` 2270` ``` by (fact continuous_rabs) ``` hoelzl@51526 ` 2271` wenzelm@63546 ` 2272` ```lemma isCont_add [simp]: "isCont f a \ isCont g a \ isCont (\x. f x + g x) a" ``` wenzelm@63546 ` 2273` ``` for f :: "'a::t2_space \ 'b::topological_monoid_add" ``` hoelzl@51526 ` 2274` ``` by (fact continuous_add) ``` hoelzl@51526 ` 2275` wenzelm@63546 ` 2276` ```lemma isCont_minus [simp]: "isCont f a \ isCont (\x. - f x) a" ``` wenzelm@63546 ` 2277` ``` for f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 2278` ``` by (fact continuous_minus) ``` hoelzl@51526 ` 2279` wenzelm@63546 ` 2280` ```lemma isCont_diff [simp]: "isCont f a \ isCont g a \ isCont (\x. f x - g x) a" ``` wenzelm@63546 ` 2281` ``` for f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 2282` ``` by (fact continuous_diff) ``` hoelzl@51526 ` 2283` wenzelm@63546 ` 2284` ```lemma isCont_mult [simp]: "isCont f a \ isCont g a \ isCont (\x. f x * g x) a" ``` wenzelm@63546 ` 2285` ``` for f g :: "'a::t2_space \ 'b::real_normed_algebra" ``` hoelzl@51526 ` 2286` ``` by (fact continuous_mult) ``` hoelzl@51526 ` 2287` wenzelm@63546 ` 2288` ```lemma (in bounded_linear) isCont: "isCont g a \ isCont (\x. f (g x)) a" ``` hoelzl@51526 ` 2289` ``` by (fact continuous) ``` hoelzl@51526 ` 2290` wenzelm@63546 ` 2291` ```lemma (in bounded_bilinear) isCont: "isCont f a \ isCont g a \ isCont (\x. f x ** g x) a" ``` hoelzl@51526 ` 2292` ``` by (fact continuous) ``` hoelzl@51526 ` 2293` lp15@60141 ` 2294` ```lemmas isCont_scaleR [simp] = ``` hoelzl@51526 ` 2295` ``` bounded_bilinear.isCont [OF bounded_bilinear_scaleR] ``` hoelzl@51526 ` 2296` hoelzl@51526 ` 2297` ```lemmas isCont_of_real [simp] = ``` hoelzl@51526 ` 2298` ``` bounded_linear.isCont [OF bounded_linear_of_real] ``` hoelzl@51526 ` 2299` wenzelm@63546 ` 2300` ```lemma isCont_power [simp]: "isCont f a \ isCont (\x. f x ^ n) a" ``` wenzelm@63546 ` 2301` ``` for f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` hoelzl@51526 ` 2302` ``` by (fact continuous_power) ``` hoelzl@51526 ` 2303` nipkow@64267 ` 2304` ```lemma isCont_sum [simp]: "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" ``` wenzelm@63546 ` 2305` ``` for f :: "'a \ 'b::t2_space \ 'c::topological_comm_monoid_add" ``` nipkow@64267 ` 2306` ``` by (auto intro: continuous_sum) ``` hoelzl@51526 ` 2307` wenzelm@63546 ` 2308` wenzelm@60758 ` 2309` ```subsection \Uniform Continuity\ ``` hoelzl@51526 ` 2310` immler@63104 ` 2311` ```lemma uniformly_continuous_on_def: ``` immler@63104 ` 2312` ``` fixes f :: "'a::metric_space \ 'b::metric_space" ``` immler@63104 ` 2313` ``` shows "uniformly_continuous_on s f \ ``` immler@63104 ` 2314` ``` (\e>0. \d>0. \x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" ``` immler@63104 ` 2315` ``` unfolding uniformly_continuous_on_uniformity ``` immler@63104 ` 2316` ``` uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal ``` immler@63104 ` 2317` ``` by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric) ``` immler@63104 ` 2318` wenzelm@63546 ` 2319` ```abbreviation isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" ``` wenzelm@63546 ` 2320` ``` where "isUCont f \ uniformly_continuous_on UNIV f" ``` wenzelm@63546 ` 2321` wenzelm@63546 ` 2322` ```lemma isUCont_def: "isUCont f \ (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" ``` immler@63104 ` 2323` ``` by (auto simp: uniformly_continuous_on_def dist_commute) ``` hoelzl@51531 ` 2324` wenzelm@63546 ` 2325` ```lemma isUCont_isCont: "isUCont f \ isCont f x" ``` immler@63104 ` 2326` ``` by (drule uniformly_continuous_imp_continuous) (simp add: continuous_on_eq_continuous_at) ``` immler@63104 ` 2327` immler@63104 ` 2328` ```lemma uniformly_continuous_on_Cauchy: ``` wenzelm@63546 ` 2329` ``` fixes f :: "'a::metric_space \ 'b::metric_space" ``` immler@63104 ` 2330` ``` assumes "uniformly_continuous_on S f" "Cauchy X" "\n. X n \ S" ``` immler@63104 ` 2331` ``` shows "Cauchy (\n. f (X n))" ``` immler@63104 ` 2332` ``` using assms ``` wenzelm@63546 ` 2333` ``` apply (simp only: uniformly_continuous_on_def) ``` immler@63104 ` 2334` ``` apply (rule metric_CauchyI) ``` wenzelm@63546 ` 2335` ``` apply (drule_tac x=e in spec) ``` wenzelm@63546 ` 2336` ``` apply safe ``` wenzelm@63546 ` 2337` ``` apply (drule_tac e=d in metric_CauchyD) ``` wenzelm@63546 ` 2338` ``` apply safe ``` wenzelm@63546 ` 2339` ``` apply (rule_tac x=M in exI) ``` wenzelm@63546 ` 2340` ``` apply simp ``` immler@63104 ` 2341` ``` done ``` hoelzl@51531 ` 2342` wenzelm@63546 ` 2343` ```lemma isUCont_Cauchy: "isUCont f \ Cauchy X \ Cauchy (\n. f (X n))" ``` immler@63104 ` 2344` ``` by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all ``` lp15@64287 ` 2345` ``` ``` lp15@64287 ` 2346` ```lemma uniformly_continuous_imp_Cauchy_continuous: ``` lp15@64287 ` 2347` ``` fixes f :: "'a::metric_space \ 'b::metric_space" ``` lp15@64287 ` 2348` ``` shows "\uniformly_continuous_on S f; Cauchy \; \n. (\ n) \ S\ \ Cauchy(f o \)" ``` lp15@64287 ` 2349` ``` by (simp add: uniformly_continuous_on_def Cauchy_def) meson ``` hoelzl@51531 ` 2350` hoelzl@51526 ` 2351` ```lemma (in bounded_linear) isUCont: "isUCont f" ``` wenzelm@63546 ` 2352` ``` unfolding isUCont_def dist_norm ``` hoelzl@51526 ` 2353` ```proof (intro allI impI) ``` wenzelm@63546 ` 2354` ``` fix r :: real ``` wenzelm@63546 ` 2355` ``` assume r: "0 < r" ``` wenzelm@63546 ` 2356` ``` obtain K where K: "0 < K" and norm_le: "norm (f x) \ norm x * K" for x ``` lp15@61649 ` 2357` ``` using pos_bounded by blast ``` hoelzl@51526 ` 2358` ``` show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" ``` hoelzl@51526 ` 2359` ``` proof (rule exI, safe) ``` nipkow@56541 ` 2360` ``` from r K show "0 < r / K" by simp ``` hoelzl@51526 ` 2361` ``` next ``` hoelzl@51526 ` 2362` ``` fix x y :: 'a ``` hoelzl@51526 ` 2363` ``` assume xy: "norm (x - y) < r / K" ``` hoelzl@51526 ` 2364` ``` have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) ``` hoelzl@51526 ` 2365` ``` also have "\ \ norm (x - y) * K" by (rule norm_le) ``` hoelzl@51526 ` 2366` ``` also from K xy have "\ < r" by (simp only: pos_less_divide_eq) ``` hoelzl@51526 ` 2367` ``` finally show "norm (f x - f y) < r" . ``` hoelzl@51526 ` 2368` ``` qed ``` hoelzl@51526 ` 2369` ```qed ``` hoelzl@51526 ` 2370` hoelzl@51526 ` 2371` ```lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" ``` wenzelm@63546 ` 2372` ``` by (rule isUCont [THEN isUCont_Cauchy]) ``` hoelzl@51526 ` 2373` lp15@60141 ` 2374` ```lemma LIM_less_bound: ``` hoelzl@51526 ` 2375` ``` fixes f :: "real \ real" ``` hoelzl@51526 ` 2376` ``` assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" ``` hoelzl@51526 ` 2377` ``` shows "0 \ f x" ``` lp15@63952 ` 2378` ```proof (rule tendsto_lowerbound) ``` wenzelm@61973 ` 2379` ``` show "(f \ f x) (at_left x)" ``` wenzelm@60758 ` 2380` ``` using \isCont f x\ by (simp add: filterlim_at_split isCont_def) ``` hoelzl@51526 ` 2381` ``` show "eventually (\x. 0 \ f x) (at_left x)" ``` hoelzl@51641 ` 2382` ``` using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) ``` hoelzl@51526 ` 2383` ```qed simp ``` hoelzl@51471 ` 2384` hoelzl@51529 ` 2385` wenzelm@60758 ` 2386` ```subsection \Nested Intervals and Bisection -- Needed for Compactness\ ``` hoelzl@51529 ` 2387` hoelzl@51529 ` 2388` ```lemma nested_sequence_unique: ``` wenzelm@61969 ` 2389` ``` assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) \ 0" ``` wenzelm@61969 ` 2390` ``` shows "\l::real. ((\n. f n \ l) \ f \ l) \ ((\n. l \ g n) \ g \ l)" ``` hoelzl@51529 ` 2391` ```proof - ``` hoelzl@51529 ` 2392` ``` have "incseq f" unfolding incseq_Suc_iff by fact ``` hoelzl@51529 ` 2393` ``` have "decseq g" unfolding decseq_Suc_iff by fact ``` wenzelm@63546 ` 2394` ``` have "f n \ g 0" for n ``` wenzelm@63546 ` 2395` ``` proof - ``` wenzelm@63546 ` 2396` ``` from \decseq g\ have "g n \ g 0" ``` wenzelm@63546 ` 2397` ``` by (rule decseqD) simp ``` wenzelm@63546 ` 2398` ``` with \\n. f n \ g n\[THEN spec, of n] show ?thesis ``` wenzelm@63546 ` 2399` ``` by auto ``` wenzelm@63546 ` 2400` ``` qed ``` wenzelm@61969 ` 2401` ``` then obtain u where "f \ u" "\i. f i \ u" ``` wenzelm@60758 ` 2402` ``` using incseq_convergent[OF \incseq f\] by auto ``` wenzelm@63546 ` 2403` ``` moreover have "f 0 \ g n" for n ``` wenzelm@63546 ` 2404` ``` proof - ``` wenzelm@60758 ` 2405` ``` from \incseq f\ have "f 0 \ f n" by (rule incseqD) simp ``` wenzelm@63546 ` 2406` ``` with \\n. f n \ g n\[THEN spec, of n] show ?thesis ``` wenzelm@63546 ` 2407` ``` by simp ``` wenzelm@63546 ` 2408` ``` qed ``` wenzelm@61969 ` 2409` ``` then obtain l where "g \ l" "\i. l \ g i" ``` wenzelm@60758 ` 2410` ``` using decseq_convergent[OF \decseq g\] by auto ``` wenzelm@61969 ` 2411` ``` moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \f \ u\ \g \ l\]] ``` hoelzl@51529 ` 2412` ``` ultimately show ?thesis by auto ``` hoelzl@51529 ` 2413` ```qed ``` hoelzl@51529 ` 2414` hoelzl@51529 ` 2415` ```lemma Bolzano[consumes 1, case_names trans local]: ``` hoelzl@51529 ` 2416` ``` fixes P :: "real \ real \ bool" ``` hoelzl@51529 ` 2417` ``` assumes [arith]: "a \ b" ``` wenzelm@63546 ` 2418` ``` and trans: "\a b c. P a b \ P b c \ a \ b \ b \ c \ P a c" ``` wenzelm@63546 ` 2419` ``` and local: "\x. a \ x \ x \ b \ \d>0. \a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51529 ` 2420` ``` shows "P a b" ``` hoelzl@51529 ` 2421` ```proof - ``` wenzelm@63040 ` 2422` ``` define bisect where "bisect = ``` wenzelm@63040 ` 2423` ``` rec_nat (a, b) (\n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" ``` wenzelm@63040 ` 2424` ``` define l u where "l n = fst (bisect n)" and "u n = snd (bisect n)" for n ``` hoelzl@51529 ` 2425` ``` have l[simp]: "l 0 = a" "\n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)" ``` hoelzl@51529 ` 2426` ``` and u[simp]: "u 0 = b" "\n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)" ``` hoelzl@51529 ` 2427` ``` by (simp_all add: l_def u_def bisect_def split: prod.split) ``` hoelzl@51529 ` 2428` wenzelm@63546 ` 2429` ``` have [simp]: "l n \ u n" for n by (induct n) auto ``` hoelzl@51529 ` 2430` wenzelm@61969 ` 2431` ``` have "\x. ((\n. l n \ x) \ l \ x) \ ((\n. x \ u n) \ u \ x)" ``` hoelzl@51529 ` 2432` ``` proof (safe intro!: nested_sequence_unique) ``` wenzelm@63546 ` 2433` ``` show "l n \ l (Suc n)" "u (Suc n) \ u n" for n ``` wenzelm@63546 ` 2434` ``` by (induct n) auto ``` hoelzl@51529 ` 2435` ``` next ``` wenzelm@63546 ` 2436` ``` have "l n - u n = (a - b) / 2^n" for n ``` wenzelm@63546 ` 2437` ``` by (induct n) (auto simp: field_simps) ``` wenzelm@63546 ` 2438` ``` then show "(\n. l n - u n) \ 0" ``` wenzelm@63546 ` 2439` ``` by (simp add: LIMSEQ_divide_realpow_zero) ``` hoelzl@51529 ` 2440` ``` qed fact ``` wenzelm@63546 ` 2441` ``` then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l \ x" "u \ x" ``` wenzelm@63546 ` 2442` ``` by auto ``` wenzelm@63546 ` 2443` ``` obtain d where "0 < d" and d: "a \ x \ x \ b \ b - a < d \ P a b" for a b ``` wenzelm@60758 ` 2444` ``` using \l 0 \ x\ \x \ u 0\ local[of x] by auto ``` hoelzl@51529 ` 2445` hoelzl@51529 ` 2446` ``` show "P a b" ``` hoelzl@51529 ` 2447` ``` proof (rule ccontr) ``` lp15@60141 ` 2448` ``` assume "\ P a b" ``` wenzelm@63546 ` 2449` ``` have "\ P (l n) (u n)" for n ``` wenzelm@63546 ` 2450` ``` proof (induct n) ``` wenzelm@63546 ` 2451` ``` case 0 ``` wenzelm@63546 ` 2452` ``` then show ?case ``` wenzelm@63546 ` 2453` ``` by (simp add: \\ P a b\) ``` wenzelm@63546 ` 2454` ``` next ``` wenzelm@63546 ` 2455` ``` case (Suc n) ``` wenzelm@63546 ` 2456` ``` with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case ``` wenzelm@63546 ` 2457` ``` by auto ``` wenzelm@63546 ` 2458` ``` qed ``` hoelzl@51529 ` 2459` ``` moreover ``` wenzelm@63546 ` 2460` ``` { ``` wenzelm@63546 ` 2461` ``` have "eventually (\n. x - d / 2 < l n) sequentially" ``` wenzelm@61969 ` 2462` ``` using \0 < d\ \l \ x\ by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 2463` ``` moreover have "eventually (\n. u n < x + d / 2) sequentially" ``` wenzelm@61969 ` 2464` ``` using \0 < d\ \u \ x\ by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 2465` ``` ultimately have "eventually (\n. P (l n) (u n)) sequentially" ``` hoelzl@51529 ` 2466` ``` proof eventually_elim ``` wenzelm@63546 ` 2467` ``` case (elim n) ``` hoelzl@51529 ` 2468` ``` from add_strict_mono[OF this] have "u n - l n < d" by simp ``` hoelzl@51529 ` 2469` ``` with x show "P (l n) (u n)" by (rule d) ``` wenzelm@63546 ` 2470` ``` qed ``` wenzelm@63546 ` 2471` ``` } ``` hoelzl@51529 ` 2472` ``` ultimately show False by simp ``` hoelzl@51529 ` 2473` ``` qed ``` hoelzl@51529 ` 2474` ```qed ``` hoelzl@51529 ` 2475` hoelzl@51529 ` 2476` ```lemma compact_Icc[simp, intro]: "compact {a .. b::real}" ``` hoelzl@51529 ` 2477` ```proof (cases "a \ b", rule compactI) ```