equal
deleted
inserted
replaced
1 section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close> |
1 section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close> |
2 |
2 |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
3 text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close> |
4 |
4 |
5 theory Cauchy_Integral_Theorem |
5 theory Cauchy_Integral_Theorem |
6 imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space |
6 imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Retracts |
7 begin |
7 begin |
8 |
8 |
9 lemma leibniz_rule_holomorphic: |
9 lemma leibniz_rule_holomorphic: |
10 fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex" |
10 fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex" |
11 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)" |
11 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)" |