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)