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 Weierstrass_Theorems Ordered_Euclidean_Space |
6 imports Complex_Transcendental Henstock_Kurzweil_Integration Weierstrass_Theorems Ordered_Euclidean_Space |
7 begin |
7 begin |
|
8 |
|
9 lemma leibniz_rule_holomorphic: |
|
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)" |
|
12 assumes "\<And>x. x \<in> U \<Longrightarrow> (f x) integrable_on cbox a b" |
|
13 assumes "continuous_on (U \<times> (cbox a b)) (\<lambda>(x, t). fx x t)" |
|
14 assumes "convex U" |
|
15 shows "(\<lambda>x. integral (cbox a b) (f x)) holomorphic_on U" |
|
16 using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)] |
|
17 by (auto simp: holomorphic_on_def) |
|
18 |
|
19 lemma Ln_measurable [measurable]: "Ln \<in> measurable borel borel" |
|
20 proof - |
|
21 have *: "Ln (-of_real x) = of_real (ln x) + \<i> * pi" if "x > 0" for x |
|
22 using that by (subst Ln_minus) (auto simp: Ln_of_real) |
|
23 have **: "Ln (of_real x) = of_real (ln (-x)) + \<i> * pi" if "x < 0" for x |
|
24 using *[of "-x"] that by simp |
|
25 have cont: "(\<lambda>x. indicat_real (- \<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel_measurable borel" |
|
26 by (intro borel_measurable_continuous_on_indicator continuous_intros) auto |
|
27 have "(\<lambda>x. if x \<in> \<real>\<^sub>\<le>\<^sub>0 then ln (-Re x) + \<i> * pi else indicator (-\<real>\<^sub>\<le>\<^sub>0) x *\<^sub>R Ln x) \<in> borel \<rightarrow>\<^sub>M borel" |
|
28 (is "?f \<in> _") by (rule measurable_If_set[OF _ cont]) auto |
|
29 hence "(\<lambda>x. if x = 0 then Ln 0 else ?f x) \<in> borel \<rightarrow>\<^sub>M borel" by measurable |
|
30 also have "(\<lambda>x. if x = 0 then Ln 0 else ?f x) = Ln" |
|
31 by (auto simp: fun_eq_iff ** nonpos_Reals_def) |
|
32 finally show ?thesis . |
|
33 qed |
|
34 |
|
35 lemma powr_complex_measurable [measurable]: |
|
36 assumes [measurable]: "f \<in> measurable M borel" "g \<in> measurable M borel" |
|
37 shows "(\<lambda>x. f x powr g x :: complex) \<in> measurable M borel" |
|
38 using assms by (simp add: powr_def) |
8 |
39 |
9 subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close> |
40 subsection\<^marker>\<open>tag unimportant\<close> \<open>Homeomorphisms of arc images\<close> |
10 |
41 |
11 lemma homeomorphism_arc: |
42 lemma homeomorphism_arc: |
12 fixes g :: "real \<Rightarrow> 'a::t2_space" |
43 fixes g :: "real \<Rightarrow> 'a::t2_space" |