A number of theorems contributed by Jeremy Avigad
authorpaulson
Fri Nov 13 11:33:33 2009 +0000 (2009-11-13)
changeset 33654abf780db30ea
parent 33640 0d82107dc07a
child 33655 c6dde2106128
A number of theorems contributed by Jeremy Avigad
src/HOL/Deriv.thy
     1.1 --- a/src/HOL/Deriv.thy	Thu Nov 12 17:21:51 2009 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Fri Nov 13 11:33:33 2009 +0000
     1.3 @@ -273,6 +273,11 @@
     1.4        "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D"
     1.5  by (drule DERIV_mult' [OF DERIV_const], simp)
     1.6  
     1.7 +lemma DERIV_cdivide: "DERIV f x :> D ==> DERIV (%x. f x / c) x :> D / c"
     1.8 +  apply (subgoal_tac "DERIV (%x. (1 / c) * f x) x :> (1 / c) * D", force)
     1.9 +  apply (erule DERIV_cmult)
    1.10 +  done
    1.11 +
    1.12  text {* Standard version *}
    1.13  lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db"
    1.14  by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute)
    1.15 @@ -702,14 +707,10 @@
    1.16  apply safe
    1.17  apply simp_all
    1.18  apply (rename_tac x xa ya M Ma)
    1.19 -apply (cut_tac x = M and y = Ma in linorder_linear, safe)
    1.20 -apply (rule_tac x = Ma in exI, clarify)
    1.21 -apply (cut_tac x = xb and y = xa in linorder_linear, force)
    1.22 -apply (rule_tac x = M in exI, clarify)
    1.23 -apply (cut_tac x = xb and y = xa in linorder_linear, force)
    1.24 +apply (metis linorder_not_less order_le_less real_le_trans)
    1.25  apply (case_tac "a \<le> x & x \<le> b")
    1.26 -apply (rule_tac [2] x = 1 in exI)
    1.27 -prefer 2 apply force
    1.28 + prefer 2
    1.29 + apply (rule_tac x = 1 in exI, force)
    1.30  apply (simp add: LIM_eq isCont_iff)
    1.31  apply (drule_tac x = x in spec, auto)
    1.32  apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
    1.33 @@ -815,7 +816,7 @@
    1.34  
    1.35  text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
    1.36  
    1.37 -lemma DERIV_left_inc:
    1.38 +lemma DERIV_pos_inc_right:
    1.39    fixes f :: "real => real"
    1.40    assumes der: "DERIV f x :> l"
    1.41        and l:   "0 < l"
    1.42 @@ -845,7 +846,7 @@
    1.43    qed
    1.44  qed
    1.45  
    1.46 -lemma DERIV_left_dec:
    1.47 +lemma DERIV_neg_dec_left:
    1.48    fixes f :: "real => real"
    1.49    assumes der: "DERIV f x :> l"
    1.50        and l:   "l < 0"
    1.51 @@ -875,6 +876,21 @@
    1.52    qed
    1.53  qed
    1.54  
    1.55 +
    1.56 +lemma DERIV_pos_inc_left:
    1.57 +  fixes f :: "real => real"
    1.58 +  shows "DERIV f x :> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x - h) < f(x)"
    1.59 +  apply (rule DERIV_neg_dec_left [of "%x. - f x" x "-l", simplified])
    1.60 +  apply (auto simp add: DERIV_minus) 
    1.61 +  done
    1.62 +
    1.63 +lemma DERIV_neg_dec_right:
    1.64 +  fixes f :: "real => real"
    1.65 +  shows "DERIV f x :> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>d > 0. \<forall>h > 0. h < d --> f(x) > f(x + h)"
    1.66 +  apply (rule DERIV_pos_inc_right [of "%x. - f x" x "-l", simplified])
    1.67 +  apply (auto simp add: DERIV_minus) 
    1.68 +  done
    1.69 +
    1.70  lemma DERIV_local_max:
    1.71    fixes f :: "real => real"
    1.72    assumes der: "DERIV f x :> l"
    1.73 @@ -885,7 +901,7 @@
    1.74    case equal thus ?thesis .
    1.75  next
    1.76    case less
    1.77 -  from DERIV_left_dec [OF der less]
    1.78 +  from DERIV_neg_dec_left [OF der less]
    1.79    obtain d' where d': "0 < d'"
    1.80               and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x-h)" by blast
    1.81    from real_lbound_gt_zero [OF d d']
    1.82 @@ -894,7 +910,7 @@
    1.83    show ?thesis by (auto simp add: abs_if)
    1.84  next
    1.85    case greater
    1.86 -  from DERIV_left_inc [OF der greater]
    1.87 +  from DERIV_pos_inc_right [OF der greater]
    1.88    obtain d' where d': "0 < d'"
    1.89               and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)" by blast
    1.90    from real_lbound_gt_zero [OF d d']
    1.91 @@ -1205,6 +1221,87 @@
    1.92    ultimately show ?thesis using neq by (force simp add: add_commute)
    1.93  qed
    1.94  
    1.95 +(* A function with positive derivative is increasing. 
    1.96 +   A simple proof using the MVT, by Jeremy Avigad. And variants.
    1.97 +*)
    1.98 +
    1.99 +lemma DERIV_pos_imp_increasing:
   1.100 +  fixes a::real and b::real and f::"real => real"
   1.101 +  assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
   1.102 +  shows "f a < f b"
   1.103 +proof (rule ccontr)
   1.104 +  assume "~ f a < f b"
   1.105 +  from assms have "EX l z. a < z & z < b & DERIV f z :> l
   1.106 +      & f b - f a = (b - a) * l"
   1.107 +    by (metis MVT DERIV_isCont differentiableI real_less_def)
   1.108 +  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
   1.109 +      and "f b - f a = (b - a) * l"
   1.110 +    by auto
   1.111 +  
   1.112 +  from prems have "~(l > 0)"
   1.113 +    by (metis assms(1) linorder_not_le mult_le_0_iff real_le_eq_diff)
   1.114 +  with prems show False
   1.115 +    by (metis DERIV_unique real_less_def)
   1.116 +qed
   1.117 +
   1.118 +
   1.119 +lemma DERIV_nonneg_imp_nonincreasing:
   1.120 +  fixes a::real and b::real and f::"real => real"
   1.121 +  assumes "a \<le> b" and
   1.122 +    "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
   1.123 +  shows "f a \<le> f b"
   1.124 +proof (rule ccontr, cases "a = b")
   1.125 +  assume "~ f a \<le> f b"
   1.126 +  assume "a = b"
   1.127 +  with prems show False by auto
   1.128 +  next assume "~ f a \<le> f b"
   1.129 +  assume "a ~= b"
   1.130 +  with assms have "EX l z. a < z & z < b & DERIV f z :> l
   1.131 +      & f b - f a = (b - a) * l"
   1.132 +    apply (intro MVT)
   1.133 +    apply auto
   1.134 +    apply (metis DERIV_isCont)
   1.135 +    apply (metis differentiableI real_less_def)
   1.136 +    done
   1.137 +  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
   1.138 +      and "f b - f a = (b - a) * l"
   1.139 +    by auto
   1.140 +  from prems have "~(l >= 0)"
   1.141 +    by (metis diff_self le_eqI le_iff_diff_le_0 real_le_anti_sym real_le_linear
   1.142 +              split_mult_pos_le)
   1.143 +  with prems show False
   1.144 +    by (metis DERIV_unique order_less_imp_le)
   1.145 +qed
   1.146 +
   1.147 +lemma DERIV_neg_imp_decreasing:
   1.148 +  fixes a::real and b::real and f::"real => real"
   1.149 +  assumes "a < b" and
   1.150 +    "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y < 0)"
   1.151 +  shows "f a > f b"
   1.152 +proof -
   1.153 +  have "(%x. -f x) a < (%x. -f x) b"
   1.154 +    apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
   1.155 +    apply (insert prems, auto)
   1.156 +    apply (metis DERIV_minus neg_0_less_iff_less)
   1.157 +    done
   1.158 +  thus ?thesis
   1.159 +    by simp
   1.160 +qed
   1.161 +
   1.162 +lemma DERIV_nonpos_imp_nonincreasing:
   1.163 +  fixes a::real and b::real and f::"real => real"
   1.164 +  assumes "a \<le> b" and
   1.165 +    "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<le> 0)"
   1.166 +  shows "f a \<ge> f b"
   1.167 +proof -
   1.168 +  have "(%x. -f x) a \<le> (%x. -f x) b"
   1.169 +    apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"])
   1.170 +    apply (insert prems, auto)
   1.171 +    apply (metis DERIV_minus neg_0_le_iff_le)
   1.172 +    done
   1.173 +  thus ?thesis
   1.174 +    by simp
   1.175 +qed
   1.176  
   1.177  subsection {* Continuous injective functions *}
   1.178