author paulson Fri Nov 13 11:33:33 2009 +0000 (2009-11-13) changeset 33654 abf780db30ea parent 33640 0d82107dc07a child 33655 c6dde2106128
A number of theorems contributed by Jeremy Avigad
 src/HOL/Deriv.thy file | annotate | diff | revisions
```     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.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
```