# HG changeset patch # User huffman # Date 1313333664 25200 # Node ID 0639898074ae54b3c683ad589dfd5ed5af239715 # Parent 013f7b14f6ff343e814e27e1f0af4769b6a95dd1 generalize lemmas about LIM and LIMSEQ to tendsto diff -r 013f7b14f6ff -r 0639898074ae src/HOL/Lim.thy --- a/src/HOL/Lim.thy Sat Aug 13 18:10:14 2011 -0700 +++ b/src/HOL/Lim.thy Sun Aug 14 07:54:24 2011 -0700 @@ -95,7 +95,7 @@ lemma LIM_add_zero: fixes f g :: "'a::topological_space \ 'b::real_normed_vector" shows "\f -- a --> 0; g -- a --> 0\ \ (\x. f x + g x) -- a --> 0" -by (drule (1) LIM_add, simp) + by (rule tendsto_add_zero) lemma LIM_minus: fixes f :: "'a::topological_space \ 'b::real_normed_vector" @@ -170,16 +170,16 @@ by (rule tendsto_norm_zero_iff) lemma LIM_rabs: "f -- a --> (l::real) \ (\x. \f x\) -- a --> \l\" -by (fold real_norm_def, rule LIM_norm) + by (rule tendsto_rabs) lemma LIM_rabs_zero: "f -- a --> (0::real) \ (\x. \f x\) -- a --> 0" -by (fold real_norm_def, rule LIM_norm_zero) + by (rule tendsto_rabs_zero) lemma LIM_rabs_zero_cancel: "(\x. \f x\) -- a --> (0::real) \ f -- a --> 0" -by (fold real_norm_def, rule LIM_norm_zero_cancel) + by (rule tendsto_rabs_zero_cancel) lemma LIM_rabs_zero_iff: "(\x. \f x\) -- a --> (0::real) = f -- a --> 0" -by (fold real_norm_def, rule LIM_norm_zero_iff) + by (rule tendsto_rabs_zero_iff) lemma at_neq_bot: fixes a :: "'a::real_normed_algebra_1" @@ -345,7 +345,7 @@ lemma (in bounded_linear) LIM_zero: "g -- a --> 0 \ (\x. f (g x)) -- a --> 0" -by (drule LIM, simp only: zero) + by (rule tendsto_zero) text {* Bounded Bilinear Operators *} @@ -358,15 +358,15 @@ assumes f: "f -- a --> 0" assumes g: "g -- a --> 0" shows "(\x. f x ** g x) -- a --> 0" -using LIM [OF f g] by (simp add: zero_left) + using f g by (rule tendsto_zero) lemma (in bounded_bilinear) LIM_left_zero: "f -- a --> 0 \ (\x. f x ** c) -- a --> 0" -by (rule bounded_linear.LIM_zero [OF bounded_linear_left]) + by (rule tendsto_left_zero) lemma (in bounded_bilinear) LIM_right_zero: "f -- a --> 0 \ (\x. c ** f x) -- a --> 0" -by (rule bounded_linear.LIM_zero [OF bounded_linear_right]) + by (rule tendsto_right_zero) lemmas LIM_mult = mult.LIM @@ -384,7 +384,7 @@ fixes f :: "'a::topological_space \ 'b::{power,real_normed_algebra}" assumes f: "f -- a --> l" shows "(\x. f x ^ n) -- a --> l ^ n" -by (induct n, simp, simp add: LIM_mult f) + using assms by (rule tendsto_power) subsubsection {* Derived theorems about @{term LIM} *} @@ -401,8 +401,7 @@ lemma LIM_sgn: fixes f :: "'a::topological_space \ 'b::real_normed_vector" shows "\f -- a --> l; l \ 0\ \ (\x. sgn (f x)) -- a --> sgn l" -unfolding sgn_div_norm -by (simp add: LIM_scaleR LIM_inverse LIM_norm) + by (rule tendsto_sgn) subsection {* Continuity *} @@ -511,11 +510,7 @@ fixes f :: "'a \ 'b::topological_space \ 'c::real_normed_vector" fixes A :: "'a set" assumes "finite A" shows "\ i \ A. isCont (f i) x \ isCont (\ x. \ i \ A. f i x) x" - using `finite A` -proof induct - case (insert a F) show "isCont (\ x. \ i \ (insert a F). f i x) x" - unfolding setsum_insert[OF `finite F` `a \ F`] by (rule isCont_add, auto simp add: insert) -qed auto + unfolding isCont_def by (simp add: tendsto_setsum) lemma LIM_less_bound: fixes f :: "real \ real" assumes "b < x" and all_le: "\ x' \ { b <..< x}. 0 \ f x'" and isCont: "isCont f x" diff -r 013f7b14f6ff -r 0639898074ae src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sat Aug 13 18:10:14 2011 -0700 +++ b/src/HOL/Limits.thy Sun Aug 14 07:54:24 2011 -0700 @@ -623,6 +623,8 @@ qed qed +subsubsection {* Norms *} + lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp @@ -642,11 +644,34 @@ "((\x. norm (f x)) ---> 0) A \ (f ---> 0) A" unfolding tendsto_iff dist_norm by simp +lemma tendsto_rabs [tendsto_intros]: + "(f ---> (l::real)) A \ ((\x. \f x\) ---> \l\) A" + by (fold real_norm_def, rule tendsto_norm) + +lemma tendsto_rabs_zero: + "(f ---> (0::real)) A \ ((\x. \f x\) ---> 0) A" + by (fold real_norm_def, rule tendsto_norm_zero) + +lemma tendsto_rabs_zero_cancel: + "((\x. \f x\) ---> (0::real)) A \ (f ---> 0) A" + by (fold real_norm_def, rule tendsto_norm_zero_cancel) + +lemma tendsto_rabs_zero_iff: + "((\x. \f x\) ---> (0::real)) A \ (f ---> 0) A" + by (fold real_norm_def, rule tendsto_norm_zero_iff) + +subsubsection {* Addition and subtraction *} + lemma tendsto_add [tendsto_intros]: fixes a b :: "'a::real_normed_vector" shows "\(f ---> a) A; (g ---> b) A\ \ ((\x. f x + g x) ---> a + b) A" by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add) +lemma tendsto_add_zero: + fixes f g :: "'a::type \ 'b::real_normed_vector" + shows "\(f ---> 0) A; (g ---> 0) A\ \ ((\x. f x + g x) ---> 0) A" + by (drule (1) tendsto_add, simp) + lemma tendsto_minus [tendsto_intros]: fixes a :: "'a::real_normed_vector" shows "(f ---> a) A \ ((\x. - f x) ---> - a) A" @@ -668,29 +693,61 @@ shows "((\x. \i\S. f i x) ---> (\i\S. a i)) A" proof (cases "finite S") assume "finite S" thus ?thesis using assms - proof (induct set: finite) - case empty show ?case - by (simp add: tendsto_const) - next - case (insert i F) thus ?case - by (simp add: tendsto_add) - qed + by (induct, simp add: tendsto_const, simp add: tendsto_add) next assume "\ finite S" thus ?thesis by (simp add: tendsto_const) qed +subsubsection {* Linear operators and multiplication *} + lemma (in bounded_linear) tendsto [tendsto_intros]: "(g ---> a) A \ ((\x. f (g x)) ---> f a) A" by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun) +lemma (in bounded_linear) tendsto_zero: + "(g ---> 0) A \ ((\x. f (g x)) ---> 0) A" + by (drule tendsto, simp only: zero) + lemma (in bounded_bilinear) tendsto [tendsto_intros]: "\(f ---> a) A; (g ---> b) A\ \ ((\x. f x ** g x) ---> a ** b) A" by (simp only: tendsto_Zfun_iff prod_diff_prod Zfun_add Zfun Zfun_left Zfun_right) +lemma (in bounded_bilinear) tendsto_zero: + assumes f: "(f ---> 0) A" + assumes g: "(g ---> 0) A" + shows "((\x. f x ** g x) ---> 0) A" + using tendsto [OF f g] by (simp add: zero_left) -subsection {* Continuity of Inverse *} +lemma (in bounded_bilinear) tendsto_left_zero: + "(f ---> 0) A \ ((\x. f x ** c) ---> 0) A" + by (rule bounded_linear.tendsto_zero [OF bounded_linear_left]) + +lemma (in bounded_bilinear) tendsto_right_zero: + "(f ---> 0) A \ ((\x. c ** f x) ---> 0) A" + by (rule bounded_linear.tendsto_zero [OF bounded_linear_right]) + +lemmas tendsto_mult = mult.tendsto + +lemma tendsto_power [tendsto_intros]: + fixes f :: "'a \ 'b::{power,real_normed_algebra}" + shows "(f ---> a) A \ ((\x. f x ^ n) ---> a ^ n) A" + by (induct n) (simp_all add: tendsto_const tendsto_mult) + +lemma tendsto_setprod [tendsto_intros]: + fixes f :: "'a \ 'b \ 'c::{real_normed_algebra,comm_ring_1}" + assumes "\i. i \ S \ (f i ---> L i) A" + shows "((\x. \i\S. f i x) ---> (\i\S. L i)) A" +proof (cases "finite S") + assume "finite S" thus ?thesis using assms + by (induct, simp add: tendsto_const, simp add: tendsto_mult) +next + assume "\ finite S" thus ?thesis + by (simp add: tendsto_const) +qed + +subsubsection {* Inverse and division *} lemma (in bounded_bilinear) Zfun_prod_Bfun: assumes f: "Zfun f A" @@ -815,6 +872,13 @@ \ ((\x. f x / g x) ---> a / b) A" by (simp add: mult.tendsto tendsto_inverse divide_inverse) +lemma tendsto_sgn [tendsto_intros]: + fixes l :: "'a::real_normed_vector" + shows "\(f ---> l) A; l \ 0\ \ ((\x. sgn (f x)) ---> sgn l) A" + unfolding sgn_div_norm by (simp add: tendsto_intros) + +subsubsection {* Uniqueness *} + lemma tendsto_unique: fixes f :: "'a \ 'b::t2_space" assumes "\ trivial_limit A" "(f ---> l) A" "(f ---> l') A" diff -r 013f7b14f6ff -r 0639898074ae src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Sat Aug 13 18:10:14 2011 -0700 +++ b/src/HOL/SEQ.thy Sun Aug 14 07:54:24 2011 -0700 @@ -441,7 +441,7 @@ lemma LIMSEQ_pow: fixes a :: "'a::{power, real_normed_algebra}" shows "X ----> a \ (\n. (X n) ^ m) ----> a ^ m" -by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult) + by (rule tendsto_power) lemma LIMSEQ_setsum: fixes L :: "'a \ 'b::real_normed_vector" @@ -453,23 +453,7 @@ fixes L :: "'a \ 'b::{real_normed_algebra,comm_ring_1}" assumes n: "\n. n \ S \ X n ----> L n" shows "(\m. \n\S. X n m) ----> (\n\S. L n)" -proof (cases "finite S") - case True - thus ?thesis using n - proof (induct) - case empty - show ?case - by (simp add: LIMSEQ_const) - next - case insert - thus ?case - by (simp add: LIMSEQ_mult) - qed -next - case False - thus ?thesis - by (simp add: setprod_def LIMSEQ_const) -qed + using assms by (rule tendsto_setprod) lemma LIMSEQ_add_const: (* FIXME: delete *) fixes a :: "'a::real_normed_vector" @@ -501,13 +485,13 @@ lemma LIMSEQ_norm_zero: fixes X :: "nat \ 'a::real_normed_vector" shows "((\n. norm (X n)) ----> 0) \ (X ----> 0)" -by (simp add: LIMSEQ_iff) + by (rule tendsto_norm_zero_iff) lemma LIMSEQ_rabs_zero: "((%n. \f n\) ----> 0) = (f ----> (0::real))" -by (simp add: LIMSEQ_iff) + by (rule tendsto_rabs_zero_iff) lemma LIMSEQ_imp_rabs: "f ----> (l::real) ==> (%n. \f n\) ----> \l\" -by (drule LIMSEQ_norm, simp) + by (rule tendsto_rabs) text{*An unbounded sequence's inverse tends to 0*}