398 lemma has_field_derivative_higher_deriv: |
398 lemma has_field_derivative_higher_deriv: |
399 "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk> |
399 "\<lbrakk>f holomorphic_on S; open S; x \<in> S\<rbrakk> |
400 \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)" |
400 \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)" |
401 by (metis (no_types, opaque_lifting) DERIV_deriv_iff_field_differentiable at_within_open comp_apply |
401 by (metis (no_types, opaque_lifting) DERIV_deriv_iff_field_differentiable at_within_open comp_apply |
402 funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def) |
402 funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def) |
|
403 |
|
404 lemma higher_deriv_cmult: |
|
405 assumes "f holomorphic_on A" "x \<in> A" "open A" |
|
406 shows "(deriv ^^ j) (\<lambda>x. c * f x) x = c * (deriv ^^ j) f x" |
|
407 using assms |
|
408 proof (induction j arbitrary: f x) |
|
409 case (Suc j f x) |
|
410 have "deriv ((deriv ^^ j) (\<lambda>x. c * f x)) x = deriv (\<lambda>x. c * (deriv ^^ j) f x) x" |
|
411 using eventually_nhds_in_open[of A x] assms(2,3) Suc.prems |
|
412 by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH) |
|
413 also have "\<dots> = c * deriv ((deriv ^^ j) f) x" using Suc.prems assms(2,3) |
|
414 by (intro deriv_cmult holomorphic_on_imp_differentiable_at holomorphic_higher_deriv) auto |
|
415 finally show ?case by simp |
|
416 qed simp_all |
403 |
417 |
404 lemma valid_path_compose_holomorphic: |
418 lemma valid_path_compose_holomorphic: |
405 assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S" |
419 assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S" |
406 shows "valid_path (f \<circ> g)" |
420 shows "valid_path (f \<circ> g)" |
407 proof (rule valid_path_compose[OF \<open>valid_path g\<close>]) |
421 proof (rule valid_path_compose[OF \<open>valid_path g\<close>]) |