src/HOL/Transcendental.thy
changeset 65204 d23eded35a33
parent 65109 a79c1080f1e9
child 65552 f533820e7248
     1.1 --- a/src/HOL/Transcendental.thy	Sun Mar 12 19:06:10 2017 +0100
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 10 23:16:40 2017 +0100
     1.3 @@ -1493,6 +1493,8 @@
     1.4    apply (simp add: scaleR_conv_of_real)
     1.5    done
     1.6  
     1.7 +lemmas of_real_exp = exp_of_real[symmetric]
     1.8 +
     1.9  corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
    1.10    by (metis Reals_cases Reals_of_real exp_of_real)
    1.11  
    1.12 @@ -1795,6 +1797,10 @@
    1.13    for x :: real
    1.14    using ln_less_cancel_iff [of x 1] by simp
    1.15  
    1.16 +lemma ln_le_zero_iff [simp]: "0 < x \<Longrightarrow> ln x \<le> 0 \<longleftrightarrow> x \<le> 1"
    1.17 +  for x :: real
    1.18 +  by (metis less_numeral_extra(1) ln_le_cancel_iff ln_one)
    1.19 +
    1.20  lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
    1.21    for x :: real
    1.22    using ln_less_cancel_iff [of 1 x] by simp
    1.23 @@ -2347,6 +2353,10 @@
    1.24    by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
    1.25       (auto simp: eventually_at_top_dense)
    1.26  
    1.27 +lemma filtermap_ln_at_right: "filtermap ln (at_right (0::real)) = at_bot"
    1.28 +  by (auto intro!: filtermap_fun_inverse[where g="\<lambda>x. exp x"] ln_at_0
    1.29 +      simp: filterlim_at exp_at_bot)
    1.30 +
    1.31  lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
    1.32  proof (induct k)
    1.33    case 0