--- a/src/HOL/Transcendental.thy Sun Mar 12 19:06:10 2017 +0100
+++ b/src/HOL/Transcendental.thy Fri Mar 10 23:16:40 2017 +0100
@@ -1493,6 +1493,8 @@
apply (simp add: scaleR_conv_of_real)
done
+lemmas of_real_exp = exp_of_real[symmetric]
+
corollary exp_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> exp z \<in> \<real>"
by (metis Reals_cases Reals_of_real exp_of_real)
@@ -1795,6 +1797,10 @@
for x :: real
using ln_less_cancel_iff [of x 1] by simp
+lemma ln_le_zero_iff [simp]: "0 < x \<Longrightarrow> ln x \<le> 0 \<longleftrightarrow> x \<le> 1"
+ for x :: real
+ by (metis less_numeral_extra(1) ln_le_cancel_iff ln_one)
+
lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
for x :: real
using ln_less_cancel_iff [of 1 x] by simp
@@ -2347,6 +2353,10 @@
by (intro filtermap_fun_inverse[of ln] exp_at_top ln_at_top)
(auto simp: eventually_at_top_dense)
+lemma filtermap_ln_at_right: "filtermap ln (at_right (0::real)) = at_bot"
+ by (auto intro!: filtermap_fun_inverse[where g="\<lambda>x. exp x"] ln_at_0
+ simp: filterlim_at exp_at_bot)
+
lemma tendsto_power_div_exp_0: "((\<lambda>x. x ^ k / exp x) \<longlongrightarrow> (0::real)) at_top"
proof (induct k)
case 0