tendsto lemmas for ln and powr
authorhuffman
Thu Dec 15 17:21:29 2011 +0100 (2011-12-15)
changeset 459150e5a87b772f9
parent 45914 eaf6728d2512
child 45916 758671e966a0
tendsto lemmas for ln and powr
src/HOL/Log.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Log.thy	Sun Dec 18 14:28:14 2011 +0100
     1.2 +++ b/src/HOL/Log.thy	Thu Dec 15 17:21:29 2011 +0100
     1.3 @@ -285,6 +285,10 @@
     1.4    finally show ?thesis .
     1.5  qed
     1.6  
     1.7 +lemma tendsto_powr [tendsto_intros]:
     1.8 +  "\<lbrakk>(f ---> a) F; (g ---> b) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
     1.9 +  unfolding powr_def by (intro tendsto_intros)
    1.10 +
    1.11  (* FIXME: generalize by replacing d by with g x and g ---> d? *)
    1.12  lemma tendsto_zero_powrI:
    1.13    assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
     2.1 --- a/src/HOL/Transcendental.thy	Sun Dec 18 14:28:14 2011 +0100
     2.2 +++ b/src/HOL/Transcendental.thy	Thu Dec 15 17:21:29 2011 +0100
     2.3 @@ -1166,6 +1166,10 @@
     2.4    apply (rule isCont_inverse_function [where f=exp], simp_all)
     2.5    done
     2.6  
     2.7 +lemma tendsto_ln [tendsto_intros]:
     2.8 +  "\<lbrakk>(f ---> a) F; 0 < a\<rbrakk> \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
     2.9 +  by (rule isCont_tendsto_compose [OF isCont_ln])
    2.10 +
    2.11  lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
    2.12    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
    2.13    apply (erule DERIV_cong [OF DERIV_exp exp_ln])