src/HOL/Analysis/Complex_Analysis_Basics.thy
 changeset 67371 2d9cf74943e1 parent 67167 88d1c9d86f48 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Jan 07 22:18:59 2018 +0100
1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Jan 08 17:11:25 2018 +0000
1.3 @@ -401,6 +401,16 @@
1.4    finally show \<dots> .
1.5  qed (insert assms, auto)
1.6
1.7 +lemma leibniz_rule_holomorphic:
1.8 +  fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex"
1.9 +  assumes "\<And>x t. x \<in> U \<Longrightarrow> t \<in> cbox a b \<Longrightarrow> ((\<lambda>x. f x t) has_field_derivative fx x t) (at x within U)"
1.10 +  assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b"
1.11 +  assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)"
1.12 +  assumes "convex U"
1.13 +  shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U"
1.14 +  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
1.15 +  by (auto simp: holomorphic_on_def)
1.16 +
1.17  lemma DERIV_deriv_iff_field_differentiable:
1.18    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
1.19    unfolding field_differentiable_def by (metis DERIV_imp_deriv)
```