# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1706202487 0
# Node ID 1b0fc6ceb750641b4ad0d223ce65e6600bff3f4d
# Parent  cb933e165dc33831444d8c4ed66f5033b0b8a182
Three new lemmas

diff -r cb933e165dc3 -r 1b0fc6ceb750 src/HOL/Filter.thy
--- 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"
diff -r cb933e165dc3 -r 1b0fc6ceb750 src/HOL/Transcendental.thy
--- 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"