src/HOL/Analysis/Complex_Analysis_Basics.thy
 changeset 68721 53ad5c01be3f parent 68296 69d680e94961 child 69064 5840724b1d71
```     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 00:19:23 2018 +0100
1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat Aug 04 01:03:39 2018 +0200
1.3 @@ -41,6 +41,24 @@
1.4  lemma linear_cnj: "linear cnj"
1.5    using bounded_linear.linear[OF bounded_linear_cnj] .
1.6
1.7 +lemma vector_derivative_cnj_within:
1.8 +  assumes "at x within A \<noteq> bot" and "f differentiable at x within A"
1.9 +  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x within A) =
1.10 +             cnj (vector_derivative f (at x within A))" (is "_ = cnj ?D")
1.11 +proof -
1.12 +  let ?D = "vector_derivative f (at x within A)"
1.13 +  from assms have "(f has_vector_derivative ?D) (at x within A)"
1.14 +    by (subst (asm) vector_derivative_works)
1.15 +  hence "((\<lambda>x. cnj (f x)) has_vector_derivative cnj ?D) (at x within A)"
1.16 +    by (rule has_vector_derivative_cnj)
1.17 +  thus ?thesis using assms by (auto dest: vector_derivative_within)
1.18 +qed
1.19 +
1.20 +lemma vector_derivative_cnj:
1.21 +  assumes "f differentiable at x"
1.22 +  shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
1.23 +  using assms by (intro vector_derivative_cnj_within) auto
1.24 +
1.25  lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
1.26    by auto
1.27
1.28 @@ -286,6 +304,35 @@
1.29    "f holomorphic_on s \<Longrightarrow> g holomorphic_on t \<Longrightarrow> f ` s \<subseteq> t \<Longrightarrow> (g o f) holomorphic_on s"
1.30    by (metis holomorphic_on_compose holomorphic_on_subset)
1.31
1.32 +lemma holomorphic_on_balls_imp_entire:
1.33 +  assumes "\<not>bdd_above A" "\<And>r. r \<in> A \<Longrightarrow> f holomorphic_on ball c r"
1.34 +  shows   "f holomorphic_on B"
1.35 +proof (rule holomorphic_on_subset)
1.36 +  show "f holomorphic_on UNIV" unfolding holomorphic_on_def
1.37 +  proof
1.38 +    fix z :: complex
1.39 +    from \<open>\<not>bdd_above A\<close> obtain r where r: "r \<in> A" "r > norm (z - c)"
1.40 +      by (meson bdd_aboveI not_le)
1.41 +    with assms(2) have "f holomorphic_on ball c r" by blast
1.42 +    moreover from r have "z \<in> ball c r" by (auto simp: dist_norm norm_minus_commute)
1.43 +    ultimately show "f field_differentiable at z"
1.44 +      by (auto simp: holomorphic_on_def at_within_open[of _ "ball c r"])
1.45 +  qed
1.46 +qed auto
1.47 +
1.48 +lemma holomorphic_on_balls_imp_entire':
1.49 +  assumes "\<And>r. r > 0 \<Longrightarrow> f holomorphic_on ball c r"
1.50 +  shows   "f holomorphic_on B"
1.51 +proof (rule holomorphic_on_balls_imp_entire)
1.52 +  {
1.53 +    fix M :: real
1.54 +    have "\<exists>x. x > max M 0" by (intro gt_ex)
1.55 +    hence "\<exists>x>0. x > M" by auto
1.56 +  }
1.57 +  thus "\<not>bdd_above {(0::real)<..}" unfolding bdd_above_def
1.58 +    by (auto simp: not_le)
1.59 +qed (insert assms, auto)
1.60 +
1.61  lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \<Longrightarrow> (\<lambda>z. -(f z)) holomorphic_on s"
1.62    by (metis field_differentiable_minus holomorphic_on_def)
1.63
```