src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 67167 88d1c9d86f48
parent 67135 1a94352812f4
child 67371 2d9cf74943e1
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Dec 11 17:28:32 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Dec 12 10:01:14 2017 +0100
     1.3 @@ -379,6 +379,28 @@
     1.4    "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
     1.5    by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
     1.6  
     1.7 +lemma holomorphic_on_Un [holomorphic_intros]:
     1.8 +  assumes "f holomorphic_on A" "f holomorphic_on B" "open A" "open B"
     1.9 +  shows   "f holomorphic_on (A \<union> B)"
    1.10 +  using assms by (auto simp: holomorphic_on_def  at_within_open[of _ A] 
    1.11 +                             at_within_open[of _ B]  at_within_open[of _ "A \<union> B"] open_Un)
    1.12 +
    1.13 +lemma holomorphic_on_If_Un [holomorphic_intros]:
    1.14 +  assumes "f holomorphic_on A" "g holomorphic_on B" "open A" "open B"
    1.15 +  assumes "\<And>z. z \<in> A \<Longrightarrow> z \<in> B \<Longrightarrow> f z = g z"
    1.16 +  shows   "(\<lambda>z. if z \<in> A then f z else g z) holomorphic_on (A \<union> B)" (is "?h holomorphic_on _")
    1.17 +proof (intro holomorphic_on_Un)
    1.18 +  note \<open>f holomorphic_on A\<close>
    1.19 +  also have "f holomorphic_on A \<longleftrightarrow> ?h holomorphic_on A"
    1.20 +    by (intro holomorphic_cong) auto
    1.21 +  finally show \<dots> .
    1.22 +next
    1.23 +  note \<open>g holomorphic_on B\<close>
    1.24 +  also have "g holomorphic_on B \<longleftrightarrow> ?h holomorphic_on B"
    1.25 +    using assms by (intro holomorphic_cong) auto
    1.26 +  finally show \<dots> .
    1.27 +qed (insert assms, auto)
    1.28 +
    1.29  lemma DERIV_deriv_iff_field_differentiable:
    1.30    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.31    unfolding field_differentiable_def by (metis DERIV_imp_deriv)