200 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" |
200 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" |
201 assumes f: "DERIV f x :> D" |
201 assumes f: "DERIV f x :> D" |
202 shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)" |
202 shows "DERIV (\<lambda>x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)" |
203 proof (induct n) |
203 proof (induct n) |
204 case 0 |
204 case 0 |
205 show ?case by (simp add: power_Suc f) |
205 show ?case by (simp add: f) |
206 case (Suc k) |
206 case (Suc k) |
207 from DERIV_mult' [OF f Suc] show ?case |
207 from DERIV_mult' [OF f Suc] show ?case |
208 apply (simp only: of_nat_Suc ring_distribs mult_1_left) |
208 apply (simp only: of_nat_Suc ring_distribs mult_1_left) |
209 apply (simp only: power_Suc algebra_simps) |
209 apply (simp only: power_Suc algebra_simps) |
210 done |
210 done |
212 |
212 |
213 lemma DERIV_power: |
213 lemma DERIV_power: |
214 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" |
214 fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,recpower}" |
215 assumes f: "DERIV f x :> D" |
215 assumes f: "DERIV f x :> D" |
216 shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))" |
216 shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))" |
217 by (cases "n", simp, simp add: DERIV_power_Suc f) |
217 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc) |
218 |
218 |
219 |
219 |
220 text {* Caratheodory formulation of derivative at a point *} |
220 text {* Caratheodory formulation of derivative at a point *} |
221 |
221 |
222 lemma CARAT_DERIV: |
222 lemma CARAT_DERIV: |
287 text{*Power of -1*} |
287 text{*Power of -1*} |
288 |
288 |
289 lemma DERIV_inverse: |
289 lemma DERIV_inverse: |
290 fixes x :: "'a::{real_normed_field,recpower}" |
290 fixes x :: "'a::{real_normed_field,recpower}" |
291 shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" |
291 shows "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" |
292 by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc) |
292 by (drule DERIV_inverse' [OF DERIV_ident]) simp |
293 |
293 |
294 text{*Derivative of inverse*} |
294 text{*Derivative of inverse*} |
295 lemma DERIV_inverse_fun: |
295 lemma DERIV_inverse_fun: |
296 fixes x :: "'a::{real_normed_field,recpower}" |
296 fixes x :: "'a::{real_normed_field,recpower}" |
297 shows "[| DERIV f x :> d; f(x) \<noteq> 0 |] |
297 shows "[| DERIV f x :> d; f(x) \<noteq> 0 |] |
298 ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" |
298 ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" |
299 by (drule (1) DERIV_inverse') (simp add: mult_ac power_Suc nonzero_inverse_mult_distrib) |
299 by (drule (1) DERIV_inverse') (simp add: mult_ac nonzero_inverse_mult_distrib) |
300 |
300 |
301 text{*Derivative of quotient*} |
301 text{*Derivative of quotient*} |
302 lemma DERIV_quotient: |
302 lemma DERIV_quotient: |
303 fixes x :: "'a::{real_normed_field,recpower}" |
303 fixes x :: "'a::{real_normed_field,recpower}" |
304 shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |] |
304 shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |] |
305 ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" |
305 ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" |
306 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc) |
306 by (drule (2) DERIV_divide) (simp add: mult_commute) |
307 |
307 |
308 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E" |
308 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E" |
309 by auto |
309 by auto |
310 |
310 |
311 |
311 |
405 |
405 |
406 lemma differentiable_power [simp]: |
406 lemma differentiable_power [simp]: |
407 fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a" |
407 fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a" |
408 assumes "f differentiable x" |
408 assumes "f differentiable x" |
409 shows "(\<lambda>x. f x ^ n) differentiable x" |
409 shows "(\<lambda>x. f x ^ n) differentiable x" |
410 by (induct n, simp, simp add: power_Suc prems) |
410 by (induct n, simp, simp add: prems) |
411 |
411 |
412 |
412 |
413 subsection {* Nested Intervals and Bisection *} |
413 subsection {* Nested Intervals and Bisection *} |
414 |
414 |
415 text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). |
415 text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). |