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 Retracts |
6 imports |
|
7 Complex_Transcendental |
|
8 Henstock_Kurzweil_Integration |
|
9 Weierstrass_Theorems |
|
10 Retracts |
7 begin |
11 begin |
8 |
12 |
9 lemma leibniz_rule_holomorphic: |
13 lemma leibniz_rule_holomorphic: |
10 fixes f::"complex \<Rightarrow> 'b::euclidean_space \<Rightarrow> complex" |
14 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)" |
15 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)" |
4304 } then |
4308 } then |
4305 show ?thesis |
4309 show ?thesis |
4306 by (auto simp: open_dist) |
4310 by (auto simp: open_dist) |
4307 qed |
4311 qed |
4308 |
4312 |
4309 subsection\<open>Winding number is zero "outside" a curve, in various senses\<close> |
4313 subsection\<open>Winding number is zero "outside" a curve\<close> |
4310 |
4314 |
4311 proposition winding_number_zero_in_outside: |
4315 proposition winding_number_zero_in_outside: |
4312 assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)" |
4316 assumes \<gamma>: "path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>" and z: "z \<in> outside (path_image \<gamma>)" |
4313 shows "winding_number \<gamma> z = 0" |
4317 shows "winding_number \<gamma> z = 0" |
4314 proof - |
4318 proof - |