equal
deleted
inserted
replaced
396 unfolding analytic_on_def using holomorphic_higher_deriv by blast |
396 unfolding analytic_on_def using holomorphic_higher_deriv by blast |
397 |
397 |
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, hide_lams) 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 |
403 |
404 lemma valid_path_compose_holomorphic: |
404 lemma valid_path_compose_holomorphic: |
405 assumes "valid_path g" and holo:"f holomorphic_on S" and "open S" "path_image g \<subseteq> S" |
405 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)" |
406 shows "valid_path (f \<circ> g)" |