src/HOL/Limits.thy
 author wenzelm Tue Sep 01 22:32:58 2015 +0200 (2015-09-01) changeset 61076 bdc1e2f0a86a parent 60974 6a6f15d8fbc4 child 61169 4de9ff3ea29a permissions -rw-r--r--
eliminated \<Colon>;
 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 ``` hoelzl@51524 ` 11` ```imports Real_Vector_Spaces ``` huffman@31349 ` 12` ```begin ``` huffman@31349 ` 13` wenzelm@60758 ` 14` ```subsection \Filter going to infinity norm\ ``` hoelzl@51526 ` 15` hoelzl@50324 ` 16` ```definition at_infinity :: "'a::real_normed_vector filter" where ``` hoelzl@57276 ` 17` ``` "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` hoelzl@50325 ` 24` ```lemma at_infinity_eq_at_top_bot: ``` wenzelm@61076 ` 25` ``` "(at_infinity :: real filter) = sup at_top at_bot" ``` hoelzl@57276 ` 26` ``` apply (simp add: filter_eq_iff eventually_sup eventually_at_infinity ``` hoelzl@57276 ` 27` ``` eventually_at_top_linorder eventually_at_bot_linorder) ``` hoelzl@57276 ` 28` ``` apply safe ``` hoelzl@57276 ` 29` ``` apply (rule_tac x="b" in exI, simp) ``` hoelzl@57276 ` 30` ``` apply (rule_tac x="- b" in exI, simp) ``` hoelzl@57276 ` 31` ``` apply (rule_tac x="max (- Na) N" in exI, auto simp: abs_real_def) ``` hoelzl@57276 ` 32` ``` done ``` hoelzl@50325 ` 33` hoelzl@57276 ` 34` ```lemma at_top_le_at_infinity: "at_top \ (at_infinity :: real filter)" ``` hoelzl@50325 ` 35` ``` unfolding at_infinity_eq_at_top_bot by simp ``` hoelzl@50325 ` 36` hoelzl@57276 ` 37` ```lemma at_bot_le_at_infinity: "at_bot \ (at_infinity :: real filter)" ``` hoelzl@50325 ` 38` ``` unfolding at_infinity_eq_at_top_bot by simp ``` hoelzl@50325 ` 39` hoelzl@57275 ` 40` ```lemma filterlim_at_top_imp_at_infinity: ``` hoelzl@57275 ` 41` ``` fixes f :: "_ \ real" ``` hoelzl@57275 ` 42` ``` shows "filterlim f at_top F \ filterlim f at_infinity F" ``` hoelzl@57275 ` 43` ``` by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl]) ``` hoelzl@57275 ` 44` lp15@59613 ` 45` ```lemma lim_infinity_imp_sequentially: ``` lp15@59613 ` 46` ``` "(f ---> l) at_infinity \ ((\n. f(n)) ---> l) sequentially" ``` lp15@59613 ` 47` ```by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially) ``` lp15@59613 ` 48` lp15@59613 ` 49` wenzelm@60758 ` 50` ```subsubsection \Boundedness\ ``` hoelzl@51531 ` 51` hoelzl@51531 ` 52` ```definition Bfun :: "('a \ 'b::metric_space) \ 'a filter \ bool" where ``` hoelzl@51531 ` 53` ``` Bfun_metric_def: "Bfun f F = (\y. \K>0. eventually (\x. dist (f x) y \ K) F)" ``` hoelzl@51531 ` 54` hoelzl@51531 ` 55` ```abbreviation Bseq :: "(nat \ 'a::metric_space) \ bool" where ``` hoelzl@51531 ` 56` ``` "Bseq X \ Bfun X sequentially" ``` hoelzl@51531 ` 57` hoelzl@51531 ` 58` ```lemma Bseq_conv_Bfun: "Bseq X \ Bfun X sequentially" .. ``` hoelzl@51531 ` 59` hoelzl@51531 ` 60` ```lemma Bseq_ignore_initial_segment: "Bseq X \ Bseq (\n. X (n + k))" ``` hoelzl@51531 ` 61` ``` unfolding Bfun_metric_def by (subst eventually_sequentially_seg) ``` hoelzl@51531 ` 62` hoelzl@51531 ` 63` ```lemma Bseq_offset: "Bseq (\n. X (n + k)) \ Bseq X" ``` hoelzl@51531 ` 64` ``` unfolding Bfun_metric_def by (subst (asm) eventually_sequentially_seg) ``` huffman@31355 ` 65` hoelzl@51474 ` 66` ```lemma Bfun_def: ``` hoelzl@51474 ` 67` ``` "Bfun f F \ (\K>0. eventually (\x. norm (f x) \ K) F)" ``` hoelzl@51474 ` 68` ``` unfolding Bfun_metric_def norm_conv_dist ``` hoelzl@51474 ` 69` ```proof safe ``` hoelzl@51474 ` 70` ``` fix y K assume "0 < K" and *: "eventually (\x. dist (f x) y \ K) F" ``` hoelzl@51474 ` 71` ``` moreover have "eventually (\x. dist (f x) 0 \ dist (f x) y + dist 0 y) F" ``` hoelzl@51474 ` 72` ``` by (intro always_eventually) (metis dist_commute dist_triangle) ``` hoelzl@51474 ` 73` ``` with * have "eventually (\x. dist (f x) 0 \ K + dist 0 y) F" ``` hoelzl@51474 ` 74` ``` by eventually_elim auto ``` wenzelm@60758 ` 75` ``` with \0 < K\ show "\K>0. eventually (\x. dist (f x) 0 \ K) F" ``` hoelzl@51474 ` 76` ``` by (intro exI[of _ "K + dist 0 y"] add_pos_nonneg conjI zero_le_dist) auto ``` hoelzl@51474 ` 77` ```qed auto ``` huffman@31355 ` 78` huffman@31487 ` 79` ```lemma BfunI: ``` huffman@44195 ` 80` ``` assumes K: "eventually (\x. norm (f x) \ K) F" shows "Bfun f F" ``` huffman@31355 ` 81` ```unfolding Bfun_def ``` huffman@31355 ` 82` ```proof (intro exI conjI allI) ``` huffman@31355 ` 83` ``` show "0 < max K 1" by simp ``` huffman@31355 ` 84` ```next ``` huffman@44195 ` 85` ``` show "eventually (\x. norm (f x) \ max K 1) F" ``` huffman@31355 ` 86` ``` using K by (rule eventually_elim1, simp) ``` huffman@31355 ` 87` ```qed ``` huffman@31355 ` 88` huffman@31355 ` 89` ```lemma BfunE: ``` huffman@44195 ` 90` ``` assumes "Bfun f F" ``` huffman@44195 ` 91` ``` obtains B where "0 < B" and "eventually (\x. norm (f x) \ B) F" ``` huffman@31355 ` 92` ```using assms unfolding Bfun_def by fast ``` huffman@31355 ` 93` hoelzl@51531 ` 94` ```lemma Cauchy_Bseq: "Cauchy X \ Bseq X" ``` hoelzl@51531 ` 95` ``` unfolding Cauchy_def Bfun_metric_def eventually_sequentially ``` hoelzl@51531 ` 96` ``` apply (erule_tac x=1 in allE) ``` hoelzl@51531 ` 97` ``` apply simp ``` hoelzl@51531 ` 98` ``` apply safe ``` hoelzl@51531 ` 99` ``` apply (rule_tac x="X M" in exI) ``` hoelzl@51531 ` 100` ``` apply (rule_tac x=1 in exI) ``` hoelzl@51531 ` 101` ``` apply (erule_tac x=M in allE) ``` hoelzl@51531 ` 102` ``` apply simp ``` hoelzl@51531 ` 103` ``` apply (rule_tac x=M in exI) ``` hoelzl@51531 ` 104` ``` apply (auto simp: dist_commute) ``` hoelzl@51531 ` 105` ``` done ``` hoelzl@51531 ` 106` hoelzl@51531 ` 107` wenzelm@60758 ` 108` ```subsubsection \Bounded Sequences\ ``` hoelzl@51531 ` 109` hoelzl@51531 ` 110` ```lemma BseqI': "(\n. norm (X n) \ K) \ Bseq X" ``` hoelzl@51531 ` 111` ``` by (intro BfunI) (auto simp: eventually_sequentially) ``` hoelzl@51531 ` 112` hoelzl@51531 ` 113` ```lemma BseqI2': "\n\N. norm (X n) \ K \ Bseq X" ``` hoelzl@51531 ` 114` ``` by (intro BfunI) (auto simp: eventually_sequentially) ``` hoelzl@51531 ` 115` hoelzl@51531 ` 116` ```lemma Bseq_def: "Bseq X \ (\K>0. \n. norm (X n) \ K)" ``` hoelzl@51531 ` 117` ``` unfolding Bfun_def eventually_sequentially ``` hoelzl@51531 ` 118` ```proof safe ``` hoelzl@51531 ` 119` ``` fix N K assume "0 < K" "\n\N. norm (X n) \ K" ``` hoelzl@51531 ` 120` ``` then show "\K>0. \n. norm (X n) \ K" ``` haftmann@54863 ` 121` ``` by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] max.strict_coboundedI2) ``` hoelzl@51531 ` 122` ``` (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj) ``` hoelzl@51531 ` 123` ```qed auto ``` hoelzl@51531 ` 124` hoelzl@51531 ` 125` ```lemma BseqE: "\Bseq X; \K. \0 < K; \n. norm (X n) \ K\ \ Q\ \ Q" ``` hoelzl@51531 ` 126` ```unfolding Bseq_def by auto ``` hoelzl@51531 ` 127` hoelzl@51531 ` 128` ```lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. norm (X n) \ K)" ``` hoelzl@51531 ` 129` ```by (simp add: Bseq_def) ``` hoelzl@51531 ` 130` hoelzl@51531 ` 131` ```lemma BseqI: "[| 0 < K; \n. norm (X n) \ K |] ==> Bseq X" ``` hoelzl@51531 ` 132` ```by (auto simp add: Bseq_def) ``` hoelzl@51531 ` 133` hoelzl@54263 ` 134` ```lemma Bseq_bdd_above: "Bseq (X::nat \ real) \ bdd_above (range X)" ``` hoelzl@54263 ` 135` ```proof (elim BseqE, intro bdd_aboveI2) ``` hoelzl@54263 ` 136` ``` fix K n assume "0 < K" "\n. norm (X n) \ K" then show "X n \ K" ``` hoelzl@54263 ` 137` ``` by (auto elim!: allE[of _ n]) ``` hoelzl@54263 ` 138` ```qed ``` hoelzl@54263 ` 139` hoelzl@54263 ` 140` ```lemma Bseq_bdd_below: "Bseq (X::nat \ real) \ bdd_below (range X)" ``` hoelzl@54263 ` 141` ```proof (elim BseqE, intro bdd_belowI2) ``` hoelzl@54263 ` 142` ``` fix K n assume "0 < K" "\n. norm (X n) \ K" then show "- K \ X n" ``` hoelzl@54263 ` 143` ``` by (auto elim!: allE[of _ n]) ``` hoelzl@54263 ` 144` ```qed ``` hoelzl@54263 ` 145` hoelzl@51531 ` 146` ```lemma lemma_NBseq_def: ``` hoelzl@51531 ` 147` ``` "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) \ real(Suc N))" ``` hoelzl@51531 ` 148` ```proof safe ``` hoelzl@51531 ` 149` ``` fix K :: real ``` hoelzl@51531 ` 150` ``` from reals_Archimedean2 obtain n :: nat where "K < real n" .. ``` hoelzl@51531 ` 151` ``` then have "K \ real (Suc n)" by auto ``` hoelzl@51531 ` 152` ``` moreover assume "\m. norm (X m) \ K" ``` hoelzl@51531 ` 153` ``` ultimately have "\m. norm (X m) \ real (Suc n)" ``` hoelzl@51531 ` 154` ``` by (blast intro: order_trans) ``` hoelzl@51531 ` 155` ``` then show "\N. \n. norm (X n) \ real (Suc N)" .. ``` hoelzl@51531 ` 156` ```qed (force simp add: real_of_nat_Suc) ``` hoelzl@51531 ` 157` wenzelm@60758 ` 158` ```text\alternative definition for Bseq\ ``` hoelzl@51531 ` 159` ```lemma Bseq_iff: "Bseq X = (\N. \n. norm (X n) \ real(Suc N))" ``` hoelzl@51531 ` 160` ```apply (simp add: Bseq_def) ``` hoelzl@51531 ` 161` ```apply (simp (no_asm) add: lemma_NBseq_def) ``` hoelzl@51531 ` 162` ```done ``` hoelzl@51531 ` 163` hoelzl@51531 ` 164` ```lemma lemma_NBseq_def2: ``` hoelzl@51531 ` 165` ``` "(\K > 0. \n. norm (X n) \ K) = (\N. \n. norm (X n) < real(Suc N))" ``` hoelzl@51531 ` 166` ```apply (subst lemma_NBseq_def, auto) ``` hoelzl@51531 ` 167` ```apply (rule_tac x = "Suc N" in exI) ``` hoelzl@51531 ` 168` ```apply (rule_tac [2] x = N in exI) ``` hoelzl@51531 ` 169` ```apply (auto simp add: real_of_nat_Suc) ``` hoelzl@51531 ` 170` ``` prefer 2 apply (blast intro: order_less_imp_le) ``` hoelzl@51531 ` 171` ```apply (drule_tac x = n in spec, simp) ``` hoelzl@51531 ` 172` ```done ``` hoelzl@51531 ` 173` hoelzl@51531 ` 174` ```(* yet another definition for Bseq *) ``` hoelzl@51531 ` 175` ```lemma Bseq_iff1a: "Bseq X = (\N. \n. norm (X n) < real(Suc N))" ``` hoelzl@51531 ` 176` ```by (simp add: Bseq_def lemma_NBseq_def2) ``` hoelzl@51531 ` 177` wenzelm@60758 ` 178` ```subsubsection\A Few More Equivalence Theorems for Boundedness\ ``` hoelzl@51531 ` 179` wenzelm@60758 ` 180` ```text\alternative formulation for boundedness\ ``` hoelzl@51531 ` 181` ```lemma Bseq_iff2: "Bseq X = (\k > 0. \x. \n. norm (X(n) + -x) \ k)" ``` hoelzl@51531 ` 182` ```apply (unfold Bseq_def, safe) ``` hoelzl@51531 ` 183` ```apply (rule_tac [2] x = "k + norm x" in exI) ``` hoelzl@51531 ` 184` ```apply (rule_tac x = K in exI, simp) ``` hoelzl@51531 ` 185` ```apply (rule exI [where x = 0], auto) ``` hoelzl@51531 ` 186` ```apply (erule order_less_le_trans, simp) ``` haftmann@54230 ` 187` ```apply (drule_tac x=n in spec) ``` hoelzl@51531 ` 188` ```apply (drule order_trans [OF norm_triangle_ineq2]) ``` hoelzl@51531 ` 189` ```apply simp ``` hoelzl@51531 ` 190` ```done ``` hoelzl@51531 ` 191` wenzelm@60758 ` 192` ```text\alternative formulation for boundedness\ ``` haftmann@53602 ` 193` ```lemma Bseq_iff3: ``` haftmann@53602 ` 194` ``` "Bseq X \ (\k>0. \N. \n. norm (X n + - X N) \ k)" (is "?P \ ?Q") ``` haftmann@53602 ` 195` ```proof ``` haftmann@53602 ` 196` ``` assume ?P ``` haftmann@53602 ` 197` ``` then obtain K ``` haftmann@53602 ` 198` ``` where *: "0 < K" and **: "\n. norm (X n) \ K" by (auto simp add: Bseq_def) ``` haftmann@53602 ` 199` ``` from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp ``` haftmann@54230 ` 200` ``` from ** have "\n. norm (X n - X 0) \ K + norm (X 0)" ``` haftmann@54230 ` 201` ``` by (auto intro: order_trans norm_triangle_ineq4) ``` haftmann@54230 ` 202` ``` then have "\n. norm (X n + - X 0) \ K + norm (X 0)" ``` haftmann@54230 ` 203` ``` by simp ``` wenzelm@60758 ` 204` ``` with \0 < K + norm (X 0)\ show ?Q by blast ``` haftmann@53602 ` 205` ```next ``` haftmann@53602 ` 206` ``` assume ?Q then show ?P by (auto simp add: Bseq_iff2) ``` haftmann@53602 ` 207` ```qed ``` hoelzl@51531 ` 208` hoelzl@51531 ` 209` ```lemma BseqI2: "(\n. k \ f n & f n \ (K::real)) ==> Bseq f" ``` hoelzl@51531 ` 210` ```apply (simp add: Bseq_def) ``` hoelzl@51531 ` 211` ```apply (rule_tac x = " (\k\ + \K\) + 1" in exI, auto) ``` hoelzl@51531 ` 212` ```apply (drule_tac x = n in spec, arith) ``` hoelzl@51531 ` 213` ```done ``` hoelzl@51531 ` 214` haftmann@54230 ` 215` wenzelm@60758 ` 216` ```subsubsection\Upper Bounds and Lubs of Bounded Sequences\ ``` hoelzl@51531 ` 217` hoelzl@51531 ` 218` ```lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X" ``` hoelzl@51531 ` 219` ``` by (simp add: Bseq_def) ``` hoelzl@51531 ` 220` hoelzl@51531 ` 221` ```lemma Bseq_eq_bounded: "range f \ {a .. b::real} \ Bseq f" ``` hoelzl@51531 ` 222` ``` apply (simp add: subset_eq) ``` hoelzl@51531 ` 223` ``` apply (rule BseqI'[where K="max (norm a) (norm b)"]) ``` hoelzl@51531 ` 224` ``` apply (erule_tac x=n in allE) ``` hoelzl@51531 ` 225` ``` apply auto ``` hoelzl@51531 ` 226` ``` done ``` hoelzl@51531 ` 227` hoelzl@51531 ` 228` ```lemma incseq_bounded: "incseq X \ \i. X i \ (B::real) \ Bseq X" ``` hoelzl@51531 ` 229` ``` by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def) ``` hoelzl@51531 ` 230` hoelzl@51531 ` 231` ```lemma decseq_bounded: "decseq X \ \i. (B::real) \ X i \ Bseq X" ``` hoelzl@51531 ` 232` ``` by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def) ``` hoelzl@51531 ` 233` wenzelm@60758 ` 234` ```subsection \Bounded Monotonic Sequences\ ``` hoelzl@51531 ` 235` wenzelm@60758 ` 236` ```subsubsection\A Bounded and Monotonic Sequence Converges\ ``` hoelzl@51531 ` 237` hoelzl@51531 ` 238` ```(* TODO: delete *) ``` hoelzl@51531 ` 239` ```(* FIXME: one use in NSA/HSEQ.thy *) ``` hoelzl@51531 ` 240` ```lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" ``` hoelzl@51531 ` 241` ``` apply (rule_tac x="X m" in exI) ``` hoelzl@51531 ` 242` ``` apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const]) ``` hoelzl@51531 ` 243` ``` unfolding eventually_sequentially ``` hoelzl@51531 ` 244` ``` apply blast ``` hoelzl@51531 ` 245` ``` done ``` hoelzl@51531 ` 246` wenzelm@60758 ` 247` ```subsection \Convergence to Zero\ ``` huffman@31349 ` 248` huffman@44081 ` 249` ```definition Zfun :: "('a \ 'b::real_normed_vector) \ 'a filter \ bool" ``` huffman@44195 ` 250` ``` where "Zfun f F = (\r>0. eventually (\x. norm (f x) < r) F)" ``` huffman@31349 ` 251` huffman@31349 ` 252` ```lemma ZfunI: ``` huffman@44195 ` 253` ``` "(\r. 0 < r \ eventually (\x. norm (f x) < r) F) \ Zfun f F" ``` huffman@44081 ` 254` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 255` huffman@31349 ` 256` ```lemma ZfunD: ``` huffman@44195 ` 257` ``` "\Zfun f F; 0 < r\ \ eventually (\x. norm (f x) < r) F" ``` huffman@44081 ` 258` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 259` huffman@31355 ` 260` ```lemma Zfun_ssubst: ``` huffman@44195 ` 261` ``` "eventually (\x. f x = g x) F \ Zfun g F \ Zfun f F" ``` huffman@44081 ` 262` ``` unfolding Zfun_def by (auto elim!: eventually_rev_mp) ``` huffman@31355 ` 263` huffman@44195 ` 264` ```lemma Zfun_zero: "Zfun (\x. 0) F" ``` huffman@44081 ` 265` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 266` huffman@44195 ` 267` ```lemma Zfun_norm_iff: "Zfun (\x. norm (f x)) F = Zfun (\x. f x) F" ``` huffman@44081 ` 268` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 269` huffman@31349 ` 270` ```lemma Zfun_imp_Zfun: ``` huffman@44195 ` 271` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 272` ``` assumes g: "eventually (\x. norm (g x) \ norm (f x) * K) F" ``` huffman@44195 ` 273` ``` shows "Zfun (\x. g x) F" ``` huffman@31349 ` 274` ```proof (cases) ``` huffman@31349 ` 275` ``` assume K: "0 < K" ``` huffman@31349 ` 276` ``` show ?thesis ``` huffman@31349 ` 277` ``` proof (rule ZfunI) ``` huffman@31349 ` 278` ``` fix r::real assume "0 < r" ``` nipkow@56541 ` 279` ``` hence "0 < r / K" using K by simp ``` huffman@44195 ` 280` ``` then have "eventually (\x. norm (f x) < r / K) F" ``` huffman@31487 ` 281` ``` using ZfunD [OF f] by fast ``` huffman@44195 ` 282` ``` with g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 283` ``` proof eventually_elim ``` noschinl@46887 ` 284` ``` case (elim x) ``` huffman@31487 ` 285` ``` hence "norm (f x) * K < r" ``` huffman@31349 ` 286` ``` by (simp add: pos_less_divide_eq K) ``` noschinl@46887 ` 287` ``` thus ?case ``` noschinl@46887 ` 288` ``` by (simp add: order_le_less_trans [OF elim(1)]) ``` huffman@31349 ` 289` ``` qed ``` huffman@31349 ` 290` ``` qed ``` huffman@31349 ` 291` ```next ``` huffman@31349 ` 292` ``` assume "\ 0 < K" ``` huffman@31349 ` 293` ``` hence K: "K \ 0" by (simp only: not_less) ``` huffman@31355 ` 294` ``` show ?thesis ``` huffman@31355 ` 295` ``` proof (rule ZfunI) ``` huffman@31355 ` 296` ``` fix r :: real ``` huffman@31355 ` 297` ``` assume "0 < r" ``` huffman@44195 ` 298` ``` from g show "eventually (\x. norm (g x) < r) F" ``` noschinl@46887 ` 299` ``` proof eventually_elim ``` noschinl@46887 ` 300` ``` case (elim x) ``` noschinl@46887 ` 301` ``` also have "norm (f x) * K \ norm (f x) * 0" ``` huffman@31355 ` 302` ``` using K norm_ge_zero by (rule mult_left_mono) ``` noschinl@46887 ` 303` ``` finally show ?case ``` wenzelm@60758 ` 304` ``` using \0 < r\ by simp ``` huffman@31355 ` 305` ``` qed ``` huffman@31355 ` 306` ``` qed ``` huffman@31349 ` 307` ```qed ``` huffman@31349 ` 308` huffman@44195 ` 309` ```lemma Zfun_le: "\Zfun g F; \x. norm (f x) \ norm (g x)\ \ Zfun f F" ``` huffman@44081 ` 310` ``` by (erule_tac K="1" in Zfun_imp_Zfun, simp) ``` huffman@31349 ` 311` huffman@31349 ` 312` ```lemma Zfun_add: ``` huffman@44195 ` 313` ``` assumes f: "Zfun f F" and g: "Zfun g F" ``` huffman@44195 ` 314` ``` shows "Zfun (\x. f x + g x) F" ``` huffman@31349 ` 315` ```proof (rule ZfunI) ``` huffman@31349 ` 316` ``` fix r::real assume "0 < r" ``` huffman@31349 ` 317` ``` hence r: "0 < r / 2" by simp ``` huffman@44195 ` 318` ``` have "eventually (\x. norm (f x) < r/2) F" ``` huffman@31487 ` 319` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 320` ``` moreover ``` huffman@44195 ` 321` ``` have "eventually (\x. norm (g x) < r/2) F" ``` huffman@31487 ` 322` ``` using g r by (rule ZfunD) ``` huffman@31349 ` 323` ``` ultimately ``` huffman@44195 ` 324` ``` show "eventually (\x. norm (f x + g x) < r) F" ``` noschinl@46887 ` 325` ``` proof eventually_elim ``` noschinl@46887 ` 326` ``` case (elim x) ``` huffman@31487 ` 327` ``` have "norm (f x + g x) \ norm (f x) + norm (g x)" ``` huffman@31349 ` 328` ``` by (rule norm_triangle_ineq) ``` huffman@31349 ` 329` ``` also have "\ < r/2 + r/2" ``` noschinl@46887 ` 330` ``` using elim by (rule add_strict_mono) ``` noschinl@46887 ` 331` ``` finally show ?case ``` huffman@31349 ` 332` ``` by simp ``` huffman@31349 ` 333` ``` qed ``` huffman@31349 ` 334` ```qed ``` huffman@31349 ` 335` huffman@44195 ` 336` ```lemma Zfun_minus: "Zfun f F \ Zfun (\x. - f x) F" ``` huffman@44081 ` 337` ``` unfolding Zfun_def by simp ``` huffman@31349 ` 338` huffman@44195 ` 339` ```lemma Zfun_diff: "\Zfun f F; Zfun g F\ \ Zfun (\x. f x - g x) F" ``` haftmann@54230 ` 340` ``` using Zfun_add [of f F "\x. - g x"] by (simp add: Zfun_minus) ``` huffman@31349 ` 341` huffman@31349 ` 342` ```lemma (in bounded_linear) Zfun: ``` huffman@44195 ` 343` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 344` ``` shows "Zfun (\x. f (g x)) F" ``` huffman@31349 ` 345` ```proof - ``` huffman@31349 ` 346` ``` obtain K where "\x. norm (f x) \ norm x * K" ``` huffman@31349 ` 347` ``` using bounded by fast ``` huffman@44195 ` 348` ``` then have "eventually (\x. norm (f (g x)) \ norm (g x) * K) F" ``` huffman@31355 ` 349` ``` by simp ``` huffman@31487 ` 350` ``` with g show ?thesis ``` huffman@31349 ` 351` ``` by (rule Zfun_imp_Zfun) ``` huffman@31349 ` 352` ```qed ``` huffman@31349 ` 353` huffman@31349 ` 354` ```lemma (in bounded_bilinear) Zfun: ``` huffman@44195 ` 355` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 356` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 357` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31349 ` 358` ```proof (rule ZfunI) ``` huffman@31349 ` 359` ``` fix r::real assume r: "0 < r" ``` huffman@31349 ` 360` ``` obtain K where K: "0 < K" ``` huffman@31349 ` 361` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31349 ` 362` ``` using pos_bounded by fast ``` huffman@31349 ` 363` ``` from K have K': "0 < inverse K" ``` huffman@31349 ` 364` ``` by (rule positive_imp_inverse_positive) ``` huffman@44195 ` 365` ``` have "eventually (\x. norm (f x) < r) F" ``` huffman@31487 ` 366` ``` using f r by (rule ZfunD) ``` huffman@31349 ` 367` ``` moreover ``` huffman@44195 ` 368` ``` have "eventually (\x. norm (g x) < inverse K) F" ``` huffman@31487 ` 369` ``` using g K' by (rule ZfunD) ``` huffman@31349 ` 370` ``` ultimately ``` huffman@44195 ` 371` ``` show "eventually (\x. norm (f x ** g x) < r) F" ``` noschinl@46887 ` 372` ``` proof eventually_elim ``` noschinl@46887 ` 373` ``` case (elim x) ``` huffman@31487 ` 374` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31349 ` 375` ``` by (rule norm_le) ``` huffman@31487 ` 376` ``` also have "norm (f x) * norm (g x) * K < r * inverse K * K" ``` noschinl@46887 ` 377` ``` by (intro mult_strict_right_mono mult_strict_mono' norm_ge_zero elim K) ``` huffman@31349 ` 378` ``` also from K have "r * inverse K * K = r" ``` huffman@31349 ` 379` ``` by simp ``` noschinl@46887 ` 380` ``` finally show ?case . ``` huffman@31349 ` 381` ``` qed ``` huffman@31349 ` 382` ```qed ``` huffman@31349 ` 383` huffman@31349 ` 384` ```lemma (in bounded_bilinear) Zfun_left: ``` huffman@44195 ` 385` ``` "Zfun f F \ Zfun (\x. f x ** a) F" ``` huffman@44081 ` 386` ``` by (rule bounded_linear_left [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 387` huffman@31349 ` 388` ```lemma (in bounded_bilinear) Zfun_right: ``` huffman@44195 ` 389` ``` "Zfun f F \ Zfun (\x. a ** f x) F" ``` huffman@44081 ` 390` ``` by (rule bounded_linear_right [THEN bounded_linear.Zfun]) ``` huffman@31349 ` 391` huffman@44282 ` 392` ```lemmas Zfun_mult = bounded_bilinear.Zfun [OF bounded_bilinear_mult] ``` huffman@44282 ` 393` ```lemmas Zfun_mult_right = bounded_bilinear.Zfun_right [OF bounded_bilinear_mult] ``` huffman@44282 ` 394` ```lemmas Zfun_mult_left = bounded_bilinear.Zfun_left [OF bounded_bilinear_mult] ``` huffman@31349 ` 395` huffman@44195 ` 396` ```lemma tendsto_Zfun_iff: "(f ---> a) F = Zfun (\x. f x - a) F" ``` huffman@44081 ` 397` ``` by (simp only: tendsto_iff Zfun_def dist_norm) ``` huffman@31349 ` 398` lp15@60141 ` 399` ```lemma tendsto_0_le: "\(f ---> 0) F; eventually (\x. norm (g x) \ norm (f x) * K) F\ ``` lp15@56366 ` 400` ``` \ (g ---> 0) F" ``` lp15@56366 ` 401` ``` by (simp add: Zfun_imp_Zfun tendsto_Zfun_iff) ``` lp15@56366 ` 402` wenzelm@60758 ` 403` ```subsubsection \Distance and norms\ ``` huffman@36662 ` 404` hoelzl@51531 ` 405` ```lemma tendsto_dist [tendsto_intros]: ``` hoelzl@51531 ` 406` ``` fixes l m :: "'a :: metric_space" ``` hoelzl@51531 ` 407` ``` assumes f: "(f ---> l) F" and g: "(g ---> m) F" ``` hoelzl@51531 ` 408` ``` shows "((\x. dist (f x) (g x)) ---> dist l m) F" ``` hoelzl@51531 ` 409` ```proof (rule tendstoI) ``` hoelzl@51531 ` 410` ``` fix e :: real assume "0 < e" ``` hoelzl@51531 ` 411` ``` hence e2: "0 < e/2" by simp ``` hoelzl@51531 ` 412` ``` from tendstoD [OF f e2] tendstoD [OF g e2] ``` hoelzl@51531 ` 413` ``` show "eventually (\x. dist (dist (f x) (g x)) (dist l m) < e) F" ``` hoelzl@51531 ` 414` ``` proof (eventually_elim) ``` hoelzl@51531 ` 415` ``` case (elim x) ``` hoelzl@51531 ` 416` ``` then show "dist (dist (f x) (g x)) (dist l m) < e" ``` hoelzl@51531 ` 417` ``` unfolding dist_real_def ``` hoelzl@51531 ` 418` ``` using dist_triangle2 [of "f x" "g x" "l"] ``` hoelzl@51531 ` 419` ``` using dist_triangle2 [of "g x" "l" "m"] ``` hoelzl@51531 ` 420` ``` using dist_triangle3 [of "l" "m" "f x"] ``` hoelzl@51531 ` 421` ``` using dist_triangle [of "f x" "m" "g x"] ``` hoelzl@51531 ` 422` ``` by arith ``` hoelzl@51531 ` 423` ``` qed ``` hoelzl@51531 ` 424` ```qed ``` hoelzl@51531 ` 425` hoelzl@51531 ` 426` ```lemma continuous_dist[continuous_intros]: ``` hoelzl@51531 ` 427` ``` fixes f g :: "_ \ 'a :: metric_space" ``` hoelzl@51531 ` 428` ``` shows "continuous F f \ continuous F g \ continuous F (\x. dist (f x) (g x))" ``` hoelzl@51531 ` 429` ``` unfolding continuous_def by (rule tendsto_dist) ``` hoelzl@51531 ` 430` hoelzl@56371 ` 431` ```lemma continuous_on_dist[continuous_intros]: ``` hoelzl@51531 ` 432` ``` fixes f g :: "_ \ 'a :: metric_space" ``` hoelzl@51531 ` 433` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. dist (f x) (g x))" ``` hoelzl@51531 ` 434` ``` unfolding continuous_on_def by (auto intro: tendsto_dist) ``` hoelzl@51531 ` 435` huffman@31565 ` 436` ```lemma tendsto_norm [tendsto_intros]: ``` huffman@44195 ` 437` ``` "(f ---> a) F \ ((\x. norm (f x)) ---> norm a) F" ``` huffman@44081 ` 438` ``` unfolding norm_conv_dist by (intro tendsto_intros) ``` huffman@36662 ` 439` hoelzl@51478 ` 440` ```lemma continuous_norm [continuous_intros]: ``` hoelzl@51478 ` 441` ``` "continuous F f \ continuous F (\x. norm (f x))" ``` hoelzl@51478 ` 442` ``` unfolding continuous_def by (rule tendsto_norm) ``` hoelzl@51478 ` 443` hoelzl@56371 ` 444` ```lemma continuous_on_norm [continuous_intros]: ``` hoelzl@51478 ` 445` ``` "continuous_on s f \ continuous_on s (\x. norm (f x))" ``` hoelzl@51478 ` 446` ``` unfolding continuous_on_def by (auto intro: tendsto_norm) ``` hoelzl@51478 ` 447` huffman@36662 ` 448` ```lemma tendsto_norm_zero: ``` huffman@44195 ` 449` ``` "(f ---> 0) F \ ((\x. norm (f x)) ---> 0) F" ``` huffman@44081 ` 450` ``` by (drule tendsto_norm, simp) ``` huffman@36662 ` 451` huffman@36662 ` 452` ```lemma tendsto_norm_zero_cancel: ``` huffman@44195 ` 453` ``` "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" ``` huffman@44081 ` 454` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@36662 ` 455` huffman@36662 ` 456` ```lemma tendsto_norm_zero_iff: ``` huffman@44195 ` 457` ``` "((\x. norm (f x)) ---> 0) F \ (f ---> 0) F" ``` huffman@44081 ` 458` ``` unfolding tendsto_iff dist_norm by simp ``` huffman@31349 ` 459` huffman@44194 ` 460` ```lemma tendsto_rabs [tendsto_intros]: ``` huffman@44195 ` 461` ``` "(f ---> (l::real)) F \ ((\x. \f x\) ---> \l\) F" ``` huffman@44194 ` 462` ``` by (fold real_norm_def, rule tendsto_norm) ``` huffman@44194 ` 463` hoelzl@51478 ` 464` ```lemma continuous_rabs [continuous_intros]: ``` hoelzl@51478 ` 465` ``` "continuous F f \ continuous F (\x. \f x :: real\)" ``` hoelzl@51478 ` 466` ``` unfolding real_norm_def[symmetric] by (rule continuous_norm) ``` hoelzl@51478 ` 467` hoelzl@56371 ` 468` ```lemma continuous_on_rabs [continuous_intros]: ``` hoelzl@51478 ` 469` ``` "continuous_on s f \ continuous_on s (\x. \f x :: real\)" ``` hoelzl@51478 ` 470` ``` unfolding real_norm_def[symmetric] by (rule continuous_on_norm) ``` hoelzl@51478 ` 471` huffman@44194 ` 472` ```lemma tendsto_rabs_zero: ``` huffman@44195 ` 473` ``` "(f ---> (0::real)) F \ ((\x. \f x\) ---> 0) F" ``` huffman@44194 ` 474` ``` by (fold real_norm_def, rule tendsto_norm_zero) ``` huffman@44194 ` 475` huffman@44194 ` 476` ```lemma tendsto_rabs_zero_cancel: ``` huffman@44195 ` 477` ``` "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" ``` huffman@44194 ` 478` ``` by (fold real_norm_def, rule tendsto_norm_zero_cancel) ``` huffman@44194 ` 479` huffman@44194 ` 480` ```lemma tendsto_rabs_zero_iff: ``` huffman@44195 ` 481` ``` "((\x. \f x\) ---> (0::real)) F \ (f ---> 0) F" ``` huffman@44194 ` 482` ``` by (fold real_norm_def, rule tendsto_norm_zero_iff) ``` huffman@44194 ` 483` wenzelm@60758 ` 484` ```subsubsection \Addition and subtraction\ ``` huffman@44194 ` 485` huffman@31565 ` 486` ```lemma tendsto_add [tendsto_intros]: ``` huffman@31349 ` 487` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44195 ` 488` ``` shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x + g x) ---> a + b) F" ``` huffman@44081 ` 489` ``` by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) ``` huffman@31349 ` 490` hoelzl@51478 ` 491` ```lemma continuous_add [continuous_intros]: ``` hoelzl@51478 ` 492` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 493` ``` shows "continuous F f \ continuous F g \ continuous F (\x. f x + g x)" ``` hoelzl@51478 ` 494` ``` unfolding continuous_def by (rule tendsto_add) ``` hoelzl@51478 ` 495` hoelzl@56371 ` 496` ```lemma continuous_on_add [continuous_intros]: ``` hoelzl@51478 ` 497` ``` fixes f g :: "_ \ 'b::real_normed_vector" ``` hoelzl@51478 ` 498` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x + g x)" ``` hoelzl@51478 ` 499` ``` unfolding continuous_on_def by (auto intro: tendsto_add) ``` hoelzl@51478 ` 500` huffman@44194 ` 501` ```lemma tendsto_add_zero: ``` hoelzl@51478 ` 502` ``` fixes f g :: "_ \ 'b::real_normed_vector" ``` huffman@44195 ` 503` ``` shows "\(f ---> 0) F; (g ---> 0) F\ \ ((\x. f x + g x) ---> 0) F" ``` huffman@44194 ` 504` ``` by (drule (1) tendsto_add, simp) ``` huffman@44194 ` 505` huffman@31565 ` 506` ```lemma tendsto_minus [tendsto_intros]: ``` huffman@31349 ` 507` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44195 ` 508` ``` shows "(f ---> a) F \ ((\x. - f x) ---> - a) F" ``` huffman@44081 ` 509` ``` by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus) ``` huffman@31349 ` 510` hoelzl@51478 ` 511` ```lemma continuous_minus [continuous_intros]: ``` hoelzl@51478 ` 512` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 513` ``` shows "continuous F f \ continuous F (\x. - f x)" ``` hoelzl@51478 ` 514` ``` unfolding continuous_def by (rule tendsto_minus) ``` hoelzl@51478 ` 515` hoelzl@56371 ` 516` ```lemma continuous_on_minus [continuous_intros]: ``` hoelzl@51478 ` 517` ``` fixes f :: "_ \ 'b::real_normed_vector" ``` hoelzl@51478 ` 518` ``` shows "continuous_on s f \ continuous_on s (\x. - f x)" ``` hoelzl@51478 ` 519` ``` unfolding continuous_on_def by (auto intro: tendsto_minus) ``` hoelzl@51478 ` 520` huffman@31349 ` 521` ```lemma tendsto_minus_cancel: ``` huffman@31349 ` 522` ``` fixes a :: "'a::real_normed_vector" ``` huffman@44195 ` 523` ``` shows "((\x. - f x) ---> - a) F \ (f ---> a) F" ``` huffman@44081 ` 524` ``` by (drule tendsto_minus, simp) ``` huffman@31349 ` 525` hoelzl@50330 ` 526` ```lemma tendsto_minus_cancel_left: ``` hoelzl@50330 ` 527` ``` "(f ---> - (y::_::real_normed_vector)) F \ ((\x. - f x) ---> y) F" ``` hoelzl@50330 ` 528` ``` using tendsto_minus_cancel[of f "- y" F] tendsto_minus[of f "- y" F] ``` hoelzl@50330 ` 529` ``` by auto ``` hoelzl@50330 ` 530` huffman@31565 ` 531` ```lemma tendsto_diff [tendsto_intros]: ``` huffman@31349 ` 532` ``` fixes a b :: "'a::real_normed_vector" ``` huffman@44195 ` 533` ``` shows "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x - g x) ---> a - b) F" ``` haftmann@54230 ` 534` ``` using tendsto_add [of f a F "\x. - g x" "- b"] by (simp add: tendsto_minus) ``` huffman@31349 ` 535` hoelzl@51478 ` 536` ```lemma continuous_diff [continuous_intros]: ``` hoelzl@51478 ` 537` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 538` ``` shows "continuous F f \ continuous F g \ continuous F (\x. f x - g x)" ``` hoelzl@51478 ` 539` ``` unfolding continuous_def by (rule tendsto_diff) ``` hoelzl@51478 ` 540` hoelzl@56371 ` 541` ```lemma continuous_on_diff [continuous_intros]: ``` hoelzl@51478 ` 542` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 543` ``` shows "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x - g x)" ``` hoelzl@51478 ` 544` ``` unfolding continuous_on_def by (auto intro: tendsto_diff) ``` hoelzl@51478 ` 545` huffman@31588 ` 546` ```lemma tendsto_setsum [tendsto_intros]: ``` huffman@31588 ` 547` ``` fixes f :: "'a \ 'b \ 'c::real_normed_vector" ``` huffman@44195 ` 548` ``` assumes "\i. i \ S \ (f i ---> a i) F" ``` huffman@44195 ` 549` ``` shows "((\x. \i\S. f i x) ---> (\i\S. a i)) F" ``` huffman@31588 ` 550` ```proof (cases "finite S") ``` huffman@31588 ` 551` ``` assume "finite S" thus ?thesis using assms ``` hoelzl@58729 ` 552` ``` by (induct, simp, simp add: tendsto_add) ``` hoelzl@58729 ` 553` ```qed simp ``` huffman@31588 ` 554` hoelzl@51478 ` 555` ```lemma continuous_setsum [continuous_intros]: ``` hoelzl@51478 ` 556` ``` fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" ``` hoelzl@51478 ` 557` ``` shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" ``` hoelzl@51478 ` 558` ``` unfolding continuous_def by (rule tendsto_setsum) ``` hoelzl@51478 ` 559` hoelzl@51478 ` 560` ```lemma continuous_on_setsum [continuous_intros]: ``` hoelzl@51478 ` 561` ``` fixes f :: "'a \ _ \ 'c::real_normed_vector" ``` hoelzl@51478 ` 562` ``` shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" ``` hoelzl@51478 ` 563` ``` unfolding continuous_on_def by (auto intro: tendsto_setsum) ``` hoelzl@51478 ` 564` hoelzl@50999 ` 565` ```lemmas real_tendsto_sandwich = tendsto_sandwich[where 'b=real] ``` hoelzl@50999 ` 566` wenzelm@60758 ` 567` ```subsubsection \Linear operators and multiplication\ ``` huffman@44194 ` 568` huffman@44282 ` 569` ```lemma (in bounded_linear) tendsto: ``` huffman@44195 ` 570` ``` "(g ---> a) F \ ((\x. f (g x)) ---> f a) F" ``` huffman@44081 ` 571` ``` by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) ``` huffman@31349 ` 572` hoelzl@51478 ` 573` ```lemma (in bounded_linear) continuous: ``` hoelzl@51478 ` 574` ``` "continuous F g \ continuous F (\x. f (g x))" ``` hoelzl@51478 ` 575` ``` using tendsto[of g _ F] by (auto simp: continuous_def) ``` hoelzl@51478 ` 576` hoelzl@51478 ` 577` ```lemma (in bounded_linear) continuous_on: ``` hoelzl@51478 ` 578` ``` "continuous_on s g \ continuous_on s (\x. f (g x))" ``` hoelzl@51478 ` 579` ``` using tendsto[of g] by (auto simp: continuous_on_def) ``` hoelzl@51478 ` 580` huffman@44194 ` 581` ```lemma (in bounded_linear) tendsto_zero: ``` huffman@44195 ` 582` ``` "(g ---> 0) F \ ((\x. f (g x)) ---> 0) F" ``` huffman@44194 ` 583` ``` by (drule tendsto, simp only: zero) ``` huffman@44194 ` 584` huffman@44282 ` 585` ```lemma (in bounded_bilinear) tendsto: ``` huffman@44195 ` 586` ``` "\(f ---> a) F; (g ---> b) F\ \ ((\x. f x ** g x) ---> a ** b) F" ``` huffman@44081 ` 587` ``` by (simp only: tendsto_Zfun_iff prod_diff_prod ``` huffman@44081 ` 588` ``` Zfun_add Zfun Zfun_left Zfun_right) ``` huffman@31349 ` 589` hoelzl@51478 ` 590` ```lemma (in bounded_bilinear) continuous: ``` hoelzl@51478 ` 591` ``` "continuous F f \ continuous F g \ continuous F (\x. f x ** g x)" ``` hoelzl@51478 ` 592` ``` using tendsto[of f _ F g] by (auto simp: continuous_def) ``` hoelzl@51478 ` 593` hoelzl@51478 ` 594` ```lemma (in bounded_bilinear) continuous_on: ``` hoelzl@51478 ` 595` ``` "continuous_on s f \ continuous_on s g \ continuous_on s (\x. f x ** g x)" ``` hoelzl@51478 ` 596` ``` using tendsto[of f _ _ g] by (auto simp: continuous_on_def) ``` hoelzl@51478 ` 597` huffman@44194 ` 598` ```lemma (in bounded_bilinear) tendsto_zero: ``` huffman@44195 ` 599` ``` assumes f: "(f ---> 0) F" ``` huffman@44195 ` 600` ``` assumes g: "(g ---> 0) F" ``` huffman@44195 ` 601` ``` shows "((\x. f x ** g x) ---> 0) F" ``` huffman@44194 ` 602` ``` using tendsto [OF f g] by (simp add: zero_left) ``` huffman@31355 ` 603` huffman@44194 ` 604` ```lemma (in bounded_bilinear) tendsto_left_zero: ``` huffman@44195 ` 605` ``` "(f ---> 0) F \ ((\x. f x ** c) ---> 0) F" ``` huffman@44194 ` 606` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) ``` huffman@44194 ` 607` huffman@44194 ` 608` ```lemma (in bounded_bilinear) tendsto_right_zero: ``` huffman@44195 ` 609` ``` "(f ---> 0) F \ ((\x. c ** f x) ---> 0) F" ``` huffman@44194 ` 610` ``` by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) ``` huffman@44194 ` 611` huffman@44282 ` 612` ```lemmas tendsto_of_real [tendsto_intros] = ``` huffman@44282 ` 613` ``` bounded_linear.tendsto [OF bounded_linear_of_real] ``` huffman@44282 ` 614` huffman@44282 ` 615` ```lemmas tendsto_scaleR [tendsto_intros] = ``` huffman@44282 ` 616` ``` bounded_bilinear.tendsto [OF bounded_bilinear_scaleR] ``` huffman@44282 ` 617` huffman@44282 ` 618` ```lemmas tendsto_mult [tendsto_intros] = ``` huffman@44282 ` 619` ``` bounded_bilinear.tendsto [OF bounded_bilinear_mult] ``` huffman@44194 ` 620` hoelzl@51478 ` 621` ```lemmas continuous_of_real [continuous_intros] = ``` hoelzl@51478 ` 622` ``` bounded_linear.continuous [OF bounded_linear_of_real] ``` hoelzl@51478 ` 623` hoelzl@51478 ` 624` ```lemmas continuous_scaleR [continuous_intros] = ``` hoelzl@51478 ` 625` ``` bounded_bilinear.continuous [OF bounded_bilinear_scaleR] ``` hoelzl@51478 ` 626` hoelzl@51478 ` 627` ```lemmas continuous_mult [continuous_intros] = ``` hoelzl@51478 ` 628` ``` bounded_bilinear.continuous [OF bounded_bilinear_mult] ``` hoelzl@51478 ` 629` hoelzl@56371 ` 630` ```lemmas continuous_on_of_real [continuous_intros] = ``` hoelzl@51478 ` 631` ``` bounded_linear.continuous_on [OF bounded_linear_of_real] ``` hoelzl@51478 ` 632` hoelzl@56371 ` 633` ```lemmas continuous_on_scaleR [continuous_intros] = ``` hoelzl@51478 ` 634` ``` bounded_bilinear.continuous_on [OF bounded_bilinear_scaleR] ``` hoelzl@51478 ` 635` hoelzl@56371 ` 636` ```lemmas continuous_on_mult [continuous_intros] = ``` hoelzl@51478 ` 637` ``` bounded_bilinear.continuous_on [OF bounded_bilinear_mult] ``` hoelzl@51478 ` 638` huffman@44568 ` 639` ```lemmas tendsto_mult_zero = ``` huffman@44568 ` 640` ``` bounded_bilinear.tendsto_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 641` huffman@44568 ` 642` ```lemmas tendsto_mult_left_zero = ``` huffman@44568 ` 643` ``` bounded_bilinear.tendsto_left_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 644` huffman@44568 ` 645` ```lemmas tendsto_mult_right_zero = ``` huffman@44568 ` 646` ``` bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult] ``` huffman@44568 ` 647` huffman@44194 ` 648` ```lemma tendsto_power [tendsto_intros]: ``` huffman@44194 ` 649` ``` fixes f :: "'a \ 'b::{power,real_normed_algebra}" ``` huffman@44195 ` 650` ``` shows "(f ---> a) F \ ((\x. f x ^ n) ---> a ^ n) F" ``` hoelzl@58729 ` 651` ``` by (induct n) (simp_all add: tendsto_mult) ``` huffman@44194 ` 652` hoelzl@51478 ` 653` ```lemma continuous_power [continuous_intros]: ``` hoelzl@51478 ` 654` ``` fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` hoelzl@51478 ` 655` ``` shows "continuous F f \ continuous F (\x. (f x)^n)" ``` hoelzl@51478 ` 656` ``` unfolding continuous_def by (rule tendsto_power) ``` hoelzl@51478 ` 657` hoelzl@56371 ` 658` ```lemma continuous_on_power [continuous_intros]: ``` hoelzl@51478 ` 659` ``` fixes f :: "_ \ 'b::{power,real_normed_algebra}" ``` hoelzl@51478 ` 660` ``` shows "continuous_on s f \ continuous_on s (\x. (f x)^n)" ``` hoelzl@51478 ` 661` ``` unfolding continuous_on_def by (auto intro: tendsto_power) ``` hoelzl@51478 ` 662` huffman@44194 ` 663` ```lemma tendsto_setprod [tendsto_intros]: ``` huffman@44194 ` 664` ``` fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" ``` huffman@44195 ` 665` ``` assumes "\i. i \ S \ (f i ---> L i) F" ``` huffman@44195 ` 666` ``` shows "((\x. \i\S. f i x) ---> (\i\S. L i)) F" ``` huffman@44194 ` 667` ```proof (cases "finite S") ``` huffman@44194 ` 668` ``` assume "finite S" thus ?thesis using assms ``` hoelzl@58729 ` 669` ``` by (induct, simp, simp add: tendsto_mult) ``` hoelzl@58729 ` 670` ```qed simp ``` huffman@44194 ` 671` hoelzl@51478 ` 672` ```lemma continuous_setprod [continuous_intros]: ``` hoelzl@51478 ` 673` ``` fixes f :: "'a \ 'b::t2_space \ 'c::{real_normed_algebra,comm_ring_1}" ``` hoelzl@51478 ` 674` ``` shows "(\i. i \ S \ continuous F (f i)) \ continuous F (\x. \i\S. f i x)" ``` hoelzl@51478 ` 675` ``` unfolding continuous_def by (rule tendsto_setprod) ``` hoelzl@51478 ` 676` hoelzl@51478 ` 677` ```lemma continuous_on_setprod [continuous_intros]: ``` hoelzl@51478 ` 678` ``` fixes f :: "'a \ _ \ 'c::{real_normed_algebra,comm_ring_1}" ``` hoelzl@51478 ` 679` ``` shows "(\i. i \ S \ continuous_on s (f i)) \ continuous_on s (\x. \i\S. f i x)" ``` hoelzl@51478 ` 680` ``` unfolding continuous_on_def by (auto intro: tendsto_setprod) ``` hoelzl@51478 ` 681` wenzelm@60758 ` 682` ```subsubsection \Inverse and division\ ``` huffman@31355 ` 683` huffman@31355 ` 684` ```lemma (in bounded_bilinear) Zfun_prod_Bfun: ``` huffman@44195 ` 685` ``` assumes f: "Zfun f F" ``` huffman@44195 ` 686` ``` assumes g: "Bfun g F" ``` huffman@44195 ` 687` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@31355 ` 688` ```proof - ``` huffman@31355 ` 689` ``` obtain K where K: "0 \ K" ``` huffman@31355 ` 690` ``` and norm_le: "\x y. norm (x ** y) \ norm x * norm y * K" ``` huffman@31355 ` 691` ``` using nonneg_bounded by fast ``` huffman@31355 ` 692` ``` obtain B where B: "0 < B" ``` huffman@44195 ` 693` ``` and norm_g: "eventually (\x. norm (g x) \ B) F" ``` huffman@31487 ` 694` ``` using g by (rule BfunE) ``` huffman@44195 ` 695` ``` have "eventually (\x. norm (f x ** g x) \ norm (f x) * (B * K)) F" ``` noschinl@46887 ` 696` ``` using norm_g proof eventually_elim ``` noschinl@46887 ` 697` ``` case (elim x) ``` huffman@31487 ` 698` ``` have "norm (f x ** g x) \ norm (f x) * norm (g x) * K" ``` huffman@31355 ` 699` ``` by (rule norm_le) ``` huffman@31487 ` 700` ``` also have "\ \ norm (f x) * B * K" ``` huffman@31487 ` 701` ``` by (intro mult_mono' order_refl norm_g norm_ge_zero ``` noschinl@46887 ` 702` ``` mult_nonneg_nonneg K elim) ``` huffman@31487 ` 703` ``` also have "\ = norm (f x) * (B * K)" ``` haftmann@57512 ` 704` ``` by (rule mult.assoc) ``` huffman@31487 ` 705` ``` finally show "norm (f x ** g x) \ norm (f x) * (B * K)" . ``` huffman@31355 ` 706` ``` qed ``` huffman@31487 ` 707` ``` with f show ?thesis ``` huffman@31487 ` 708` ``` by (rule Zfun_imp_Zfun) ``` huffman@31355 ` 709` ```qed ``` huffman@31355 ` 710` huffman@31355 ` 711` ```lemma (in bounded_bilinear) flip: ``` huffman@31355 ` 712` ``` "bounded_bilinear (\x y. y ** x)" ``` huffman@44081 ` 713` ``` apply default ``` huffman@44081 ` 714` ``` apply (rule add_right) ``` huffman@44081 ` 715` ``` apply (rule add_left) ``` huffman@44081 ` 716` ``` apply (rule scaleR_right) ``` huffman@44081 ` 717` ``` apply (rule scaleR_left) ``` haftmann@57512 ` 718` ``` apply (subst mult.commute) ``` huffman@44081 ` 719` ``` using bounded by fast ``` huffman@31355 ` 720` huffman@31355 ` 721` ```lemma (in bounded_bilinear) Bfun_prod_Zfun: ``` huffman@44195 ` 722` ``` assumes f: "Bfun f F" ``` huffman@44195 ` 723` ``` assumes g: "Zfun g F" ``` huffman@44195 ` 724` ``` shows "Zfun (\x. f x ** g x) F" ``` huffman@44081 ` 725` ``` using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) ``` huffman@31355 ` 726` huffman@31355 ` 727` ```lemma Bfun_inverse_lemma: ``` huffman@31355 ` 728` ``` fixes x :: "'a::real_normed_div_algebra" ``` huffman@31355 ` 729` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` huffman@44081 ` 730` ``` apply (subst nonzero_norm_inverse, clarsimp) ``` huffman@44081 ` 731` ``` apply (erule (1) le_imp_inverse_le) ``` huffman@44081 ` 732` ``` done ``` huffman@31355 ` 733` huffman@31355 ` 734` ```lemma Bfun_inverse: ``` huffman@31355 ` 735` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44195 ` 736` ``` assumes f: "(f ---> a) F" ``` huffman@31355 ` 737` ``` assumes a: "a \ 0" ``` huffman@44195 ` 738` ``` shows "Bfun (\x. inverse (f x)) F" ``` huffman@31355 ` 739` ```proof - ``` huffman@31355 ` 740` ``` from a have "0 < norm a" by simp ``` huffman@31355 ` 741` ``` hence "\r>0. r < norm a" by (rule dense) ``` huffman@31355 ` 742` ``` then obtain r where r1: "0 < r" and r2: "r < norm a" by fast ``` huffman@44195 ` 743` ``` have "eventually (\x. dist (f x) a < r) F" ``` huffman@31487 ` 744` ``` using tendstoD [OF f r1] by fast ``` huffman@44195 ` 745` ``` hence "eventually (\x. norm (inverse (f x)) \ inverse (norm a - r)) F" ``` noschinl@46887 ` 746` ``` proof eventually_elim ``` noschinl@46887 ` 747` ``` case (elim x) ``` huffman@31487 ` 748` ``` hence 1: "norm (f x - a) < r" ``` huffman@31355 ` 749` ``` by (simp add: dist_norm) ``` huffman@31487 ` 750` ``` hence 2: "f x \ 0" using r2 by auto ``` huffman@31487 ` 751` ``` hence "norm (inverse (f x)) = inverse (norm (f x))" ``` huffman@31355 ` 752` ``` by (rule nonzero_norm_inverse) ``` huffman@31355 ` 753` ``` also have "\ \ inverse (norm a - r)" ``` huffman@31355 ` 754` ``` proof (rule le_imp_inverse_le) ``` huffman@31355 ` 755` ``` show "0 < norm a - r" using r2 by simp ``` huffman@31355 ` 756` ``` next ``` huffman@31487 ` 757` ``` have "norm a - norm (f x) \ norm (a - f x)" ``` huffman@31355 ` 758` ``` by (rule norm_triangle_ineq2) ``` huffman@31487 ` 759` ``` also have "\ = norm (f x - a)" ``` huffman@31355 ` 760` ``` by (rule norm_minus_commute) ``` huffman@31355 ` 761` ``` also have "\ < r" using 1 . ``` huffman@31487 ` 762` ``` finally show "norm a - r \ norm (f x)" by simp ``` huffman@31355 ` 763` ``` qed ``` huffman@31487 ` 764` ``` finally show "norm (inverse (f x)) \ inverse (norm a - r)" . ``` huffman@31355 ` 765` ``` qed ``` huffman@31355 ` 766` ``` thus ?thesis by (rule BfunI) ``` huffman@31355 ` 767` ```qed ``` huffman@31355 ` 768` huffman@31565 ` 769` ```lemma tendsto_inverse [tendsto_intros]: ``` huffman@31355 ` 770` ``` fixes a :: "'a::real_normed_div_algebra" ``` huffman@44195 ` 771` ``` assumes f: "(f ---> a) F" ``` huffman@31355 ` 772` ``` assumes a: "a \ 0" ``` huffman@44195 ` 773` ``` shows "((\x. inverse (f x)) ---> inverse a) F" ``` huffman@31355 ` 774` ```proof - ``` huffman@31355 ` 775` ``` from a have "0 < norm a" by simp ``` huffman@44195 ` 776` ``` with f have "eventually (\x. dist (f x) a < norm a) F" ``` huffman@31355 ` 777` ``` by (rule tendstoD) ``` huffman@44195 ` 778` ``` then have "eventually (\x. f x \ 0) F" ``` huffman@31355 ` 779` ``` unfolding dist_norm by (auto elim!: eventually_elim1) ``` huffman@44627 ` 780` ``` with a have "eventually (\x. inverse (f x) - inverse a = ``` huffman@44627 ` 781` ``` - (inverse (f x) * (f x - a) * inverse a)) F" ``` huffman@44627 ` 782` ``` by (auto elim!: eventually_elim1 simp: inverse_diff_inverse) ``` huffman@44627 ` 783` ``` moreover have "Zfun (\x. - (inverse (f x) * (f x - a) * inverse a)) F" ``` huffman@44627 ` 784` ``` by (intro Zfun_minus Zfun_mult_left ``` huffman@44627 ` 785` ``` bounded_bilinear.Bfun_prod_Zfun [OF bounded_bilinear_mult] ``` huffman@44627 ` 786` ``` Bfun_inverse [OF f a] f [unfolded tendsto_Zfun_iff]) ``` huffman@44627 ` 787` ``` ultimately show ?thesis ``` huffman@44627 ` 788` ``` unfolding tendsto_Zfun_iff by (rule Zfun_ssubst) ``` huffman@31355 ` 789` ```qed ``` huffman@31355 ` 790` hoelzl@51478 ` 791` ```lemma continuous_inverse: ``` hoelzl@51478 ` 792` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` hoelzl@51478 ` 793` ``` assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 794` ``` shows "continuous F (\x. inverse (f x))" ``` hoelzl@51478 ` 795` ``` using assms unfolding continuous_def by (rule tendsto_inverse) ``` hoelzl@51478 ` 796` hoelzl@51478 ` 797` ```lemma continuous_at_within_inverse[continuous_intros]: ``` hoelzl@51478 ` 798` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` hoelzl@51478 ` 799` ``` assumes "continuous (at a within s) f" and "f a \ 0" ``` hoelzl@51478 ` 800` ``` shows "continuous (at a within s) (\x. inverse (f x))" ``` hoelzl@51478 ` 801` ``` using assms unfolding continuous_within by (rule tendsto_inverse) ``` hoelzl@51478 ` 802` hoelzl@51478 ` 803` ```lemma isCont_inverse[continuous_intros, simp]: ``` hoelzl@51478 ` 804` ``` fixes f :: "'a::t2_space \ 'b::real_normed_div_algebra" ``` hoelzl@51478 ` 805` ``` assumes "isCont f a" and "f a \ 0" ``` hoelzl@51478 ` 806` ``` shows "isCont (\x. inverse (f x)) a" ``` hoelzl@51478 ` 807` ``` using assms unfolding continuous_at by (rule tendsto_inverse) ``` hoelzl@51478 ` 808` hoelzl@56371 ` 809` ```lemma continuous_on_inverse[continuous_intros]: ``` hoelzl@51478 ` 810` ``` fixes f :: "'a::topological_space \ 'b::real_normed_div_algebra" ``` hoelzl@51478 ` 811` ``` assumes "continuous_on s f" and "\x\s. f x \ 0" ``` hoelzl@51478 ` 812` ``` shows "continuous_on s (\x. inverse (f x))" ``` hoelzl@51478 ` 813` ``` using assms unfolding continuous_on_def by (fast intro: tendsto_inverse) ``` hoelzl@51478 ` 814` huffman@31565 ` 815` ```lemma tendsto_divide [tendsto_intros]: ``` huffman@31355 ` 816` ``` fixes a b :: "'a::real_normed_field" ``` huffman@44195 ` 817` ``` shows "\(f ---> a) F; (g ---> b) F; b \ 0\ ``` huffman@44195 ` 818` ``` \ ((\x. f x / g x) ---> a / b) F" ``` huffman@44282 ` 819` ``` by (simp add: tendsto_mult tendsto_inverse divide_inverse) ``` huffman@31355 ` 820` hoelzl@51478 ` 821` ```lemma continuous_divide: ``` hoelzl@51478 ` 822` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` hoelzl@51478 ` 823` ``` assumes "continuous F f" and "continuous F g" and "g (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 824` ``` shows "continuous F (\x. (f x) / (g x))" ``` hoelzl@51478 ` 825` ``` using assms unfolding continuous_def by (rule tendsto_divide) ``` hoelzl@51478 ` 826` hoelzl@51478 ` 827` ```lemma continuous_at_within_divide[continuous_intros]: ``` hoelzl@51478 ` 828` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` hoelzl@51478 ` 829` ``` assumes "continuous (at a within s) f" "continuous (at a within s) g" and "g a \ 0" ``` hoelzl@51478 ` 830` ``` shows "continuous (at a within s) (\x. (f x) / (g x))" ``` hoelzl@51478 ` 831` ``` using assms unfolding continuous_within by (rule tendsto_divide) ``` hoelzl@51478 ` 832` hoelzl@51478 ` 833` ```lemma isCont_divide[continuous_intros, simp]: ``` hoelzl@51478 ` 834` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_field" ``` hoelzl@51478 ` 835` ``` assumes "isCont f a" "isCont g a" "g a \ 0" ``` hoelzl@51478 ` 836` ``` shows "isCont (\x. (f x) / g x) a" ``` hoelzl@51478 ` 837` ``` using assms unfolding continuous_at by (rule tendsto_divide) ``` hoelzl@51478 ` 838` hoelzl@56371 ` 839` ```lemma continuous_on_divide[continuous_intros]: ``` hoelzl@51478 ` 840` ``` fixes f :: "'a::topological_space \ 'b::real_normed_field" ``` hoelzl@51478 ` 841` ``` assumes "continuous_on s f" "continuous_on s g" and "\x\s. g x \ 0" ``` hoelzl@51478 ` 842` ``` shows "continuous_on s (\x. (f x) / (g x))" ``` hoelzl@51478 ` 843` ``` using assms unfolding continuous_on_def by (fast intro: tendsto_divide) ``` hoelzl@51478 ` 844` huffman@44194 ` 845` ```lemma tendsto_sgn [tendsto_intros]: ``` huffman@44194 ` 846` ``` fixes l :: "'a::real_normed_vector" ``` huffman@44195 ` 847` ``` shows "\(f ---> l) F; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) F" ``` huffman@44194 ` 848` ``` unfolding sgn_div_norm by (simp add: tendsto_intros) ``` huffman@44194 ` 849` hoelzl@51478 ` 850` ```lemma continuous_sgn: ``` hoelzl@51478 ` 851` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 852` ``` assumes "continuous F f" and "f (Lim F (\x. x)) \ 0" ``` hoelzl@51478 ` 853` ``` shows "continuous F (\x. sgn (f x))" ``` hoelzl@51478 ` 854` ``` using assms unfolding continuous_def by (rule tendsto_sgn) ``` hoelzl@51478 ` 855` hoelzl@51478 ` 856` ```lemma continuous_at_within_sgn[continuous_intros]: ``` hoelzl@51478 ` 857` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 858` ``` assumes "continuous (at a within s) f" and "f a \ 0" ``` hoelzl@51478 ` 859` ``` shows "continuous (at a within s) (\x. sgn (f x))" ``` hoelzl@51478 ` 860` ``` using assms unfolding continuous_within by (rule tendsto_sgn) ``` hoelzl@51478 ` 861` hoelzl@51478 ` 862` ```lemma isCont_sgn[continuous_intros]: ``` hoelzl@51478 ` 863` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 864` ``` assumes "isCont f a" and "f a \ 0" ``` hoelzl@51478 ` 865` ``` shows "isCont (\x. sgn (f x)) a" ``` hoelzl@51478 ` 866` ``` using assms unfolding continuous_at by (rule tendsto_sgn) ``` hoelzl@51478 ` 867` hoelzl@56371 ` 868` ```lemma continuous_on_sgn[continuous_intros]: ``` hoelzl@51478 ` 869` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 870` ``` assumes "continuous_on s f" and "\x\s. f x \ 0" ``` hoelzl@51478 ` 871` ``` shows "continuous_on s (\x. sgn (f x))" ``` hoelzl@51478 ` 872` ``` using assms unfolding continuous_on_def by (fast intro: tendsto_sgn) ``` hoelzl@51478 ` 873` hoelzl@50325 ` 874` ```lemma filterlim_at_infinity: ``` wenzelm@61076 ` 875` ``` fixes f :: "_ \ 'a::real_normed_vector" ``` hoelzl@50325 ` 876` ``` assumes "0 \ c" ``` hoelzl@50325 ` 877` ``` shows "(LIM x F. f x :> at_infinity) \ (\r>c. eventually (\x. r \ norm (f x)) F)" ``` hoelzl@50325 ` 878` ``` unfolding filterlim_iff eventually_at_infinity ``` hoelzl@50325 ` 879` ```proof safe ``` hoelzl@50325 ` 880` ``` fix P :: "'a \ bool" and b ``` hoelzl@50325 ` 881` ``` assume *: "\r>c. eventually (\x. r \ norm (f x)) F" ``` hoelzl@50325 ` 882` ``` and P: "\x. b \ norm x \ P x" ``` hoelzl@50325 ` 883` ``` have "max b (c + 1) > c" by auto ``` hoelzl@50325 ` 884` ``` with * have "eventually (\x. max b (c + 1) \ norm (f x)) F" ``` hoelzl@50325 ` 885` ``` by auto ``` hoelzl@50325 ` 886` ``` then show "eventually (\x. P (f x)) F" ``` hoelzl@50325 ` 887` ``` proof eventually_elim ``` hoelzl@50325 ` 888` ``` fix x assume "max b (c + 1) \ norm (f x)" ``` hoelzl@50325 ` 889` ``` with P show "P (f x)" by auto ``` hoelzl@50325 ` 890` ``` qed ``` hoelzl@50325 ` 891` ```qed force ``` hoelzl@50325 ` 892` wenzelm@60758 ` 893` ```subsection \Relate @{const at}, @{const at_left} and @{const at_right}\ ``` hoelzl@50347 ` 894` wenzelm@60758 ` 895` ```text \ ``` hoelzl@50347 ` 896` hoelzl@50347 ` 897` ```This lemmas are useful for conversion between @{term "at x"} to @{term "at_left x"} and ``` hoelzl@50347 ` 898` ```@{term "at_right x"} and also @{term "at_right 0"}. ``` hoelzl@50347 ` 899` wenzelm@60758 ` 900` ```\ ``` hoelzl@50347 ` 901` hoelzl@51471 ` 902` ```lemmas filterlim_split_at_real = filterlim_split_at[where 'a=real] ``` hoelzl@50323 ` 903` hoelzl@51641 ` 904` ```lemma filtermap_nhds_shift: "filtermap (\x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)" ``` hoelzl@60721 ` 905` ``` by (rule filtermap_fun_inverse[where g="\x. x + d"]) ``` hoelzl@60721 ` 906` ``` (auto intro!: tendsto_eq_intros filterlim_ident) ``` hoelzl@50347 ` 907` hoelzl@51641 ` 908` ```lemma filtermap_nhds_minus: "filtermap (\x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)" ``` hoelzl@60721 ` 909` ``` by (rule filtermap_fun_inverse[where g=uminus]) ``` hoelzl@60721 ` 910` ``` (auto intro!: tendsto_eq_intros filterlim_ident) ``` hoelzl@51641 ` 911` hoelzl@51641 ` 912` ```lemma filtermap_at_shift: "filtermap (\x. x - d) (at a) = at (a - d::'a::real_normed_vector)" ``` hoelzl@51641 ` 913` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50347 ` 914` hoelzl@50347 ` 915` ```lemma filtermap_at_right_shift: "filtermap (\x. x - d) (at_right a) = at_right (a - d::real)" ``` hoelzl@51641 ` 916` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50323 ` 917` hoelzl@50347 ` 918` ```lemma at_right_to_0: "at_right (a::real) = filtermap (\x. x + a) (at_right 0)" ``` hoelzl@50347 ` 919` ``` using filtermap_at_right_shift[of "-a" 0] by simp ``` hoelzl@50347 ` 920` hoelzl@50347 ` 921` ```lemma filterlim_at_right_to_0: ``` hoelzl@50347 ` 922` ``` "filterlim f F (at_right (a::real)) \ filterlim (\x. f (x + a)) F (at_right 0)" ``` hoelzl@50347 ` 923` ``` unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. ``` hoelzl@50347 ` 924` hoelzl@50347 ` 925` ```lemma eventually_at_right_to_0: ``` hoelzl@50347 ` 926` ``` "eventually P (at_right (a::real)) \ eventually (\x. P (x + a)) (at_right 0)" ``` hoelzl@50347 ` 927` ``` unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 928` hoelzl@51641 ` 929` ```lemma filtermap_at_minus: "filtermap (\x. - x) (at a) = at (- a::'a::real_normed_vector)" ``` hoelzl@51641 ` 930` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 931` hoelzl@50347 ` 932` ```lemma at_left_minus: "at_left (a::real) = filtermap (\x. - x) (at_right (- a))" ``` hoelzl@51641 ` 933` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50323 ` 934` hoelzl@50347 ` 935` ```lemma at_right_minus: "at_right (a::real) = filtermap (\x. - x) (at_left (- a))" ``` hoelzl@51641 ` 936` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 937` hoelzl@50347 ` 938` ```lemma filterlim_at_left_to_right: ``` hoelzl@50347 ` 939` ``` "filterlim f F (at_left (a::real)) \ filterlim (\x. f (- x)) F (at_right (-a))" ``` hoelzl@50347 ` 940` ``` unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. ``` hoelzl@50347 ` 941` hoelzl@50347 ` 942` ```lemma eventually_at_left_to_right: ``` hoelzl@50347 ` 943` ``` "eventually P (at_left (a::real)) \ eventually (\x. P (- x)) (at_right (-a))" ``` hoelzl@50347 ` 944` ``` unfolding at_left_minus[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 945` hoelzl@60721 ` 946` ```lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top" ``` hoelzl@60721 ` 947` ``` unfolding filterlim_at_top eventually_at_bot_dense ``` hoelzl@60721 ` 948` ``` by (metis leI minus_less_iff order_less_asym) ``` hoelzl@60721 ` 949` hoelzl@60721 ` 950` ```lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" ``` hoelzl@60721 ` 951` ``` unfolding filterlim_at_bot eventually_at_top_dense ``` hoelzl@60721 ` 952` ``` by (metis leI less_minus_iff order_less_asym) ``` hoelzl@60721 ` 953` hoelzl@50346 ` 954` ```lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)" ``` hoelzl@60721 ` 955` ``` by (rule filtermap_fun_inverse[symmetric, of uminus]) ``` hoelzl@60721 ` 956` ``` (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot) ``` hoelzl@50346 ` 957` hoelzl@50346 ` 958` ```lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)" ``` hoelzl@50346 ` 959` ``` unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident) ``` hoelzl@50346 ` 960` hoelzl@50346 ` 961` ```lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \ (LIM x at_bot. f (-x::real) :> F)" ``` hoelzl@50346 ` 962` ``` unfolding filterlim_def at_top_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 963` hoelzl@50346 ` 964` ```lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \ (LIM x at_top. f (-x::real) :> F)" ``` hoelzl@50346 ` 965` ``` unfolding filterlim_def at_bot_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 966` hoelzl@50346 ` 967` ```lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \ (LIM x F. - (f x) :: real :> at_bot)" ``` hoelzl@50346 ` 968` ``` using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] ``` hoelzl@50346 ` 969` ``` using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\x. - f x" F] ``` hoelzl@50346 ` 970` ``` by auto ``` hoelzl@50346 ` 971` hoelzl@50346 ` 972` ```lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \ (LIM x F. - (f x) :: real :> at_top)" ``` hoelzl@50346 ` 973` ``` unfolding filterlim_uminus_at_top by simp ``` hoelzl@50323 ` 974` hoelzl@50347 ` 975` ```lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" ``` hoelzl@51641 ` 976` ``` unfolding filterlim_at_top_gt[where c=0] eventually_at_filter ``` hoelzl@50347 ` 977` ```proof safe ``` hoelzl@50347 ` 978` ``` fix Z :: real assume [arith]: "0 < Z" ``` hoelzl@50347 ` 979` ``` then have "eventually (\x. x < inverse Z) (nhds 0)" ``` hoelzl@50347 ` 980` ``` by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\inverse Z\"]) ``` hoelzl@51641 ` 981` ``` then show "eventually (\x. x \ 0 \ x \ {0<..} \ Z \ inverse x) (nhds 0)" ``` hoelzl@50347 ` 982` ``` by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps) ``` hoelzl@50347 ` 983` ```qed ``` hoelzl@50347 ` 984` hoelzl@50325 ` 985` ```lemma tendsto_inverse_0: ``` wenzelm@61076 ` 986` ``` fixes x :: "_ \ 'a::real_normed_div_algebra" ``` hoelzl@50325 ` 987` ``` shows "(inverse ---> (0::'a)) at_infinity" ``` hoelzl@50325 ` 988` ``` unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity ``` hoelzl@50325 ` 989` ```proof safe ``` hoelzl@50325 ` 990` ``` fix r :: real assume "0 < r" ``` hoelzl@50325 ` 991` ``` show "\b. \x. b \ norm x \ norm (inverse x :: 'a) < r" ``` hoelzl@50325 ` 992` ``` proof (intro exI[of _ "inverse (r / 2)"] allI impI) ``` hoelzl@50325 ` 993` ``` fix x :: 'a ``` wenzelm@60758 ` 994` ``` from \0 < r\ have "0 < inverse (r / 2)" by simp ``` hoelzl@50325 ` 995` ``` also assume *: "inverse (r / 2) \ norm x" ``` hoelzl@50325 ` 996` ``` finally show "norm (inverse x) < r" ``` wenzelm@60758 ` 997` ``` using * \0 < r\ by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) ``` hoelzl@50325 ` 998` ``` qed ``` hoelzl@50325 ` 999` ```qed ``` hoelzl@50325 ` 1000` hoelzl@60721 ` 1001` ```lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)" ``` hoelzl@60721 ` 1002` ``` unfolding filterlim_at ``` hoelzl@60721 ` 1003` ``` by (auto simp: eventually_at_top_dense) ``` hoelzl@60721 ` 1004` ``` (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) ``` hoelzl@60721 ` 1005` hoelzl@60721 ` 1006` ```lemma filterlim_inverse_at_top: ``` hoelzl@60721 ` 1007` ``` "(f ---> (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" ``` hoelzl@60721 ` 1008` ``` by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) ``` hoelzl@60721 ` 1009` ``` (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal) ``` hoelzl@60721 ` 1010` hoelzl@60721 ` 1011` ```lemma filterlim_inverse_at_bot_neg: ``` hoelzl@60721 ` 1012` ``` "LIM x (at_left (0::real)). inverse x :> at_bot" ``` hoelzl@60721 ` 1013` ``` by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) ``` hoelzl@60721 ` 1014` hoelzl@60721 ` 1015` ```lemma filterlim_inverse_at_bot: ``` hoelzl@60721 ` 1016` ``` "(f ---> (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" ``` hoelzl@60721 ` 1017` ``` unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] ``` hoelzl@60721 ` 1018` ``` by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) ``` hoelzl@60721 ` 1019` hoelzl@50347 ` 1020` ```lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" ``` hoelzl@60721 ` 1021` ``` by (intro filtermap_fun_inverse[symmetric, where g=inverse]) ``` hoelzl@60721 ` 1022` ``` (auto intro: filterlim_inverse_at_top_right filterlim_inverse_at_right_top) ``` hoelzl@50347 ` 1023` hoelzl@50347 ` 1024` ```lemma eventually_at_right_to_top: ``` hoelzl@50347 ` 1025` ``` "eventually P (at_right (0::real)) \ eventually (\x. P (inverse x)) at_top" ``` hoelzl@50347 ` 1026` ``` unfolding at_right_to_top eventually_filtermap .. ``` hoelzl@50347 ` 1027` hoelzl@50347 ` 1028` ```lemma filterlim_at_right_to_top: ``` hoelzl@50347 ` 1029` ``` "filterlim f F (at_right (0::real)) \ (LIM x at_top. f (inverse x) :> F)" ``` hoelzl@50347 ` 1030` ``` unfolding filterlim_def at_right_to_top filtermap_filtermap .. ``` hoelzl@50347 ` 1031` hoelzl@50347 ` 1032` ```lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" ``` hoelzl@50347 ` 1033` ``` unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. ``` hoelzl@50347 ` 1034` hoelzl@50347 ` 1035` ```lemma eventually_at_top_to_right: ``` hoelzl@50347 ` 1036` ``` "eventually P at_top \ eventually (\x. P (inverse x)) (at_right (0::real))" ``` hoelzl@50347 ` 1037` ``` unfolding at_top_to_right eventually_filtermap .. ``` hoelzl@50347 ` 1038` hoelzl@50347 ` 1039` ```lemma filterlim_at_top_to_right: ``` hoelzl@50347 ` 1040` ``` "filterlim f F at_top \ (LIM x (at_right (0::real)). f (inverse x) :> F)" ``` hoelzl@50347 ` 1041` ``` unfolding filterlim_def at_top_to_right filtermap_filtermap .. ``` hoelzl@50347 ` 1042` hoelzl@50325 ` 1043` ```lemma filterlim_inverse_at_infinity: ``` wenzelm@61076 ` 1044` ``` fixes x :: "_ \ 'a::{real_normed_div_algebra, division_ring}" ``` hoelzl@50325 ` 1045` ``` shows "filterlim inverse at_infinity (at (0::'a))" ``` hoelzl@50325 ` 1046` ``` unfolding filterlim_at_infinity[OF order_refl] ``` hoelzl@50325 ` 1047` ```proof safe ``` hoelzl@50325 ` 1048` ``` fix r :: real assume "0 < r" ``` hoelzl@50325 ` 1049` ``` then show "eventually (\x::'a. r \ norm (inverse x)) (at 0)" ``` hoelzl@50325 ` 1050` ``` unfolding eventually_at norm_inverse ``` hoelzl@50325 ` 1051` ``` by (intro exI[of _ "inverse r"]) ``` hoelzl@50325 ` 1052` ``` (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) ``` hoelzl@50325 ` 1053` ```qed ``` hoelzl@50325 ` 1054` hoelzl@50325 ` 1055` ```lemma filterlim_inverse_at_iff: ``` wenzelm@61076 ` 1056` ``` fixes g :: "'a \ 'b::{real_normed_div_algebra, division_ring}" ``` hoelzl@50325 ` 1057` ``` shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" ``` hoelzl@50325 ` 1058` ``` unfolding filterlim_def filtermap_filtermap[symmetric] ``` hoelzl@50325 ` 1059` ```proof ``` hoelzl@50325 ` 1060` ``` assume "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1061` ``` then have "filtermap inverse (filtermap g F) \ filtermap inverse at_infinity" ``` hoelzl@50325 ` 1062` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1063` ``` also have "\ \ at 0" ``` hoelzl@51641 ` 1064` ``` using tendsto_inverse_0[where 'a='b] ``` hoelzl@51641 ` 1065` ``` by (auto intro!: exI[of _ 1] ``` hoelzl@51641 ` 1066` ``` simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity) ``` hoelzl@50325 ` 1067` ``` finally show "filtermap inverse (filtermap g F) \ at 0" . ``` hoelzl@50325 ` 1068` ```next ``` hoelzl@50325 ` 1069` ``` assume "filtermap inverse (filtermap g F) \ at 0" ``` hoelzl@50325 ` 1070` ``` then have "filtermap inverse (filtermap inverse (filtermap g F)) \ filtermap inverse (at 0)" ``` hoelzl@50325 ` 1071` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1072` ``` with filterlim_inverse_at_infinity show "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1073` ``` by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) ``` hoelzl@50325 ` 1074` ```qed ``` hoelzl@50325 ` 1075` hoelzl@51641 ` 1076` ```lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) ---> 0) F" ``` hoelzl@51641 ` 1077` ``` by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) ``` hoelzl@50419 ` 1078` lp15@59613 ` 1079` lp15@59613 ` 1080` ```lemma at_to_infinity: ``` wenzelm@61076 ` 1081` ``` fixes x :: "'a :: {real_normed_field,field}" ``` lp15@59613 ` 1082` ``` shows "(at (0::'a)) = filtermap inverse at_infinity" ``` lp15@59613 ` 1083` ```proof (rule antisym) ``` lp15@59613 ` 1084` ``` have "(inverse ---> (0::'a)) at_infinity" ``` lp15@59613 ` 1085` ``` by (fact tendsto_inverse_0) ``` lp15@59613 ` 1086` ``` then show "filtermap inverse at_infinity \ at (0::'a)" ``` lp15@59613 ` 1087` ``` apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def) ``` lp15@59613 ` 1088` ``` apply (rule_tac x="1" in exI, auto) ``` lp15@59613 ` 1089` ``` done ``` lp15@59613 ` 1090` ```next ``` lp15@59613 ` 1091` ``` have "filtermap inverse (filtermap inverse (at (0::'a))) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1092` ``` using filterlim_inverse_at_infinity unfolding filterlim_def ``` lp15@59613 ` 1093` ``` by (rule filtermap_mono) ``` lp15@59613 ` 1094` ``` then show "at (0::'a) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1095` ``` by (simp add: filtermap_ident filtermap_filtermap) ``` lp15@59613 ` 1096` ```qed ``` lp15@59613 ` 1097` lp15@59613 ` 1098` ```lemma lim_at_infinity_0: ``` haftmann@59867 ` 1099` ``` fixes l :: "'a :: {real_normed_field,field}" ``` lp15@59613 ` 1100` ``` shows "(f ---> l) at_infinity \ ((f o inverse) ---> l) (at (0::'a))" ``` lp15@59613 ` 1101` ```by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) ``` lp15@59613 ` 1102` lp15@59613 ` 1103` ```lemma lim_zero_infinity: ``` haftmann@59867 ` 1104` ``` fixes l :: "'a :: {real_normed_field,field}" ``` lp15@59613 ` 1105` ``` shows "((\x. f(1 / x)) ---> l) (at (0::'a)) \ (f ---> l) at_infinity" ``` lp15@59613 ` 1106` ```by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) ``` lp15@59613 ` 1107` lp15@59613 ` 1108` wenzelm@60758 ` 1109` ```text \ ``` hoelzl@50324 ` 1110` hoelzl@50324 ` 1111` ```We only show rules for multiplication and addition when the functions are either against a real ``` hoelzl@50324 ` 1112` ```value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}. ``` hoelzl@50324 ` 1113` wenzelm@60758 ` 1114` ```\ ``` hoelzl@50324 ` 1115` lp15@60141 ` 1116` ```lemma filterlim_tendsto_pos_mult_at_top: ``` hoelzl@50324 ` 1117` ``` assumes f: "(f ---> c) F" and c: "0 < c" ``` hoelzl@50324 ` 1118` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1119` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1120` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1121` ```proof safe ``` hoelzl@50324 ` 1122` ``` fix Z :: real assume "0 < Z" ``` wenzelm@60758 ` 1123` ``` from f \0 < c\ have "eventually (\x. c / 2 < f x) F" ``` hoelzl@50324 ` 1124` ``` by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1 ``` hoelzl@50324 ` 1125` ``` simp: dist_real_def abs_real_def split: split_if_asm) ``` hoelzl@50346 ` 1126` ``` moreover from g have "eventually (\x. (Z / c * 2) \ g x) F" ``` hoelzl@50324 ` 1127` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1128` ``` ultimately show "eventually (\x. Z \ f x * g x) F" ``` hoelzl@50324 ` 1129` ``` proof eventually_elim ``` hoelzl@50346 ` 1130` ``` fix x assume "c / 2 < f x" "Z / c * 2 \ g x" ``` wenzelm@60758 ` 1131` ``` with \0 < Z\ \0 < c\ have "c / 2 * (Z / c * 2) \ f x * g x" ``` hoelzl@50346 ` 1132` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` wenzelm@60758 ` 1133` ``` with \0 < c\ show "Z \ f x * g x" ``` hoelzl@50324 ` 1134` ``` by simp ``` hoelzl@50324 ` 1135` ``` qed ``` hoelzl@50324 ` 1136` ```qed ``` hoelzl@50324 ` 1137` lp15@60141 ` 1138` ```lemma filterlim_at_top_mult_at_top: ``` hoelzl@50324 ` 1139` ``` assumes f: "LIM x F. f x :> at_top" ``` hoelzl@50324 ` 1140` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1141` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1142` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1143` ```proof safe ``` hoelzl@50324 ` 1144` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50346 ` 1145` ``` from f have "eventually (\x. 1 \ f x) F" ``` hoelzl@50324 ` 1146` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1147` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1148` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1149` ``` ultimately show "eventually (\x. Z \ f x * g x) F" ``` hoelzl@50324 ` 1150` ``` proof eventually_elim ``` hoelzl@50346 ` 1151` ``` fix x assume "1 \ f x" "Z \ g x" ``` wenzelm@60758 ` 1152` ``` with \0 < Z\ have "1 * Z \ f x * g x" ``` hoelzl@50346 ` 1153` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` hoelzl@50346 ` 1154` ``` then show "Z \ f x * g x" ``` hoelzl@50324 ` 1155` ``` by simp ``` hoelzl@50324 ` 1156` ``` qed ``` hoelzl@50324 ` 1157` ```qed ``` hoelzl@50324 ` 1158` hoelzl@50419 ` 1159` ```lemma filterlim_tendsto_pos_mult_at_bot: ``` hoelzl@50419 ` 1160` ``` assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F" ``` hoelzl@50419 ` 1161` ``` shows "LIM x F. f x * g x :> at_bot" ``` hoelzl@50419 ` 1162` ``` using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) ``` hoelzl@50419 ` 1163` ``` unfolding filterlim_uminus_at_bot by simp ``` hoelzl@50419 ` 1164` hoelzl@60182 ` 1165` ```lemma filterlim_tendsto_neg_mult_at_bot: ``` hoelzl@60182 ` 1166` ``` assumes c: "(f ---> c) F" "(c::real) < 0" and g: "filterlim g at_top F" ``` hoelzl@60182 ` 1167` ``` shows "LIM x F. f x * g x :> at_bot" ``` hoelzl@60182 ` 1168` ``` using c filterlim_tendsto_pos_mult_at_top[of "\x. - f x" "- c" F, OF _ _ g] ``` hoelzl@60182 ` 1169` ``` unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp ``` hoelzl@60182 ` 1170` hoelzl@56330 ` 1171` ```lemma filterlim_pow_at_top: ``` hoelzl@56330 ` 1172` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1173` ``` assumes "0 < n" and f: "LIM x F. f x :> at_top" ``` hoelzl@56330 ` 1174` ``` shows "LIM x F. (f x)^n :: real :> at_top" ``` wenzelm@60758 ` 1175` ```using \0 < n\ proof (induct n) ``` hoelzl@56330 ` 1176` ``` case (Suc n) with f show ?case ``` hoelzl@56330 ` 1177` ``` by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) ``` hoelzl@56330 ` 1178` ```qed simp ``` hoelzl@56330 ` 1179` hoelzl@56330 ` 1180` ```lemma filterlim_pow_at_bot_even: ``` hoelzl@56330 ` 1181` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1182` ``` shows "0 < n \ LIM x F. f x :> at_bot \ even n \ LIM x F. (f x)^n :> at_top" ``` hoelzl@56330 ` 1183` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_top) ``` hoelzl@56330 ` 1184` hoelzl@56330 ` 1185` ```lemma filterlim_pow_at_bot_odd: ``` hoelzl@56330 ` 1186` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1187` ``` shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" ``` hoelzl@56330 ` 1188` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) ``` hoelzl@56330 ` 1189` lp15@60141 ` 1190` ```lemma filterlim_tendsto_add_at_top: ``` hoelzl@50324 ` 1191` ``` assumes f: "(f ---> c) F" ``` hoelzl@50324 ` 1192` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1193` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1194` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1195` ```proof safe ``` hoelzl@50324 ` 1196` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50324 ` 1197` ``` from f have "eventually (\x. c - 1 < f x) F" ``` hoelzl@50324 ` 1198` ``` by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def) ``` hoelzl@50346 ` 1199` ``` moreover from g have "eventually (\x. Z - (c - 1) \ g x) F" ``` hoelzl@50324 ` 1200` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1201` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1202` ``` by eventually_elim simp ``` hoelzl@50324 ` 1203` ```qed ``` hoelzl@50324 ` 1204` hoelzl@50347 ` 1205` ```lemma LIM_at_top_divide: ``` hoelzl@50347 ` 1206` ``` fixes f g :: "'a \ real" ``` hoelzl@50347 ` 1207` ``` assumes f: "(f ---> a) F" "0 < a" ``` hoelzl@50347 ` 1208` ``` assumes g: "(g ---> 0) F" "eventually (\x. 0 < g x) F" ``` hoelzl@50347 ` 1209` ``` shows "LIM x F. f x / g x :> at_top" ``` hoelzl@50347 ` 1210` ``` unfolding divide_inverse ``` hoelzl@50347 ` 1211` ``` by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) ``` hoelzl@50347 ` 1212` lp15@60141 ` 1213` ```lemma filterlim_at_top_add_at_top: ``` hoelzl@50324 ` 1214` ``` assumes f: "LIM x F. f x :> at_top" ``` hoelzl@50324 ` 1215` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1216` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1217` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1218` ```proof safe ``` hoelzl@50324 ` 1219` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50346 ` 1220` ``` from f have "eventually (\x. 0 \ f x) F" ``` hoelzl@50324 ` 1221` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1222` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1223` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1224` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1225` ``` by eventually_elim simp ``` hoelzl@50324 ` 1226` ```qed ``` hoelzl@50324 ` 1227` hoelzl@50331 ` 1228` ```lemma tendsto_divide_0: ``` wenzelm@61076 ` 1229` ``` fixes f :: "_ \ 'a::{real_normed_div_algebra, division_ring}" ``` hoelzl@50331 ` 1230` ``` assumes f: "(f ---> c) F" ``` hoelzl@50331 ` 1231` ``` assumes g: "LIM x F. g x :> at_infinity" ``` hoelzl@50331 ` 1232` ``` shows "((\x. f x / g x) ---> 0) F" ``` hoelzl@50331 ` 1233` ``` using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse) ``` hoelzl@50331 ` 1234` hoelzl@50331 ` 1235` ```lemma linear_plus_1_le_power: ``` hoelzl@50331 ` 1236` ``` fixes x :: real ``` hoelzl@50331 ` 1237` ``` assumes x: "0 \ x" ``` hoelzl@50331 ` 1238` ``` shows "real n * x + 1 \ (x + 1) ^ n" ``` hoelzl@50331 ` 1239` ```proof (induct n) ``` hoelzl@50331 ` 1240` ``` case (Suc n) ``` hoelzl@50331 ` 1241` ``` have "real (Suc n) * x + 1 \ (x + 1) * (real n * x + 1)" ``` nipkow@56536 ` 1242` ``` by (simp add: field_simps real_of_nat_Suc x) ``` hoelzl@50331 ` 1243` ``` also have "\ \ (x + 1)^Suc n" ``` hoelzl@50331 ` 1244` ``` using Suc x by (simp add: mult_left_mono) ``` hoelzl@50331 ` 1245` ``` finally show ?case . ``` hoelzl@50331 ` 1246` ```qed simp ``` hoelzl@50331 ` 1247` hoelzl@50331 ` 1248` ```lemma filterlim_realpow_sequentially_gt1: ``` hoelzl@50331 ` 1249` ``` fixes x :: "'a :: real_normed_div_algebra" ``` hoelzl@50331 ` 1250` ``` assumes x[arith]: "1 < norm x" ``` hoelzl@50331 ` 1251` ``` shows "LIM n sequentially. x ^ n :> at_infinity" ``` hoelzl@50331 ` 1252` ```proof (intro filterlim_at_infinity[THEN iffD2] allI impI) ``` hoelzl@50331 ` 1253` ``` fix y :: real assume "0 < y" ``` hoelzl@50331 ` 1254` ``` have "0 < norm x - 1" by simp ``` hoelzl@50331 ` 1255` ``` then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3) ``` hoelzl@50331 ` 1256` ``` also have "\ \ real N * (norm x - 1) + 1" by simp ``` hoelzl@50331 ` 1257` ``` also have "\ \ (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp ``` hoelzl@50331 ` 1258` ``` also have "\ = norm x ^ N" by simp ``` hoelzl@50331 ` 1259` ``` finally have "\n\N. y \ norm x ^ n" ``` hoelzl@50331 ` 1260` ``` by (metis order_less_le_trans power_increasing order_less_imp_le x) ``` hoelzl@50331 ` 1261` ``` then show "eventually (\n. y \ norm (x ^ n)) sequentially" ``` hoelzl@50331 ` 1262` ``` unfolding eventually_sequentially ``` hoelzl@50331 ` 1263` ``` by (auto simp: norm_power) ``` hoelzl@50331 ` 1264` ```qed simp ``` hoelzl@50331 ` 1265` hoelzl@51471 ` 1266` wenzelm@60758 ` 1267` ```subsection \Limits of Sequences\ ``` hoelzl@51526 ` 1268` hoelzl@51526 ` 1269` ```lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" ``` hoelzl@51526 ` 1270` ``` by simp ``` hoelzl@51526 ` 1271` hoelzl@51526 ` 1272` ```lemma LIMSEQ_iff: ``` hoelzl@51526 ` 1273` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1274` ``` shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" ``` lp15@60017 ` 1275` ```unfolding lim_sequentially dist_norm .. ``` hoelzl@51526 ` 1276` hoelzl@51526 ` 1277` ```lemma LIMSEQ_I: ``` hoelzl@51526 ` 1278` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1279` ``` shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" ``` hoelzl@51526 ` 1280` ```by (simp add: LIMSEQ_iff) ``` hoelzl@51526 ` 1281` hoelzl@51526 ` 1282` ```lemma LIMSEQ_D: ``` hoelzl@51526 ` 1283` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1284` ``` shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" ``` hoelzl@51526 ` 1285` ```by (simp add: LIMSEQ_iff) ``` hoelzl@51526 ` 1286` hoelzl@51526 ` 1287` ```lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" ``` hoelzl@51526 ` 1288` ``` unfolding tendsto_def eventually_sequentially ``` haftmann@57512 ` 1289` ``` by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) ``` hoelzl@51526 ` 1290` hoelzl@51526 ` 1291` ```lemma Bseq_inverse_lemma: ``` hoelzl@51526 ` 1292` ``` fixes x :: "'a::real_normed_div_algebra" ``` hoelzl@51526 ` 1293` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` hoelzl@51526 ` 1294` ```apply (subst nonzero_norm_inverse, clarsimp) ``` hoelzl@51526 ` 1295` ```apply (erule (1) le_imp_inverse_le) ``` hoelzl@51526 ` 1296` ```done ``` hoelzl@51526 ` 1297` hoelzl@51526 ` 1298` ```lemma Bseq_inverse: ``` hoelzl@51526 ` 1299` ``` fixes a :: "'a::real_normed_div_algebra" ``` hoelzl@51526 ` 1300` ``` shows "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" ``` hoelzl@51526 ` 1301` ``` by (rule Bfun_inverse) ``` hoelzl@51526 ` 1302` wenzelm@60758 ` 1303` ```text\Transformation of limit.\ ``` lp15@60141 ` 1304` lp15@60141 ` 1305` ```lemma eventually_at2: ``` lp15@60141 ` 1306` ``` "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" ``` lp15@60141 ` 1307` ``` unfolding eventually_at dist_nz by auto ``` lp15@60141 ` 1308` lp15@60141 ` 1309` ```lemma Lim_transform: ``` lp15@60141 ` 1310` ``` fixes a b :: "'a::real_normed_vector" ``` lp15@60141 ` 1311` ``` shows "\(g ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (f ---> a) F" ``` lp15@60141 ` 1312` ``` using tendsto_add [of g a F "\x. f x - g x" 0] by simp ``` lp15@60141 ` 1313` lp15@60141 ` 1314` ```lemma Lim_transform2: ``` lp15@60141 ` 1315` ``` fixes a b :: "'a::real_normed_vector" ``` lp15@60141 ` 1316` ``` shows "\(f ---> a) F; ((\x. f x - g x) ---> 0) F\ \ (g ---> a) F" ``` lp15@60141 ` 1317` ``` by (erule Lim_transform) (simp add: tendsto_minus_cancel) ``` lp15@60141 ` 1318` lp15@60141 ` 1319` ```lemma Lim_transform_eventually: ``` lp15@60141 ` 1320` ``` "eventually (\x. f x = g x) net \ (f ---> l) net \ (g ---> l) net" ``` lp15@60141 ` 1321` ``` apply (rule topological_tendstoI) ``` lp15@60141 ` 1322` ``` apply (drule (2) topological_tendstoD) ``` lp15@60141 ` 1323` ``` apply (erule (1) eventually_elim2, simp) ``` lp15@60141 ` 1324` ``` done ``` lp15@60141 ` 1325` lp15@60141 ` 1326` ```lemma Lim_transform_within: ``` lp15@60141 ` 1327` ``` assumes "0 < d" ``` lp15@60141 ` 1328` ``` and "\x'\S. 0 < dist x' x \ dist x' x < d \ f x' = g x'" ``` lp15@60141 ` 1329` ``` and "(f ---> l) (at x within S)" ``` lp15@60141 ` 1330` ``` shows "(g ---> l) (at x within S)" ``` lp15@60141 ` 1331` ```proof (rule Lim_transform_eventually) ``` lp15@60141 ` 1332` ``` show "eventually (\x. f x = g x) (at x within S)" ``` lp15@60141 ` 1333` ``` using assms(1,2) by (auto simp: dist_nz eventually_at) ``` lp15@60141 ` 1334` ``` show "(f ---> l) (at x within S)" by fact ``` lp15@60141 ` 1335` ```qed ``` lp15@60141 ` 1336` lp15@60141 ` 1337` ```lemma Lim_transform_at: ``` lp15@60141 ` 1338` ``` assumes "0 < d" ``` lp15@60141 ` 1339` ``` and "\x'. 0 < dist x' x \ dist x' x < d \ f x' = g x'" ``` lp15@60141 ` 1340` ``` and "(f ---> l) (at x)" ``` lp15@60141 ` 1341` ``` shows "(g ---> l) (at x)" ``` lp15@60141 ` 1342` ``` using _ assms(3) ``` lp15@60141 ` 1343` ```proof (rule Lim_transform_eventually) ``` lp15@60141 ` 1344` ``` show "eventually (\x. f x = g x) (at x)" ``` lp15@60141 ` 1345` ``` unfolding eventually_at2 ``` lp15@60141 ` 1346` ``` using assms(1,2) by auto ``` lp15@60141 ` 1347` ```qed ``` lp15@60141 ` 1348` wenzelm@60758 ` 1349` ```text\Common case assuming being away from some crucial point like 0.\ ``` hoelzl@51526 ` 1350` lp15@60141 ` 1351` ```lemma Lim_transform_away_within: ``` lp15@60141 ` 1352` ``` fixes a b :: "'a::t1_space" ``` lp15@60141 ` 1353` ``` assumes "a \ b" ``` lp15@60141 ` 1354` ``` and "\x\S. x \ a \ x \ b \ f x = g x" ``` lp15@60141 ` 1355` ``` and "(f ---> l) (at a within S)" ``` lp15@60141 ` 1356` ``` shows "(g ---> l) (at a within S)" ``` lp15@60141 ` 1357` ```proof (rule Lim_transform_eventually) ``` lp15@60141 ` 1358` ``` show "(f ---> l) (at a within S)" by fact ``` lp15@60141 ` 1359` ``` show "eventually (\x. f x = g x) (at a within S)" ``` lp15@60141 ` 1360` ``` unfolding eventually_at_topological ``` lp15@60141 ` 1361` ``` by (rule exI [where x="- {b}"], simp add: open_Compl assms) ``` lp15@60141 ` 1362` ```qed ``` lp15@60141 ` 1363` lp15@60141 ` 1364` ```lemma Lim_transform_away_at: ``` lp15@60141 ` 1365` ``` fixes a b :: "'a::t1_space" ``` lp15@60141 ` 1366` ``` assumes ab: "a\b" ``` lp15@60141 ` 1367` ``` and fg: "\x. x \ a \ x \ b \ f x = g x" ``` lp15@60141 ` 1368` ``` and fl: "(f ---> l) (at a)" ``` lp15@60141 ` 1369` ``` shows "(g ---> l) (at a)" ``` lp15@60141 ` 1370` ``` using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp ``` lp15@60141 ` 1371` wenzelm@60758 ` 1372` ```text\Alternatively, within an open set.\ ``` hoelzl@51526 ` 1373` lp15@60141 ` 1374` ```lemma Lim_transform_within_open: ``` lp15@60141 ` 1375` ``` assumes "open S" and "a \ S" ``` lp15@60141 ` 1376` ``` and "\x\S. x \ a \ f x = g x" ``` lp15@60141 ` 1377` ``` and "(f ---> l) (at a)" ``` lp15@60141 ` 1378` ``` shows "(g ---> l) (at a)" ``` lp15@60141 ` 1379` ```proof (rule Lim_transform_eventually) ``` lp15@60141 ` 1380` ``` show "eventually (\x. f x = g x) (at a)" ``` lp15@60141 ` 1381` ``` unfolding eventually_at_topological ``` lp15@60141 ` 1382` ``` using assms(1,2,3) by auto ``` lp15@60141 ` 1383` ``` show "(f ---> l) (at a)" by fact ``` lp15@60141 ` 1384` ```qed ``` lp15@60141 ` 1385` wenzelm@60758 ` 1386` ```text\A congruence rule allowing us to transform limits assuming not at point.\ ``` lp15@60141 ` 1387` lp15@60141 ` 1388` ```(* FIXME: Only one congruence rule for tendsto can be used at a time! *) ``` lp15@60141 ` 1389` lp15@60141 ` 1390` ```lemma Lim_cong_within(*[cong add]*): ``` lp15@60141 ` 1391` ``` assumes "a = b" ``` lp15@60141 ` 1392` ``` and "x = y" ``` lp15@60141 ` 1393` ``` and "S = T" ``` lp15@60141 ` 1394` ``` and "\x. x \ b \ x \ T \ f x = g x" ``` lp15@60141 ` 1395` ``` shows "(f ---> x) (at a within S) \ (g ---> y) (at b within T)" ``` lp15@60141 ` 1396` ``` unfolding tendsto_def eventually_at_topological ``` lp15@60141 ` 1397` ``` using assms by simp ``` lp15@60141 ` 1398` lp15@60141 ` 1399` ```lemma Lim_cong_at(*[cong add]*): ``` lp15@60141 ` 1400` ``` assumes "a = b" "x = y" ``` lp15@60141 ` 1401` ``` and "\x. x \ a \ f x = g x" ``` lp15@60141 ` 1402` ``` shows "((\x. f x) ---> x) (at a) \ ((g ---> y) (at a))" ``` lp15@60141 ` 1403` ``` unfolding tendsto_def eventually_at_topological ``` lp15@60141 ` 1404` ``` using assms by simp ``` wenzelm@60758 ` 1405` ```text\An unbounded sequence's inverse tends to 0\ ``` hoelzl@51526 ` 1406` hoelzl@51526 ` 1407` ```lemma LIMSEQ_inverse_zero: ``` hoelzl@51526 ` 1408` ``` "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) ----> 0" ``` hoelzl@51526 ` 1409` ``` apply (rule filterlim_compose[OF tendsto_inverse_0]) ``` hoelzl@51526 ` 1410` ``` apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) ``` hoelzl@51526 ` 1411` ``` apply (metis abs_le_D1 linorder_le_cases linorder_not_le) ``` hoelzl@51526 ` 1412` ``` done ``` hoelzl@51526 ` 1413` wenzelm@60758 ` 1414` ```text\The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity\ ``` hoelzl@51526 ` 1415` hoelzl@51526 ` 1416` ```lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" ``` hoelzl@51526 ` 1417` ``` by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc ``` hoelzl@51526 ` 1418` ``` filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity) ``` hoelzl@51526 ` 1419` wenzelm@60758 ` 1420` ```text\The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to ``` wenzelm@60758 ` 1421` ```infinity is now easily proved\ ``` hoelzl@51526 ` 1422` hoelzl@51526 ` 1423` ```lemma LIMSEQ_inverse_real_of_nat_add: ``` hoelzl@51526 ` 1424` ``` "(%n. r + inverse(real(Suc n))) ----> r" ``` hoelzl@51526 ` 1425` ``` using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto ``` hoelzl@51526 ` 1426` hoelzl@51526 ` 1427` ```lemma LIMSEQ_inverse_real_of_nat_add_minus: ``` hoelzl@51526 ` 1428` ``` "(%n. r + -inverse(real(Suc n))) ----> r" ``` hoelzl@51526 ` 1429` ``` using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] ``` hoelzl@51526 ` 1430` ``` by auto ``` hoelzl@51526 ` 1431` hoelzl@51526 ` 1432` ```lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: ``` hoelzl@51526 ` 1433` ``` "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" ``` hoelzl@51526 ` 1434` ``` using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] ``` hoelzl@51526 ` 1435` ``` by auto ``` hoelzl@51526 ` 1436` wenzelm@60758 ` 1437` ```subsection \Convergence on sequences\ ``` hoelzl@51526 ` 1438` hoelzl@51526 ` 1439` ```lemma convergent_add: ``` hoelzl@51526 ` 1440` ``` fixes X Y :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1441` ``` assumes "convergent (\n. X n)" ``` hoelzl@51526 ` 1442` ``` assumes "convergent (\n. Y n)" ``` hoelzl@51526 ` 1443` ``` shows "convergent (\n. X n + Y n)" ``` hoelzl@51526 ` 1444` ``` using assms unfolding convergent_def by (fast intro: tendsto_add) ``` hoelzl@51526 ` 1445` hoelzl@51526 ` 1446` ```lemma convergent_setsum: ``` hoelzl@51526 ` 1447` ``` fixes X :: "'a \ nat \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1448` ``` assumes "\i. i \ A \ convergent (\n. X i n)" ``` hoelzl@51526 ` 1449` ``` shows "convergent (\n. \i\A. X i n)" ``` hoelzl@51526 ` 1450` ```proof (cases "finite A") ``` hoelzl@51526 ` 1451` ``` case True from this and assms show ?thesis ``` hoelzl@51526 ` 1452` ``` by (induct A set: finite) (simp_all add: convergent_const convergent_add) ``` hoelzl@51526 ` 1453` ```qed (simp add: convergent_const) ``` hoelzl@51526 ` 1454` hoelzl@51526 ` 1455` ```lemma (in bounded_linear) convergent: ``` hoelzl@51526 ` 1456` ``` assumes "convergent (\n. X n)" ``` hoelzl@51526 ` 1457` ``` shows "convergent (\n. f (X n))" ``` hoelzl@51526 ` 1458` ``` using assms unfolding convergent_def by (fast intro: tendsto) ``` hoelzl@51526 ` 1459` hoelzl@51526 ` 1460` ```lemma (in bounded_bilinear) convergent: ``` hoelzl@51526 ` 1461` ``` assumes "convergent (\n. X n)" and "convergent (\n. Y n)" ``` hoelzl@51526 ` 1462` ``` shows "convergent (\n. X n ** Y n)" ``` hoelzl@51526 ` 1463` ``` using assms unfolding convergent_def by (fast intro: tendsto) ``` hoelzl@51526 ` 1464` hoelzl@51526 ` 1465` ```lemma convergent_minus_iff: ``` hoelzl@51526 ` 1466` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1467` ``` shows "convergent X \ convergent (\n. - X n)" ``` hoelzl@51526 ` 1468` ```apply (simp add: convergent_def) ``` hoelzl@51526 ` 1469` ```apply (auto dest: tendsto_minus) ``` hoelzl@51526 ` 1470` ```apply (drule tendsto_minus, auto) ``` hoelzl@51526 ` 1471` ```done ``` hoelzl@51526 ` 1472` hoelzl@51526 ` 1473` wenzelm@60758 ` 1474` ```text \A monotone sequence converges to its least upper bound.\ ``` hoelzl@51526 ` 1475` hoelzl@54263 ` 1476` ```lemma LIMSEQ_incseq_SUP: ``` hoelzl@54263 ` 1477` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" ``` hoelzl@54263 ` 1478` ``` assumes u: "bdd_above (range X)" ``` hoelzl@54263 ` 1479` ``` assumes X: "incseq X" ``` hoelzl@54263 ` 1480` ``` shows "X ----> (SUP i. X i)" ``` hoelzl@54263 ` 1481` ``` by (rule order_tendstoI) ``` hoelzl@54263 ` 1482` ``` (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) ``` hoelzl@51526 ` 1483` hoelzl@54263 ` 1484` ```lemma LIMSEQ_decseq_INF: ``` hoelzl@54263 ` 1485` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" ``` hoelzl@54263 ` 1486` ``` assumes u: "bdd_below (range X)" ``` hoelzl@54263 ` 1487` ``` assumes X: "decseq X" ``` hoelzl@54263 ` 1488` ``` shows "X ----> (INF i. X i)" ``` hoelzl@54263 ` 1489` ``` by (rule order_tendstoI) ``` hoelzl@54263 ` 1490` ``` (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) ``` hoelzl@51526 ` 1491` wenzelm@60758 ` 1492` ```text\Main monotonicity theorem\ ``` hoelzl@51526 ` 1493` hoelzl@51526 ` 1494` ```lemma Bseq_monoseq_convergent: "Bseq X \ monoseq X \ convergent (X::nat\real)" ``` hoelzl@54263 ` 1495` ``` by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below) ``` hoelzl@54263 ` 1496` hoelzl@54263 ` 1497` ```lemma Bseq_mono_convergent: "Bseq X \ (\m n. m \ n \ X m \ X n) \ convergent (X::nat\real)" ``` hoelzl@54263 ` 1498` ``` by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) ``` hoelzl@51526 ` 1499` hoelzl@51526 ` 1500` ```lemma Cauchy_iff: ``` hoelzl@51526 ` 1501` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1502` ``` shows "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" ``` hoelzl@51526 ` 1503` ``` unfolding Cauchy_def dist_norm .. ``` hoelzl@51526 ` 1504` hoelzl@51526 ` 1505` ```lemma CauchyI: ``` hoelzl@51526 ` 1506` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1507` ``` shows "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" ``` hoelzl@51526 ` 1508` ```by (simp add: Cauchy_iff) ``` hoelzl@51526 ` 1509` hoelzl@51526 ` 1510` ```lemma CauchyD: ``` hoelzl@51526 ` 1511` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1512` ``` shows "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" ``` hoelzl@51526 ` 1513` ```by (simp add: Cauchy_iff) ``` hoelzl@51526 ` 1514` hoelzl@51526 ` 1515` ```lemma incseq_convergent: ``` hoelzl@51526 ` 1516` ``` fixes X :: "nat \ real" ``` hoelzl@51526 ` 1517` ``` assumes "incseq X" and "\i. X i \ B" ``` hoelzl@51526 ` 1518` ``` obtains L where "X ----> L" "\i. X i \ L" ``` hoelzl@51526 ` 1519` ```proof atomize_elim ``` wenzelm@60758 ` 1520` ``` from incseq_bounded[OF assms] \incseq X\ Bseq_monoseq_convergent[of X] ``` hoelzl@51526 ` 1521` ``` obtain L where "X ----> L" ``` hoelzl@51526 ` 1522` ``` by (auto simp: convergent_def monoseq_def incseq_def) ``` wenzelm@60758 ` 1523` ``` with \incseq X\ show "\L. X ----> L \ (\i. X i \ L)" ``` hoelzl@51526 ` 1524` ``` by (auto intro!: exI[of _ L] incseq_le) ``` hoelzl@51526 ` 1525` ```qed ``` hoelzl@51526 ` 1526` hoelzl@51526 ` 1527` ```lemma decseq_convergent: ``` hoelzl@51526 ` 1528` ``` fixes X :: "nat \ real" ``` hoelzl@51526 ` 1529` ``` assumes "decseq X" and "\i. B \ X i" ``` hoelzl@51526 ` 1530` ``` obtains L where "X ----> L" "\i. L \ X i" ``` hoelzl@51526 ` 1531` ```proof atomize_elim ``` wenzelm@60758 ` 1532` ``` from decseq_bounded[OF assms] \decseq X\ Bseq_monoseq_convergent[of X] ``` hoelzl@51526 ` 1533` ``` obtain L where "X ----> L" ``` hoelzl@51526 ` 1534` ``` by (auto simp: convergent_def monoseq_def decseq_def) ``` wenzelm@60758 ` 1535` ``` with \decseq X\ show "\L. X ----> L \ (\i. L \ X i)" ``` hoelzl@51526 ` 1536` ``` by (auto intro!: exI[of _ L] decseq_le) ``` hoelzl@51526 ` 1537` ```qed ``` hoelzl@51526 ` 1538` wenzelm@60758 ` 1539` ```subsubsection \Cauchy Sequences are Bounded\ ``` hoelzl@51526 ` 1540` wenzelm@60758 ` 1541` ```text\A Cauchy sequence is bounded -- this is the standard ``` wenzelm@60758 ` 1542` ``` proof mechanization rather than the nonstandard proof\ ``` hoelzl@51526 ` 1543` hoelzl@51526 ` 1544` ```lemma lemmaCauchy: "\n \ M. norm (X M - X n) < (1::real) ``` hoelzl@51526 ` 1545` ``` ==> \n \ M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" ``` hoelzl@51526 ` 1546` ```apply (clarify, drule spec, drule (1) mp) ``` hoelzl@51526 ` 1547` ```apply (simp only: norm_minus_commute) ``` hoelzl@51526 ` 1548` ```apply (drule order_le_less_trans [OF norm_triangle_ineq2]) ``` hoelzl@51526 ` 1549` ```apply simp ``` hoelzl@51526 ` 1550` ```done ``` hoelzl@51526 ` 1551` wenzelm@60758 ` 1552` ```subsection \Power Sequences\ ``` hoelzl@51526 ` 1553` wenzelm@60758 ` 1554` ```text\The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term ``` hoelzl@51526 ` 1555` ```"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and ``` wenzelm@60758 ` 1556` ``` also fact that bounded and monotonic sequence converges.\ ``` hoelzl@51526 ` 1557` hoelzl@51526 ` 1558` ```lemma Bseq_realpow: "[| 0 \ (x::real); x \ 1 |] ==> Bseq (%n. x ^ n)" ``` hoelzl@51526 ` 1559` ```apply (simp add: Bseq_def) ``` hoelzl@51526 ` 1560` ```apply (rule_tac x = 1 in exI) ``` hoelzl@51526 ` 1561` ```apply (simp add: power_abs) ``` hoelzl@51526 ` 1562` ```apply (auto dest: power_mono) ``` hoelzl@51526 ` 1563` ```done ``` hoelzl@51526 ` 1564` hoelzl@51526 ` 1565` ```lemma monoseq_realpow: fixes x :: real shows "[| 0 \ x; x \ 1 |] ==> monoseq (%n. x ^ n)" ``` hoelzl@51526 ` 1566` ```apply (clarify intro!: mono_SucI2) ``` hoelzl@51526 ` 1567` ```apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) ``` hoelzl@51526 ` 1568` ```done ``` hoelzl@51526 ` 1569` hoelzl@51526 ` 1570` ```lemma convergent_realpow: ``` hoelzl@51526 ` 1571` ``` "[| 0 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" ``` hoelzl@51526 ` 1572` ```by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) ``` hoelzl@51526 ` 1573` hoelzl@51526 ` 1574` ```lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" ``` hoelzl@51526 ` 1575` ``` by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 1576` hoelzl@51526 ` 1577` ```lemma LIMSEQ_realpow_zero: ``` hoelzl@51526 ` 1578` ``` "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" ``` hoelzl@51526 ` 1579` ```proof cases ``` hoelzl@51526 ` 1580` ``` assume "0 \ x" and "x \ 0" ``` hoelzl@51526 ` 1581` ``` hence x0: "0 < x" by simp ``` hoelzl@51526 ` 1582` ``` assume x1: "x < 1" ``` hoelzl@51526 ` 1583` ``` from x0 x1 have "1 < inverse x" ``` hoelzl@51526 ` 1584` ``` by (rule one_less_inverse) ``` hoelzl@51526 ` 1585` ``` hence "(\n. inverse (inverse x ^ n)) ----> 0" ``` hoelzl@51526 ` 1586` ``` by (rule LIMSEQ_inverse_realpow_zero) ``` hoelzl@51526 ` 1587` ``` thus ?thesis by (simp add: power_inverse) ``` hoelzl@58729 ` 1588` ```qed (rule LIMSEQ_imp_Suc, simp) ``` hoelzl@51526 ` 1589` hoelzl@51526 ` 1590` ```lemma LIMSEQ_power_zero: ``` hoelzl@51526 ` 1591` ``` fixes x :: "'a::{real_normed_algebra_1}" ``` hoelzl@51526 ` 1592` ``` shows "norm x < 1 \ (\n. x ^ n) ----> 0" ``` hoelzl@51526 ` 1593` ```apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) ``` hoelzl@51526 ` 1594` ```apply (simp only: tendsto_Zfun_iff, erule Zfun_le) ``` hoelzl@51526 ` 1595` ```apply (simp add: power_abs norm_power_ineq) ``` hoelzl@51526 ` 1596` ```done ``` hoelzl@51526 ` 1597` hoelzl@51526 ` 1598` ```lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) ----> 0" ``` hoelzl@51526 ` 1599` ``` by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 1600` wenzelm@60758 ` 1601` ```text\Limit of @{term "c^n"} for @{term"\c\ < 1"}\ ``` hoelzl@51526 ` 1602` hoelzl@51526 ` 1603` ```lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" ``` hoelzl@51526 ` 1604` ``` by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) ``` hoelzl@51526 ` 1605` hoelzl@51526 ` 1606` ```lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) ----> 0" ``` hoelzl@51526 ` 1607` ``` by (rule LIMSEQ_power_zero) simp ``` hoelzl@51526 ` 1608` hoelzl@51526 ` 1609` wenzelm@60758 ` 1610` ```subsection \Limits of Functions\ ``` hoelzl@51526 ` 1611` hoelzl@51526 ` 1612` ```lemma LIM_eq: ``` hoelzl@51526 ` 1613` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1614` ``` shows "f -- a --> L = ``` hoelzl@51526 ` 1615` ``` (\r>0.\s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r)" ``` hoelzl@51526 ` 1616` ```by (simp add: LIM_def dist_norm) ``` hoelzl@51526 ` 1617` hoelzl@51526 ` 1618` ```lemma LIM_I: ``` hoelzl@51526 ` 1619` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1620` ``` shows "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) ``` hoelzl@51526 ` 1621` ``` ==> f -- a --> L" ``` hoelzl@51526 ` 1622` ```by (simp add: LIM_eq) ``` hoelzl@51526 ` 1623` hoelzl@51526 ` 1624` ```lemma LIM_D: ``` hoelzl@51526 ` 1625` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1626` ``` shows "[| f -- a --> L; 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" ``` hoelzl@51526 ` 1628` ```by (simp add: LIM_eq) ``` hoelzl@51526 ` 1629` hoelzl@51526 ` 1630` ```lemma LIM_offset: ``` hoelzl@51526 ` 1631` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1632` ``` shows "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" ``` hoelzl@51641 ` 1633` ``` unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp ``` hoelzl@51526 ` 1634` hoelzl@51526 ` 1635` ```lemma LIM_offset_zero: ``` hoelzl@51526 ` 1636` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1637` ``` shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" ``` haftmann@57512 ` 1638` ```by (drule_tac k="a" in LIM_offset, simp add: add.commute) ``` hoelzl@51526 ` 1639` hoelzl@51526 ` 1640` ```lemma LIM_offset_zero_cancel: ``` hoelzl@51526 ` 1641` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1642` ``` shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" ``` hoelzl@51526 ` 1643` ```by (drule_tac k="- a" in LIM_offset, simp) ``` hoelzl@51526 ` 1644` hoelzl@51642 ` 1645` ```lemma LIM_offset_zero_iff: ``` hoelzl@51642 ` 1646` ``` fixes f :: "'a :: real_normed_vector \ _" ``` hoelzl@51642 ` 1647` ``` shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" ``` hoelzl@51642 ` 1648` ``` using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto ``` hoelzl@51642 ` 1649` hoelzl@51526 ` 1650` ```lemma LIM_zero: ``` hoelzl@51526 ` 1651` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1652` ``` shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" ``` hoelzl@51526 ` 1653` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1654` hoelzl@51526 ` 1655` ```lemma LIM_zero_cancel: ``` hoelzl@51526 ` 1656` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1657` ``` shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" ``` hoelzl@51526 ` 1658` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1659` hoelzl@51526 ` 1660` ```lemma LIM_zero_iff: ``` hoelzl@51526 ` 1661` ``` fixes f :: "'a::metric_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1662` ``` shows "((\x. f x - l) ---> 0) F = (f ---> l) F" ``` hoelzl@51526 ` 1663` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1664` hoelzl@51526 ` 1665` ```lemma LIM_imp_LIM: ``` hoelzl@51526 ` 1666` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1667` ``` fixes g :: "'a::topological_space \ 'c::real_normed_vector" ``` hoelzl@51526 ` 1668` ``` assumes f: "f -- a --> l" ``` hoelzl@51526 ` 1669` ``` assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" ``` hoelzl@51526 ` 1670` ``` shows "g -- a --> m" ``` hoelzl@51526 ` 1671` ``` by (rule metric_LIM_imp_LIM [OF f], ``` hoelzl@51526 ` 1672` ``` simp add: dist_norm le) ``` hoelzl@51526 ` 1673` hoelzl@51526 ` 1674` ```lemma LIM_equal2: ``` hoelzl@51526 ` 1675` ``` fixes f g :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1676` ``` assumes 1: "0 < R" ``` hoelzl@51526 ` 1677` ``` assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" ``` hoelzl@51526 ` 1678` ``` shows "g -- a --> l \ f -- a --> l" ``` hoelzl@51526 ` 1679` ```by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) ``` hoelzl@51526 ` 1680` hoelzl@51526 ` 1681` ```lemma LIM_compose2: ``` hoelzl@51526 ` 1682` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1683` ``` assumes f: "f -- a --> b" ``` hoelzl@51526 ` 1684` ``` assumes g: "g -- b --> c" ``` hoelzl@51526 ` 1685` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" ``` hoelzl@51526 ` 1686` ``` shows "(\x. g (f x)) -- a --> c" ``` hoelzl@51526 ` 1687` ```by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) ``` hoelzl@51526 ` 1688` hoelzl@51526 ` 1689` ```lemma real_LIM_sandwich_zero: ``` hoelzl@51526 ` 1690` ``` fixes f g :: "'a::topological_space \ real" ``` hoelzl@51526 ` 1691` ``` assumes f: "f -- a --> 0" ``` hoelzl@51526 ` 1692` ``` assumes 1: "\x. x \ a \ 0 \ g x" ``` hoelzl@51526 ` 1693` ``` assumes 2: "\x. x \ a \ g x \ f x" ``` hoelzl@51526 ` 1694` ``` shows "g -- a --> 0" ``` hoelzl@51526 ` 1695` ```proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) ``` hoelzl@51526 ` 1696` ``` fix x assume x: "x \ a" ``` hoelzl@51526 ` 1697` ``` have "norm (g x - 0) = g x" by (simp add: 1 x) ``` hoelzl@51526 ` 1698` ``` also have "g x \ f x" by (rule 2 [OF x]) ``` hoelzl@51526 ` 1699` ``` also have "f x \ \f x\" by (rule abs_ge_self) ``` hoelzl@51526 ` 1700` ``` also have "\f x\ = norm (f x - 0)" by simp ``` hoelzl@51526 ` 1701` ``` finally show "norm (g x - 0) \ norm (f x - 0)" . ``` hoelzl@51526 ` 1702` ```qed ``` hoelzl@51526 ` 1703` hoelzl@51526 ` 1704` wenzelm@60758 ` 1705` ```subsection \Continuity\ ``` hoelzl@51526 ` 1706` hoelzl@51526 ` 1707` ```lemma LIM_isCont_iff: ``` hoelzl@51526 ` 1708` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1709` ``` shows "(f -- a --> f a) = ((\h. f (a + h)) -- 0 --> f a)" ``` hoelzl@51526 ` 1710` ```by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) ``` hoelzl@51526 ` 1711` hoelzl@51526 ` 1712` ```lemma isCont_iff: ``` hoelzl@51526 ` 1713` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1714` ``` shows "isCont f x = (\h. f (x + h)) -- 0 --> f x" ``` hoelzl@51526 ` 1715` ```by (simp add: isCont_def LIM_isCont_iff) ``` hoelzl@51526 ` 1716` hoelzl@51526 ` 1717` ```lemma isCont_LIM_compose2: ``` hoelzl@51526 ` 1718` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1719` ``` assumes f [unfolded isCont_def]: "isCont f a" ``` hoelzl@51526 ` 1720` ``` assumes g: "g -- f a --> l" ``` hoelzl@51526 ` 1721` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" ``` hoelzl@51526 ` 1722` ``` shows "(\x. g (f x)) -- a --> l" ``` hoelzl@51526 ` 1723` ```by (rule LIM_compose2 [OF f g inj]) ``` hoelzl@51526 ` 1724` hoelzl@51526 ` 1725` hoelzl@51526 ` 1726` ```lemma isCont_norm [simp]: ``` hoelzl@51526 ` 1727` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1728` ``` shows "isCont f a \ isCont (\x. norm (f x)) a" ``` hoelzl@51526 ` 1729` ``` by (fact continuous_norm) ``` hoelzl@51526 ` 1730` hoelzl@51526 ` 1731` ```lemma isCont_rabs [simp]: ``` hoelzl@51526 ` 1732` ``` fixes f :: "'a::t2_space \ real" ``` hoelzl@51526 ` 1733` ``` shows "isCont f a \ isCont (\x. \f x\) a" ``` hoelzl@51526 ` 1734` ``` by (fact continuous_rabs) ``` hoelzl@51526 ` 1735` hoelzl@51526 ` 1736` ```lemma isCont_add [simp]: ``` hoelzl@51526 ` 1737` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1738` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" ``` hoelzl@51526 ` 1739` ``` by (fact continuous_add) ``` hoelzl@51526 ` 1740` hoelzl@51526 ` 1741` ```lemma isCont_minus [simp]: ``` hoelzl@51526 ` 1742` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1743` ``` shows "isCont f a \ isCont (\x. - f x) a" ``` hoelzl@51526 ` 1744` ``` by (fact continuous_minus) ``` hoelzl@51526 ` 1745` hoelzl@51526 ` 1746` ```lemma isCont_diff [simp]: ``` hoelzl@51526 ` 1747` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1748` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" ``` hoelzl@51526 ` 1749` ``` by (fact continuous_diff) ``` hoelzl@51526 ` 1750` hoelzl@51526 ` 1751` ```lemma isCont_mult [simp]: ``` hoelzl@51526 ` 1752` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" ``` hoelzl@51526 ` 1753` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" ``` hoelzl@51526 ` 1754` ``` by (fact continuous_mult) ``` hoelzl@51526 ` 1755` hoelzl@51526 ` 1756` ```lemma (in bounded_linear) isCont: ``` hoelzl@51526 ` 1757` ``` "isCont g a \ isCont (\x. f (g x)) a" ``` hoelzl@51526 ` 1758` ``` by (fact continuous) ``` hoelzl@51526 ` 1759` hoelzl@51526 ` 1760` ```lemma (in bounded_bilinear) isCont: ``` hoelzl@51526 ` 1761` ``` "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" ``` hoelzl@51526 ` 1762` ``` by (fact continuous) ``` hoelzl@51526 ` 1763` lp15@60141 ` 1764` ```lemmas isCont_scaleR [simp] = ``` hoelzl@51526 ` 1765` ``` bounded_bilinear.isCont [OF bounded_bilinear_scaleR] ``` hoelzl@51526 ` 1766` hoelzl@51526 ` 1767` ```lemmas isCont_of_real [simp] = ``` hoelzl@51526 ` 1768` ``` bounded_linear.isCont [OF bounded_linear_of_real] ``` hoelzl@51526 ` 1769` hoelzl@51526 ` 1770` ```lemma isCont_power [simp]: ``` hoelzl@51526 ` 1771` ``` fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` hoelzl@51526 ` 1772` ``` shows "isCont f a \ isCont (\x. f x ^ n) a" ``` hoelzl@51526 ` 1773` ``` by (fact continuous_power) ``` hoelzl@51526 ` 1774` hoelzl@51526 ` 1775` ```lemma isCont_setsum [simp]: ``` hoelzl@51526 ` 1776` ``` fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" ``` hoelzl@51526 ` 1777` ``` shows "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" ``` hoelzl@51526 ` 1778` ``` by (auto intro: continuous_setsum) ``` hoelzl@51526 ` 1779` wenzelm@60758 ` 1780` ```subsection \Uniform Continuity\ ``` hoelzl@51526 ` 1781` hoelzl@51531 ` 1782` ```definition ``` hoelzl@51531 ` 1783` ``` isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where ``` hoelzl@51531 ` 1784` ``` "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" ``` hoelzl@51531 ` 1785` hoelzl@51531 ` 1786` ```lemma isUCont_isCont: "isUCont f ==> isCont f x" ``` hoelzl@51531 ` 1787` ```by (simp add: isUCont_def isCont_def LIM_def, force) ``` hoelzl@51531 ` 1788` hoelzl@51531 ` 1789` ```lemma isUCont_Cauchy: ``` hoelzl@51531 ` 1790` ``` "\isUCont f; Cauchy X\ \ Cauchy (\n. f (X n))" ``` hoelzl@51531 ` 1791` ```unfolding isUCont_def ``` hoelzl@51531 ` 1792` ```apply (rule metric_CauchyI) ``` hoelzl@51531 ` 1793` ```apply (drule_tac x=e in spec, safe) ``` hoelzl@51531 ` 1794` ```apply (drule_tac e=s in metric_CauchyD, safe) ``` hoelzl@51531 ` 1795` ```apply (rule_tac x=M in exI, simp) ``` hoelzl@51531 ` 1796` ```done ``` hoelzl@51531 ` 1797` hoelzl@51526 ` 1798` ```lemma (in bounded_linear) isUCont: "isUCont f" ``` hoelzl@51526 ` 1799` ```unfolding isUCont_def dist_norm ``` hoelzl@51526 ` 1800` ```proof (intro allI impI) ``` hoelzl@51526 ` 1801` ``` fix r::real assume r: "0 < r" ``` hoelzl@51526 ` 1802` ``` obtain K where K: "0 < K" and norm_le: "\x. norm (f x) \ norm x * K" ``` hoelzl@51526 ` 1803` ``` using pos_bounded by fast ``` hoelzl@51526 ` 1804` ``` show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" ``` hoelzl@51526 ` 1805` ``` proof (rule exI, safe) ``` nipkow@56541 ` 1806` ``` from r K show "0 < r / K" by simp ``` hoelzl@51526 ` 1807` ``` next ``` hoelzl@51526 ` 1808` ``` fix x y :: 'a ``` hoelzl@51526 ` 1809` ``` assume xy: "norm (x - y) < r / K" ``` hoelzl@51526 ` 1810` ``` have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) ``` hoelzl@51526 ` 1811` ``` also have "\ \ norm (x - y) * K" by (rule norm_le) ``` hoelzl@51526 ` 1812` ``` also from K xy have "\ < r" by (simp only: pos_less_divide_eq) ``` hoelzl@51526 ` 1813` ``` finally show "norm (f x - f y) < r" . ``` hoelzl@51526 ` 1814` ``` qed ``` hoelzl@51526 ` 1815` ```qed ``` hoelzl@51526 ` 1816` hoelzl@51526 ` 1817` ```lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" ``` hoelzl@51526 ` 1818` ```by (rule isUCont [THEN isUCont_Cauchy]) ``` hoelzl@51526 ` 1819` lp15@60141 ` 1820` ```lemma LIM_less_bound: ``` hoelzl@51526 ` 1821` ``` fixes f :: "real \ real" ``` hoelzl@51526 ` 1822` ``` assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" ``` hoelzl@51526 ` 1823` ``` shows "0 \ f x" ``` hoelzl@51526 ` 1824` ```proof (rule tendsto_le_const) ``` hoelzl@51526 ` 1825` ``` show "(f ---> f x) (at_left x)" ``` wenzelm@60758 ` 1826` ``` using \isCont f x\ by (simp add: filterlim_at_split isCont_def) ``` hoelzl@51526 ` 1827` ``` show "eventually (\x. 0 \ f x) (at_left x)" ``` hoelzl@51641 ` 1828` ``` using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) ``` hoelzl@51526 ` 1829` ```qed simp ``` hoelzl@51471 ` 1830` hoelzl@51529 ` 1831` wenzelm@60758 ` 1832` ```subsection \Nested Intervals and Bisection -- Needed for Compactness\ ``` hoelzl@51529 ` 1833` hoelzl@51529 ` 1834` ```lemma nested_sequence_unique: ``` hoelzl@51529 ` 1835` ``` assumes "\n. f n \ f (Suc n)" "\n. g (Suc n) \ g n" "\n. f n \ g n" "(\n. f n - g n) ----> 0" ``` hoelzl@51529 ` 1836` ``` shows "\l::real. ((\n. f n \ l) \ f ----> l) \ ((\n. l \ g n) \ g ----> l)" ``` hoelzl@51529 ` 1837` ```proof - ``` hoelzl@51529 ` 1838` ``` have "incseq f" unfolding incseq_Suc_iff by fact ``` hoelzl@51529 ` 1839` ``` have "decseq g" unfolding decseq_Suc_iff by fact ``` hoelzl@51529 ` 1840` hoelzl@51529 ` 1841` ``` { fix n ``` wenzelm@60758 ` 1842` ``` from \decseq g\ have "g n \ g 0" by (rule decseqD) simp ``` wenzelm@60758 ` 1843` ``` with \\n. f n \ g n\[THEN spec, of n] have "f n \ g 0" by auto } ``` hoelzl@51529 ` 1844` ``` then obtain u where "f ----> u" "\i. f i \ u" ``` wenzelm@60758 ` 1845` ``` using incseq_convergent[OF \incseq f\] by auto ``` hoelzl@51529 ` 1846` ``` moreover ``` hoelzl@51529 ` 1847` ``` { fix n ``` wenzelm@60758 ` 1848` ``` from \incseq f\ have "f 0 \ f n" by (rule incseqD) simp ``` wenzelm@60758 ` 1849` ``` with \\n. f n \ g n\[THEN spec, of n] have "f 0 \ g n" by simp } ``` hoelzl@51529 ` 1850` ``` then obtain l where "g ----> l" "\i. l \ g i" ``` wenzelm@60758 ` 1851` ``` using decseq_convergent[OF \decseq g\] by auto ``` wenzelm@60758 ` 1852` ``` moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF \f ----> u\ \g ----> l\]] ``` hoelzl@51529 ` 1853` ``` ultimately show ?thesis by auto ``` hoelzl@51529 ` 1854` ```qed ``` hoelzl@51529 ` 1855` hoelzl@51529 ` 1856` ```lemma Bolzano[consumes 1, case_names trans local]: ``` hoelzl@51529 ` 1857` ``` fixes P :: "real \ real \ bool" ``` hoelzl@51529 ` 1858` ``` assumes [arith]: "a \ b" ``` hoelzl@51529 ` 1859` ``` assumes trans: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" ``` hoelzl@51529 ` 1860` ``` assumes local: "\x. a \ x \ x \ b \ \d>0. \a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51529 ` 1861` ``` shows "P a b" ``` hoelzl@51529 ` 1862` ```proof - ``` blanchet@55415 ` 1863` ``` def bisect \ "rec_nat (a, b) (\n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" ``` hoelzl@51529 ` 1864` ``` def l \ "\n. fst (bisect n)" and u \ "\n. snd (bisect n)" ``` hoelzl@51529 ` 1865` ``` 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 ` 1866` ``` 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 ` 1867` ``` by (simp_all add: l_def u_def bisect_def split: prod.split) ``` hoelzl@51529 ` 1868` hoelzl@51529 ` 1869` ``` { fix n have "l n \ u n" by (induct n) auto } note this[simp] ``` hoelzl@51529 ` 1870` hoelzl@51529 ` 1871` ``` have "\x. ((\n. l n \ x) \ l ----> x) \ ((\n. x \ u n) \ u ----> x)" ``` hoelzl@51529 ` 1872` ``` proof (safe intro!: nested_sequence_unique) ``` hoelzl@51529 ` 1873` ``` fix n show "l n \ l (Suc n)" "u (Suc n) \ u n" by (induct n) auto ``` hoelzl@51529 ` 1874` ``` next ``` hoelzl@51529 ` 1875` ``` { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) } ``` hoelzl@51529 ` 1876` ``` then show "(\n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero) ``` hoelzl@51529 ` 1877` ``` qed fact ``` hoelzl@51529 ` 1878` ``` then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l ----> x" "u ----> x" by auto ``` hoelzl@51529 ` 1879` ``` obtain d where "0 < d" and d: "\a b. a \ x \ x \ b \ b - a < d \ P a b" ``` wenzelm@60758 ` 1880` ``` using \l 0 \ x\ \x \ u 0\ local[of x] by auto ``` hoelzl@51529 ` 1881` hoelzl@51529 ` 1882` ``` show "P a b" ``` hoelzl@51529 ` 1883` ``` proof (rule ccontr) ``` lp15@60141 ` 1884` ``` assume "\ P a b" ``` hoelzl@51529 ` 1885` ``` { fix n have "\ P (l n) (u n)" ``` hoelzl@51529 ` 1886` ``` proof (induct n) ``` hoelzl@51529 ` 1887` ``` case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto ``` wenzelm@60758 ` 1888` ``` qed (simp add: \\ P a b\) } ``` hoelzl@51529 ` 1889` ``` moreover ``` hoelzl@51529 ` 1890` ``` { have "eventually (\n. x - d / 2 < l n) sequentially" ``` wenzelm@60758 ` 1891` ``` using \0 < d\ \l ----> x\ by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 1892` ``` moreover have "eventually (\n. u n < x + d / 2) sequentially" ``` wenzelm@60758 ` 1893` ``` using \0 < d\ \u ----> x\ by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 1894` ``` ultimately have "eventually (\n. P (l n) (u n)) sequentially" ``` hoelzl@51529 ` 1895` ``` proof eventually_elim ``` hoelzl@51529 ` 1896` ``` fix n assume "x - d / 2 < l n" "u n < x + d / 2" ``` hoelzl@51529 ` 1897` ``` from add_strict_mono[OF this] have "u n - l n < d" by simp ``` hoelzl@51529 ` 1898` ``` with x show "P (l n) (u n)" by (rule d) ``` hoelzl@51529 ` 1899` ``` qed } ``` hoelzl@51529 ` 1900` ``` ultimately show False by simp ``` hoelzl@51529 ` 1901` ``` qed ``` hoelzl@51529 ` 1902` ```qed ``` hoelzl@51529 ` 1903` hoelzl@51529 ` 1904` ```lemma compact_Icc[simp, intro]: "compact {a .. b::real}" ``` hoelzl@51529 ` 1905` ```proof (cases "a \ b", rule compactI) ``` hoelzl@51529 ` 1906` ``` fix C assume C: "a \ b" "\t\C. open t" "{a..b} \ \C" ``` hoelzl@51529 ` 1907` ``` def T == "{a .. b}" ``` hoelzl@51529 ` 1908` ``` from C(1,3) show "\C'\C. finite C' \ {a..b} \ \C'" ``` hoelzl@51529 ` 1909` ``` proof (induct rule: Bolzano) ``` hoelzl@51529 ` 1910` ``` case (trans a b c) ``` hoelzl@51529 ` 1911` ``` then have *: "{a .. c} = {a .. b} \ {b .. c}" by auto ``` hoelzl@51529 ` 1912` ``` from trans obtain C1 C2 where "C1\C \ finite C1 \ {a..b} \ \C1" "C2\C \ finite C2 \ {b..c} \ \C2" ``` hoelzl@51529 ` 1913` ``` by (auto simp: *) ``` hoelzl@51529 ` 1914` ``` with trans show ?case ``` hoelzl@51529 ` 1915` ``` unfolding * by (intro exI[of _ "C1 \ C2"]) auto ``` hoelzl@51529 ` 1916` ``` next ``` hoelzl@51529 ` 1917` ``` case (local x) ``` hoelzl@51529 ` 1918` ``` then have "x \ \C" using C by auto ``` hoelzl@51529 ` 1919` ``` with C(2) obtain c where "x \ c" "open c" "c \ C" by auto ``` hoelzl@51529 ` 1920` ``` then obtain e where "0 < e" "{x - e <..< x + e} \ c" ``` hoelzl@51529 ` 1921` ``` by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff) ``` wenzelm@60758 ` 1922` ``` with \c \ C\ show ?case ``` hoelzl@51529 ` 1923` ``` by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto ``` hoelzl@51529 ` 1924` ``` qed ``` hoelzl@51529 ` 1925` ```qed simp ``` hoelzl@51529 ` 1926` hoelzl@51529 ` 1927` hoelzl@57447 ` 1928` ```lemma continuous_image_closed_interval: ``` hoelzl@57447 ` 1929` ``` fixes a b and f :: "real \ real" ``` hoelzl@57447 ` 1930` ``` defines "S \ {a..b}" ``` hoelzl@57447 ` 1931` ``` assumes "a \ b" and f: "continuous_on S f" ``` hoelzl@57447 ` 1932` ``` shows "\c d. f`S = {c..d} \ c \ d" ``` hoelzl@57447 ` 1933` ```proof - ``` hoelzl@57447 ` 1934` ``` have S: "compact S" "S \ {}" ``` wenzelm@60758 ` 1935` ``` using \a \ b\ by (auto simp: S_def) ``` hoelzl@57447 ` 1936` ``` obtain c where "c \ S" "\d\S. f d \ f c" ``` hoelzl@57447 ` 1937` ``` using continuous_attains_sup[OF S f] by auto ``` hoelzl@57447 ` 1938` ``` moreover obtain d where "d \ S" "\c\S. f d \ f c" ``` hoelzl@57447 ` 1939` ``` using continuous_attains_inf[OF S f] by auto ``` hoelzl@57447 ` 1940` ``` moreover have "connected (f`S)" ``` hoelzl@57447 ` 1941` ``` using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def) ``` hoelzl@57447 ` 1942` ``` ultimately have "f ` S = {f d .. f c} \ f d \ f c" ``` hoelzl@57447 ` 1943` ``` by (auto simp: connected_iff_interval) ``` hoelzl@57447 ` 1944` ``` then show ?thesis ``` hoelzl@57447 ` 1945` ``` by auto ``` hoelzl@57447 ` 1946` ```qed ``` hoelzl@57447 ` 1947` lp15@60974 ` 1948` ```lemma open_Collect_positive: ``` lp15@60974 ` 1949` ``` fixes f :: "'a::t2_space \ real" ``` lp15@60974 ` 1950` ``` assumes f: "continuous_on s f" ``` lp15@60974 ` 1951` ``` shows "\A. open A \ A \ s = {x\s. 0 < f x}" ``` lp15@60974 ` 1952` ``` using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"] ``` lp15@60974 ` 1953` ``` by (auto simp: Int_def field_simps) ``` lp15@60974 ` 1954` lp15@60974 ` 1955` ```lemma open_Collect_less_Int: ``` lp15@60974 ` 1956` ``` fixes f g :: "'a::t2_space \ real" ``` lp15@60974 ` 1957` ``` assumes f: "continuous_on s f" and g: "continuous_on s g" ``` lp15@60974 ` 1958` ``` shows "\A. open A \ A \ s = {x\s. f x < g x}" ``` lp15@60974 ` 1959` ``` using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps) ``` lp15@60974 ` 1960` lp15@60974 ` 1961` wenzelm@60758 ` 1962` ```subsection \Boundedness of continuous functions\ ``` hoelzl@51529 ` 1963` wenzelm@60758 ` 1964` ```text\By bisection, function continuous on closed interval is bounded above\ ``` hoelzl@51529 ` 1965` hoelzl@51529 ` 1966` ```lemma isCont_eq_Ub: ``` hoelzl@51529 ` 1967` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1968` ``` shows "a \ b \ \x::real. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1969` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51529 ` 1970` ``` using continuous_attains_sup[of "{a .. b}" f] ``` hoelzl@51529 ` 1971` ``` by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) ``` hoelzl@51529 ` 1972` hoelzl@51529 ` 1973` ```lemma isCont_eq_Lb: ``` hoelzl@51529 ` 1974` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1975` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1976` ``` \M. (\x. a \ x \ x \ b \ M \ f x) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51529 ` 1977` ``` using continuous_attains_inf[of "{a .. b}" f] ``` hoelzl@51529 ` 1978` ``` by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) ``` hoelzl@51529 ` 1979` hoelzl@51529 ` 1980` ```lemma isCont_bounded: ``` hoelzl@51529 ` 1981` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1982` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ \M. \x. a \ x \ x \ b \ f x \ M" ``` hoelzl@51529 ` 1983` ``` using isCont_eq_Ub[of a b f] by auto ``` hoelzl@51529 ` 1984` hoelzl@51529 ` 1985` ```lemma isCont_has_Ub: ``` hoelzl@51529 ` 1986` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1987` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1988` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\N. N < M \ (\x. a \ x \ x \ b \ N < f x))" ``` hoelzl@51529 ` 1989` ``` using isCont_eq_Ub[of a b f] by auto ``` hoelzl@51529 ` 1990` hoelzl@51529 ` 1991` ```(*HOL style here: object-level formulations*) ``` hoelzl@51529 ` 1992` ```lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & ``` hoelzl@51529 ` 1993` ``` (\x. a \ x & x \ b --> isCont f x)) ``` hoelzl@51529 ` 1994` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` hoelzl@51529 ` 1995` ``` by (blast intro: IVT) ``` hoelzl@51529 ` 1996` hoelzl@51529 ` 1997` ```lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & ``` hoelzl@51529 ` 1998` ``` (\x. a \ x & x \ b --> isCont f x)) ``` hoelzl@51529 ` 1999` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` hoelzl@51529 ` 2000` ``` by (blast intro: IVT2) ``` hoelzl@51529 ` 2001` hoelzl@51529 ` 2002` ```lemma isCont_Lb_Ub: ``` hoelzl@51529 ` 2003` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 2004` ``` assumes "a \ b" "\x. a \ x \ x \ b \ isCont f x" ``` lp15@60141 ` 2005` ``` shows "\L M. (\x. a \ x \ x \ b \ L \ f x \ f x \ M) \ ``` hoelzl@51529 ` 2006` ``` (\y. L \ y \ y \ M \ (\x. a \ x \ x \ b \ (f x = y)))" ``` hoelzl@51529 ` 2007` ```proof - ``` hoelzl@51529 ` 2008` ``` obtain M where M: "a \ M" "M \ b" "\x. a \ x \ x \ b \ f x \ f M" ``` hoelzl@51529 ` 2009` ``` using isCont_eq_Ub[OF assms] by auto ``` hoelzl@51529 ` 2010` ``` obtain L where L: "a \ L" "L \ b" "\x. a \ x \ x \ b \ f L \ f x" ``` hoelzl@51529 ` 2011` ``` using isCont_eq_Lb[OF assms] by auto ``` hoelzl@51529 ` 2012` ``` show ?thesis ``` hoelzl@51529 ` 2013` ``` using IVT[of f L _ M] IVT2[of f L _ M] M L assms ``` hoelzl@51529 ` 2014` ``` apply (rule_tac x="f L" in exI) ``` hoelzl@51529 ` 2015` ``` apply (rule_tac x="f M" in exI) ``` hoelzl@51529 ` 2016` ``` apply (cases "L \ M") ``` hoelzl@51529 ` 2017` ``` apply (simp, metis order_trans) ``` hoelzl@51529 ` 2018` ``` apply (simp, metis order_trans) ``` hoelzl@51529 ` 2019` ``` done ``` hoelzl@51529 ` 2020` ```qed ``` hoelzl@51529 ` 2021` hoelzl@51529 ` 2022` wenzelm@60758 ` 2023` ```text\Continuity of inverse function\ ``` hoelzl@51529 ` 2024` hoelzl@51529 ` 2025` ```lemma isCont_inverse_function: ``` hoelzl@51529 ` 2026` ``` fixes f g :: "real \ real" ``` hoelzl@51529 ` 2027` ``` assumes d: "0 < d" ``` hoelzl@51529 ` 2028` ``` and inj: "\z. \z-x\ \ d \ g (f z) = z" ``` hoelzl@51529 ` 2029` ``` and cont: "\z. \z-x\ \ d \ isCont f z" ``` hoelzl@51529 ` 2030` ``` shows "isCont g (f x)" ``` hoelzl@51529 ` 2031` ```proof - ``` hoelzl@51529 ` 2032` ``` let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}" ``` hoelzl@51529 ` 2033` hoelzl@51529 ` 2034` ``` have f: "continuous_on ?D f" ``` hoelzl@51529 ` 2035` ``` using cont by (intro continuous_at_imp_continuous_on ballI) auto ``` hoelzl@51529 ` 2036` ``` then have g: "continuous_on (f`?D) g" ``` hoelzl@51529 ` 2037` ``` using inj by (intro continuous_on_inv) auto ``` hoelzl@51529 ` 2038` hoelzl@51529 ` 2039` ``` from d f have "{min ?A ?B <..< max ?A ?B} \ f ` ?D" ``` hoelzl@51529 ` 2040` ``` by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max) ``` hoelzl@51529 ` 2041` ``` with g have "continuous_on {min ?A ?B <..< max ?A ?B} g" ``` hoelzl@51529 ` 2042` ``` by (rule continuous_on_subset) ``` hoelzl@51529 ` 2043` ``` moreover ``` hoelzl@51529 ` 2044` ``` have "(?A < f x \ f x < ?B) \ (?B < f x \ f x < ?A)" ``` hoelzl@51529 ` 2045` ``` using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto ``` hoelzl@51529 ` 2046` ``` then have "f x \ {min ?A ?B <..< max ?A ?B}" ``` hoelzl@51529 ` 2047` ``` by auto ``` hoelzl@51529 ` 2048` ``` ultimately ``` hoelzl@51529 ` 2049` ``` show ?thesis ``` hoelzl@51529 ` 2050` ``` by (simp add: continuous_on_eq_continuous_at) ``` hoelzl@51529 ` 2051` ```qed ``` hoelzl@51529 ` 2052` hoelzl@51529 ` 2053` ```lemma isCont_inverse_function2: ``` hoelzl@51529 ` 2054` ``` fixes f g :: "real \ real" shows ``` hoelzl@51529 ` 2055` ``` "\a < x; x < b; ``` hoelzl@51529 ` 2056` ``` \z. a \ z \ z \ b \ g (f z) = z; ``` hoelzl@51529 ` 2057` ``` \z. a \ z \ z \ b \ isCont f z\ ``` hoelzl@51529 ` 2058` ``` \ isCont g (f x)" ``` hoelzl@51529 ` 2059` ```apply (rule isCont_inverse_function ``` hoelzl@51529 ` 2060` ``` [where f=f and d="min (x - a) (b - x)"]) ``` hoelzl@51529 ` 2061` ```apply (simp_all add: abs_le_iff) ``` hoelzl@51529 ` 2062` ```done ``` hoelzl@51529 ` 2063` hoelzl@51529 ` 2064` ```(* need to rename second isCont_inverse *) ``` hoelzl@51529 ` 2065` hoelzl@51529 ` 2066` ```lemma isCont_inv_fun: ``` hoelzl@51529 ` 2067` ``` fixes f g :: "real \ real" ``` lp15@60141 ` 2068` ``` shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; ``` lp15@60141 ` 2069` ``` \z. \z - x\ \ d --> isCont f z |] ``` hoelzl@51529 ` 2070` ``` ==> isCont g (f x)" ``` hoelzl@51529 ` 2071` ```by (rule isCont_inverse_function) ``` hoelzl@51529 ` 2072` wenzelm@60758 ` 2073` ```text\Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110\ ``` hoelzl@51529 ` 2074` ```lemma LIM_fun_gt_zero: ``` hoelzl@51529 ` 2075` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 2076` ``` shows "f -- c --> l \ 0 < l \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ 0 < f x)" ``` hoelzl@51529 ` 2077` ```apply (drule (1) LIM_D, clarify) ``` hoelzl@51529 ` 2078` ```apply (rule_tac x = s in exI) ``` hoelzl@51529 ` 2079` ```apply (simp add: abs_less_iff) ``` hoelzl@51529 ` 2080` ```done ``` hoelzl@51529 ` 2081` hoelzl@51529 ` 2082` ```lemma LIM_fun_less_zero: ``` hoelzl@51529 ` 2083` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 2084` ``` shows "f -- c --> l \ l < 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x < 0)" ``` hoelzl@51529 ` 2085` ```apply (drule LIM_D [where r="-l"], simp, clarify) ``` hoelzl@51529 ` 2086` ```apply (rule_tac x = s in exI) ``` hoelzl@51529 ` 2087` ```apply (simp add: abs_less_iff) ``` hoelzl@51529 ` 2088` ```done ``` hoelzl@51529 ` 2089` hoelzl@51529 ` 2090` ```lemma LIM_fun_not_zero: ``` hoelzl@51529 ` 2091` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 2092` ``` shows "f -- c --> l \ l \ 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x \ 0)" ``` hoelzl@51529 ` 2093` ``` using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff) ``` hoelzl@51531 ` 2094` huffman@31349 ` 2095` ```end ``` hoelzl@50324 ` 2096`