src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 66486 ffaaa83543b2
parent 66453 cc19f7ca2ed6
child 66827 c94531b5007d
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 22 14:34:26 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 22 21:36:48 2017 +0200
     1.3 @@ -367,6 +367,14 @@
     1.4    "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
     1.5    unfolding holomorphic_on_def by (metis field_differentiable_sum)
     1.6  
     1.7 +lemma holomorphic_pochhammer [holomorphic_intros]:
     1.8 +  "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
     1.9 +  by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
    1.10 +
    1.11 +lemma holomorphic_on_scaleR [holomorphic_intros]:
    1.12 +  "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
    1.13 +  by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
    1.14 +
    1.15  lemma DERIV_deriv_iff_field_differentiable:
    1.16    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.17    unfolding field_differentiable_def by (metis DERIV_imp_deriv)