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)
```