# HG changeset patch
# User nipkow
# Date 1752610684 -3600
# Node ID 5a77044eaab22d387c884a0756153564b6bf6e57
# Parent  3e1521dc095df327e956f30ec23b8bf27ab9430b
added lemmas

diff -r 3e1521dc095d -r 5a77044eaab2 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jul 14 18:41:41 2025 +0100
+++ b/src/HOL/Transcendental.thy	Tue Jul 15 21:18:04 2025 +0100
@@ -2133,12 +2133,17 @@
 
 lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
   for x :: real
-  using exp_ge_add_one_self[of "ln x"] by simp
+using exp_ge_add_one_self[of "ln x"] by simp
 
 corollary ln_diff_le: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x - ln y \<le> (x - y) / y"
   for x :: real
 by (metis diff_divide_distrib divide_pos_pos divide_self ln_divide_pos ln_le_minus_one order_less_irrefl)
 
+lemma ln_add1_ge:
+  fixes t::real
+  shows "t\<ge>0 \<Longrightarrow> ln (t+1) \<ge> t / (1+t)"
+using ln_diff_le [of 1 "t+1"] by (simp add: add.commute)
+
 lemma ln_eq_minus_one:
   fixes x :: real
   assumes "0 < x" "ln x = x - 1"
@@ -2183,6 +2188,15 @@
   qed
 qed
 
+corollary ln_diff_less: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x \<noteq> y \<Longrightarrow> ln x - ln y < (x - y) / y" for x :: real
+using ln_eq_minus_one[of "x/y"] ln_diff_le[of x y]
+by (fastforce simp: diff_divide_distrib ln_divide_pos)
+
+lemma ln_add1_gt:
+  fixes t::real
+  shows "t>0 \<Longrightarrow> ln (t+1) > t / (1+t)"
+using ln_diff_less [of 1 "t+1"] ln_one by(simp add: diff_divide_distrib add.commute)
+
 lemma ln_add_one_self_less_self:
   fixes x :: real
   assumes "x > 0"