src/HOL/Lim.thy
 author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51478 270b21f3ae0a parent 51473 1210309fddab permissions -rw-r--r--
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
 paulson@10751 ` 1` ```(* Title : Lim.thy ``` paulson@10751 ` 2` ``` Author : Jacques D. Fleuriot ``` paulson@10751 ` 3` ``` Copyright : 1998 University of Cambridge ``` paulson@14477 ` 4` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` paulson@10751 ` 5` ```*) ``` paulson@10751 ` 6` huffman@21165 ` 7` ```header{* Limits and Continuity *} ``` paulson@10751 ` 8` nipkow@15131 ` 9` ```theory Lim ``` haftmann@29197 ` 10` ```imports SEQ ``` nipkow@15131 ` 11` ```begin ``` paulson@14477 ` 12` huffman@31392 ` 13` ```subsection {* Limits of Functions *} ``` huffman@31349 ` 14` paulson@14477 ` 15` ```lemma LIM_eq: ``` huffman@31338 ` 16` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` huffman@31338 ` 17` ``` shows "f -- a --> L = ``` huffman@20561 ` 18` ``` (\r>0.\s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r)" ``` huffman@31338 ` 19` ```by (simp add: LIM_def dist_norm) ``` paulson@14477 ` 20` huffman@20552 ` 21` ```lemma LIM_I: ``` huffman@31338 ` 22` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` huffman@31338 ` 23` ``` shows "(!!r. 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r) ``` huffman@20552 ` 24` ``` ==> f -- a --> L" ``` huffman@20552 ` 25` ```by (simp add: LIM_eq) ``` huffman@20552 ` 26` paulson@14477 ` 27` ```lemma LIM_D: ``` huffman@31338 ` 28` ``` fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector" ``` huffman@31338 ` 29` ``` shows "[| f -- a --> L; 0 \s>0.\x. x \ a & norm (x-a) < s --> norm (f x - L) < r" ``` paulson@14477 ` 31` ```by (simp add: LIM_eq) ``` paulson@14477 ` 32` huffman@31338 ` 33` ```lemma LIM_offset: ``` huffman@36662 ` 34` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31338 ` 35` ``` shows "f -- a --> L \ (\x. f (x + k)) -- a - k --> L" ``` huffman@36662 ` 36` ```apply (rule topological_tendstoI) ``` huffman@36662 ` 37` ```apply (drule (2) topological_tendstoD) ``` huffman@36662 ` 38` ```apply (simp only: eventually_at dist_norm) ``` huffman@36662 ` 39` ```apply (clarify, rule_tac x=d in exI, safe) ``` huffman@20756 ` 40` ```apply (drule_tac x="x + k" in spec) ``` nipkow@29667 ` 41` ```apply (simp add: algebra_simps) ``` huffman@20756 ` 42` ```done ``` huffman@20756 ` 43` huffman@31338 ` 44` ```lemma LIM_offset_zero: ``` huffman@36662 ` 45` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31338 ` 46` ``` shows "f -- a --> L \ (\h. f (a + h)) -- 0 --> L" ``` huffman@21239 ` 47` ```by (drule_tac k="a" in LIM_offset, simp add: add_commute) ``` huffman@21239 ` 48` huffman@31338 ` 49` ```lemma LIM_offset_zero_cancel: ``` huffman@36662 ` 50` ``` fixes a :: "'a::real_normed_vector" ``` huffman@31338 ` 51` ``` shows "(\h. f (a + h)) -- 0 --> L \ f -- a --> L" ``` huffman@21239 ` 52` ```by (drule_tac k="- a" in LIM_offset, simp) ``` huffman@21239 ` 53` huffman@31338 ` 54` ```lemma LIM_zero: ``` huffman@36662 ` 55` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` huffman@44570 ` 56` ``` shows "(f ---> l) F \ ((\x. f x - l) ---> 0) F" ``` huffman@36662 ` 57` ```unfolding tendsto_iff dist_norm by simp ``` huffman@21239 ` 58` huffman@31338 ` 59` ```lemma LIM_zero_cancel: ``` huffman@36662 ` 60` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` huffman@44570 ` 61` ``` shows "((\x. f x - l) ---> 0) F \ (f ---> l) F" ``` huffman@36662 ` 62` ```unfolding tendsto_iff dist_norm by simp ``` huffman@21239 ` 63` huffman@31338 ` 64` ```lemma LIM_zero_iff: ``` huffman@31338 ` 65` ``` fixes f :: "'a::metric_space \ 'b::real_normed_vector" ``` huffman@44570 ` 66` ``` shows "((\x. f x - l) ---> 0) F = (f ---> l) F" ``` huffman@36662 ` 67` ```unfolding tendsto_iff dist_norm by simp ``` huffman@21399 ` 68` huffman@31338 ` 69` ```lemma LIM_imp_LIM: ``` huffman@36662 ` 70` ``` fixes f :: "'a::topological_space \ 'b::real_normed_vector" ``` huffman@36662 ` 71` ``` fixes g :: "'a::topological_space \ 'c::real_normed_vector" ``` huffman@31338 ` 72` ``` assumes f: "f -- a --> l" ``` huffman@31338 ` 73` ``` assumes le: "\x. x \ a \ norm (g x - m) \ norm (f x - l)" ``` huffman@31338 ` 74` ``` shows "g -- a --> m" ``` huffman@44251 ` 75` ``` by (rule metric_LIM_imp_LIM [OF f], ``` huffman@44251 ` 76` ``` simp add: dist_norm le) ``` huffman@31338 ` 77` huffman@31338 ` 78` ```lemma LIM_equal2: ``` huffman@36662 ` 79` ``` fixes f g :: "'a::real_normed_vector \ 'b::topological_space" ``` huffman@31338 ` 80` ``` assumes 1: "0 < R" ``` huffman@31338 ` 81` ``` assumes 2: "\x. \x \ a; norm (x - a) < R\ \ f x = g x" ``` huffman@31338 ` 82` ``` shows "g -- a --> l \ f -- a --> l" ``` huffman@36662 ` 83` ```by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm) ``` huffman@31338 ` 84` huffman@23040 ` 85` ```lemma LIM_compose2: ``` huffman@31338 ` 86` ``` fixes a :: "'a::real_normed_vector" ``` huffman@23040 ` 87` ``` assumes f: "f -- a --> b" ``` huffman@23040 ` 88` ``` assumes g: "g -- b --> c" ``` huffman@23040 ` 89` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ b" ``` huffman@23040 ` 90` ``` shows "(\x. g (f x)) -- a --> c" ``` huffman@31338 ` 91` ```by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]]) ``` huffman@23040 ` 92` huffman@21282 ` 93` ```lemma real_LIM_sandwich_zero: ``` huffman@36662 ` 94` ``` fixes f g :: "'a::topological_space \ real" ``` huffman@21282 ` 95` ``` assumes f: "f -- a --> 0" ``` huffman@21282 ` 96` ``` assumes 1: "\x. x \ a \ 0 \ g x" ``` huffman@21282 ` 97` ``` assumes 2: "\x. x \ a \ g x \ f x" ``` huffman@21282 ` 98` ``` shows "g -- a --> 0" ``` hoelzl@51471 ` 99` ```proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *) ``` huffman@21282 ` 100` ``` fix x assume x: "x \ a" ``` huffman@21282 ` 101` ``` have "norm (g x - 0) = g x" by (simp add: 1 x) ``` huffman@21282 ` 102` ``` also have "g x \ f x" by (rule 2 [OF x]) ``` huffman@21282 ` 103` ``` also have "f x \ \f x\" by (rule abs_ge_self) ``` huffman@21282 ` 104` ``` also have "\f x\ = norm (f x - 0)" by simp ``` huffman@21282 ` 105` ``` finally show "norm (g x - 0) \ norm (f x - 0)" . ``` huffman@21282 ` 106` ```qed ``` huffman@21282 ` 107` paulson@14477 ` 108` huffman@20755 ` 109` ```subsection {* Continuity *} ``` paulson@14477 ` 110` huffman@31338 ` 111` ```lemma LIM_isCont_iff: ``` huffman@36665 ` 112` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` huffman@31338 ` 113` ``` shows "(f -- a --> f a) = ((\h. f (a + h)) -- 0 --> f a)" ``` huffman@21239 ` 114` ```by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel]) ``` huffman@21239 ` 115` huffman@31338 ` 116` ```lemma isCont_iff: ``` huffman@36665 ` 117` ``` fixes f :: "'a::real_normed_vector \ 'b::topological_space" ``` huffman@31338 ` 118` ``` shows "isCont f x = (\h. f (x + h)) -- 0 --> f x" ``` huffman@21239 ` 119` ```by (simp add: isCont_def LIM_isCont_iff) ``` huffman@21239 ` 120` huffman@23040 ` 121` ```lemma isCont_LIM_compose2: ``` huffman@31338 ` 122` ``` fixes a :: "'a::real_normed_vector" ``` huffman@23040 ` 123` ``` assumes f [unfolded isCont_def]: "isCont f a" ``` huffman@23040 ` 124` ``` assumes g: "g -- f a --> l" ``` huffman@23040 ` 125` ``` assumes inj: "\d>0. \x. x \ a \ norm (x - a) < d \ f x \ f a" ``` huffman@23040 ` 126` ``` shows "(\x. g (f x)) -- a --> l" ``` huffman@23040 ` 127` ```by (rule LIM_compose2 [OF f g inj]) ``` huffman@23040 ` 128` hoelzl@51478 ` 129` hoelzl@51478 ` 130` ```lemma isCont_norm [simp]: ``` hoelzl@51478 ` 131` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 132` ``` shows "isCont f a \ isCont (\x. norm (f x)) a" ``` hoelzl@51478 ` 133` ``` by (fact continuous_norm) ``` hoelzl@51478 ` 134` hoelzl@51478 ` 135` ```lemma isCont_rabs [simp]: ``` hoelzl@51478 ` 136` ``` fixes f :: "'a::t2_space \ real" ``` hoelzl@51478 ` 137` ``` shows "isCont f a \ isCont (\x. \f x\) a" ``` hoelzl@51478 ` 138` ``` by (fact continuous_rabs) ``` hoelzl@51478 ` 139` hoelzl@51478 ` 140` ```lemma isCont_add [simp]: ``` hoelzl@51478 ` 141` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 142` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x + g x) a" ``` hoelzl@51478 ` 143` ``` by (fact continuous_add) ``` hoelzl@51478 ` 144` hoelzl@51478 ` 145` ```lemma isCont_minus [simp]: ``` hoelzl@51478 ` 146` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 147` ``` shows "isCont f a \ isCont (\x. - f x) a" ``` hoelzl@51478 ` 148` ``` by (fact continuous_minus) ``` hoelzl@51478 ` 149` hoelzl@51478 ` 150` ```lemma isCont_diff [simp]: ``` hoelzl@51478 ` 151` ``` fixes f :: "'a::t2_space \ 'b::real_normed_vector" ``` hoelzl@51478 ` 152` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x - g x) a" ``` hoelzl@51478 ` 153` ``` by (fact continuous_diff) ``` hoelzl@51478 ` 154` hoelzl@51478 ` 155` ```lemma isCont_mult [simp]: ``` hoelzl@51478 ` 156` ``` fixes f g :: "'a::t2_space \ 'b::real_normed_algebra" ``` hoelzl@51478 ` 157` ``` shows "\isCont f a; isCont g a\ \ isCont (\x. f x * g x) a" ``` hoelzl@51478 ` 158` ``` by (fact continuous_mult) ``` hoelzl@51478 ` 159` huffman@44233 ` 160` ```lemma (in bounded_linear) isCont: ``` huffman@44233 ` 161` ``` "isCont g a \ isCont (\x. f (g x)) a" ``` hoelzl@51478 ` 162` ``` by (fact continuous) ``` huffman@21282 ` 163` huffman@21282 ` 164` ```lemma (in bounded_bilinear) isCont: ``` huffman@21282 ` 165` ``` "\isCont f a; isCont g a\ \ isCont (\x. f x ** g x) a" ``` hoelzl@51478 ` 166` ``` by (fact continuous) ``` huffman@21282 ` 167` hoelzl@51478 ` 168` ```lemmas isCont_scaleR [simp] = ``` huffman@44282 ` 169` ``` bounded_bilinear.isCont [OF bounded_bilinear_scaleR] ``` huffman@21239 ` 170` huffman@44282 ` 171` ```lemmas isCont_of_real [simp] = ``` huffman@44282 ` 172` ``` bounded_linear.isCont [OF bounded_linear_of_real] ``` huffman@22627 ` 173` huffman@44233 ` 174` ```lemma isCont_power [simp]: ``` hoelzl@51478 ` 175` ``` fixes f :: "'a::t2_space \ 'b::{power,real_normed_algebra}" ``` huffman@22627 ` 176` ``` shows "isCont f a \ isCont (\x. f x ^ n) a" ``` hoelzl@51478 ` 177` ``` by (fact continuous_power) ``` huffman@29885 ` 178` huffman@44233 ` 179` ```lemma isCont_setsum [simp]: ``` hoelzl@51478 ` 180` ``` fixes f :: "'a \ 'b::t2_space \ 'c::real_normed_vector" ``` huffman@44233 ` 181` ``` shows "\i\A. isCont (f i) a \ isCont (\x. \i\A. f i x) a" ``` hoelzl@51478 ` 182` ``` by (auto intro: continuous_setsum) ``` paulson@15228 ` 183` huffman@44233 ` 184` ```lemmas isCont_intros = ``` huffman@44233 ` 185` ``` isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus ``` huffman@44233 ` 186` ``` isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR ``` huffman@44233 ` 187` ``` isCont_of_real isCont_power isCont_sgn isCont_setsum ``` hoelzl@29803 ` 188` huffman@20755 ` 189` ```subsection {* Uniform Continuity *} ``` huffman@20755 ` 190` huffman@23118 ` 191` ```lemma (in bounded_linear) isUCont: "isUCont f" ``` huffman@31338 ` 192` ```unfolding isUCont_def dist_norm ``` huffman@23118 ` 193` ```proof (intro allI impI) ``` huffman@23118 ` 194` ``` fix r::real assume r: "0 < r" ``` huffman@23118 ` 195` ``` obtain K where K: "0 < K" and norm_le: "\x. norm (f x) \ norm x * K" ``` huffman@23118 ` 196` ``` using pos_bounded by fast ``` huffman@23118 ` 197` ``` show "\s>0. \x y. norm (x - y) < s \ norm (f x - f y) < r" ``` huffman@23118 ` 198` ``` proof (rule exI, safe) ``` huffman@23118 ` 199` ``` from r K show "0 < r / K" by (rule divide_pos_pos) ``` huffman@23118 ` 200` ``` next ``` huffman@23118 ` 201` ``` fix x y :: 'a ``` huffman@23118 ` 202` ``` assume xy: "norm (x - y) < r / K" ``` huffman@23118 ` 203` ``` have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff) ``` huffman@23118 ` 204` ``` also have "\ \ norm (x - y) * K" by (rule norm_le) ``` huffman@23118 ` 205` ``` also from K xy have "\ < r" by (simp only: pos_less_divide_eq) ``` huffman@23118 ` 206` ``` finally show "norm (f x - f y) < r" . ``` huffman@23118 ` 207` ``` qed ``` huffman@23118 ` 208` ```qed ``` huffman@23118 ` 209` huffman@23118 ` 210` ```lemma (in bounded_linear) Cauchy: "Cauchy X \ Cauchy (\n. f (X n))" ``` huffman@23118 ` 211` ```by (rule isUCont [THEN isUCont_Cauchy]) ``` huffman@23118 ` 212` paulson@14477 ` 213` hoelzl@50331 ` 214` ```lemma LIM_less_bound: ``` hoelzl@50331 ` 215` ``` fixes f :: "real \ real" ``` hoelzl@50331 ` 216` ``` assumes ev: "b < x" "\ x' \ { b <..< x}. 0 \ f x'" and "isCont f x" ``` hoelzl@50331 ` 217` ``` shows "0 \ f x" ``` hoelzl@50331 ` 218` ```proof (rule tendsto_le_const) ``` hoelzl@50331 ` 219` ``` show "(f ---> f x) (at_left x)" ``` hoelzl@50331 ` 220` ``` using `isCont f x` by (simp add: filterlim_at_split isCont_def) ``` hoelzl@50331 ` 221` ``` show "eventually (\x. 0 \ f x) (at_left x)" ``` hoelzl@50331 ` 222` ``` using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"]) ``` hoelzl@50331 ` 223` ```qed simp ``` hoelzl@50331 ` 224` paulson@10751 ` 225` ```end ```