--- a/src/HOL/Transcendental.thy Wed Sep 27 13:34:15 2023 +0100
+++ b/src/HOL/Transcendental.thy Fri Sep 29 13:59:56 2023 +0100
@@ -1867,7 +1867,7 @@
by (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
(auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
-lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
+lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1/x"
for x :: real
by (rule DERIV_ln[THEN DERIV_cong]) (simp_all add: divide_inverse)
@@ -1890,7 +1890,7 @@
then have "0 < x" and "x < 2" by auto
have "norm (1 - x) < 1"
using \<open>0 < x\<close> and \<open>x < 2\<close> by auto
- have "1 / x = 1 / (1 - (1 - x))" by auto
+ have "1/x = 1 / (1 - (1 - x))" by auto
also have "\<dots> = (\<Sum> n. (1 - x)^n)"
using geometric_sums[OF \<open>norm (1 - x) < 1\<close>] by (rule sums_unique)
also have "\<dots> = suminf (?f' x)"
@@ -2218,9 +2218,8 @@
shows "x = 1"
proof -
let ?l = "\<lambda>y. ln y - y + 1"
- have D: "\<And>x::real. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
+ have D: "\<And>x::real. 0 < x \<Longrightarrow> DERIV ?l x :> (1/x - 1)"
by (auto intro!: derivative_eq_intros)
-
show ?thesis
proof (cases rule: linorder_cases)
assume "x < 1"
@@ -2257,6 +2256,12 @@
qed
qed
+lemma ln_add_one_self_less_self:
+ fixes x :: real
+ assumes "x > 0"
+ shows "ln (1 + x) < x"
+ by (smt (verit, best) assms ln_eq_minus_one ln_le_minus_one)
+
lemma ln_x_over_x_tendsto_0: "((\<lambda>x::real. ln x / x) \<longlongrightarrow> 0) at_top"
proof (rule lhospital_at_top_at_top[where f' = inverse and g' = "\<lambda>_. 1"])
from eventually_gt_at_top[of "0::real"]
@@ -2265,6 +2270,16 @@
qed (use tendsto_inverse_0 in
\<open>auto simp: filterlim_ident dest!: tendsto_mono[OF at_top_le_at_infinity]\<close>)
+corollary exp_1_gt_powr:
+ assumes "x > (0::real)"
+ shows "exp 1 > (1 + 1/x) powr x"
+proof -
+ have "ln (1 + 1/x) < 1/x"
+ using ln_add_one_self_less_self assms by simp
+ thus "exp 1 > (1 + 1/x) powr x" using assms
+ by (simp add: field_simps powr_def)
+qed
+
lemma exp_ge_one_plus_x_over_n_power_n:
assumes "x \<ge> - real n" "n > 0"
shows "(1 + x / of_nat n) ^ n \<le> exp x"
@@ -2805,7 +2820,7 @@
lemma powr_int:
assumes "x > 0"
- shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))"
+ shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1/x ^ nat (-i))"
by (simp add: assms inverse_eq_divide powr_real_of_int)
lemma power_of_nat_log_ge: "b > 1 \<Longrightarrow> b ^ nat \<lceil>log b x\<rceil> \<ge> x"
@@ -2836,11 +2851,11 @@
for x :: real
using powr_realpow [of x 1] by simp
-lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
+lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1/x"
for x :: real
using powr_int [of x "- 1"] by simp
-lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
+lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1/x ^ numeral n"
for x :: real
using powr_int [of x "- numeral n"] by simp
@@ -6184,7 +6199,7 @@
lemma arctan_inverse:
assumes "x \<noteq> 0"
- shows "arctan (1 / x) = sgn x * pi/2 - arctan x"
+ shows "arctan (1/x) = sgn x * pi/2 - arctan x"
proof (rule arctan_unique)
have \<section>: "x > 0 \<Longrightarrow> arctan x < pi"
using arctan_bounded [of x] by linarith
@@ -6193,7 +6208,7 @@
show "sgn x * pi/2 - arctan x < pi/2"
using arctan_bounded [of "- x"] assms
by (auto simp: algebra_simps sgn_real_def arctan_minus)
- show "tan (sgn x * pi/2 - arctan x) = 1 / x"
+ show "tan (sgn x * pi/2 - arctan x) = 1/x"
unfolding tan_inverse [of "arctan x", unfolded tan_arctan] sgn_real_def
by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
qed