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