# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1395842437 0
# Node ID d8d2a2b971682cd2d9717eb51555f54e3c47c610
# Parent  bf1bdf335ea01076994d0fe9968e7a9496417344
Some useful lemmas

diff -r bf1bdf335ea0 -r d8d2a2b97168 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Mar 26 09:19:04 2014 +0100
+++ b/src/HOL/Deriv.thy	Wed Mar 26 14:00:37 2014 +0000
@@ -1364,6 +1364,33 @@
     by simp
 qed
 
+lemma DERIV_pos_imp_increasing_at_bot:
+  fixes f :: "real => real"
+  assumes "\<And>x. x \<le> b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
+      and lim: "(f ---> flim) at_bot"
+  shows "flim < f b"
+proof -
+  have "flim \<le> f (b - 1)"
+    apply (rule tendsto_ge_const [OF _ lim])
+    apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
+    apply (rule_tac x="b - 2" in exI)
+    apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
+    done
+  also have "... < f b"
+    by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
+  finally show ?thesis .
+qed
+
+lemma DERIV_neg_imp_decreasing_at_top:
+  fixes f :: "real => real"
+  assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
+      and lim: "(f ---> flim) at_top"
+  shows "flim < f b"
+  apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified])
+  apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less)
+  apply (metis filterlim_at_top_mirror lim)
+  done
+
 text {* Derivative of inverse function *}
 
 lemma DERIV_inverse_function:
diff -r bf1bdf335ea0 -r d8d2a2b97168 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Mar 26 09:19:04 2014 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Mar 26 14:00:37 2014 +0000
@@ -615,6 +615,14 @@
   "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   unfolding eventually_at_bot_dense by auto
 
+lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_bot_linorder order_refl)
+
+lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
+  unfolding trivial_limit_def
+  by (metis eventually_at_top_linorder order_refl)
+
 subsection {* Sequentially *}
 
 abbreviation sequentially :: "nat filter"
@@ -1034,10 +1042,17 @@
 lemma tendsto_le_const:
   fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   assumes F: "\<not> trivial_limit F"
-  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
+  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
   shows "a \<le> x"
   using F x tendsto_const a by (rule tendsto_le)
 
+lemma tendsto_ge_const:
+  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
+  assumes F: "\<not> trivial_limit F"
+  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
+  shows "a \<ge> x"
+  by (rule tendsto_le [OF F tendsto_const x a])
+
 subsubsection {* Rules about @{const Lim} *}
 
 lemma (in t2_space) tendsto_Lim: