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