--- 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:
--- 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: