--- a/src/HOL/Filter.thy Wed Jan 24 23:53:51 2024 +0100
+++ b/src/HOL/Filter.thy Thu Jan 25 17:08:07 2024 +0000
@@ -575,6 +575,13 @@
finally show ?case .
qed auto
+lemma eventually_le_le:
+ fixes P :: "'a \<Rightarrow> ('b :: preorder)"
+ assumes "eventually (\<lambda>x. P x \<le> Q x) F"
+ assumes "eventually (\<lambda>x. Q x \<le> R x) F"
+ shows "eventually (\<lambda>x. P x \<le> R x) F"
+using assms by eventually_elim (rule order_trans)
+
subsubsection \<open>Map function for filters\<close>
definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
--- a/src/HOL/Transcendental.thy Wed Jan 24 23:53:51 2024 +0100
+++ b/src/HOL/Transcendental.thy Thu Jan 25 17:08:07 2024 +0000
@@ -2915,6 +2915,15 @@
lemma ln_bound: "0 < x \<Longrightarrow> ln x \<le> x" for x :: real
using ln_le_minus_one by force
+lemma powr_less_one:
+ fixes x::real
+ assumes "1 < x" "y < 0"
+ shows "x powr y < 1"
+using assms less_log_iff by force
+
+lemma powr_le_one_le: "\<And>x y::real. 0 < x \<Longrightarrow> x \<le> 1 \<Longrightarrow> 1 \<le> y \<Longrightarrow> x powr y \<le> x"
+ by (smt (verit) ln_gt_zero_imp_gt_one ln_le_cancel_iff ln_powr mult_le_cancel_right2)
+
lemma powr_mono:
fixes x :: real
assumes "a \<le> b" and "1 \<le> x" shows "x powr a \<le> x powr b"