src/HOL/Limits.thy
 author paulson Thu Mar 05 17:30:29 2015 +0000 (2015-03-05) changeset 59613 7103019278f0 parent 58889 5b7a9633cfa8 child 59867 58043346ca64 permissions -rw-r--r--
The function frac. Various lemmas about limits, series, the exp function, etc.
 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@58889 ` 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` hoelzl@51526 ` 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: ``` hoelzl@50325 ` 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` hoelzl@51531 ` 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 ``` hoelzl@51474 ` 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` hoelzl@51531 ` 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` hoelzl@51531 ` 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` hoelzl@51531 ` 178` ```subsubsection{*A Few More Equivalence Theorems for Boundedness*} ``` hoelzl@51531 ` 179` hoelzl@51531 ` 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` hoelzl@51531 ` 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 ``` haftmann@54230 ` 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` hoelzl@51531 ` 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` hoelzl@51531 ` 234` ```subsection {* Bounded Monotonic Sequences *} ``` hoelzl@51531 ` 235` hoelzl@51531 ` 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` huffman@31349 ` 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 ``` huffman@31355 ` 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@56366 ` 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` huffman@44205 ` 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` huffman@44194 ` 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` huffman@44194 ` 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` huffman@44194 ` 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: ``` hoelzl@50325 ` 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` hoelzl@50347 ` 893` ```subsection {* Relate @{const at}, @{const at_left} and @{const at_right} *} ``` hoelzl@50347 ` 894` hoelzl@50347 ` 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` hoelzl@50347 ` 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_homeomorph: ``` hoelzl@51641 ` 905` ``` assumes f: "continuous (at a) f" ``` hoelzl@51641 ` 906` ``` assumes g: "continuous (at (f a)) g" ``` hoelzl@51641 ` 907` ``` assumes bij1: "\x. f (g x) = x" and bij2: "\x. g (f x) = x" ``` hoelzl@51641 ` 908` ``` shows "filtermap f (nhds a) = nhds (f a)" ``` hoelzl@51641 ` 909` ``` unfolding filter_eq_iff eventually_filtermap eventually_nhds ``` hoelzl@51641 ` 910` ```proof safe ``` hoelzl@51641 ` 911` ``` fix P S assume S: "open S" "f a \ S" and P: "\x\S. P x" ``` hoelzl@51641 ` 912` ``` from continuous_within_topological[THEN iffD1, rule_format, OF f S] P ``` hoelzl@51641 ` 913` ``` show "\S. open S \ a \ S \ (\x\S. P (f x))" by auto ``` hoelzl@51641 ` 914` ```next ``` hoelzl@51641 ` 915` ``` fix P S assume S: "open S" "a \ S" and P: "\x\S. P (f x)" ``` hoelzl@51641 ` 916` ``` with continuous_within_topological[THEN iffD1, rule_format, OF g, of S] bij2 ``` hoelzl@51641 ` 917` ``` obtain A where "open A" "f a \ A" "(\y\A. g y \ S)" ``` hoelzl@51641 ` 918` ``` by (metis UNIV_I) ``` hoelzl@51641 ` 919` ``` with P bij1 show "\S. open S \ f a \ S \ (\x\S. P x)" ``` hoelzl@51641 ` 920` ``` by (force intro!: exI[of _ A]) ``` hoelzl@51641 ` 921` ```qed ``` hoelzl@50347 ` 922` hoelzl@51641 ` 923` ```lemma filtermap_nhds_shift: "filtermap (\x. x - d) (nhds a) = nhds (a - d::'a::real_normed_vector)" ``` hoelzl@51641 ` 924` ``` by (rule filtermap_homeomorph[where g="\x. x + d"]) (auto intro: continuous_intros) ``` hoelzl@50347 ` 925` hoelzl@51641 ` 926` ```lemma filtermap_nhds_minus: "filtermap (\x. - x) (nhds a) = nhds (- a::'a::real_normed_vector)" ``` hoelzl@51641 ` 927` ``` by (rule filtermap_homeomorph[where g=uminus]) (auto intro: continuous_minus) ``` hoelzl@51641 ` 928` hoelzl@51641 ` 929` ```lemma filtermap_at_shift: "filtermap (\x. x - d) (at a) = at (a - d::'a::real_normed_vector)" ``` hoelzl@51641 ` 930` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50347 ` 931` hoelzl@50347 ` 932` ```lemma filtermap_at_right_shift: "filtermap (\x. x - d) (at_right a) = at_right (a - d::real)" ``` hoelzl@51641 ` 933` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric]) ``` hoelzl@50323 ` 934` hoelzl@50347 ` 935` ```lemma at_right_to_0: "at_right (a::real) = filtermap (\x. x + a) (at_right 0)" ``` hoelzl@50347 ` 936` ``` using filtermap_at_right_shift[of "-a" 0] by simp ``` hoelzl@50347 ` 937` hoelzl@50347 ` 938` ```lemma filterlim_at_right_to_0: ``` hoelzl@50347 ` 939` ``` "filterlim f F (at_right (a::real)) \ filterlim (\x. f (x + a)) F (at_right 0)" ``` hoelzl@50347 ` 940` ``` unfolding filterlim_def filtermap_filtermap at_right_to_0[of a] .. ``` hoelzl@50347 ` 941` hoelzl@50347 ` 942` ```lemma eventually_at_right_to_0: ``` hoelzl@50347 ` 943` ``` "eventually P (at_right (a::real)) \ eventually (\x. P (x + a)) (at_right 0)" ``` hoelzl@50347 ` 944` ``` unfolding at_right_to_0[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 945` hoelzl@51641 ` 946` ```lemma filtermap_at_minus: "filtermap (\x. - x) (at a) = at (- a::'a::real_normed_vector)" ``` hoelzl@51641 ` 947` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 948` hoelzl@50347 ` 949` ```lemma at_left_minus: "at_left (a::real) = filtermap (\x. - x) (at_right (- a))" ``` hoelzl@51641 ` 950` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50323 ` 951` hoelzl@50347 ` 952` ```lemma at_right_minus: "at_right (a::real) = filtermap (\x. - x) (at_left (- a))" ``` hoelzl@51641 ` 953` ``` by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric]) ``` hoelzl@50347 ` 954` hoelzl@50347 ` 955` ```lemma filterlim_at_left_to_right: ``` hoelzl@50347 ` 956` ``` "filterlim f F (at_left (a::real)) \ filterlim (\x. f (- x)) F (at_right (-a))" ``` hoelzl@50347 ` 957` ``` unfolding filterlim_def filtermap_filtermap at_left_minus[of a] .. ``` hoelzl@50347 ` 958` hoelzl@50347 ` 959` ```lemma eventually_at_left_to_right: ``` hoelzl@50347 ` 960` ``` "eventually P (at_left (a::real)) \ eventually (\x. P (- x)) (at_right (-a))" ``` hoelzl@50347 ` 961` ``` unfolding at_left_minus[of a] by (simp add: eventually_filtermap) ``` hoelzl@50347 ` 962` hoelzl@50346 ` 963` ```lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)" ``` hoelzl@50346 ` 964` ``` unfolding filter_eq_iff eventually_filtermap eventually_at_top_linorder eventually_at_bot_linorder ``` hoelzl@50346 ` 965` ``` by (metis le_minus_iff minus_minus) ``` hoelzl@50346 ` 966` hoelzl@50346 ` 967` ```lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)" ``` hoelzl@50346 ` 968` ``` unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident) ``` hoelzl@50346 ` 969` hoelzl@50346 ` 970` ```lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \ (LIM x at_bot. f (-x::real) :> F)" ``` hoelzl@50346 ` 971` ``` unfolding filterlim_def at_top_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 972` hoelzl@50346 ` 973` ```lemma filterlim_at_bot_mirror: "(LIM x at_bot. f x :> F) \ (LIM x at_top. f (-x::real) :> F)" ``` hoelzl@50346 ` 974` ``` unfolding filterlim_def at_bot_mirror filtermap_filtermap .. ``` hoelzl@50346 ` 975` hoelzl@50323 ` 976` ```lemma filterlim_uminus_at_top_at_bot: "LIM x at_bot. - x :: real :> at_top" ``` hoelzl@50323 ` 977` ``` unfolding filterlim_at_top eventually_at_bot_dense ``` hoelzl@50346 ` 978` ``` by (metis leI minus_less_iff order_less_asym) ``` hoelzl@50323 ` 979` hoelzl@50323 ` 980` ```lemma filterlim_uminus_at_bot_at_top: "LIM x at_top. - x :: real :> at_bot" ``` hoelzl@50323 ` 981` ``` unfolding filterlim_at_bot eventually_at_top_dense ``` hoelzl@50346 ` 982` ``` by (metis leI less_minus_iff order_less_asym) ``` hoelzl@50323 ` 983` hoelzl@50346 ` 984` ```lemma filterlim_uminus_at_top: "(LIM x F. f x :> at_top) \ (LIM x F. - (f x) :: real :> at_bot)" ``` hoelzl@50346 ` 985` ``` using filterlim_compose[OF filterlim_uminus_at_bot_at_top, of f F] ``` hoelzl@50346 ` 986` ``` using filterlim_compose[OF filterlim_uminus_at_top_at_bot, of "\x. - f x" F] ``` hoelzl@50346 ` 987` ``` by auto ``` hoelzl@50346 ` 988` hoelzl@50346 ` 989` ```lemma filterlim_uminus_at_bot: "(LIM x F. f x :> at_bot) \ (LIM x F. - (f x) :: real :> at_top)" ``` hoelzl@50346 ` 990` ``` unfolding filterlim_uminus_at_top by simp ``` hoelzl@50323 ` 991` hoelzl@50347 ` 992` ```lemma filterlim_inverse_at_top_right: "LIM x at_right (0::real). inverse x :> at_top" ``` hoelzl@51641 ` 993` ``` unfolding filterlim_at_top_gt[where c=0] eventually_at_filter ``` hoelzl@50347 ` 994` ```proof safe ``` hoelzl@50347 ` 995` ``` fix Z :: real assume [arith]: "0 < Z" ``` hoelzl@50347 ` 996` ``` then have "eventually (\x. x < inverse Z) (nhds 0)" ``` hoelzl@50347 ` 997` ``` by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\inverse Z\"]) ``` hoelzl@51641 ` 998` ``` then show "eventually (\x. x \ 0 \ x \ {0<..} \ Z \ inverse x) (nhds 0)" ``` hoelzl@50347 ` 999` ``` by (auto elim!: eventually_elim1 simp: inverse_eq_divide field_simps) ``` hoelzl@50347 ` 1000` ```qed ``` hoelzl@50347 ` 1001` hoelzl@50347 ` 1002` ```lemma filterlim_inverse_at_top: ``` hoelzl@50347 ` 1003` ``` "(f ---> (0 :: real)) F \ eventually (\x. 0 < f x) F \ LIM x F. inverse (f x) :> at_top" ``` hoelzl@50347 ` 1004` ``` by (intro filterlim_compose[OF filterlim_inverse_at_top_right]) ``` hoelzl@51641 ` 1005` ``` (simp add: filterlim_def eventually_filtermap eventually_elim1 at_within_def le_principal) ``` hoelzl@50347 ` 1006` hoelzl@50347 ` 1007` ```lemma filterlim_inverse_at_bot_neg: ``` hoelzl@50347 ` 1008` ``` "LIM x (at_left (0::real)). inverse x :> at_bot" ``` hoelzl@50347 ` 1009` ``` by (simp add: filterlim_inverse_at_top_right filterlim_uminus_at_bot filterlim_at_left_to_right) ``` hoelzl@50347 ` 1010` hoelzl@50347 ` 1011` ```lemma filterlim_inverse_at_bot: ``` hoelzl@50347 ` 1012` ``` "(f ---> (0 :: real)) F \ eventually (\x. f x < 0) F \ LIM x F. inverse (f x) :> at_bot" ``` hoelzl@50347 ` 1013` ``` unfolding filterlim_uminus_at_bot inverse_minus_eq[symmetric] ``` hoelzl@50347 ` 1014` ``` by (rule filterlim_inverse_at_top) (simp_all add: tendsto_minus_cancel_left[symmetric]) ``` hoelzl@50347 ` 1015` hoelzl@50325 ` 1016` ```lemma tendsto_inverse_0: ``` hoelzl@50325 ` 1017` ``` fixes x :: "_ \ 'a\real_normed_div_algebra" ``` hoelzl@50325 ` 1018` ``` shows "(inverse ---> (0::'a)) at_infinity" ``` hoelzl@50325 ` 1019` ``` unfolding tendsto_Zfun_iff diff_0_right Zfun_def eventually_at_infinity ``` hoelzl@50325 ` 1020` ```proof safe ``` hoelzl@50325 ` 1021` ``` fix r :: real assume "0 < r" ``` hoelzl@50325 ` 1022` ``` show "\b. \x. b \ norm x \ norm (inverse x :: 'a) < r" ``` hoelzl@50325 ` 1023` ``` proof (intro exI[of _ "inverse (r / 2)"] allI impI) ``` hoelzl@50325 ` 1024` ``` fix x :: 'a ``` hoelzl@50325 ` 1025` ``` from `0 < r` have "0 < inverse (r / 2)" by simp ``` hoelzl@50325 ` 1026` ``` also assume *: "inverse (r / 2) \ norm x" ``` hoelzl@50325 ` 1027` ``` finally show "norm (inverse x) < r" ``` hoelzl@50325 ` 1028` ``` using * `0 < r` by (subst nonzero_norm_inverse) (simp_all add: inverse_eq_divide field_simps) ``` hoelzl@50325 ` 1029` ``` qed ``` hoelzl@50325 ` 1030` ```qed ``` hoelzl@50325 ` 1031` hoelzl@50347 ` 1032` ```lemma at_right_to_top: "(at_right (0::real)) = filtermap inverse at_top" ``` hoelzl@50347 ` 1033` ```proof (rule antisym) ``` hoelzl@50347 ` 1034` ``` have "(inverse ---> (0::real)) at_top" ``` hoelzl@50347 ` 1035` ``` by (metis tendsto_inverse_0 filterlim_mono at_top_le_at_infinity order_refl) ``` hoelzl@50347 ` 1036` ``` then show "filtermap inverse at_top \ at_right (0::real)" ``` hoelzl@51641 ` 1037` ``` by (simp add: le_principal eventually_filtermap eventually_gt_at_top filterlim_def at_within_def) ``` hoelzl@50347 ` 1038` ```next ``` hoelzl@50347 ` 1039` ``` have "filtermap inverse (filtermap inverse (at_right (0::real))) \ filtermap inverse at_top" ``` hoelzl@50347 ` 1040` ``` using filterlim_inverse_at_top_right unfolding filterlim_def by (rule filtermap_mono) ``` hoelzl@50347 ` 1041` ``` then show "at_right (0::real) \ filtermap inverse at_top" ``` hoelzl@50347 ` 1042` ``` by (simp add: filtermap_ident filtermap_filtermap) ``` hoelzl@50347 ` 1043` ```qed ``` hoelzl@50347 ` 1044` hoelzl@50347 ` 1045` ```lemma eventually_at_right_to_top: ``` hoelzl@50347 ` 1046` ``` "eventually P (at_right (0::real)) \ eventually (\x. P (inverse x)) at_top" ``` hoelzl@50347 ` 1047` ``` unfolding at_right_to_top eventually_filtermap .. ``` hoelzl@50347 ` 1048` hoelzl@50347 ` 1049` ```lemma filterlim_at_right_to_top: ``` hoelzl@50347 ` 1050` ``` "filterlim f F (at_right (0::real)) \ (LIM x at_top. f (inverse x) :> F)" ``` hoelzl@50347 ` 1051` ``` unfolding filterlim_def at_right_to_top filtermap_filtermap .. ``` hoelzl@50347 ` 1052` hoelzl@50347 ` 1053` ```lemma at_top_to_right: "at_top = filtermap inverse (at_right (0::real))" ``` hoelzl@50347 ` 1054` ``` unfolding at_right_to_top filtermap_filtermap inverse_inverse_eq filtermap_ident .. ``` hoelzl@50347 ` 1055` hoelzl@50347 ` 1056` ```lemma eventually_at_top_to_right: ``` hoelzl@50347 ` 1057` ``` "eventually P at_top \ eventually (\x. P (inverse x)) (at_right (0::real))" ``` hoelzl@50347 ` 1058` ``` unfolding at_top_to_right eventually_filtermap .. ``` hoelzl@50347 ` 1059` hoelzl@50347 ` 1060` ```lemma filterlim_at_top_to_right: ``` hoelzl@50347 ` 1061` ``` "filterlim f F at_top \ (LIM x (at_right (0::real)). f (inverse x) :> F)" ``` hoelzl@50347 ` 1062` ``` unfolding filterlim_def at_top_to_right filtermap_filtermap .. ``` hoelzl@50347 ` 1063` hoelzl@50325 ` 1064` ```lemma filterlim_inverse_at_infinity: ``` hoelzl@50325 ` 1065` ``` fixes x :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" ``` hoelzl@50325 ` 1066` ``` shows "filterlim inverse at_infinity (at (0::'a))" ``` hoelzl@50325 ` 1067` ``` unfolding filterlim_at_infinity[OF order_refl] ``` hoelzl@50325 ` 1068` ```proof safe ``` hoelzl@50325 ` 1069` ``` fix r :: real assume "0 < r" ``` hoelzl@50325 ` 1070` ``` then show "eventually (\x::'a. r \ norm (inverse x)) (at 0)" ``` hoelzl@50325 ` 1071` ``` unfolding eventually_at norm_inverse ``` hoelzl@50325 ` 1072` ``` by (intro exI[of _ "inverse r"]) ``` hoelzl@50325 ` 1073` ``` (auto simp: norm_conv_dist[symmetric] field_simps inverse_eq_divide) ``` hoelzl@50325 ` 1074` ```qed ``` hoelzl@50325 ` 1075` hoelzl@50325 ` 1076` ```lemma filterlim_inverse_at_iff: ``` hoelzl@50325 ` 1077` ``` fixes g :: "'a \ 'b\{real_normed_div_algebra, division_ring_inverse_zero}" ``` hoelzl@50325 ` 1078` ``` shows "(LIM x F. inverse (g x) :> at 0) \ (LIM x F. g x :> at_infinity)" ``` hoelzl@50325 ` 1079` ``` unfolding filterlim_def filtermap_filtermap[symmetric] ``` hoelzl@50325 ` 1080` ```proof ``` hoelzl@50325 ` 1081` ``` assume "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1082` ``` then have "filtermap inverse (filtermap g F) \ filtermap inverse at_infinity" ``` hoelzl@50325 ` 1083` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1084` ``` also have "\ \ at 0" ``` hoelzl@51641 ` 1085` ``` using tendsto_inverse_0[where 'a='b] ``` hoelzl@51641 ` 1086` ``` by (auto intro!: exI[of _ 1] ``` hoelzl@51641 ` 1087` ``` simp: le_principal eventually_filtermap filterlim_def at_within_def eventually_at_infinity) ``` hoelzl@50325 ` 1088` ``` finally show "filtermap inverse (filtermap g F) \ at 0" . ``` hoelzl@50325 ` 1089` ```next ``` hoelzl@50325 ` 1090` ``` assume "filtermap inverse (filtermap g F) \ at 0" ``` hoelzl@50325 ` 1091` ``` then have "filtermap inverse (filtermap inverse (filtermap g F)) \ filtermap inverse (at 0)" ``` hoelzl@50325 ` 1092` ``` by (rule filtermap_mono) ``` hoelzl@50325 ` 1093` ``` with filterlim_inverse_at_infinity show "filtermap g F \ at_infinity" ``` hoelzl@50325 ` 1094` ``` by (auto intro: order_trans simp: filterlim_def filtermap_filtermap) ``` hoelzl@50325 ` 1095` ```qed ``` hoelzl@50325 ` 1096` hoelzl@51641 ` 1097` ```lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \ ((\x. inverse (f x) :: real) ---> 0) F" ``` hoelzl@51641 ` 1098` ``` by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff) ``` hoelzl@50419 ` 1099` lp15@59613 ` 1100` lp15@59613 ` 1101` ```lemma at_to_infinity: ``` lp15@59613 ` 1102` ``` fixes x :: "'a \ {real_normed_field,field_inverse_zero}" ``` lp15@59613 ` 1103` ``` shows "(at (0::'a)) = filtermap inverse at_infinity" ``` lp15@59613 ` 1104` ```proof (rule antisym) ``` lp15@59613 ` 1105` ``` have "(inverse ---> (0::'a)) at_infinity" ``` lp15@59613 ` 1106` ``` by (fact tendsto_inverse_0) ``` lp15@59613 ` 1107` ``` then show "filtermap inverse at_infinity \ at (0::'a)" ``` lp15@59613 ` 1108` ``` apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def) ``` lp15@59613 ` 1109` ``` apply (rule_tac x="1" in exI, auto) ``` lp15@59613 ` 1110` ``` done ``` lp15@59613 ` 1111` ```next ``` lp15@59613 ` 1112` ``` have "filtermap inverse (filtermap inverse (at (0::'a))) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1113` ``` using filterlim_inverse_at_infinity unfolding filterlim_def ``` lp15@59613 ` 1114` ``` by (rule filtermap_mono) ``` lp15@59613 ` 1115` ``` then show "at (0::'a) \ filtermap inverse at_infinity" ``` lp15@59613 ` 1116` ``` by (simp add: filtermap_ident filtermap_filtermap) ``` lp15@59613 ` 1117` ```qed ``` lp15@59613 ` 1118` lp15@59613 ` 1119` ```lemma lim_at_infinity_0: ``` lp15@59613 ` 1120` ``` fixes l :: "'a :: {real_normed_field,field_inverse_zero}" ``` lp15@59613 ` 1121` ``` shows "(f ---> l) at_infinity \ ((f o inverse) ---> l) (at (0::'a))" ``` lp15@59613 ` 1122` ```by (simp add: tendsto_compose_filtermap at_to_infinity filtermap_filtermap) ``` lp15@59613 ` 1123` lp15@59613 ` 1124` ```lemma lim_zero_infinity: ``` lp15@59613 ` 1125` ``` fixes l :: "'a :: {real_normed_field,field_inverse_zero}" ``` lp15@59613 ` 1126` ``` shows "((\x. f(1 / x)) ---> l) (at (0::'a)) \ (f ---> l) at_infinity" ``` lp15@59613 ` 1127` ```by (simp add: inverse_eq_divide lim_at_infinity_0 comp_def) ``` lp15@59613 ` 1128` lp15@59613 ` 1129` hoelzl@50324 ` 1130` ```text {* ``` hoelzl@50324 ` 1131` hoelzl@50324 ` 1132` ```We only show rules for multiplication and addition when the functions are either against a real ``` hoelzl@50324 ` 1133` ```value or against infinity. Further rules are easy to derive by using @{thm filterlim_uminus_at_top}. ``` hoelzl@50324 ` 1134` hoelzl@50324 ` 1135` ```*} ``` hoelzl@50324 ` 1136` hoelzl@50324 ` 1137` ```lemma filterlim_tendsto_pos_mult_at_top: ``` hoelzl@50324 ` 1138` ``` assumes f: "(f ---> c) F" and c: "0 < c" ``` hoelzl@50324 ` 1139` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1140` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1141` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1142` ```proof safe ``` hoelzl@50324 ` 1143` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50324 ` 1144` ``` from f `0 < c` have "eventually (\x. c / 2 < f x) F" ``` hoelzl@50324 ` 1145` ``` by (auto dest!: tendstoD[where e="c / 2"] elim!: eventually_elim1 ``` hoelzl@50324 ` 1146` ``` simp: dist_real_def abs_real_def split: split_if_asm) ``` hoelzl@50346 ` 1147` ``` moreover from g have "eventually (\x. (Z / c * 2) \ 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 "c / 2 < f x" "Z / c * 2 \ g x" ``` hoelzl@50346 ` 1152` ``` with `0 < Z` `0 < c` have "c / 2 * (Z / c * 2) \ f x * g x" ``` hoelzl@50346 ` 1153` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` hoelzl@50346 ` 1154` ``` with `0 < c` show "Z \ f x * g x" ``` hoelzl@50324 ` 1155` ``` by simp ``` hoelzl@50324 ` 1156` ``` qed ``` hoelzl@50324 ` 1157` ```qed ``` hoelzl@50324 ` 1158` hoelzl@50324 ` 1159` ```lemma filterlim_at_top_mult_at_top: ``` hoelzl@50324 ` 1160` ``` assumes f: "LIM x F. f x :> at_top" ``` hoelzl@50324 ` 1161` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1162` ``` shows "LIM x F. (f x * g x :: real) :> at_top" ``` hoelzl@50324 ` 1163` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1164` ```proof safe ``` hoelzl@50324 ` 1165` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50346 ` 1166` ``` from f have "eventually (\x. 1 \ f x) F" ``` hoelzl@50324 ` 1167` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1168` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1169` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1170` ``` ultimately show "eventually (\x. Z \ f x * g x) F" ``` hoelzl@50324 ` 1171` ``` proof eventually_elim ``` hoelzl@50346 ` 1172` ``` fix x assume "1 \ f x" "Z \ g x" ``` hoelzl@50346 ` 1173` ``` with `0 < Z` have "1 * Z \ f x * g x" ``` hoelzl@50346 ` 1174` ``` by (intro mult_mono) (auto simp: zero_le_divide_iff) ``` hoelzl@50346 ` 1175` ``` then show "Z \ f x * g x" ``` hoelzl@50324 ` 1176` ``` by simp ``` hoelzl@50324 ` 1177` ``` qed ``` hoelzl@50324 ` 1178` ```qed ``` hoelzl@50324 ` 1179` hoelzl@50419 ` 1180` ```lemma filterlim_tendsto_pos_mult_at_bot: ``` hoelzl@50419 ` 1181` ``` assumes "(f ---> c) F" "0 < (c::real)" "filterlim g at_bot F" ``` hoelzl@50419 ` 1182` ``` shows "LIM x F. f x * g x :> at_bot" ``` hoelzl@50419 ` 1183` ``` using filterlim_tendsto_pos_mult_at_top[OF assms(1,2), of "\x. - g x"] assms(3) ``` hoelzl@50419 ` 1184` ``` unfolding filterlim_uminus_at_bot by simp ``` hoelzl@50419 ` 1185` hoelzl@56330 ` 1186` ```lemma filterlim_pow_at_top: ``` hoelzl@56330 ` 1187` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1188` ``` assumes "0 < n" and f: "LIM x F. f x :> at_top" ``` hoelzl@56330 ` 1189` ``` shows "LIM x F. (f x)^n :: real :> at_top" ``` hoelzl@56330 ` 1190` ```using `0 < n` proof (induct n) ``` hoelzl@56330 ` 1191` ``` case (Suc n) with f show ?case ``` hoelzl@56330 ` 1192` ``` by (cases "n = 0") (auto intro!: filterlim_at_top_mult_at_top) ``` hoelzl@56330 ` 1193` ```qed simp ``` hoelzl@56330 ` 1194` hoelzl@56330 ` 1195` ```lemma filterlim_pow_at_bot_even: ``` hoelzl@56330 ` 1196` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1197` ``` shows "0 < n \ LIM x F. f x :> at_bot \ even n \ LIM x F. (f x)^n :> at_top" ``` hoelzl@56330 ` 1198` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_top) ``` hoelzl@56330 ` 1199` hoelzl@56330 ` 1200` ```lemma filterlim_pow_at_bot_odd: ``` hoelzl@56330 ` 1201` ``` fixes f :: "real \ real" ``` hoelzl@56330 ` 1202` ``` shows "0 < n \ LIM x F. f x :> at_bot \ odd n \ LIM x F. (f x)^n :> at_bot" ``` hoelzl@56330 ` 1203` ``` using filterlim_pow_at_top[of n "\x. - f x" F] by (simp add: filterlim_uminus_at_bot) ``` hoelzl@56330 ` 1204` hoelzl@50324 ` 1205` ```lemma filterlim_tendsto_add_at_top: ``` hoelzl@50324 ` 1206` ``` assumes f: "(f ---> c) F" ``` hoelzl@50324 ` 1207` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1208` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1209` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1210` ```proof safe ``` hoelzl@50324 ` 1211` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50324 ` 1212` ``` from f have "eventually (\x. c - 1 < f x) F" ``` hoelzl@50324 ` 1213` ``` by (auto dest!: tendstoD[where e=1] elim!: eventually_elim1 simp: dist_real_def) ``` hoelzl@50346 ` 1214` ``` moreover from g have "eventually (\x. Z - (c - 1) \ g x) F" ``` hoelzl@50324 ` 1215` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1216` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1217` ``` by eventually_elim simp ``` hoelzl@50324 ` 1218` ```qed ``` hoelzl@50324 ` 1219` hoelzl@50347 ` 1220` ```lemma LIM_at_top_divide: ``` hoelzl@50347 ` 1221` ``` fixes f g :: "'a \ real" ``` hoelzl@50347 ` 1222` ``` assumes f: "(f ---> a) F" "0 < a" ``` hoelzl@50347 ` 1223` ``` assumes g: "(g ---> 0) F" "eventually (\x. 0 < g x) F" ``` hoelzl@50347 ` 1224` ``` shows "LIM x F. f x / g x :> at_top" ``` hoelzl@50347 ` 1225` ``` unfolding divide_inverse ``` hoelzl@50347 ` 1226` ``` by (rule filterlim_tendsto_pos_mult_at_top[OF f]) (rule filterlim_inverse_at_top[OF g]) ``` hoelzl@50347 ` 1227` hoelzl@50324 ` 1228` ```lemma filterlim_at_top_add_at_top: ``` hoelzl@50324 ` 1229` ``` assumes f: "LIM x F. f x :> at_top" ``` hoelzl@50324 ` 1230` ``` assumes g: "LIM x F. g x :> at_top" ``` hoelzl@50324 ` 1231` ``` shows "LIM x F. (f x + g x :: real) :> at_top" ``` hoelzl@50324 ` 1232` ``` unfolding filterlim_at_top_gt[where c=0] ``` hoelzl@50324 ` 1233` ```proof safe ``` hoelzl@50324 ` 1234` ``` fix Z :: real assume "0 < Z" ``` hoelzl@50346 ` 1235` ``` from f have "eventually (\x. 0 \ f x) F" ``` hoelzl@50324 ` 1236` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1237` ``` moreover from g have "eventually (\x. Z \ g x) F" ``` hoelzl@50324 ` 1238` ``` unfolding filterlim_at_top by auto ``` hoelzl@50346 ` 1239` ``` ultimately show "eventually (\x. Z \ f x + g x) F" ``` hoelzl@50324 ` 1240` ``` by eventually_elim simp ``` hoelzl@50324 ` 1241` ```qed ``` hoelzl@50324 ` 1242` hoelzl@50331 ` 1243` ```lemma tendsto_divide_0: ``` hoelzl@50331 ` 1244` ``` fixes f :: "_ \ 'a\{real_normed_div_algebra, division_ring_inverse_zero}" ``` hoelzl@50331 ` 1245` ``` assumes f: "(f ---> c) F" ``` hoelzl@50331 ` 1246` ``` assumes g: "LIM x F. g x :> at_infinity" ``` hoelzl@50331 ` 1247` ``` shows "((\x. f x / g x) ---> 0) F" ``` hoelzl@50331 ` 1248` ``` using tendsto_mult[OF f filterlim_compose[OF tendsto_inverse_0 g]] by (simp add: divide_inverse) ``` hoelzl@50331 ` 1249` hoelzl@50331 ` 1250` ```lemma linear_plus_1_le_power: ``` hoelzl@50331 ` 1251` ``` fixes x :: real ``` hoelzl@50331 ` 1252` ``` assumes x: "0 \ x" ``` hoelzl@50331 ` 1253` ``` shows "real n * x + 1 \ (x + 1) ^ n" ``` hoelzl@50331 ` 1254` ```proof (induct n) ``` hoelzl@50331 ` 1255` ``` case (Suc n) ``` hoelzl@50331 ` 1256` ``` have "real (Suc n) * x + 1 \ (x + 1) * (real n * x + 1)" ``` nipkow@56536 ` 1257` ``` by (simp add: field_simps real_of_nat_Suc x) ``` hoelzl@50331 ` 1258` ``` also have "\ \ (x + 1)^Suc n" ``` hoelzl@50331 ` 1259` ``` using Suc x by (simp add: mult_left_mono) ``` hoelzl@50331 ` 1260` ``` finally show ?case . ``` hoelzl@50331 ` 1261` ```qed simp ``` hoelzl@50331 ` 1262` hoelzl@50331 ` 1263` ```lemma filterlim_realpow_sequentially_gt1: ``` hoelzl@50331 ` 1264` ``` fixes x :: "'a :: real_normed_div_algebra" ``` hoelzl@50331 ` 1265` ``` assumes x[arith]: "1 < norm x" ``` hoelzl@50331 ` 1266` ``` shows "LIM n sequentially. x ^ n :> at_infinity" ``` hoelzl@50331 ` 1267` ```proof (intro filterlim_at_infinity[THEN iffD2] allI impI) ``` hoelzl@50331 ` 1268` ``` fix y :: real assume "0 < y" ``` hoelzl@50331 ` 1269` ``` have "0 < norm x - 1" by simp ``` hoelzl@50331 ` 1270` ``` then obtain N::nat where "y < real N * (norm x - 1)" by (blast dest: reals_Archimedean3) ``` hoelzl@50331 ` 1271` ``` also have "\ \ real N * (norm x - 1) + 1" by simp ``` hoelzl@50331 ` 1272` ``` also have "\ \ (norm x - 1 + 1) ^ N" by (rule linear_plus_1_le_power) simp ``` hoelzl@50331 ` 1273` ``` also have "\ = norm x ^ N" by simp ``` hoelzl@50331 ` 1274` ``` finally have "\n\N. y \ norm x ^ n" ``` hoelzl@50331 ` 1275` ``` by (metis order_less_le_trans power_increasing order_less_imp_le x) ``` hoelzl@50331 ` 1276` ``` then show "eventually (\n. y \ norm (x ^ n)) sequentially" ``` hoelzl@50331 ` 1277` ``` unfolding eventually_sequentially ``` hoelzl@50331 ` 1278` ``` by (auto simp: norm_power) ``` hoelzl@50331 ` 1279` ```qed simp ``` hoelzl@50331 ` 1280` hoelzl@51471 ` 1281` hoelzl@51526 ` 1282` ```subsection {* Limits of Sequences *} ``` hoelzl@51526 ` 1283` hoelzl@51526 ` 1284` ```lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z" ``` hoelzl@51526 ` 1285` ``` by simp ``` hoelzl@51526 ` 1286` hoelzl@51526 ` 1287` ```lemma LIMSEQ_iff: ``` hoelzl@51526 ` 1288` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1289` ``` shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" ``` hoelzl@51526 ` 1290` ```unfolding LIMSEQ_def dist_norm .. ``` hoelzl@51526 ` 1291` hoelzl@51526 ` 1292` ```lemma LIMSEQ_I: ``` hoelzl@51526 ` 1293` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1294` ``` shows "(\r. 0 < r \ \no. \n\no. norm (X n - L) < r) \ X ----> L" ``` hoelzl@51526 ` 1295` ```by (simp add: LIMSEQ_iff) ``` hoelzl@51526 ` 1296` hoelzl@51526 ` 1297` ```lemma LIMSEQ_D: ``` hoelzl@51526 ` 1298` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1299` ``` shows "\X ----> L; 0 < r\ \ \no. \n\no. norm (X n - L) < r" ``` hoelzl@51526 ` 1300` ```by (simp add: LIMSEQ_iff) ``` hoelzl@51526 ` 1301` hoelzl@51526 ` 1302` ```lemma LIMSEQ_linear: "\ X ----> x ; l > 0 \ \ (\ n. X (n * l)) ----> x" ``` hoelzl@51526 ` 1303` ``` unfolding tendsto_def eventually_sequentially ``` haftmann@57512 ` 1304` ``` by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute) ``` hoelzl@51526 ` 1305` hoelzl@51526 ` 1306` ```lemma Bseq_inverse_lemma: ``` hoelzl@51526 ` 1307` ``` fixes x :: "'a::real_normed_div_algebra" ``` hoelzl@51526 ` 1308` ``` shows "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r" ``` hoelzl@51526 ` 1309` ```apply (subst nonzero_norm_inverse, clarsimp) ``` hoelzl@51526 ` 1310` ```apply (erule (1) le_imp_inverse_le) ``` hoelzl@51526 ` 1311` ```done ``` hoelzl@51526 ` 1312` hoelzl@51526 ` 1313` ```lemma Bseq_inverse: ``` hoelzl@51526 ` 1314` ``` fixes a :: "'a::real_normed_div_algebra" ``` hoelzl@51526 ` 1315` ``` shows "\X ----> a; a \ 0\ \ Bseq (\n. inverse (X n))" ``` hoelzl@51526 ` 1316` ``` by (rule Bfun_inverse) ``` hoelzl@51526 ` 1317` hoelzl@51526 ` 1318` ```lemma LIMSEQ_diff_approach_zero: ``` hoelzl@51526 ` 1319` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1320` ``` shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L" ``` hoelzl@51526 ` 1321` ``` by (drule (1) tendsto_add, simp) ``` hoelzl@51526 ` 1322` hoelzl@51526 ` 1323` ```lemma LIMSEQ_diff_approach_zero2: ``` hoelzl@51526 ` 1324` ``` fixes L :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1325` ``` shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L" ``` hoelzl@51526 ` 1326` ``` by (drule (1) tendsto_diff, simp) ``` hoelzl@51526 ` 1327` hoelzl@51526 ` 1328` ```text{*An unbounded sequence's inverse tends to 0*} ``` hoelzl@51526 ` 1329` hoelzl@51526 ` 1330` ```lemma LIMSEQ_inverse_zero: ``` hoelzl@51526 ` 1331` ``` "\r::real. \N. \n\N. r < X n \ (\n. inverse (X n)) ----> 0" ``` hoelzl@51526 ` 1332` ``` apply (rule filterlim_compose[OF tendsto_inverse_0]) ``` hoelzl@51526 ` 1333` ``` apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially) ``` hoelzl@51526 ` 1334` ``` apply (metis abs_le_D1 linorder_le_cases linorder_not_le) ``` hoelzl@51526 ` 1335` ``` done ``` hoelzl@51526 ` 1336` hoelzl@51526 ` 1337` ```text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} ``` hoelzl@51526 ` 1338` hoelzl@51526 ` 1339` ```lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" ``` hoelzl@51526 ` 1340` ``` by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc ``` hoelzl@51526 ` 1341` ``` filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity) ``` hoelzl@51526 ` 1342` hoelzl@51526 ` 1343` ```text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to ``` hoelzl@51526 ` 1344` ```infinity is now easily proved*} ``` hoelzl@51526 ` 1345` hoelzl@51526 ` 1346` ```lemma LIMSEQ_inverse_real_of_nat_add: ``` hoelzl@51526 ` 1347` ``` "(%n. r + inverse(real(Suc n))) ----> r" ``` hoelzl@51526 ` 1348` ``` using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto ``` hoelzl@51526 ` 1349` hoelzl@51526 ` 1350` ```lemma LIMSEQ_inverse_real_of_nat_add_minus: ``` hoelzl@51526 ` 1351` ``` "(%n. r + -inverse(real(Suc n))) ----> r" ``` hoelzl@51526 ` 1352` ``` using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]] ``` hoelzl@51526 ` 1353` ``` by auto ``` hoelzl@51526 ` 1354` hoelzl@51526 ` 1355` ```lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: ``` hoelzl@51526 ` 1356` ``` "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" ``` hoelzl@51526 ` 1357` ``` using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]] ``` hoelzl@51526 ` 1358` ``` by auto ``` hoelzl@51526 ` 1359` hoelzl@51526 ` 1360` ```subsection {* Convergence on sequences *} ``` hoelzl@51526 ` 1361` hoelzl@51526 ` 1362` ```lemma convergent_add: ``` hoelzl@51526 ` 1363` ``` fixes X Y :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1364` ``` assumes "convergent (\n. X n)" ``` hoelzl@51526 ` 1365` ``` assumes "convergent (\n. Y n)" ``` hoelzl@51526 ` 1366` ``` shows "convergent (\n. X n + Y n)" ``` hoelzl@51526 ` 1367` ``` using assms unfolding convergent_def by (fast intro: tendsto_add) ``` hoelzl@51526 ` 1368` hoelzl@51526 ` 1369` ```lemma convergent_setsum: ``` hoelzl@51526 ` 1370` ``` fixes X :: "'a \ nat \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1371` ``` assumes "\i. i \ A \ convergent (\n. X i n)" ``` hoelzl@51526 ` 1372` ``` shows "convergent (\n. \i\A. X i n)" ``` hoelzl@51526 ` 1373` ```proof (cases "finite A") ``` hoelzl@51526 ` 1374` ``` case True from this and assms show ?thesis ``` hoelzl@51526 ` 1375` ``` by (induct A set: finite) (simp_all add: convergent_const convergent_add) ``` hoelzl@51526 ` 1376` ```qed (simp add: convergent_const) ``` hoelzl@51526 ` 1377` hoelzl@51526 ` 1378` ```lemma (in bounded_linear) convergent: ``` hoelzl@51526 ` 1379` ``` assumes "convergent (\n. X n)" ``` hoelzl@51526 ` 1380` ``` shows "convergent (\n. f (X n))" ``` hoelzl@51526 ` 1381` ``` using assms unfolding convergent_def by (fast intro: tendsto) ``` hoelzl@51526 ` 1382` hoelzl@51526 ` 1383` ```lemma (in bounded_bilinear) convergent: ``` hoelzl@51526 ` 1384` ``` assumes "convergent (\n. X n)" and "convergent (\n. Y n)" ``` hoelzl@51526 ` 1385` ``` shows "convergent (\n. X n ** Y n)" ``` hoelzl@51526 ` 1386` ``` using assms unfolding convergent_def by (fast intro: tendsto) ``` hoelzl@51526 ` 1387` hoelzl@51526 ` 1388` ```lemma convergent_minus_iff: ``` hoelzl@51526 ` 1389` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1390` ``` shows "convergent X \ convergent (\n. - X n)" ``` hoelzl@51526 ` 1391` ```apply (simp add: convergent_def) ``` hoelzl@51526 ` 1392` ```apply (auto dest: tendsto_minus) ``` hoelzl@51526 ` 1393` ```apply (drule tendsto_minus, auto) ``` hoelzl@51526 ` 1394` ```done ``` hoelzl@51526 ` 1395` hoelzl@51526 ` 1396` hoelzl@51526 ` 1397` ```text {* A monotone sequence converges to its least upper bound. *} ``` hoelzl@51526 ` 1398` hoelzl@54263 ` 1399` ```lemma LIMSEQ_incseq_SUP: ``` hoelzl@54263 ` 1400` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" ``` hoelzl@54263 ` 1401` ``` assumes u: "bdd_above (range X)" ``` hoelzl@54263 ` 1402` ``` assumes X: "incseq X" ``` hoelzl@54263 ` 1403` ``` shows "X ----> (SUP i. X i)" ``` hoelzl@54263 ` 1404` ``` by (rule order_tendstoI) ``` hoelzl@54263 ` 1405` ``` (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u]) ``` hoelzl@51526 ` 1406` hoelzl@54263 ` 1407` ```lemma LIMSEQ_decseq_INF: ``` hoelzl@54263 ` 1408` ``` fixes X :: "nat \ 'a::{conditionally_complete_linorder, linorder_topology}" ``` hoelzl@54263 ` 1409` ``` assumes u: "bdd_below (range X)" ``` hoelzl@54263 ` 1410` ``` assumes X: "decseq X" ``` hoelzl@54263 ` 1411` ``` shows "X ----> (INF i. X i)" ``` hoelzl@54263 ` 1412` ``` by (rule order_tendstoI) ``` hoelzl@54263 ` 1413` ``` (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u]) ``` hoelzl@51526 ` 1414` hoelzl@51526 ` 1415` ```text{*Main monotonicity theorem*} ``` hoelzl@51526 ` 1416` hoelzl@51526 ` 1417` ```lemma Bseq_monoseq_convergent: "Bseq X \ monoseq X \ convergent (X::nat\real)" ``` hoelzl@54263 ` 1418` ``` by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below) ``` hoelzl@54263 ` 1419` hoelzl@54263 ` 1420` ```lemma Bseq_mono_convergent: "Bseq X \ (\m n. m \ n \ X m \ X n) \ convergent (X::nat\real)" ``` hoelzl@54263 ` 1421` ``` by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def) ``` hoelzl@51526 ` 1422` hoelzl@51526 ` 1423` ```lemma Cauchy_iff: ``` hoelzl@51526 ` 1424` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1425` ``` shows "Cauchy X \ (\e>0. \M. \m\M. \n\M. norm (X m - X n) < e)" ``` hoelzl@51526 ` 1426` ``` unfolding Cauchy_def dist_norm .. ``` hoelzl@51526 ` 1427` hoelzl@51526 ` 1428` ```lemma CauchyI: ``` hoelzl@51526 ` 1429` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1430` ``` shows "(\e. 0 < e \ \M. \m\M. \n\M. norm (X m - X n) < e) \ Cauchy X" ``` hoelzl@51526 ` 1431` ```by (simp add: Cauchy_iff) ``` hoelzl@51526 ` 1432` hoelzl@51526 ` 1433` ```lemma CauchyD: ``` hoelzl@51526 ` 1434` ``` fixes X :: "nat \ 'a::real_normed_vector" ``` hoelzl@51526 ` 1435` ``` shows "\Cauchy X; 0 < e\ \ \M. \m\M. \n\M. norm (X m - X n) < e" ``` hoelzl@51526 ` 1436` ```by (simp add: Cauchy_iff) ``` hoelzl@51526 ` 1437` hoelzl@51526 ` 1438` ```lemma incseq_convergent: ``` hoelzl@51526 ` 1439` ``` fixes X :: "nat \ real" ``` hoelzl@51526 ` 1440` ``` assumes "incseq X" and "\i. X i \ B" ``` hoelzl@51526 ` 1441` ``` obtains L where "X ----> L" "\i. X i \ L" ``` hoelzl@51526 ` 1442` ```proof atomize_elim ``` hoelzl@51526 ` 1443` ``` from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X] ``` hoelzl@51526 ` 1444` ``` obtain L where "X ----> L" ``` hoelzl@51526 ` 1445` ``` by (auto simp: convergent_def monoseq_def incseq_def) ``` hoelzl@51526 ` 1446` ``` with `incseq X` show "\L. X ----> L \ (\i. X i \ L)" ``` hoelzl@51526 ` 1447` ``` by (auto intro!: exI[of _ L] incseq_le) ``` hoelzl@51526 ` 1448` ```qed ``` hoelzl@51526 ` 1449` hoelzl@51526 ` 1450` ```lemma decseq_convergent: ``` hoelzl@51526 ` 1451` ``` fixes X :: "nat \ real" ``` hoelzl@51526 ` 1452` ``` assumes "decseq X" and "\i. B \ X i" ``` hoelzl@51526 ` 1453` ``` obtains L where "X ----> L" "\i. L \ X i" ``` hoelzl@51526 ` 1454` ```proof atomize_elim ``` hoelzl@51526 ` 1455` ``` from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X] ``` hoelzl@51526 ` 1456` ``` obtain L where "X ----> L" ``` hoelzl@51526 ` 1457` ``` by (auto simp: convergent_def monoseq_def decseq_def) ``` hoelzl@51526 ` 1458` ``` with `decseq X` show "\L. X ----> L \ (\i. L \ X i)" ``` hoelzl@51526 ` 1459` ``` by (auto intro!: exI[of _ L] decseq_le) ``` hoelzl@51526 ` 1460` ```qed ``` hoelzl@51526 ` 1461` hoelzl@51526 ` 1462` ```subsubsection {* Cauchy Sequences are Bounded *} ``` hoelzl@51526 ` 1463` hoelzl@51526 ` 1464` ```text{*A Cauchy sequence is bounded -- this is the standard ``` hoelzl@51526 ` 1465` ``` proof mechanization rather than the nonstandard proof*} ``` hoelzl@51526 ` 1466` hoelzl@51526 ` 1467` ```lemma lemmaCauchy: "\n \ M. norm (X M - X n) < (1::real) ``` hoelzl@51526 ` 1468` ``` ==> \n \ M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)" ``` hoelzl@51526 ` 1469` ```apply (clarify, drule spec, drule (1) mp) ``` hoelzl@51526 ` 1470` ```apply (simp only: norm_minus_commute) ``` hoelzl@51526 ` 1471` ```apply (drule order_le_less_trans [OF norm_triangle_ineq2]) ``` hoelzl@51526 ` 1472` ```apply simp ``` hoelzl@51526 ` 1473` ```done ``` hoelzl@51526 ` 1474` hoelzl@51526 ` 1475` ```subsection {* Power Sequences *} ``` hoelzl@51526 ` 1476` hoelzl@51526 ` 1477` ```text{*The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term ``` hoelzl@51526 ` 1478` ```"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and ``` hoelzl@51526 ` 1479` ``` also fact that bounded and monotonic sequence converges.*} ``` hoelzl@51526 ` 1480` hoelzl@51526 ` 1481` ```lemma Bseq_realpow: "[| 0 \ (x::real); x \ 1 |] ==> Bseq (%n. x ^ n)" ``` hoelzl@51526 ` 1482` ```apply (simp add: Bseq_def) ``` hoelzl@51526 ` 1483` ```apply (rule_tac x = 1 in exI) ``` hoelzl@51526 ` 1484` ```apply (simp add: power_abs) ``` hoelzl@51526 ` 1485` ```apply (auto dest: power_mono) ``` hoelzl@51526 ` 1486` ```done ``` hoelzl@51526 ` 1487` hoelzl@51526 ` 1488` ```lemma monoseq_realpow: fixes x :: real shows "[| 0 \ x; x \ 1 |] ==> monoseq (%n. x ^ n)" ``` hoelzl@51526 ` 1489` ```apply (clarify intro!: mono_SucI2) ``` hoelzl@51526 ` 1490` ```apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) ``` hoelzl@51526 ` 1491` ```done ``` hoelzl@51526 ` 1492` hoelzl@51526 ` 1493` ```lemma convergent_realpow: ``` hoelzl@51526 ` 1494` ``` "[| 0 \ (x::real); x \ 1 |] ==> convergent (%n. x ^ n)" ``` hoelzl@51526 ` 1495` ```by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) ``` hoelzl@51526 ` 1496` hoelzl@51526 ` 1497` ```lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" ``` hoelzl@51526 ` 1498` ``` by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 1499` hoelzl@51526 ` 1500` ```lemma LIMSEQ_realpow_zero: ``` hoelzl@51526 ` 1501` ``` "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" ``` hoelzl@51526 ` 1502` ```proof cases ``` hoelzl@51526 ` 1503` ``` assume "0 \ x" and "x \ 0" ``` hoelzl@51526 ` 1504` ``` hence x0: "0 < x" by simp ``` hoelzl@51526 ` 1505` ``` assume x1: "x < 1" ``` hoelzl@51526 ` 1506` ``` from x0 x1 have "1 < inverse x" ``` hoelzl@51526 ` 1507` ``` by (rule one_less_inverse) ``` hoelzl@51526 ` 1508` ``` hence "(\n. inverse (inverse x ^ n)) ----> 0" ``` hoelzl@51526 ` 1509` ``` by (rule LIMSEQ_inverse_realpow_zero) ``` hoelzl@51526 ` 1510` ``` thus ?thesis by (simp add: power_inverse) ``` hoelzl@58729 ` 1511` ```qed (rule LIMSEQ_imp_Suc, simp) ``` hoelzl@51526 ` 1512` hoelzl@51526 ` 1513` ```lemma LIMSEQ_power_zero: ``` hoelzl@51526 ` 1514` ``` fixes x :: "'a::{real_normed_algebra_1}" ``` hoelzl@51526 ` 1515` ``` shows "norm x < 1 \ (\n. x ^ n) ----> 0" ``` hoelzl@51526 ` 1516` ```apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero]) ``` hoelzl@51526 ` 1517` ```apply (simp only: tendsto_Zfun_iff, erule Zfun_le) ``` hoelzl@51526 ` 1518` ```apply (simp add: power_abs norm_power_ineq) ``` hoelzl@51526 ` 1519` ```done ``` hoelzl@51526 ` 1520` hoelzl@51526 ` 1521` ```lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) ----> 0" ``` hoelzl@51526 ` 1522` ``` by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp ``` hoelzl@51526 ` 1523` hoelzl@51526 ` 1524` ```text{*Limit of @{term "c^n"} for @{term"\c\ < 1"}*} ``` hoelzl@51526 ` 1525` hoelzl@51526 ` 1526` ```lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) ----> 0" ``` hoelzl@51526 ` 1527` ``` by (rule LIMSEQ_realpow_zero [OF abs_ge_zero]) ``` hoelzl@51526 ` 1528` hoelzl@51526 ` 1529` ```lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 \ (\n. c ^ n :: real) ----> 0" ``` hoelzl@51526 ` 1530` ``` by (rule LIMSEQ_power_zero) simp ``` hoelzl@51526 ` 1531` hoelzl@51526 ` 1532` hoelzl@51526 ` 1533` ```subsection {* Limits of Functions *} ``` hoelzl@51526 ` 1534` hoelzl@51526 ` 1535` ```lemma LIM_eq: ``` hoelzl@51526 ` 1536` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1537` ``` shows "f -- a --> L = ``` hoelzl@51526 ` 1538` ``` (\r>0.\s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r)" ``` hoelzl@51526 ` 1539` ```by (simp add: LIM_def dist_norm) ``` hoelzl@51526 ` 1540` hoelzl@51526 ` 1541` ```lemma LIM_I: ``` hoelzl@51526 ` 1542` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1543` ``` shows "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) ``` hoelzl@51526 ` 1544` ``` ==> f -- a --> L" ``` hoelzl@51526 ` 1545` ```by (simp add: LIM_eq) ``` hoelzl@51526 ` 1546` hoelzl@51526 ` 1547` ```lemma LIM_D: ``` hoelzl@51526 ` 1548` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` hoelzl@51526 ` 1549` ``` shows "[| f -- a --> L; 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" ``` hoelzl@51526 ` 1551` ```by (simp add: LIM_eq) ``` hoelzl@51526 ` 1552` hoelzl@51526 ` 1553` ```lemma LIM_offset: ``` hoelzl@51526 ` 1554` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1555` ``` shows "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" ``` hoelzl@51641 ` 1556` ``` unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp ``` hoelzl@51526 ` 1557` hoelzl@51526 ` 1558` ```lemma LIM_offset_zero: ``` hoelzl@51526 ` 1559` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1560` ``` shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" ``` haftmann@57512 ` 1561` ```by (drule_tac k="a" in LIM_offset, simp add: add.commute) ``` hoelzl@51526 ` 1562` hoelzl@51526 ` 1563` ```lemma LIM_offset_zero_cancel: ``` hoelzl@51526 ` 1564` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1565` ``` shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" ``` hoelzl@51526 ` 1566` ```by (drule_tac k="- a" in LIM_offset, simp) ``` hoelzl@51526 ` 1567` hoelzl@51642 ` 1568` ```lemma LIM_offset_zero_iff: ``` hoelzl@51642 ` 1569` ``` fixes f :: "'a :: real_normed_vector \ _" ``` hoelzl@51642 ` 1570` ``` shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" ``` hoelzl@51642 ` 1571` ``` using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto ``` hoelzl@51642 ` 1572` hoelzl@51526 ` 1573` ```lemma LIM_zero: ``` hoelzl@51526 ` 1574` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1575` ``` shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" ``` hoelzl@51526 ` 1576` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1577` hoelzl@51526 ` 1578` ```lemma LIM_zero_cancel: ``` hoelzl@51526 ` 1579` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1580` ``` shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" ``` hoelzl@51526 ` 1581` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1582` hoelzl@51526 ` 1583` ```lemma LIM_zero_iff: ``` hoelzl@51526 ` 1584` ``` fixes f :: "'a::metric_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1585` ``` shows "((\x. f x - l) ---> 0) F = (f ---> l) F" ``` hoelzl@51526 ` 1586` ```unfolding tendsto_iff dist_norm by simp ``` hoelzl@51526 ` 1587` hoelzl@51526 ` 1588` ```lemma LIM_imp_LIM: ``` hoelzl@51526 ` 1589` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1590` ``` fixes g :: "'a::topological_space \ 'c::real_normed_vector" ``` hoelzl@51526 ` 1591` ``` assumes f: "f -- a --> l" ``` hoelzl@51526 ` 1592` ``` assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" ``` hoelzl@51526 ` 1593` ``` shows "g -- a --> m" ``` hoelzl@51526 ` 1594` ``` by (rule metric_LIM_imp_LIM [OF f], ``` hoelzl@51526 ` 1595` ``` simp add: dist_norm le) ``` hoelzl@51526 ` 1596` hoelzl@51526 ` 1597` ```lemma LIM_equal2: ``` hoelzl@51526 ` 1598` ``` fixes f g :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1599` ``` assumes 1: "0 < R" ``` hoelzl@51526 ` 1600` ``` assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" ``` hoelzl@51526 ` 1601` ``` shows "g -- a --> l \ f -- a --> l" ``` hoelzl@51526 ` 1602` ```by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) ``` hoelzl@51526 ` 1603` hoelzl@51526 ` 1604` ```lemma LIM_compose2: ``` hoelzl@51526 ` 1605` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1606` ``` assumes f: "f -- a --> b" ``` hoelzl@51526 ` 1607` ``` assumes g: "g -- b --> c" ``` hoelzl@51526 ` 1608` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" ``` hoelzl@51526 ` 1609` ``` shows "(\x. g (f x)) -- a --> c" ``` hoelzl@51526 ` 1610` ```by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) ``` hoelzl@51526 ` 1611` hoelzl@51526 ` 1612` ```lemma real_LIM_sandwich_zero: ``` hoelzl@51526 ` 1613` ``` fixes f g :: "'a::topological_space \ real" ``` hoelzl@51526 ` 1614` ``` assumes f: "f -- a --> 0" ``` hoelzl@51526 ` 1615` ``` assumes 1: "\x. x \ a \ 0 \ g x" ``` hoelzl@51526 ` 1616` ``` assumes 2: "\x. x \ a \ g x \ f x" ``` hoelzl@51526 ` 1617` ``` shows "g -- a --> 0" ``` hoelzl@51526 ` 1618` ```proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) ``` hoelzl@51526 ` 1619` ``` fix x assume x: "x \ a" ``` hoelzl@51526 ` 1620` ``` have "norm (g x - 0) = g x" by (simp add: 1 x) ``` hoelzl@51526 ` 1621` ``` also have "g x \ f x" by (rule 2 [OF x]) ``` hoelzl@51526 ` 1622` ``` also have "f x \ \f x\" by (rule abs_ge_self) ``` hoelzl@51526 ` 1623` ``` also have "\f x\ = norm (f x - 0)" by simp ``` hoelzl@51526 ` 1624` ``` finally show "norm (g x - 0) \ norm (f x - 0)" . ``` hoelzl@51526 ` 1625` ```qed ``` hoelzl@51526 ` 1626` hoelzl@51526 ` 1627` hoelzl@51526 ` 1628` ```subsection {* Continuity *} ``` hoelzl@51526 ` 1629` hoelzl@51526 ` 1630` ```lemma LIM_isCont_iff: ``` hoelzl@51526 ` 1631` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1632` ``` shows "(f -- a --> f a) = ((\h. f (a + h)) -- 0 --> f a)" ``` hoelzl@51526 ` 1633` ```by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) ``` hoelzl@51526 ` 1634` hoelzl@51526 ` 1635` ```lemma isCont_iff: ``` hoelzl@51526 ` 1636` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` hoelzl@51526 ` 1637` ``` shows "isCont f x = (\h. f (x + h)) -- 0 --> f x" ``` hoelzl@51526 ` 1638` ```by (simp add: isCont_def LIM_isCont_iff) ``` hoelzl@51526 ` 1639` hoelzl@51526 ` 1640` ```lemma isCont_LIM_compose2: ``` hoelzl@51526 ` 1641` ``` fixes a :: "'a::real_normed_vector" ``` hoelzl@51526 ` 1642` ``` assumes f [unfolded isCont_def]: "isCont f a" ``` hoelzl@51526 ` 1643` ``` assumes g: "g -- f a --> l" ``` hoelzl@51526 ` 1644` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" ``` hoelzl@51526 ` 1645` ``` shows "(\x. g (f x)) -- a --> l" ``` hoelzl@51526 ` 1646` ```by (rule LIM_compose2 [OF f g inj]) ``` hoelzl@51526 ` 1647` hoelzl@51526 ` 1648` hoelzl@51526 ` 1649` ```lemma isCont_norm [simp]: ``` hoelzl@51526 ` 1650` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1651` ``` shows "isCont f a \ isCont (\x. norm (f x)) a" ``` hoelzl@51526 ` 1652` ``` by (fact continuous_norm) ``` hoelzl@51526 ` 1653` hoelzl@51526 ` 1654` ```lemma isCont_rabs [simp]: ``` hoelzl@51526 ` 1655` ``` fixes f :: "'a::t2_space \ real" ``` hoelzl@51526 ` 1656` ``` shows "isCont f a \ isCont (\x. \f x\) a" ``` hoelzl@51526 ` 1657` ``` by (fact continuous_rabs) ``` hoelzl@51526 ` 1658` hoelzl@51526 ` 1659` ```lemma isCont_add [simp]: ``` hoelzl@51526 ` 1660` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1661` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" ``` hoelzl@51526 ` 1662` ``` by (fact continuous_add) ``` hoelzl@51526 ` 1663` hoelzl@51526 ` 1664` ```lemma isCont_minus [simp]: ``` hoelzl@51526 ` 1665` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1666` ``` shows "isCont f a \ isCont (\x. - f x) a" ``` hoelzl@51526 ` 1667` ``` by (fact continuous_minus) ``` hoelzl@51526 ` 1668` hoelzl@51526 ` 1669` ```lemma isCont_diff [simp]: ``` hoelzl@51526 ` 1670` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51526 ` 1671` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" ``` hoelzl@51526 ` 1672` ``` by (fact continuous_diff) ``` hoelzl@51526 ` 1673` hoelzl@51526 ` 1674` ```lemma isCont_mult [simp]: ``` hoelzl@51526 ` 1675` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" ``` hoelzl@51526 ` 1676` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" ``` hoelzl@51526 ` 1677` ``` by (fact continuous_mult) ``` hoelzl@51526 ` 1678` hoelzl@51526 ` 1679` ```lemma (in bounded_linear) isCont: ``` hoelzl@51526 ` 1680` ``` "isCont g a \ isCont (\x. f (g x)) a" ``` hoelzl@51526 ` 1681` ``` by (fact continuous) ``` hoelzl@51526 ` 1682` hoelzl@51526 ` 1683` ```lemma (in bounded_bilinear) isCont: ``` hoelzl@51526 ` 1684` ``` "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" ``` hoelzl@51526 ` 1685` ``` by (fact continuous) ``` hoelzl@51526 ` 1686` hoelzl@51526 ` 1687` ```lemmas isCont_scaleR [simp] = ``` hoelzl@51526 ` 1688` ``` bounded_bilinear.isCont [OF bounded_bilinear_scaleR] ``` hoelzl@51526 ` 1689` hoelzl@51526 ` 1690` ```lemmas isCont_of_real [simp] = ``` hoelzl@51526 ` 1691` ``` bounded_linear.isCont [OF bounded_linear_of_real] ``` hoelzl@51526 ` 1692` hoelzl@51526 ` 1693` ```lemma isCont_power [simp]: ``` hoelzl@51526 ` 1694` ``` fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` hoelzl@51526 ` 1695` ``` shows "isCont f a \ isCont (\x. f x ^ n) a" ``` hoelzl@51526 ` 1696` ``` by (fact continuous_power) ``` hoelzl@51526 ` 1697` hoelzl@51526 ` 1698` ```lemma isCont_setsum [simp]: ``` hoelzl@51526 ` 1699` ``` fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" ``` hoelzl@51526 ` 1700` ``` shows "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" ``` hoelzl@51526 ` 1701` ``` by (auto intro: continuous_setsum) ``` hoelzl@51526 ` 1702` hoelzl@51526 ` 1703` ```subsection {* Uniform Continuity *} ``` hoelzl@51526 ` 1704` hoelzl@51531 ` 1705` ```definition ``` hoelzl@51531 ` 1706` ``` isUCont :: "['a::metric_space \ 'b::metric_space] \ bool" where ``` hoelzl@51531 ` 1707` ``` "isUCont f = (\r>0. \s>0. \x y. dist x y < s \ dist (f x) (f y) < r)" ``` hoelzl@51531 ` 1708` hoelzl@51531 ` 1709` ```lemma isUCont_isCont: "isUCont f ==> isCont f x" ``` hoelzl@51531 ` 1710` ```by (simp add: isUCont_def isCont_def LIM_def, force) ``` hoelzl@51531 ` 1711` hoelzl@51531 ` 1712` ```lemma isUCont_Cauchy: ``` hoelzl@51531 ` 1713` ``` "\isUCont f; Cauchy X\ \ Cauchy (\n. f (X n))" ``` hoelzl@51531 ` 1714` ```unfolding isUCont_def ``` hoelzl@51531 ` 1715` ```apply (rule metric_CauchyI) ``` hoelzl@51531 ` 1716` ```apply (drule_tac x=e in spec, safe) ``` hoelzl@51531 ` 1717` ```apply (drule_tac e=s in metric_CauchyD, safe) ``` hoelzl@51531 ` 1718` ```apply (rule_tac x=M in exI, simp) ``` hoelzl@51531 ` 1719` ```done ``` hoelzl@51531 ` 1720` hoelzl@51526 ` 1721` ```lemma (in bounded_linear) isUCont: "isUCont f" ``` hoelzl@51526 ` 1722` ```unfolding isUCont_def dist_norm ``` hoelzl@51526 ` 1723` ```proof (intro allI impI) ``` hoelzl@51526 ` 1724` ``` fix r::real assume r: "0 < r" ``` hoelzl@51526 ` 1725` ``` obtain K where K: "0 < K" and norm_le: "\x. norm (f x) \ norm x * K" ``` hoelzl@51526 ` 1726` ``` using pos_bounded by fast ``` hoelzl@51526 ` 1727` ``` show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" ``` hoelzl@51526 ` 1728` ``` proof (rule exI, safe) ``` nipkow@56541 ` 1729` ``` from r K show "0 < r / K" by simp ``` hoelzl@51526 ` 1730` ``` next ``` hoelzl@51526 ` 1731` ``` fix x y :: 'a ``` hoelzl@51526 ` 1732` ``` assume xy: "norm (x - y) < r / K" ``` hoelzl@51526 ` 1733` ``` have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) ``` hoelzl@51526 ` 1734` ``` also have "\ \ norm (x - y) * K" by (rule norm_le) ``` hoelzl@51526 ` 1735` ``` also from K xy have "\ < r" by (simp only: pos_less_divide_eq) ``` hoelzl@51526 ` 1736` ``` finally show "norm (f x - f y) < r" . ``` hoelzl@51526 ` 1737` ``` qed ``` hoelzl@51526 ` 1738` ```qed ``` hoelzl@51526 ` 1739` hoelzl@51526 ` 1740` ```lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" ``` hoelzl@51526 ` 1741` ```by (rule isUCont [THEN isUCont_Cauchy]) ``` hoelzl@51526 ` 1742` hoelzl@51526 ` 1743` ```lemma LIM_less_bound: ``` hoelzl@51526 ` 1744` ``` fixes f :: "real \ real" ``` hoelzl@51526 ` 1745` ``` assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" ``` hoelzl@51526 ` 1746` ``` shows "0 \ f x" ``` hoelzl@51526 ` 1747` ```proof (rule tendsto_le_const) ``` hoelzl@51526 ` 1748` ``` show "(f ---> f x) (at_left x)" ``` hoelzl@51526 ` 1749` ``` using `isCont f x` by (simp add: filterlim_at_split isCont_def) ``` hoelzl@51526 ` 1750` ``` show "eventually (\x. 0 \ f x) (at_left x)" ``` hoelzl@51641 ` 1751` ``` using ev by (auto simp: eventually_at dist_real_def intro!: exI[of _ "x - b"]) ``` hoelzl@51526 ` 1752` ```qed simp ``` hoelzl@51471 ` 1753` hoelzl@51529 ` 1754` hoelzl@51529 ` 1755` ```subsection {* Nested Intervals and Bisection -- Needed for Compactness *} ``` hoelzl@51529 ` 1756` hoelzl@51529 ` 1757` ```lemma nested_sequence_unique: ``` hoelzl@51529 ` 1758` ``` 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 ` 1759` ``` shows "\l::real. ((\n. f n \ l) \ f ----> l) \ ((\n. l \ g n) \ g ----> l)" ``` hoelzl@51529 ` 1760` ```proof - ``` hoelzl@51529 ` 1761` ``` have "incseq f" unfolding incseq_Suc_iff by fact ``` hoelzl@51529 ` 1762` ``` have "decseq g" unfolding decseq_Suc_iff by fact ``` hoelzl@51529 ` 1763` hoelzl@51529 ` 1764` ``` { fix n ``` hoelzl@51529 ` 1765` ``` from `decseq g` have "g n \ g 0" by (rule decseqD) simp ``` hoelzl@51529 ` 1766` ``` with `\n. f n \ g n`[THEN spec, of n] have "f n \ g 0" by auto } ``` hoelzl@51529 ` 1767` ``` then obtain u where "f ----> u" "\i. f i \ u" ``` hoelzl@51529 ` 1768` ``` using incseq_convergent[OF `incseq f`] by auto ``` hoelzl@51529 ` 1769` ``` moreover ``` hoelzl@51529 ` 1770` ``` { fix n ``` hoelzl@51529 ` 1771` ``` from `incseq f` have "f 0 \ f n" by (rule incseqD) simp ``` hoelzl@51529 ` 1772` ``` with `\n. f n \ g n`[THEN spec, of n] have "f 0 \ g n" by simp } ``` hoelzl@51529 ` 1773` ``` then obtain l where "g ----> l" "\i. l \ g i" ``` hoelzl@51529 ` 1774` ``` using decseq_convergent[OF `decseq g`] by auto ``` hoelzl@51529 ` 1775` ``` moreover note LIMSEQ_unique[OF assms(4) tendsto_diff[OF `f ----> u` `g ----> l`]] ``` hoelzl@51529 ` 1776` ``` ultimately show ?thesis by auto ``` hoelzl@51529 ` 1777` ```qed ``` hoelzl@51529 ` 1778` hoelzl@51529 ` 1779` ```lemma Bolzano[consumes 1, case_names trans local]: ``` hoelzl@51529 ` 1780` ``` fixes P :: "real \ real \ bool" ``` hoelzl@51529 ` 1781` ``` assumes [arith]: "a \ b" ``` hoelzl@51529 ` 1782` ``` assumes trans: "\a b c. \P a b; P b c; a \ b; b \ c\ \ P a c" ``` hoelzl@51529 ` 1783` ``` assumes local: "\x. a \ x \ x \ b \ \d>0. \a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51529 ` 1784` ``` shows "P a b" ``` hoelzl@51529 ` 1785` ```proof - ``` blanchet@55415 ` 1786` ``` 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 ` 1787` ``` def l \ "\n. fst (bisect n)" and u \ "\n. snd (bisect n)" ``` hoelzl@51529 ` 1788` ``` 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 ` 1789` ``` 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 ` 1790` ``` by (simp_all add: l_def u_def bisect_def split: prod.split) ``` hoelzl@51529 ` 1791` hoelzl@51529 ` 1792` ``` { fix n have "l n \ u n" by (induct n) auto } note this[simp] ``` hoelzl@51529 ` 1793` hoelzl@51529 ` 1794` ``` have "\x. ((\n. l n \ x) \ l ----> x) \ ((\n. x \ u n) \ u ----> x)" ``` hoelzl@51529 ` 1795` ``` proof (safe intro!: nested_sequence_unique) ``` hoelzl@51529 ` 1796` ``` fix n show "l n \ l (Suc n)" "u (Suc n) \ u n" by (induct n) auto ``` hoelzl@51529 ` 1797` ``` next ``` hoelzl@51529 ` 1798` ``` { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) } ``` hoelzl@51529 ` 1799` ``` then show "(\n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero) ``` hoelzl@51529 ` 1800` ``` qed fact ``` hoelzl@51529 ` 1801` ``` then obtain x where x: "\n. l n \ x" "\n. x \ u n" and "l ----> x" "u ----> x" by auto ``` hoelzl@51529 ` 1802` ``` obtain d where "0 < d" and d: "\a b. a \ x \ x \ b \ b - a < d \ P a b" ``` hoelzl@51529 ` 1803` ``` using `l 0 \ x` `x \ u 0` local[of x] by auto ``` hoelzl@51529 ` 1804` hoelzl@51529 ` 1805` ``` show "P a b" ``` hoelzl@51529 ` 1806` ``` proof (rule ccontr) ``` hoelzl@51529 ` 1807` ``` assume "\ P a b" ``` hoelzl@51529 ` 1808` ``` { fix n have "\ P (l n) (u n)" ``` hoelzl@51529 ` 1809` ``` proof (induct n) ``` hoelzl@51529 ` 1810` ``` case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto ``` hoelzl@51529 ` 1811` ``` qed (simp add: `\ P a b`) } ``` hoelzl@51529 ` 1812` ``` moreover ``` hoelzl@51529 ` 1813` ``` { have "eventually (\n. x - d / 2 < l n) sequentially" ``` hoelzl@51529 ` 1814` ``` using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 1815` ``` moreover have "eventually (\n. u n < x + d / 2) sequentially" ``` hoelzl@51529 ` 1816` ``` using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto ``` hoelzl@51529 ` 1817` ``` ultimately have "eventually (\n. P (l n) (u n)) sequentially" ``` hoelzl@51529 ` 1818` ``` proof eventually_elim ``` hoelzl@51529 ` 1819` ``` fix n assume "x - d / 2 < l n" "u n < x + d / 2" ``` hoelzl@51529 ` 1820` ``` from add_strict_mono[OF this] have "u n - l n < d" by simp ``` hoelzl@51529 ` 1821` ``` with x show "P (l n) (u n)" by (rule d) ``` hoelzl@51529 ` 1822` ``` qed } ``` hoelzl@51529 ` 1823` ``` ultimately show False by simp ``` hoelzl@51529 ` 1824` ``` qed ``` hoelzl@51529 ` 1825` ```qed ``` hoelzl@51529 ` 1826` hoelzl@51529 ` 1827` ```lemma compact_Icc[simp, intro]: "compact {a .. b::real}" ``` hoelzl@51529 ` 1828` ```proof (cases "a \ b", rule compactI) ``` hoelzl@51529 ` 1829` ``` fix C assume C: "a \ b" "\t\C. open t" "{a..b} \ \C" ``` hoelzl@51529 ` 1830` ``` def T == "{a .. b}" ``` hoelzl@51529 ` 1831` ``` from C(1,3) show "\C'\C. finite C' \ {a..b} \ \C'" ``` hoelzl@51529 ` 1832` ``` proof (induct rule: Bolzano) ``` hoelzl@51529 ` 1833` ``` case (trans a b c) ``` hoelzl@51529 ` 1834` ``` then have *: "{a .. c} = {a .. b} \ {b .. c}" by auto ``` hoelzl@51529 ` 1835` ``` from trans obtain C1 C2 where "C1\C \ finite C1 \ {a..b} \ \C1" "C2\C \ finite C2 \ {b..c} \ \C2" ``` hoelzl@51529 ` 1836` ``` by (auto simp: *) ``` hoelzl@51529 ` 1837` ``` with trans show ?case ``` hoelzl@51529 ` 1838` ``` unfolding * by (intro exI[of _ "C1 \ C2"]) auto ``` hoelzl@51529 ` 1839` ``` next ``` hoelzl@51529 ` 1840` ``` case (local x) ``` hoelzl@51529 ` 1841` ``` then have "x \ \C" using C by auto ``` hoelzl@51529 ` 1842` ``` with C(2) obtain c where "x \ c" "open c" "c \ C" by auto ``` hoelzl@51529 ` 1843` ``` then obtain e where "0 < e" "{x - e <..< x + e} \ c" ``` hoelzl@51529 ` 1844` ``` by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff) ``` hoelzl@51529 ` 1845` ``` with `c \ C` show ?case ``` hoelzl@51529 ` 1846` ``` by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto ``` hoelzl@51529 ` 1847` ``` qed ``` hoelzl@51529 ` 1848` ```qed simp ``` hoelzl@51529 ` 1849` hoelzl@51529 ` 1850` hoelzl@57447 ` 1851` ```lemma continuous_image_closed_interval: ``` hoelzl@57447 ` 1852` ``` fixes a b and f :: "real \ real" ``` hoelzl@57447 ` 1853` ``` defines "S \ {a..b}" ``` hoelzl@57447 ` 1854` ``` assumes "a \ b" and f: "continuous_on S f" ``` hoelzl@57447 ` 1855` ``` shows "\c d. f`S = {c..d} \ c \ d" ``` hoelzl@57447 ` 1856` ```proof - ``` hoelzl@57447 ` 1857` ``` have S: "compact S" "S \ {}" ``` hoelzl@57447 ` 1858` ``` using `a \ b` by (auto simp: S_def) ``` hoelzl@57447 ` 1859` ``` obtain c where "c \ S" "\d\S. f d \ f c" ``` hoelzl@57447 ` 1860` ``` using continuous_attains_sup[OF S f] by auto ``` hoelzl@57447 ` 1861` ``` moreover obtain d where "d \ S" "\c\S. f d \ f c" ``` hoelzl@57447 ` 1862` ``` using continuous_attains_inf[OF S f] by auto ``` hoelzl@57447 ` 1863` ``` moreover have "connected (f`S)" ``` hoelzl@57447 ` 1864` ``` using connected_continuous_image[OF f] connected_Icc by (auto simp: S_def) ``` hoelzl@57447 ` 1865` ``` ultimately have "f ` S = {f d .. f c} \ f d \ f c" ``` hoelzl@57447 ` 1866` ``` by (auto simp: connected_iff_interval) ``` hoelzl@57447 ` 1867` ``` then show ?thesis ``` hoelzl@57447 ` 1868` ``` by auto ``` hoelzl@57447 ` 1869` ```qed ``` hoelzl@57447 ` 1870` hoelzl@51529 ` 1871` ```subsection {* Boundedness of continuous functions *} ``` hoelzl@51529 ` 1872` hoelzl@51529 ` 1873` ```text{*By bisection, function continuous on closed interval is bounded above*} ``` hoelzl@51529 ` 1874` hoelzl@51529 ` 1875` ```lemma isCont_eq_Ub: ``` hoelzl@51529 ` 1876` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1877` ``` shows "a \ b \ \x::real. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1878` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51529 ` 1879` ``` using continuous_attains_sup[of "{a .. b}" f] ``` hoelzl@51529 ` 1880` ``` by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) ``` hoelzl@51529 ` 1881` hoelzl@51529 ` 1882` ```lemma isCont_eq_Lb: ``` hoelzl@51529 ` 1883` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1884` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1885` ``` \M. (\x. a \ x \ x \ b \ M \ f x) \ (\x. a \ x \ x \ b \ f x = M)" ``` hoelzl@51529 ` 1886` ``` using continuous_attains_inf[of "{a .. b}" f] ``` hoelzl@51529 ` 1887` ``` by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def) ``` hoelzl@51529 ` 1888` hoelzl@51529 ` 1889` ```lemma isCont_bounded: ``` hoelzl@51529 ` 1890` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1891` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ \M. \x. a \ x \ x \ b \ f x \ M" ``` hoelzl@51529 ` 1892` ``` using isCont_eq_Ub[of a b f] by auto ``` hoelzl@51529 ` 1893` hoelzl@51529 ` 1894` ```lemma isCont_has_Ub: ``` hoelzl@51529 ` 1895` ``` fixes f :: "real \ 'a::linorder_topology" ``` hoelzl@51529 ` 1896` ``` shows "a \ b \ \x. a \ x \ x \ b \ isCont f x \ ``` hoelzl@51529 ` 1897` ``` \M. (\x. a \ x \ x \ b \ f x \ M) \ (\N. N < M \ (\x. a \ x \ x \ b \ N < f x))" ``` hoelzl@51529 ` 1898` ``` using isCont_eq_Ub[of a b f] by auto ``` hoelzl@51529 ` 1899` hoelzl@51529 ` 1900` ```(*HOL style here: object-level formulations*) ``` hoelzl@51529 ` 1901` ```lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & ``` hoelzl@51529 ` 1902` ``` (\x. a \ x & x \ b --> isCont f x)) ``` hoelzl@51529 ` 1903` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` hoelzl@51529 ` 1904` ``` by (blast intro: IVT) ``` hoelzl@51529 ` 1905` hoelzl@51529 ` 1906` ```lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & ``` hoelzl@51529 ` 1907` ``` (\x. a \ x & x \ b --> isCont f x)) ``` hoelzl@51529 ` 1908` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` hoelzl@51529 ` 1909` ``` by (blast intro: IVT2) ``` hoelzl@51529 ` 1910` hoelzl@51529 ` 1911` ```lemma isCont_Lb_Ub: ``` hoelzl@51529 ` 1912` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 1913` ``` assumes "a \ b" "\x. a \ x \ x \ b \ isCont f x" ``` hoelzl@51529 ` 1914` ``` shows "\L M. (\x. a \ x \ x \ b \ L \ f x \ f x \ M) \ ``` hoelzl@51529 ` 1915` ``` (\y. L \ y \ y \ M \ (\x. a \ x \ x \ b \ (f x = y)))" ``` hoelzl@51529 ` 1916` ```proof - ``` hoelzl@51529 ` 1917` ``` obtain M where M: "a \ M" "M \ b" "\x. a \ x \ x \ b \ f x \ f M" ``` hoelzl@51529 ` 1918` ``` using isCont_eq_Ub[OF assms] by auto ``` hoelzl@51529 ` 1919` ``` obtain L where L: "a \ L" "L \ b" "\x. a \ x \ x \ b \ f L \ f x" ``` hoelzl@51529 ` 1920` ``` using isCont_eq_Lb[OF assms] by auto ``` hoelzl@51529 ` 1921` ``` show ?thesis ``` hoelzl@51529 ` 1922` ``` using IVT[of f L _ M] IVT2[of f L _ M] M L assms ``` hoelzl@51529 ` 1923` ``` apply (rule_tac x="f L" in exI) ``` hoelzl@51529 ` 1924` ``` apply (rule_tac x="f M" in exI) ``` hoelzl@51529 ` 1925` ``` apply (cases "L \ M") ``` hoelzl@51529 ` 1926` ``` apply (simp, metis order_trans) ``` hoelzl@51529 ` 1927` ``` apply (simp, metis order_trans) ``` hoelzl@51529 ` 1928` ``` done ``` hoelzl@51529 ` 1929` ```qed ``` hoelzl@51529 ` 1930` hoelzl@51529 ` 1931` hoelzl@51529 ` 1932` ```text{*Continuity of inverse function*} ``` hoelzl@51529 ` 1933` hoelzl@51529 ` 1934` ```lemma isCont_inverse_function: ``` hoelzl@51529 ` 1935` ``` fixes f g :: "real \ real" ``` hoelzl@51529 ` 1936` ``` assumes d: "0 < d" ``` hoelzl@51529 ` 1937` ``` and inj: "\z. \z-x\ \ d \ g (f z) = z" ``` hoelzl@51529 ` 1938` ``` and cont: "\z. \z-x\ \ d \ isCont f z" ``` hoelzl@51529 ` 1939` ``` shows "isCont g (f x)" ``` hoelzl@51529 ` 1940` ```proof - ``` hoelzl@51529 ` 1941` ``` let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}" ``` hoelzl@51529 ` 1942` hoelzl@51529 ` 1943` ``` have f: "continuous_on ?D f" ``` hoelzl@51529 ` 1944` ``` using cont by (intro continuous_at_imp_continuous_on ballI) auto ``` hoelzl@51529 ` 1945` ``` then have g: "continuous_on (f`?D) g" ``` hoelzl@51529 ` 1946` ``` using inj by (intro continuous_on_inv) auto ``` hoelzl@51529 ` 1947` hoelzl@51529 ` 1948` ``` from d f have "{min ?A ?B <..< max ?A ?B} \ f ` ?D" ``` hoelzl@51529 ` 1949` ``` by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max) ``` hoelzl@51529 ` 1950` ``` with g have "continuous_on {min ?A ?B <..< max ?A ?B} g" ``` hoelzl@51529 ` 1951` ``` by (rule continuous_on_subset) ``` hoelzl@51529 ` 1952` ``` moreover ``` hoelzl@51529 ` 1953` ``` have "(?A < f x \ f x < ?B) \ (?B < f x \ f x < ?A)" ``` hoelzl@51529 ` 1954` ``` using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto ``` hoelzl@51529 ` 1955` ``` then have "f x \ {min ?A ?B <..< max ?A ?B}" ``` hoelzl@51529 ` 1956` ``` by auto ``` hoelzl@51529 ` 1957` ``` ultimately ``` hoelzl@51529 ` 1958` ``` show ?thesis ``` hoelzl@51529 ` 1959` ``` by (simp add: continuous_on_eq_continuous_at) ``` hoelzl@51529 ` 1960` ```qed ``` hoelzl@51529 ` 1961` hoelzl@51529 ` 1962` ```lemma isCont_inverse_function2: ``` hoelzl@51529 ` 1963` ``` fixes f g :: "real \ real" shows ``` hoelzl@51529 ` 1964` ``` "\a < x; x < b; ``` hoelzl@51529 ` 1965` ``` \z. a \ z \ z \ b \ g (f z) = z; ``` hoelzl@51529 ` 1966` ``` \z. a \ z \ z \ b \ isCont f z\ ``` hoelzl@51529 ` 1967` ``` \ isCont g (f x)" ``` hoelzl@51529 ` 1968` ```apply (rule isCont_inverse_function ``` hoelzl@51529 ` 1969` ``` [where f=f and d="min (x - a) (b - x)"]) ``` hoelzl@51529 ` 1970` ```apply (simp_all add: abs_le_iff) ``` hoelzl@51529 ` 1971` ```done ``` hoelzl@51529 ` 1972` hoelzl@51529 ` 1973` ```(* need to rename second isCont_inverse *) ``` hoelzl@51529 ` 1974` hoelzl@51529 ` 1975` ```lemma isCont_inv_fun: ``` hoelzl@51529 ` 1976` ``` fixes f g :: "real \ real" ``` hoelzl@51529 ` 1977` ``` shows "[| 0 < d; \z. \z - x\ \ d --> g(f(z)) = z; ``` hoelzl@51529 ` 1978` ``` \z. \z - x\ \ d --> isCont f z |] ``` hoelzl@51529 ` 1979` ``` ==> isCont g (f x)" ``` hoelzl@51529 ` 1980` ```by (rule isCont_inverse_function) ``` hoelzl@51529 ` 1981` hoelzl@51529 ` 1982` ```text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*} ``` hoelzl@51529 ` 1983` ```lemma LIM_fun_gt_zero: ``` hoelzl@51529 ` 1984` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 1985` ``` shows "f -- c --> l \ 0 < l \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ 0 < f x)" ``` hoelzl@51529 ` 1986` ```apply (drule (1) LIM_D, clarify) ``` hoelzl@51529 ` 1987` ```apply (rule_tac x = s in exI) ``` hoelzl@51529 ` 1988` ```apply (simp add: abs_less_iff) ``` hoelzl@51529 ` 1989` ```done ``` hoelzl@51529 ` 1990` hoelzl@51529 ` 1991` ```lemma LIM_fun_less_zero: ``` hoelzl@51529 ` 1992` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 1993` ``` shows "f -- c --> l \ l < 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x < 0)" ``` hoelzl@51529 ` 1994` ```apply (drule LIM_D [where r="-l"], simp, clarify) ``` hoelzl@51529 ` 1995` ```apply (rule_tac x = s in exI) ``` hoelzl@51529 ` 1996` ```apply (simp add: abs_less_iff) ``` hoelzl@51529 ` 1997` ```done ``` hoelzl@51529 ` 1998` hoelzl@51529 ` 1999` ```lemma LIM_fun_not_zero: ``` hoelzl@51529 ` 2000` ``` fixes f :: "real \ real" ``` hoelzl@51529 ` 2001` ``` shows "f -- c --> l \ l \ 0 \ \r. 0 < r \ (\x. x \ c \ \c - x\ < r \ f x \ 0)" ``` hoelzl@51529 ` 2002` ``` 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 ` 2003` huffman@31349 ` 2004` ```end ``` hoelzl@50324 ` 2005`