# HG changeset patch
# User wenzelm
# Date 1752613992 -7200
# Node ID e70239b753a006b300a342b6bbfe026f35a2d9b9
# Parent  5a77044eaab22d387c884a0756153564b6bf6e57# Parent  fa1c57d4269987f193dceaa7a8694ff9eec4ac60
merged

diff -r fa1c57d42699 -r e70239b753a0 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jul 15 22:05:06 2025 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jul 15 23:13:12 2025 +0200
@@ -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"