author | huffman |

Wed Dec 24 11:17:37 2008 -0800 (2008-12-24) | |

changeset 29169 | 6a5f1d8d7344 |

parent 29168 | ff13de554ed0 |

child 29170 | dad3933c88dd |

more proofs about differentiable

1.1 --- a/src/HOL/Deriv.thy Wed Dec 24 09:26:18 2008 -0800 1.2 +++ b/src/HOL/Deriv.thy Wed Dec 24 11:17:37 2008 -0800 1.3 @@ -20,12 +20,6 @@ 1.4 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where 1.5 "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" 1.6 1.7 -definition 1.8 - differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 1.9 - (infixl "differentiable" 60) where 1.10 - "f differentiable x = (\<exists>D. DERIV f x :> D)" 1.11 - 1.12 - 1.13 consts 1.14 Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" 1.15 primrec 1.16 @@ -316,63 +310,104 @@ 1.17 1.18 subsection {* Differentiability predicate *} 1.19 1.20 +definition 1.21 + differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" 1.22 + (infixl "differentiable" 60) where 1.23 + "f differentiable x = (\<exists>D. DERIV f x :> D)" 1.24 + 1.25 +lemma differentiableE [elim?]: 1.26 + assumes "f differentiable x" 1.27 + obtains df where "DERIV f x :> df" 1.28 + using prems unfolding differentiable_def .. 1.29 + 1.30 lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D" 1.31 by (simp add: differentiable_def) 1.32 1.33 lemma differentiableI: "DERIV f x :> D ==> f differentiable x" 1.34 by (force simp add: differentiable_def) 1.35 1.36 -lemma differentiable_const: "(\<lambda>z. a) differentiable x" 1.37 - apply (unfold differentiable_def) 1.38 - apply (rule_tac x=0 in exI) 1.39 - apply simp 1.40 - done 1.41 +lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x" 1.42 + by (rule DERIV_ident [THEN differentiableI]) 1.43 + 1.44 +lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x" 1.45 + by (rule DERIV_const [THEN differentiableI]) 1.46 1.47 -lemma differentiable_sum: 1.48 +lemma differentiable_compose: 1.49 + assumes f: "f differentiable (g x)" 1.50 + assumes g: "g differentiable x" 1.51 + shows "(\<lambda>x. f (g x)) differentiable x" 1.52 +proof - 1.53 + from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" .. 1.54 + moreover 1.55 + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. 1.56 + ultimately 1.57 + have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2) 1.58 + thus ?thesis by (rule differentiableI) 1.59 +qed 1.60 + 1.61 +lemma differentiable_sum [simp]: 1.62 assumes "f differentiable x" 1.63 and "g differentiable x" 1.64 shows "(\<lambda>x. f x + g x) differentiable x" 1.65 proof - 1.66 - from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) 1.67 - then obtain df where "DERIV f x :> df" .. 1.68 - moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 1.69 - then obtain dg where "DERIV g x :> dg" .. 1.70 - ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add) 1.71 - hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto 1.72 - thus ?thesis by (fold differentiable_def) 1.73 + from `f differentiable x` obtain df where "DERIV f x :> df" .. 1.74 + moreover 1.75 + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. 1.76 + ultimately 1.77 + have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add) 1.78 + thus ?thesis by (rule differentiableI) 1.79 +qed 1.80 + 1.81 +lemma differentiable_minus [simp]: 1.82 + assumes "f differentiable x" 1.83 + shows "(\<lambda>x. - f x) differentiable x" 1.84 +proof - 1.85 + from `f differentiable x` obtain df where "DERIV f x :> df" .. 1.86 + hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus) 1.87 + thus ?thesis by (rule differentiableI) 1.88 qed 1.89 1.90 -lemma differentiable_diff: 1.91 +lemma differentiable_diff [simp]: 1.92 assumes "f differentiable x" 1.93 - and "g differentiable x" 1.94 + assumes "g differentiable x" 1.95 shows "(\<lambda>x. f x - g x) differentiable x" 1.96 + unfolding diff_minus using prems by simp 1.97 + 1.98 +lemma differentiable_mult [simp]: 1.99 + assumes "f differentiable x" 1.100 + assumes "g differentiable x" 1.101 + shows "(\<lambda>x. f x * g x) differentiable x" 1.102 proof - 1.103 - from prems have "f differentiable x" by simp 1.104 + from `f differentiable x` obtain df where "DERIV f x :> df" .. 1.105 moreover 1.106 - from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 1.107 - then obtain dg where "DERIV g x :> dg" .. 1.108 - then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus) 1.109 - hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto 1.110 - hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def) 1.111 - ultimately 1.112 - show ?thesis 1.113 - by (auto simp: diff_def dest: differentiable_sum) 1.114 + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. 1.115 + ultimately 1.116 + have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult) 1.117 + thus ?thesis by (rule differentiableI) 1.118 qed 1.119 1.120 -lemma differentiable_mult: 1.121 - assumes "f differentiable x" 1.122 - and "g differentiable x" 1.123 - shows "(\<lambda>x. f x * g x) differentiable x" 1.124 +lemma differentiable_inverse [simp]: 1.125 + assumes "f differentiable x" and "f x \<noteq> 0" 1.126 + shows "(\<lambda>x. inverse (f x)) differentiable x" 1.127 proof - 1.128 - from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) 1.129 - then obtain df where "DERIV f x :> df" .. 1.130 - moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) 1.131 - then obtain dg where "DERIV g x :> dg" .. 1.132 - ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult) 1.133 - hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto 1.134 - thus ?thesis by (fold differentiable_def) 1.135 + from `f differentiable x` obtain df where "DERIV f x :> df" .. 1.136 + hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))" 1.137 + using `f x \<noteq> 0` by (rule DERIV_inverse') 1.138 + thus ?thesis by (rule differentiableI) 1.139 qed 1.140 1.141 +lemma differentiable_divide [simp]: 1.142 + assumes "f differentiable x" 1.143 + assumes "g differentiable x" and "g x \<noteq> 0" 1.144 + shows "(\<lambda>x. f x / g x) differentiable x" 1.145 + unfolding divide_inverse using prems by simp 1.146 + 1.147 +lemma differentiable_power [simp]: 1.148 + fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a" 1.149 + assumes "f differentiable x" 1.150 + shows "(\<lambda>x. f x ^ n) differentiable x" 1.151 + by (induct n, simp, simp add: power_Suc prems) 1.152 + 1.153 1.154 subsection {* Nested Intervals and Bisection *} 1.155