--- a/src/HOL/Fields.thy Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Fields.thy Mon Jul 29 10:13:52 2024 +0100
@@ -949,7 +949,7 @@
by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
lemma divide_left_mono:
- "\<lbrakk>b \<le> a; 0 \<le> c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
+ "\<lbrakk>b \<le> a; 0 \<le> c; 0 < b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
lemma divide_strict_left_mono_neg:
@@ -957,16 +957,16 @@
by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
lemma mult_imp_div_pos_le: "0 < y \<Longrightarrow> x \<le> z * y \<Longrightarrow> x / y \<le> z"
-by (subst pos_divide_le_eq, assumption+)
+ by (subst pos_divide_le_eq, assumption+)
lemma mult_imp_le_div_pos: "0 < y \<Longrightarrow> z * y \<le> x \<Longrightarrow> z \<le> x / y"
-by(simp add:field_simps)
+ by(simp add:field_simps)
lemma mult_imp_div_pos_less: "0 < y \<Longrightarrow> x < z * y \<Longrightarrow> x / y < z"
-by(simp add:field_simps)
+ by(simp add:field_simps)
lemma mult_imp_less_div_pos: "0 < y \<Longrightarrow> z * y < x \<Longrightarrow> z < x / y"
-by(simp add:field_simps)
+ by(simp add:field_simps)
lemma frac_le:
assumes "0 \<le> y" "x \<le> y" "0 < w" "w \<le> z"
@@ -1010,6 +1010,11 @@
using assms by (force intro: mult_imp_less_div_pos mult_le_less_imp_less)
qed
+text \<open>As above, with a better name\<close>
+lemma divide_mono:
+ "\<lbrakk>b \<le> a; c \<le> d; 0 < b; 0 \<le> c\<rbrakk> \<Longrightarrow> c / a \<le> d / b"
+ by (simp add: frac_le)
+
lemma less_half_sum: "a < b \<Longrightarrow> a < (a+b) / (1+1)"
by (simp add: field_simps zero_less_two)
--- a/src/HOL/Library/Discrete.thy Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Library/Discrete.thy Mon Jul 29 10:13:52 2024 +0100
@@ -63,7 +63,7 @@
then show ?thesis by (simp add: log_rec)
qed
-lemma log_exp [simp]: "log (2 ^ n) = n"
+lemma log_power [simp]: "log (2 ^ n) = n"
by (induct n) simp_all
lemma log_mono: "mono log"
--- a/src/HOL/Real.thy Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Real.thy Mon Jul 29 10:13:52 2024 +0100
@@ -1303,6 +1303,8 @@
for x y :: real
by auto
+lemma mult_ge1_I: "\<lbrakk>x\<ge>1; y\<ge>1\<rbrakk> \<Longrightarrow> x*y \<ge> (1::real)"
+ using mult_mono by fastforce
subsection \<open>Lemmas about powers\<close>
--- a/src/HOL/Transcendental.thy Sun Jul 28 14:45:41 2024 +0100
+++ b/src/HOL/Transcendental.thy Mon Jul 29 10:13:52 2024 +0100
@@ -1494,6 +1494,16 @@
for x y :: real
by (auto simp: linorder_not_less [symmetric])
+lemma exp_mono:
+ fixes x y :: real
+ assumes "x \<le> y"
+ shows "exp x \<le> exp y"
+ using assms exp_le_cancel_iff by fastforce
+
+lemma exp_minus': "exp (-x) = 1 / (exp x)"
+ for x :: "'a::{real_normed_field,banach}"
+ by (simp add: exp_minus inverse_eq_divide)
+
lemma exp_inj_iff [iff]: "exp x = exp y \<longleftrightarrow> x = y"
for x y :: real
by (simp add: order_eq_iff)
@@ -1668,8 +1678,11 @@
for x :: real
by (simp add: linorder_not_less [symmetric])
-lemma ln_mono: "\<And>x::real. \<lbrakk>x \<le> y; 0 < x; 0 < y\<rbrakk> \<Longrightarrow> ln x \<le> ln y"
- using ln_le_cancel_iff by presburger
+lemma ln_mono: "\<And>x::real. \<lbrakk>x \<le> y; 0 < x\<rbrakk> \<Longrightarrow> ln x \<le> ln y"
+ by simp
+
+lemma ln_strict_mono: "\<And>x::real. \<lbrakk>x < y; 0 < x\<rbrakk> \<Longrightarrow> ln x < ln y"
+ by simp
lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
for x :: real
@@ -2327,6 +2340,9 @@
\<comment> \<open>logarithm of \<^term>\<open>x\<close> to base \<^term>\<open>a\<close>\<close>
where "log a x = ln x / ln a"
+lemma log_exp [simp]: "log b (exp x) = x / ln b"
+ by (simp add: log_def)
+
lemma tendsto_log [tendsto_intros]:
"(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> 0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> b\<noteq>0 \<Longrightarrow>
((\<lambda>x. log (f x) (g x)) \<longlongrightarrow> log a b) F"