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
 src/HOL/Deriv.thy file | annotate | diff | revisions
```     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
```