278 lemma GDERIV_DERIV_compose: |
278 lemma GDERIV_DERIV_compose: |
279 "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk> |
279 "\<lbrakk>GDERIV f x :> df; DERIV g (f x) :> dg\<rbrakk> |
280 \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df" |
280 \<Longrightarrow> GDERIV (\<lambda>x. g (f x)) x :> scaleR dg df" |
281 unfolding gderiv_def has_field_derivative_def |
281 unfolding gderiv_def has_field_derivative_def |
282 apply (drule (1) has_derivative_compose) |
282 apply (drule (1) has_derivative_compose) |
283 apply (simp add: mult_ac) |
283 apply (simp add: ac_simps) |
284 done |
284 done |
285 |
285 |
286 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d" |
286 lemma has_derivative_subst: "\<lbrakk>FDERIV f x :> df; df = d\<rbrakk> \<Longrightarrow> FDERIV f x :> d" |
287 by simp |
287 by simp |
288 |
288 |
311 \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x |
311 \<Longrightarrow> GDERIV (\<lambda>x. scaleR (f x) (g x)) x |
312 :> (scaleR (f x) dg + scaleR df (g x))" |
312 :> (scaleR (f x) dg + scaleR df (g x))" |
313 unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right |
313 unfolding gderiv_def has_field_derivative_def inner_add_right inner_scaleR_right |
314 apply (rule has_derivative_subst) |
314 apply (rule has_derivative_subst) |
315 apply (erule (1) has_derivative_scaleR) |
315 apply (erule (1) has_derivative_scaleR) |
316 apply (simp add: mult_ac) |
316 apply (simp add: ac_simps) |
317 done |
317 done |
318 |
318 |
319 lemma GDERIV_mult: |
319 lemma GDERIV_mult: |
320 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk> |
320 "\<lbrakk>GDERIV f x :> df; GDERIV g x :> dg\<rbrakk> |
321 \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" |
321 \<Longrightarrow> GDERIV (\<lambda>x. f x * g x) x :> scaleR (f x) dg + scaleR (g x) df" |
322 unfolding gderiv_def |
322 unfolding gderiv_def |
323 apply (rule has_derivative_subst) |
323 apply (rule has_derivative_subst) |
324 apply (erule (1) has_derivative_mult) |
324 apply (erule (1) has_derivative_mult) |
325 apply (simp add: inner_add mult_ac) |
325 apply (simp add: inner_add ac_simps) |
326 done |
326 done |
327 |
327 |
328 lemma GDERIV_inverse: |
328 lemma GDERIV_inverse: |
329 "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk> |
329 "\<lbrakk>GDERIV f x :> df; f x \<noteq> 0\<rbrakk> |
330 \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df" |
330 \<Longrightarrow> GDERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x))\<^sup>2 *\<^sub>R df" |