Some useful lemmas
authorpaulson <lp15@cam.ac.uk>
Wed Mar 26 14:00:37 2014 +0000 (2014-03-26)
changeset 56289d8d2a2b97168
parent 56288 bf1bdf335ea0
child 56290 801a72ad52d3
Some useful lemmas
src/HOL/Deriv.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Deriv.thy	Wed Mar 26 09:19:04 2014 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Wed Mar 26 14:00:37 2014 +0000
     1.3 @@ -1364,6 +1364,33 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 +lemma DERIV_pos_imp_increasing_at_bot:
     1.8 +  fixes f :: "real => real"
     1.9 +  assumes "\<And>x. x \<le> b \<Longrightarrow> (EX y. DERIV f x :> y & y > 0)"
    1.10 +      and lim: "(f ---> flim) at_bot"
    1.11 +  shows "flim < f b"
    1.12 +proof -
    1.13 +  have "flim \<le> f (b - 1)"
    1.14 +    apply (rule tendsto_ge_const [OF _ lim])
    1.15 +    apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
    1.16 +    apply (rule_tac x="b - 2" in exI)
    1.17 +    apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
    1.18 +    done
    1.19 +  also have "... < f b"
    1.20 +    by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
    1.21 +  finally show ?thesis .
    1.22 +qed
    1.23 +
    1.24 +lemma DERIV_neg_imp_decreasing_at_top:
    1.25 +  fixes f :: "real => real"
    1.26 +  assumes der: "\<And>x. x \<ge> b \<Longrightarrow> (EX y. DERIV f x :> y & y < 0)"
    1.27 +      and lim: "(f ---> flim) at_top"
    1.28 +  shows "flim < f b"
    1.29 +  apply (rule DERIV_pos_imp_increasing_at_bot [where f = "\<lambda>i. f (-i)" and b = "-b", simplified])
    1.30 +  apply (metis DERIV_mirror der le_minus_iff neg_0_less_iff_less)
    1.31 +  apply (metis filterlim_at_top_mirror lim)
    1.32 +  done
    1.33 +
    1.34  text {* Derivative of inverse function *}
    1.35  
    1.36  lemma DERIV_inverse_function:
     2.1 --- a/src/HOL/Topological_Spaces.thy	Wed Mar 26 09:19:04 2014 +0100
     2.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Mar 26 14:00:37 2014 +0000
     2.3 @@ -615,6 +615,14 @@
     2.4    "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
     2.5    unfolding eventually_at_bot_dense by auto
     2.6  
     2.7 +lemma trivial_limit_at_bot_linorder: "\<not> trivial_limit (at_bot ::('a::linorder) filter)"
     2.8 +  unfolding trivial_limit_def
     2.9 +  by (metis eventually_at_bot_linorder order_refl)
    2.10 +
    2.11 +lemma trivial_limit_at_top_linorder: "\<not> trivial_limit (at_top ::('a::linorder) filter)"
    2.12 +  unfolding trivial_limit_def
    2.13 +  by (metis eventually_at_top_linorder order_refl)
    2.14 +
    2.15  subsection {* Sequentially *}
    2.16  
    2.17  abbreviation sequentially :: "nat filter"
    2.18 @@ -1034,10 +1042,17 @@
    2.19  lemma tendsto_le_const:
    2.20    fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
    2.21    assumes F: "\<not> trivial_limit F"
    2.22 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>x. a \<le> f x) F"
    2.23 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
    2.24    shows "a \<le> x"
    2.25    using F x tendsto_const a by (rule tendsto_le)
    2.26  
    2.27 +lemma tendsto_ge_const:
    2.28 +  fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
    2.29 +  assumes F: "\<not> trivial_limit F"
    2.30 +  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
    2.31 +  shows "a \<ge> x"
    2.32 +  by (rule tendsto_le [OF F tendsto_const x a])
    2.33 +
    2.34  subsubsection {* Rules about @{const Lim} *}
    2.35  
    2.36  lemma (in t2_space) tendsto_Lim: