43 |
43 |
44 lemma has_contour_integral_midpoint: |
44 lemma has_contour_integral_midpoint: |
45 assumes "(f has_contour_integral i) (linepath a (midpoint a b))" |
45 assumes "(f has_contour_integral i) (linepath a (midpoint a b))" |
46 "(f has_contour_integral j) (linepath (midpoint a b) b)" |
46 "(f has_contour_integral j) (linepath (midpoint a b) b)" |
47 shows "(f has_contour_integral (i + j)) (linepath a b)" |
47 shows "(f has_contour_integral (i + j)) (linepath a b)" |
48 apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"]) |
48 proof (rule has_contour_integral_split) |
49 using assms |
49 show "midpoint a b - a = (1/2) *\<^sub>R (b - a)" |
50 apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) |
50 using assms by (auto simp: midpoint_def scaleR_conv_of_real) |
51 done |
51 qed (use assms in auto) |
52 |
52 |
53 lemma contour_integral_midpoint: |
53 lemma contour_integral_midpoint: |
54 "continuous_on (closed_segment a b) f |
54 assumes "continuous_on (closed_segment a b) f" |
55 \<Longrightarrow> contour_integral (linepath a b) f = |
55 shows "contour_integral (linepath a b) f = |
56 contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" |
56 contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" |
57 apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"]) |
57 proof (rule contour_integral_split) |
58 apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) |
58 show "midpoint a b - a = (1/2) *\<^sub>R (b - a)" |
59 done |
59 using assms by (auto simp: midpoint_def scaleR_conv_of_real) |
|
60 qed (use assms in auto) |
60 |
61 |
61 text\<open>A couple of special case lemmas that are useful below\<close> |
62 text\<open>A couple of special case lemmas that are useful below\<close> |
62 |
63 |
63 lemma triangle_linear_has_chain_integral: |
64 lemma triangle_linear_has_chain_integral: |
64 "((\<lambda>x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" |
65 "((\<lambda>x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" |
65 apply (rule Cauchy_theorem_primitive [of UNIV "\<lambda>x. m/2 * x^2 + d*x"]) |
66 proof (rule Cauchy_theorem_primitive) |
66 apply (auto intro!: derivative_eq_intros) |
67 show "\<And>x. x \<in> UNIV \<Longrightarrow> ((\<lambda>x. m / 2 * x\<^sup>2 + d * x) has_field_derivative m * x + d) (at x)" |
67 done |
68 by (auto intro!: derivative_eq_intros) |
|
69 qed auto |
68 |
70 |
69 lemma has_chain_integral_chain_integral3: |
71 lemma has_chain_integral_chain_integral3: |
70 "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d) |
72 assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d)" |
71 \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" |
73 (is "(f has_contour_integral i) ?g") |
72 apply (subst contour_integral_unique [symmetric], assumption) |
74 shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" |
73 apply (drule has_contour_integral_integrable) |
75 (is "?lhs = _") |
74 apply (simp add: valid_path_join) |
76 proof - |
75 done |
77 have "f contour_integrable_on ?g" |
|
78 using assms contour_integrable_on_def by blast |
|
79 then have "?lhs = contour_integral ?g f" |
|
80 by (simp add: valid_path_join has_contour_integral_integrable) |
|
81 then show ?thesis |
|
82 using assms contour_integral_unique by blast |
|
83 qed |
76 |
84 |
77 lemma has_chain_integral_chain_integral4: |
85 lemma has_chain_integral_chain_integral4: |
78 "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e) |
86 assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e)" |
79 \<Longrightarrow> contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i" |
87 (is "(f has_contour_integral i) ?g") |
80 apply (subst contour_integral_unique [symmetric], assumption) |
88 shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i" |
81 apply (drule has_contour_integral_integrable) |
89 (is "?lhs = _") |
82 apply (simp add: valid_path_join) |
90 proof - |
83 done |
91 have "f contour_integrable_on ?g" |
|
92 using assms contour_integrable_on_def by blast |
|
93 then have "?lhs = contour_integral ?g f" |
|
94 by (simp add: valid_path_join has_contour_integral_integrable) |
|
95 then show ?thesis |
|
96 using assms contour_integral_unique by blast |
|
97 qed |
84 |
98 |
85 subsection\<^marker>\<open>tag unimportant\<close> \<open>The key quadrisection step\<close> |
99 subsection\<^marker>\<open>tag unimportant\<close> \<open>The key quadrisection step\<close> |
86 |
100 |
87 lemma norm_sum_half: |
101 lemma norm_sum_half: |
88 assumes "norm(a + b) \<ge> e" |
102 assumes "norm(a + b) \<ge> e" |
125 "continuous_on (closed_segment a' c') f" |
139 "continuous_on (closed_segment a' c') f" |
126 "continuous_on (closed_segment b' a') f" |
140 "continuous_on (closed_segment b' a') f" |
127 unfolding a'_def b'_def c'_def |
141 unfolding a'_def b'_def c'_def |
128 by (rule continuous_on_subset [OF f], |
142 by (rule continuous_on_subset [OF f], |
129 metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ |
143 metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ |
130 let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f" |
144 define pathint where "pathint x y \<equiv> contour_integral(linepath x y) f" for x y |
131 have *: "?pathint a b + ?pathint b c + ?pathint c a = |
145 have *: "pathint a b + pathint b c + pathint c a = |
132 (?pathint a c' + ?pathint c' b' + ?pathint b' a) + |
146 (pathint a c' + pathint c' b' + pathint b' a) + |
133 (?pathint a' c' + ?pathint c' b + ?pathint b a') + |
147 (pathint a' c' + pathint c' b + pathint b a') + |
134 (?pathint a' c + ?pathint c b' + ?pathint b' a') + |
148 (pathint a' c + pathint c b' + pathint b' a') + |
135 (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" |
149 (pathint a' b' + pathint b' c' + pathint c' a')" |
|
150 unfolding pathint_def |
136 by (simp add: fcont' contour_integral_reverse_linepath) (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc) |
151 by (simp add: fcont' contour_integral_reverse_linepath) (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc) |
137 have [simp]: "\<And>x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" |
152 have [simp]: "\<And>x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" |
138 by (metis left_diff_distrib mult.commute norm_mult_numeral1) |
153 by (metis left_diff_distrib mult.commute norm_mult_numeral1) |
139 have [simp]: "\<And>x y. cmod (x - y) = cmod (y - x)" |
154 have [simp]: "\<And>x y. cmod (x - y) = cmod (y - x)" |
140 by (simp add: norm_minus_commute) |
155 by (simp add: norm_minus_commute) |
141 consider "e * K\<^sup>2 / 4 \<le> cmod (?pathint a c' + ?pathint c' b' + ?pathint b' a)" | |
156 consider "e * K\<^sup>2 / 4 \<le> cmod (pathint a c' + pathint c' b' + pathint b' a)" | |
142 "e * K\<^sup>2 / 4 \<le> cmod (?pathint a' c' + ?pathint c' b + ?pathint b a')" | |
157 "e * K\<^sup>2 / 4 \<le> cmod (pathint a' c' + pathint c' b + pathint b a')" | |
143 "e * K\<^sup>2 / 4 \<le> cmod (?pathint a' c + ?pathint c b' + ?pathint b' a')" | |
158 "e * K\<^sup>2 / 4 \<le> cmod (pathint a' c + pathint c b' + pathint b' a')" | |
144 "e * K\<^sup>2 / 4 \<le> cmod (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" |
159 "e * K\<^sup>2 / 4 \<le> cmod (pathint a' b' + pathint b' c' + pathint c' a')" |
145 using assms unfolding * by (blast intro: that dest!: norm_sum_lemma) |
160 using assms by (metis "*" norm_sum_lemma pathint_def) |
146 then show ?thesis |
161 then show ?thesis |
147 proof cases |
162 proof cases |
148 case 1 then have "?\<Phi> a c' b'" |
163 case 1 then have "?\<Phi> a c' b'" |
149 using assms |
164 using assms unfolding pathint_def [symmetric] |
150 apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
165 apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
151 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
166 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
152 done |
167 done |
153 then show ?thesis by blast |
168 then show ?thesis by blast |
154 next |
169 next |
155 case 2 then have "?\<Phi> a' c' b" |
170 case 2 then have "?\<Phi> a' c' b" |
156 using assms |
171 using assms unfolding pathint_def [symmetric] |
157 apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
172 apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
158 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
173 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
159 done |
174 done |
160 then show ?thesis by blast |
175 then show ?thesis by blast |
161 next |
176 next |
162 case 3 then have "?\<Phi> a' c b'" |
177 case 3 then have "?\<Phi> a' c b'" |
163 using assms |
178 using assms unfolding pathint_def [symmetric] |
164 apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
179 apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
165 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
180 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
166 done |
181 done |
167 then show ?thesis by blast |
182 then show ?thesis by blast |
168 next |
183 next |
169 case 4 then have "?\<Phi> a' b' c'" |
184 case 4 then have "?\<Phi> a' b' c'" |
170 using assms |
185 using assms unfolding pathint_def [symmetric] |
171 apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
186 apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) |
172 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
187 apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) |
173 done |
188 done |
174 then show ?thesis by blast |
189 then show ?thesis by blast |
175 qed |
190 qed |
441 next |
458 next |
442 case False |
459 case False |
443 have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" |
460 have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" |
444 using f continuous_on_subset segments_subset_convex_hull by metis+ |
461 using f continuous_on_subset segments_subset_convex_hull by metis+ |
445 moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f + |
462 moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f + |
446 contour_integral (linepath c b) f = 0" |
463 contour_integral (linepath c b) f = 0" |
447 apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) |
464 proof (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) |
448 using False c |
465 show "continuous_on (convex hull {b, a, c}) f" |
449 apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps) |
466 by (simp add: f insert_commute) |
450 done |
467 show "c - b = (1 - k) *\<^sub>R (a - b)" |
|
468 using c by (auto simp: algebra_simps) |
|
469 qed (use False in auto) |
451 ultimately show ?thesis |
470 ultimately show ?thesis |
452 apply (auto simp: contour_integral_reverse_linepath) |
471 by (metis (no_types, lifting) contour_integral_reverse_linepath eq_neg_iff_add_eq_0 minus_add_cancel) |
453 using add_eq_0_iff by force |
472 qed |
454 qed |
473 |
455 |
474 |
456 lemma Cauchy_theorem_triangle_interior: |
475 proposition Cauchy_theorem_triangle_interior: |
457 assumes contf: "continuous_on (convex hull {a,b,c}) f" |
476 assumes contf: "continuous_on (convex hull {a,b,c}) f" |
458 and holf: "f holomorphic_on interior (convex hull {a,b,c})" |
477 and holf: "f holomorphic_on interior (convex hull {a,b,c})" |
459 shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" |
478 shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" |
460 proof - |
479 proof - |
|
480 define pathint where "pathint \<equiv> \<lambda>x y. contour_integral(linepath x y) f" |
461 have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" |
481 have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" |
462 using contf continuous_on_subset segments_subset_convex_hull by metis+ |
482 using contf continuous_on_subset segments_subset_convex_hull by metis+ |
463 have "bounded (f ` (convex hull {a,b,c}))" |
483 have "bounded (f ` (convex hull {a,b,c}))" |
464 by (simp add: compact_continuous_image compact_convex_hull compact_imp_bounded contf) |
484 by (simp add: compact_continuous_image compact_convex_hull compact_imp_bounded contf) |
465 then obtain B where "0 < B" and Bnf: "\<And>x. x \<in> convex hull {a,b,c} \<Longrightarrow> norm (f x) \<le> B" |
485 then obtain B where "0 < B" and Bnf: "\<And>x. x \<in> convex hull {a,b,c} \<Longrightarrow> norm (f x) \<le> B" |
501 by (simp add: collinear_3_eq_affine_dependent) |
521 by (simp add: collinear_3_eq_affine_dependent) |
502 with False obtain d where "c \<noteq> a" "a \<noteq> b" "b \<noteq> c" "c - b = d *\<^sub>R (a - b)" |
522 with False obtain d where "c \<noteq> a" "a \<noteq> b" "b \<noteq> c" "c - b = d *\<^sub>R (a - b)" |
503 by (auto simp: collinear_3 collinear_lemma) |
523 by (auto simp: collinear_3 collinear_lemma) |
504 then have "False" |
524 then have "False" |
505 using False Cauchy_theorem_flat [OF contf'] pi_eq_y ynz |
525 using False Cauchy_theorem_flat [OF contf'] pi_eq_y ynz |
506 by (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath) |
526 by (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath pathint_def) |
507 } |
527 } |
508 then obtain d where d: "d \<in> interior (convex hull {a, b, c})" |
528 then obtain d where d: "d \<in> interior (convex hull {a, b, c})" |
509 by blast |
529 by blast |
510 { fix d1 |
530 { fix d1 |
511 assume d1_pos: "0 < d1" |
531 assume d1_pos: "0 < d1" |
512 and d1: "\<And>x x'. \<lbrakk>x\<in>convex hull {a, b, c}; x'\<in>convex hull {a, b, c}; cmod (x' - x) < d1\<rbrakk> |
532 and d1: "\<And>x x'. \<lbrakk>x\<in>convex hull {a, b, c}; x'\<in>convex hull {a, b, c}; cmod (x' - x) < d1\<rbrakk> |
513 \<Longrightarrow> cmod (f x' - f x) < cmod y / (24 * C)" |
533 \<Longrightarrow> cmod (f x' - f x) < cmod y / (24 * C)" |
514 define e where "e = min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))" |
534 define e where "e = min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))" |
515 define shrink where "shrink x = x - e *\<^sub>R (x - d)" for x |
535 define shrink where "shrink x = x - e *\<^sub>R (x - d)" for x |
516 let ?pathint = "\<lambda>x y. contour_integral(linepath x y) f" |
|
517 have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B" |
536 have e: "0 < e" "e \<le> 1" "e \<le> d1 / (4 * C)" "e \<le> cmod y / 24 / C / B" |
518 using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def) |
537 using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def) |
519 then have eCB: "24 * e * C * B \<le> cmod y" |
|
520 using \<open>C>0\<close> \<open>B>0\<close> by (simp add: field_simps) |
|
521 have e_le_d1: "e * (4 * C) \<le> d1" |
538 have e_le_d1: "e * (4 * C) \<le> d1" |
522 using e \<open>C>0\<close> by (simp add: field_simps) |
539 using e \<open>C>0\<close> by (simp add: field_simps) |
523 have "shrink a \<in> interior(convex hull {a,b,c})" |
540 have "shrink a \<in> interior(convex hull {a,b,c})" |
524 "shrink b \<in> interior(convex hull {a,b,c})" |
541 "shrink b \<in> interior(convex hull {a,b,c})" |
525 "shrink c \<in> interior(convex hull {a,b,c})" |
542 "shrink c \<in> interior(convex hull {a,b,c})" |
526 using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) |
543 using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) |
527 then have fhp0: "(f has_contour_integral 0) |
544 then have fhp0: "(f has_contour_integral 0) |
528 (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))" |
545 (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))" |
529 by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal) |
546 by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal) |
530 then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0" |
547 then have f_0_shrink: "pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a) = 0" |
531 by (simp add: has_chain_integral_chain_integral3) |
548 by (simp add: has_chain_integral_chain_integral3 pathint_def) |
532 have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)" |
549 have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)" |
533 "f contour_integrable_on linepath (shrink b) (shrink c)" |
550 "f contour_integrable_on linepath (shrink b) (shrink c)" |
534 "f contour_integrable_on linepath (shrink c) (shrink a)" |
551 "f contour_integrable_on linepath (shrink c) (shrink a)" |
535 using fhp0 by (auto simp: valid_path_join dest: has_contour_integral_integrable) |
552 using fhp0 by (auto simp: valid_path_join dest: has_contour_integral_integrable) |
536 have cmod_shr: "\<And>x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)" |
553 have cmod_shr: "\<And>x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)" |
538 have sh_eq: "\<And>a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)" |
555 have sh_eq: "\<And>a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)" |
539 by (simp add: algebra_simps) |
556 by (simp add: algebra_simps) |
540 have "cmod y / (24 * C) \<le> cmod y / cmod (b - a) / 12" |
557 have "cmod y / (24 * C) \<le> cmod y / cmod (b - a) / 12" |
541 using False \<open>C>0\<close> diff_2C [of b a] ynz |
558 using False \<open>C>0\<close> diff_2C [of b a] ynz |
542 by (auto simp: field_split_simps hull_inc) |
559 by (auto simp: field_split_simps hull_inc) |
543 have less_C: "\<lbrakk>u \<in> convex hull {a, b, c}; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> x * cmod u < C" for x u |
560 have less_C: "x * cmod u < C" if "u \<in> convex hull {a,b,c}" "0 \<le> x" "x \<le> 1" for x u |
544 apply (cases "x=0", simp add: \<open>0<C\<close>) |
561 proof (cases "x=0") |
545 using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast |
562 case False |
|
563 with that show ?thesis |
|
564 using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast |
|
565 qed (simp add: \<open>0<C\<close>) |
546 { fix u v |
566 { fix u v |
547 assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v" |
567 assume uv: "u \<in> convex hull {a, b, c}" "v \<in> convex hull {a, b, c}" "u\<noteq>v" |
548 and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)" |
568 and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)" |
549 have shr_uv: "shrink u \<in> interior(convex hull {a,b,c})" |
569 have shr_uv: "shrink u \<in> interior(convex hull {a,b,c})" |
550 "shrink v \<in> interior(convex hull {a,b,c})" |
570 "shrink v \<in> interior(convex hull {a,b,c})" |
551 using d e uv |
571 using d e uv |
552 by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) |
572 by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) |
553 have cmod_fuv: "\<And>x. 0\<le>x \<Longrightarrow> x\<le>1 \<Longrightarrow> cmod (f (linepath (shrink u) (shrink v) x)) \<le> B" |
573 have cmod_fuv: "\<And>x. 0\<le>x \<Longrightarrow> x\<le>1 \<Longrightarrow> cmod (f (linepath (shrink u) (shrink v) x)) \<le> B" |
554 using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD]) |
574 using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD]) |
555 have By_uv: "B * (12 * (e * cmod (u - v))) \<le> cmod y" |
|
556 apply (rule order_trans [OF _ eCB]) |
|
557 using e \<open>B>0\<close> diff_2C [of u v] uv |
|
558 by (auto simp: field_simps) |
|
559 { fix x::real assume x: "0\<le>x" "x\<le>1" |
575 { fix x::real assume x: "0\<le>x" "x\<le>1" |
|
576 have "\<bar>1 - x\<bar> * cmod u < C" "\<bar>x\<bar> * cmod v < C" |
|
577 using uv x by (auto intro!: less_C) |
|
578 moreover have "\<bar>x\<bar> * cmod d < C" "\<bar>1 - x\<bar> * cmod d < C" |
|
579 using x d interior_subset by (auto intro!: less_C) |
|
580 ultimately |
560 have cmod_less_4C: "cmod ((1 - x) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>R d) < (C+C) + (C+C)" |
581 have cmod_less_4C: "cmod ((1 - x) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>R d) < (C+C) + (C+C)" |
561 apply (rule add_strict_mono; rule norm_triangle_half_l [of _ 0]) |
582 by (metis add_strict_mono le_less_trans norm_scaleR norm_triangle_ineq4) |
562 using uv x d interior_subset |
|
563 apply (auto simp: hull_inc intro!: less_C) |
|
564 done |
|
565 have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))" |
583 have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))" |
566 by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real) |
584 by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real) |
567 have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1" |
585 have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1" |
568 apply (simp only: ll norm_mult scaleR_diff_right) |
586 unfolding ll norm_mult scaleR_diff_right |
569 using \<open>e>0\<close> cmod_less_4C apply (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1]) |
587 using \<open>e>0\<close> cmod_less_4C by (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1]) |
570 done |
|
571 have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" |
|
572 using x uv shr_uv cmod_less_dt |
|
573 by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) |
|
574 also have "\<dots> \<le> cmod y / cmod (v - u) / 12" |
|
575 using False uv \<open>C>0\<close> diff_2C [of v u] ynz |
|
576 by (auto simp: field_split_simps hull_inc) |
|
577 finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \<le> cmod y / cmod (v - u) / 12" |
|
578 by simp |
|
579 then have cmod_12_le: "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) * 12 \<le> cmod y" |
|
580 using uv False by (auto simp: field_simps) |
|
581 have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + |
588 have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + |
582 cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) |
589 cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) |
583 \<le> B * (cmod y / 24 / C / B * 2 * C) + 2 * C * (cmod y / 24 / C)" |
590 \<le> B * (cmod y / 24 / C / B * 2 * C) + 2 * C * (cmod y / 24 / C)" |
584 apply (rule add_mono [OF mult_mono]) |
591 proof (intro add_mono [OF mult_mono]) |
585 using By_uv e \<open>0 < B\<close> \<open>0 < C\<close> x apply (simp_all add: cmod_fuv cmod_shr cmod_12_le) |
592 show "cmod (f (linepath (shrink u) (shrink v) x)) \<le> B" |
586 apply (simp add: field_simps) |
593 using cmod_fuv x by blast |
587 done |
594 have "B * (12 * (e * cmod (u - v))) \<le> 24 * e * C * B" |
|
595 using e \<open>B>0\<close> diff_2C [of u v] uv by (auto simp: field_simps) |
|
596 also have "\<dots> \<le> cmod y" |
|
597 using \<open>C>0\<close> \<open>B>0\<close> e by (simp add: field_simps) |
|
598 finally show "cmod (shrink v - shrink u - (v - u)) \<le> cmod y / 24 / C / B * 2 * C" |
|
599 using \<open>0 < B\<close> \<open>0 < C\<close> by (simp add: cmod_shr mult_ac divide_simps) |
|
600 have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" |
|
601 using x uv shr_uv cmod_less_dt |
|
602 by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) |
|
603 also have "\<dots> \<le> cmod y / cmod (v - u) / 12" |
|
604 using False uv \<open>C>0\<close> diff_2C [of v u] ynz |
|
605 by (auto simp: field_split_simps hull_inc) |
|
606 finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \<le> cmod y / cmod (v - u) / 12" |
|
607 by simp |
|
608 then show "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) |
|
609 \<le> 2 * C * (cmod y / 24 / C)" |
|
610 using uv C by (simp add: field_simps) |
|
611 qed (use \<open>0 < B\<close> in auto) |
588 also have "\<dots> \<le> cmod y / 6" |
612 also have "\<dots> \<le> cmod y / 6" |
589 by simp |
613 by simp |
590 finally have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + |
614 finally have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + |
591 cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) |
615 cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) |
592 \<le> cmod y / 6" . |
616 \<le> cmod y / 6" . |
593 } note cmod_diff_le = this |
617 } note cmod_diff_le = this |
594 have f_uv: "continuous_on (closed_segment u v) f" |
618 have f_uv: "continuous_on (closed_segment u v) f" |
595 by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull]) |
619 by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull]) |
596 have **: "\<And>f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)" |
620 have **: "\<And>f' x' f x::complex. f'*x' - f*x = f' * (x' - x) + x * (f' - f)" |
597 by (simp add: algebra_simps) |
621 by (simp add: algebra_simps) |
598 have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) |
622 have "norm (pathint (shrink u) (shrink v) - pathint u v) |
599 \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))" |
623 \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))" |
600 apply (rule has_integral_bound |
624 apply (rule has_integral_bound |
601 [of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" |
625 [of _ "\<lambda>x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" |
602 _ 0 1]) |
626 _ 0 1]) |
603 using ynz \<open>0 < B\<close> \<open>0 < C\<close> |
627 using ynz \<open>0 < B\<close> \<open>0 < C\<close> |
604 apply (simp_all del: le_divide_eq_numeral1) |
628 apply (simp_all add: pathint_def has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral |
605 apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral |
629 fpi_uv f_uv contour_integrable_continuous_linepath del: le_divide_eq_numeral1) |
606 fpi_uv f_uv contour_integrable_continuous_linepath) |
|
607 apply (auto simp: ** norm_triangle_le norm_mult cmod_diff_le simp del: le_divide_eq_numeral1) |
630 apply (auto simp: ** norm_triangle_le norm_mult cmod_diff_le simp del: le_divide_eq_numeral1) |
608 done |
631 done |
609 also have "\<dots> \<le> norm y / 6" |
632 also have "\<dots> \<le> norm y / 6" |
610 by simp |
633 by simp |
611 finally have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) \<le> norm y / 6" . |
634 finally have "norm (pathint (shrink u) (shrink v) - pathint u v) \<le> norm y / 6" . |
612 } note * = this |
635 } note * = this |
613 have "norm (?pathint (shrink a) (shrink b) - ?pathint a b) \<le> norm y / 6" |
636 have "norm (pathint (shrink a) (shrink b) - pathint a b) \<le> norm y / 6" |
614 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
637 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
615 moreover |
638 moreover |
616 have "norm (?pathint (shrink b) (shrink c) - ?pathint b c) \<le> norm y / 6" |
639 have "norm (pathint (shrink b) (shrink c) - pathint b c) \<le> norm y / 6" |
617 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
640 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
618 moreover |
641 moreover |
619 have "norm (?pathint (shrink c) (shrink a) - ?pathint c a) \<le> norm y / 6" |
642 have "norm (pathint (shrink c) (shrink a) - pathint c a) \<le> norm y / 6" |
620 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
643 using False fpi_abc by (rule_tac *) (auto simp: hull_inc) |
621 ultimately |
644 ultimately |
622 have "norm((?pathint (shrink a) (shrink b) - ?pathint a b) + |
645 have "norm((pathint (shrink a) (shrink b) - pathint a b) + |
623 (?pathint (shrink b) (shrink c) - ?pathint b c) + (?pathint (shrink c) (shrink a) - ?pathint c a)) |
646 (pathint (shrink b) (shrink c) - pathint b c) + (pathint (shrink c) (shrink a) - pathint c a)) |
624 \<le> norm y / 6 + norm y / 6 + norm y / 6" |
647 \<le> norm y / 6 + norm y / 6 + norm y / 6" |
625 by (metis norm_triangle_le add_mono) |
648 by (metis norm_triangle_le add_mono) |
626 also have "\<dots> = norm y / 2" |
649 also have "\<dots> = norm y / 2" |
627 by simp |
650 by simp |
628 finally have "norm((?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a)) - |
651 finally have "norm((pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a)) - |
629 (?pathint a b + ?pathint b c + ?pathint c a)) |
652 (pathint a b + pathint b c + pathint c a)) |
630 \<le> norm y / 2" |
653 \<le> norm y / 2" |
631 by (simp add: algebra_simps) |
654 by (simp add: algebra_simps) |
632 then |
655 then |
633 have "norm(?pathint a b + ?pathint b c + ?pathint c a) \<le> norm y / 2" |
656 have "norm(pathint a b + pathint b c + pathint c a) \<le> norm y / 2" |
634 by (simp add: f_0_shrink) (metis (mono_tags) add.commute minus_add_distrib norm_minus_cancel uminus_add_conv_diff) |
657 by (simp add: f_0_shrink) (metis (mono_tags) add.commute minus_add_distrib norm_minus_cancel uminus_add_conv_diff) |
635 then have "False" |
658 then have "False" |
636 using pi_eq_y ynz by auto |
659 using pi_eq_y ynz by auto |
637 } |
660 } |
638 note * = this |
661 note * = this |
986 |
1012 |
987 subsection\<^marker>\<open>tag unimportant\<close> \<open>Generalize integrability to local primitives\<close> |
1013 subsection\<^marker>\<open>tag unimportant\<close> \<open>Generalize integrability to local primitives\<close> |
988 |
1014 |
989 lemma contour_integral_local_primitive_lemma: |
1015 lemma contour_integral_local_primitive_lemma: |
990 fixes f :: "complex\<Rightarrow>complex" |
1016 fixes f :: "complex\<Rightarrow>complex" |
991 shows |
1017 assumes gpd: "g piecewise_differentiable_on {a..b}" |
992 "\<lbrakk>g piecewise_differentiable_on {a..b}; |
1018 and dh: "\<And>x. x \<in> S \<Longrightarrow> (f has_field_derivative f' x) (at x within S)" |
993 \<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative f' x) (at x within s); |
1019 and gs: "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> S" |
994 \<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s\<rbrakk> |
1020 shows |
995 \<Longrightarrow> (\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) |
1021 "(\<lambda>x. f' (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b}" |
996 integrable_on {a..b}" |
1022 proof (cases "cbox a b = {}") |
997 apply (cases "cbox a b = {}", force) |
1023 case False |
998 apply (simp add: integrable_on_def) |
1024 then show ?thesis |
999 apply (rule exI) |
1025 unfolding integrable_on_def by (auto intro: assms contour_integral_primitive_lemma) |
1000 apply (rule contour_integral_primitive_lemma, assumption+) |
1026 qed auto |
1001 using atLeastAtMost_iff by blast |
|
1002 |
1027 |
1003 lemma contour_integral_local_primitive_any: |
1028 lemma contour_integral_local_primitive_any: |
1004 fixes f :: "complex \<Rightarrow> complex" |
1029 fixes f :: "complex \<Rightarrow> complex" |
1005 assumes gpd: "g piecewise_differentiable_on {a..b}" |
1030 assumes gpd: "g piecewise_differentiable_on {a..b}" |
1006 and dh: "\<And>x. x \<in> s |
1031 and dh: "\<And>x. x \<in> S |
1007 \<Longrightarrow> \<exists>d h. 0 < d \<and> |
1032 \<Longrightarrow> \<exists>d h. 0 < d \<and> |
1008 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
1033 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within S))" |
1009 and gs: "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> s" |
1034 and gs: "\<And>x. x \<in> {a..b} \<Longrightarrow> g x \<in> S" |
1010 shows "(\<lambda>x. f(g x) * vector_derivative g (at x)) integrable_on {a..b}" |
1035 shows "(\<lambda>x. f(g x) * vector_derivative g (at x)) integrable_on {a..b}" |
1011 proof - |
1036 proof - |
1012 { fix x |
1037 { fix x |
1013 assume x: "a \<le> x" "x \<le> b" |
1038 assume x: "a \<le> x" "x \<le> b" |
1014 obtain d h where d: "0 < d" |
1039 obtain d h where d: "0 < d" |
1015 and h: "(\<And>y. norm(y - g x) < d \<Longrightarrow> (h has_field_derivative f y) (at y within s))" |
1040 and h: "(\<And>y. norm(y - g x) < d \<Longrightarrow> (h has_field_derivative f y) (at y within S))" |
1016 using x gs dh by (metis atLeastAtMost_iff) |
1041 using x gs dh by (metis atLeastAtMost_iff) |
1017 have "continuous_on {a..b} g" using gpd piecewise_differentiable_on_def by blast |
1042 have "continuous_on {a..b} g" using gpd piecewise_differentiable_on_def by blast |
1018 then obtain e where e: "e>0" and lessd: "\<And>x'. x' \<in> {a..b} \<Longrightarrow> \<bar>x' - x\<bar> < e \<Longrightarrow> cmod (g x' - g x) < d" |
1043 then obtain e where e: "e>0" and lessd: "\<And>x'. x' \<in> {a..b} \<Longrightarrow> \<bar>x' - x\<bar> < e \<Longrightarrow> cmod (g x' - g x) < d" |
1019 using x d |
1044 using x d by (fastforce simp: dist_norm continuous_on_iff) |
1020 apply (auto simp: dist_norm continuous_on_iff) |
1045 have "\<exists>e>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> {u..v} \<subseteq> ball x e \<and> (u \<le> v \<longrightarrow> a \<le> u \<and> v \<le> b) \<longrightarrow> |
1021 apply (drule_tac x=x in bspec) |
|
1022 using x apply simp |
|
1023 apply (drule_tac x=d in spec, auto) |
|
1024 done |
|
1025 have "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> {u..v} \<subseteq> ball x d \<and> (u \<le> v \<longrightarrow> a \<le> u \<and> v \<le> b) \<longrightarrow> |
|
1026 (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {u..v}" |
1046 (\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {u..v}" |
1027 apply (rule_tac x=e in exI) |
1047 proof - |
1028 using e |
1048 have "(\<lambda>x. f (g x) * vector_derivative g (at x within {u..v})) integrable_on {u..v}" |
1029 apply (simp add: integrable_on_localized_vector_derivative [symmetric], clarify) |
1049 if "u \<le> x" "x \<le> v" and ball: "{u..v} \<subseteq> ball x e" and auvb: "u \<le> v \<Longrightarrow> a \<le> u \<and> v \<le> b" |
1030 apply (rule_tac f = h and s = "g ` {u..v}" in contour_integral_local_primitive_lemma) |
1050 for u v |
1031 apply (meson atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset) |
1051 proof (rule contour_integral_local_primitive_lemma) |
1032 apply (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h], force) |
1052 show "g piecewise_differentiable_on {u..v}" |
1033 done |
1053 by (metis atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset auvb) |
|
1054 show "\<And>x. x \<in> g ` {u..v} \<Longrightarrow> (h has_field_derivative f x) (at x within g ` {u..v})" |
|
1055 using that by (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h]) |
|
1056 qed auto |
|
1057 then show ?thesis |
|
1058 using e integrable_on_localized_vector_derivative by blast |
|
1059 qed |
1034 } then |
1060 } then |
1035 show ?thesis |
1061 show ?thesis |
1036 by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified]) |
1062 by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified]) |
1037 qed |
1063 qed |
1038 |
1064 |
1039 lemma contour_integral_local_primitive: |
1065 lemma contour_integral_local_primitive: |
1040 fixes f :: "complex \<Rightarrow> complex" |
1066 fixes f :: "complex \<Rightarrow> complex" |
1041 assumes g: "valid_path g" "path_image g \<subseteq> s" |
1067 assumes g: "valid_path g" "path_image g \<subseteq> S" |
1042 and dh: "\<And>x. x \<in> s |
1068 and dh: "\<And>x. x \<in> S |
1043 \<Longrightarrow> \<exists>d h. 0 < d \<and> |
1069 \<Longrightarrow> \<exists>d h. 0 < d \<and> |
1044 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
1070 (\<forall>y. norm(y - x) < d \<longrightarrow> (h has_field_derivative f y) (at y within S))" |
1045 shows "f contour_integrable_on g" |
1071 shows "f contour_integrable_on g" |
1046 using g |
1072 proof - |
1047 apply (simp add: valid_path_def path_image_def contour_integrable_on_def has_contour_integral_def |
1073 have "(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {0..1}" |
1048 has_integral_localized_vector_derivative integrable_on_def [symmetric]) |
1074 using contour_integral_local_primitive_any [OF _ dh] g |
1049 using contour_integral_local_primitive_any [OF _ dh] |
1075 unfolding path_image_def valid_path_def |
1050 by (meson image_subset_iff piecewise_C1_imp_differentiable) |
1076 by (metis (no_types, lifting) image_subset_iff piecewise_C1_imp_differentiable) |
|
1077 then show ?thesis |
|
1078 using contour_integrable_on by presburger |
|
1079 qed |
1051 |
1080 |
1052 |
1081 |
1053 text\<open>In particular if a function is holomorphic\<close> |
1082 text\<open>In particular if a function is holomorphic\<close> |
1054 |
1083 |
1055 lemma contour_integrable_holomorphic: |
1084 lemma contour_integrable_holomorphic: |
1056 assumes contf: "continuous_on s f" |
1085 assumes contf: "continuous_on S f" |
1057 and os: "open s" |
1086 and os: "open S" |
1058 and k: "finite k" |
1087 and k: "finite k" |
1059 and g: "valid_path g" "path_image g \<subseteq> s" |
1088 and g: "valid_path g" "path_image g \<subseteq> S" |
1060 and fcd: "\<And>x. x \<in> s - k \<Longrightarrow> f field_differentiable at x" |
1089 and fcd: "\<And>x. x \<in> S - k \<Longrightarrow> f field_differentiable at x" |
1061 shows "f contour_integrable_on g" |
1090 shows "f contour_integrable_on g" |
1062 proof - |
1091 proof - |
1063 { fix z |
1092 { fix z |
1064 assume z: "z \<in> s" |
1093 assume z: "z \<in> S" |
1065 obtain d where "d>0" and d: "ball z d \<subseteq> s" using \<open>open s\<close> z |
1094 obtain d where "d>0" and d: "ball z d \<subseteq> S" using \<open>open S\<close> z |
1066 by (auto simp: open_contains_ball) |
1095 by (auto simp: open_contains_ball) |
1067 then have contfb: "continuous_on (ball z d) f" |
1096 then have contfb: "continuous_on (ball z d) f" |
1068 using contf continuous_on_subset by blast |
1097 using contf continuous_on_subset by blast |
1069 obtain h where "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within ball z d)" |
1098 obtain h where "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within ball z d)" |
1070 by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD) |
1099 by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD) |
1071 then have "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within s)" |
1100 then have "\<forall>y\<in>ball z d. (h has_field_derivative f y) (at y within S)" |
1072 by (metis open_ball at_within_open d os subsetCE) |
1101 by (metis open_ball at_within_open d os subsetCE) |
1073 then have "\<exists>h. (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
1102 then have "\<exists>h. (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within S))" |
1074 by (force simp: dist_norm norm_minus_commute) |
1103 by (force simp: dist_norm norm_minus_commute) |
1075 then have "\<exists>d h. 0 < d \<and> (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within s))" |
1104 then have "\<exists>d h. 0 < d \<and> (\<forall>y. cmod (y - z) < d \<longrightarrow> (h has_field_derivative f y) (at y within S))" |
1076 using \<open>0 < d\<close> by blast |
1105 using \<open>0 < d\<close> by blast |
1077 } |
1106 } |
1078 then show ?thesis |
1107 then show ?thesis |
1079 by (rule contour_integral_local_primitive [OF g]) |
1108 by (rule contour_integral_local_primitive [OF g]) |
1080 qed |
1109 qed |
1082 lemma contour_integrable_holomorphic_simple: |
1111 lemma contour_integrable_holomorphic_simple: |
1083 assumes fh: "f holomorphic_on S" |
1112 assumes fh: "f holomorphic_on S" |
1084 and os: "open S" |
1113 and os: "open S" |
1085 and g: "valid_path g" "path_image g \<subseteq> S" |
1114 and g: "valid_path g" "path_image g \<subseteq> S" |
1086 shows "f contour_integrable_on g" |
1115 shows "f contour_integrable_on g" |
1087 apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g]) |
1116 proof - |
1088 apply (simp add: fh holomorphic_on_imp_continuous_on) |
1117 have "\<And>x. x \<in> S \<Longrightarrow> f field_differentiable at x" |
1089 using fh by (simp add: field_differentiable_def holomorphic_on_open os) |
1118 using fh holomorphic_on_imp_differentiable_at os by blast |
|
1119 moreover have "continuous_on S f" |
|
1120 by (simp add: fh holomorphic_on_imp_continuous_on) |
|
1121 ultimately show ?thesis |
|
1122 by (metis Diff_empty contour_integrable_holomorphic finite.emptyI g os) |
|
1123 qed |
1090 |
1124 |
1091 lemma continuous_on_inversediff: |
1125 lemma continuous_on_inversediff: |
1092 fixes z:: "'a::real_normed_field" shows "z \<notin> S \<Longrightarrow> continuous_on S (\<lambda>w. 1 / (w - z))" |
1126 fixes z:: "'a::real_normed_field" shows "z \<notin> S \<Longrightarrow> continuous_on S (\<lambda>w. 1 / (w - z))" |
1093 by (rule continuous_intros | force)+ |
1127 by (rule continuous_intros | force)+ |
1094 |
1128 |
1095 lemma contour_integrable_inversediff: |
1129 lemma contour_integrable_inversediff: |
1096 "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) contour_integrable_on g" |
1130 assumes g: "valid_path g" |
1097 apply (rule contour_integrable_holomorphic_simple [of _ "UNIV-{z}"]) |
1131 and notin: "z \<notin> path_image g" |
1098 apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros) |
1132 shows "(\<lambda>w. 1 / (w-z)) contour_integrable_on g" |
1099 done |
1133 proof (rule contour_integrable_holomorphic_simple) |
|
1134 show "(\<lambda>w. 1 / (w-z)) holomorphic_on UNIV - {z}" |
|
1135 by (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros) |
|
1136 qed (use assms in auto) |
1100 |
1137 |
1101 text\<open>Key fact that path integral is the same for a "nearby" path. This is the |
1138 text\<open>Key fact that path integral is the same for a "nearby" path. This is the |
1102 main lemma for the homotopy form of Cauchy's theorem and is also useful |
1139 main lemma for the homotopy form of Cauchy's theorem and is also useful |
1103 if we want "without loss of generality" to assume some nice properties of a |
1140 if we want "without loss of generality" to assume some nice properties of a |
1104 path (e.g. smoothness). It can also be used to define the integrals of |
1141 path (e.g. smoothness). It can also be used to define the integrals of |
1233 show "\<bar>real n / real N - x\<bar> < d" |
1269 show "\<bar>real n / real N - x\<bar> < d" |
1234 using x N by (auto simp: field_simps) |
1270 using x N by (auto simp: field_simps) |
1235 qed (use x01 Suc.prems in auto) |
1271 qed (use x01 Suc.prems in auto) |
1236 then have ptx: "cmod (p t - p x) < 2*ee (p t)/3" |
1272 then have ptx: "cmod (p t - p x) < 2*ee (p t)/3" |
1237 using e3le eepi [OF t] by simp |
1273 using e3le eepi [OF t] by simp |
1238 have "cmod (p t - g x) < 2*ee (p t)/3 + e/3 " |
1274 have "cmod (p t - g x) < 2*ee (p t)/3 + e/3" |
1239 apply (rule norm_diff_triangle_less [OF ptx]) |
1275 using ghp x01 |
1240 using ghp x01 by (simp add: norm_minus_commute) |
1276 by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx]) |
1241 also have "\<dots> \<le> ee (p t)" |
1277 also have "\<dots> \<le> ee (p t)" |
1242 using e3le eepi [OF t] by simp |
1278 using e3le eepi [OF t] by simp |
1243 finally have gg: "cmod (p t - g x) < ee (p t)" . |
1279 finally have gg: "cmod (p t - g x) < ee (p t)" . |
1244 have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 " |
1280 have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 " |
1245 apply (rule norm_diff_triangle_less [OF ptx]) |
1281 using ghp x01 |
1246 using ghp x01 by (simp add: norm_minus_commute) |
1282 by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx]) |
1247 also have "\<dots> \<le> ee (p t)" |
1283 also have "\<dots> \<le> ee (p t)" |
1248 using e3le eepi [OF t] by simp |
1284 using e3le eepi [OF t] by simp |
1249 finally have "cmod (p t - g x) < ee (p t)" |
1285 finally have "cmod (p t - g x) < ee (p t)" "cmod (p t - h x) < ee (p t)" |
1250 "cmod (p t - h x) < ee (p t)" |
|
1251 using gg by auto |
1286 using gg by auto |
1252 } note ptgh_ee = this |
1287 } note ptgh_ee = this |
1253 have "closed_segment (g (real n / real N)) (h (real n / real N)) = path_image (linepath (h (n/N)) (g (n/N)))" |
1288 have "closed_segment (g (n/N)) (h (n/N)) = path_image (linepath (h (n/N)) (g (n/N)))" |
1254 by (simp add: closed_segment_commute) |
1289 by (simp add: closed_segment_commute) |
1255 also have pi_hgn: "\<dots> \<subseteq> ball (p t) (ee (p t))" |
1290 also have pi_hgn: "\<dots> \<subseteq> ball (p t) (ee (p t))" |
1256 using ptgh_ee [of "n/N"] Suc.prems |
1291 using ptgh_ee [of "n/N"] Suc.prems |
1257 by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) |
1292 by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) |
1258 finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \<subseteq> S" |
1293 finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \<subseteq> S" |
1265 by (auto simp: Path_Connected.path_image_join field_simps) |
1300 by (auto simp: Path_Connected.path_image_join field_simps) |
1266 have pi_subset_ball: |
1301 have pi_subset_ball: |
1267 "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++ |
1302 "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++ |
1268 subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N))) |
1303 subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N))) |
1269 \<subseteq> ball (p t) (ee (p t))" |
1304 \<subseteq> ball (p t) (ee (p t))" |
1270 apply (intro subset_path_image_join pi_hgn pi_ghn') |
1305 proof (intro subset_path_image_join pi_hgn pi_ghn') |
1271 using \<open>N>0\<close> Suc.prems |
1306 show "path_image (subpath (n/N) ((1+n) / N) g) \<subseteq> ball (p t) (ee (p t))" |
1272 apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee) |
1307 "path_image (subpath ((1+n) / N) (n/N) h) \<subseteq> ball (p t) (ee (p t))" |
1273 done |
1308 using \<open>N>0\<close> Suc.prems |
|
1309 by (auto simp: path_image_subpath dist_norm field_simps ptgh_ee) |
|
1310 qed |
1274 have pi0: "(f has_contour_integral 0) |
1311 have pi0: "(f has_contour_integral 0) |
1275 (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ |
1312 (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ |
1276 subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" |
1313 subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" |
1277 apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"]) |
1314 proof (rule Cauchy_theorem_primitive) |
1278 apply (metis ff open_ball at_within_open pi t) |
1315 show "\<And>x. x \<in> ball (p t) (ee (p t)) |
1279 using Suc.prems pi_subset_ball apply (simp_all add: valid_path_join valid_path_subpath g h) |
1316 \<Longrightarrow> (ff (p t) has_field_derivative f x) (at x within ball (p t) (ee (p t)))" |
1280 done |
1317 by (metis ff open_ball at_within_open pi t) |
1281 have fpa1: "f contour_integrable_on subpath (real n / real N) (real (Suc n) / real N) g" |
1318 qed (use Suc.prems pi_subset_ball in \<open>simp_all add: valid_path_subpath g h\<close>) |
|
1319 have fpa1: "f contour_integrable_on subpath (n/N) (real (Suc n) / real N) g" |
1282 using Suc.prems by (simp add: contour_integrable_subpath g fpa) |
1320 using Suc.prems by (simp add: contour_integrable_subpath g fpa) |
1283 have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))" |
1321 have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))" |
1284 using gh_n's |
1322 using gh_n's |
1285 by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) |
1323 by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) |
1286 have fpa3: "f contour_integrable_on linepath (h (real n / real N)) (g (real n / real N))" |
1324 have fpa3: "f contour_integrable_on linepath (h (n/N)) (g (n/N))" |
1287 using gh_ns |
1325 using gh_ns |
1288 by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) |
1326 by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) |
1289 have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f + |
1327 have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f + |
1290 contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f + |
1328 contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f + |
1291 contour_integral (subpath ((Suc n) / N) (n/N) h) f + |
1329 contour_integral (subpath ((Suc n) / N) (n/N) h) f + |
1385 show "cmod (vector_derivative p (at x)) \<le> L" |
1425 show "cmod (vector_derivative p (at x)) \<le> L" |
1386 by (metis nop' p'(2) that vector_derivative_at) |
1426 by (metis nop' p'(2) that vector_derivative_at) |
1387 show "cmod (f (p x)) \<le> B" |
1427 show "cmod (f (p x)) \<le> B" |
1388 by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that) |
1428 by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that) |
1389 qed (use \<open>L>0\<close> in auto) |
1429 qed (use \<open>L>0\<close> in auto) |
1390 ultimately have "cmod (contour_integral g f) \<le> L * B" |
1430 ultimately |
1391 apply (simp only: pi [OF f]) |
1431 have "cmod (integral {0..1} (\<lambda>x. f (p x) * vector_derivative p (at x))) \<le> L * B" |
1392 apply (simp only: contour_integral_integral) |
1432 by (intro order_trans [OF integral_norm_bound_integral]) |
1393 apply (rule order_trans [OF integral_norm_bound_integral]) |
1433 (auto simp: mult.commute norm_mult contour_integrable_on) |
1394 apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult) |
1434 then have "cmod (contour_integral g f) \<le> L * B" |
1395 done |
1435 using contour_integral_integral f pi by presburger |
1396 } then |
1436 } then |
1397 show ?thesis using \<open>L > 0\<close> |
1437 show ?thesis using \<open>L > 0\<close> |
1398 by (intro exI[of _ L]) auto |
1438 by (intro exI[of _ L]) auto |
1399 qed |
1439 qed |
1400 |
1440 |
1401 |
1441 |
1402 subsection\<open>Homotopy forms of Cauchy's theorem\<close> |
1442 subsection\<open>Homotopy forms of Cauchy's theorem\<close> |
1403 |
1443 |
1404 lemma Cauchy_theorem_homotopic: |
1444 lemma Cauchy_theorem_homotopic: |
1405 assumes hom: "if atends then homotopic_paths s g h else homotopic_loops s g h" |
1445 assumes hom: "if atends then homotopic_paths S g h else homotopic_loops S g h" |
1406 and "open s" and f: "f holomorphic_on s" |
1446 and "open S" and f: "f holomorphic_on S" |
1407 and vpg: "valid_path g" and vph: "valid_path h" |
1447 and vpg: "valid_path g" and vph: "valid_path h" |
1408 shows "contour_integral g f = contour_integral h f" |
1448 shows "contour_integral g f = contour_integral h f" |
1409 proof - |
1449 proof - |
1410 have pathsf: "linked_paths atends g h" |
1450 have pathsf: "linked_paths atends g h" |
1411 using hom by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop) |
1451 using hom by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop) |
1412 obtain k :: "real \<times> real \<Rightarrow> complex" |
1452 obtain k :: "real \<times> real \<Rightarrow> complex" |
1413 where contk: "continuous_on ({0..1} \<times> {0..1}) k" |
1453 where contk: "continuous_on ({0..1} \<times> {0..1}) k" |
1414 and ks: "k ` ({0..1} \<times> {0..1}) \<subseteq> s" |
1454 and ks: "k ` ({0..1} \<times> {0..1}) \<subseteq> S" |
1415 and k [simp]: "\<forall>x. k (0, x) = g x" "\<forall>x. k (1, x) = h x" |
1455 and k [simp]: "\<forall>x. k (0, x) = g x" "\<forall>x. k (1, x) = h x" |
1416 and ksf: "\<forall>t\<in>{0..1}. linked_paths atends g (\<lambda>x. k (t, x))" |
1456 and ksf: "\<forall>t\<in>{0..1}. linked_paths atends g (\<lambda>x. k (t, x))" |
1417 using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: if_split_asm) |
1457 using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: if_split_asm) |
1418 have ucontk: "uniformly_continuous_on ({0..1} \<times> {0..1}) k" |
1458 have ucontk: "uniformly_continuous_on ({0..1} \<times> {0..1}) k" |
1419 by (blast intro: compact_Times compact_uniformly_continuous [OF contk]) |
1459 by (blast intro: compact_Times compact_uniformly_continuous [OF contk]) |
1420 { fix t::real assume t: "t \<in> {0..1}" |
1460 { fix t::real assume t: "t \<in> {0..1}" |
1421 have pak: "path (k \<circ> (\<lambda>u. (t, u)))" |
1461 have "Pair t ` {0..1} \<subseteq> {0..1} \<times> {0..1}" |
|
1462 using t by force |
|
1463 then have pak: "path (k \<circ> (\<lambda>u. (t, u)))" |
1422 unfolding path_def |
1464 unfolding path_def |
1423 apply (rule continuous_intros continuous_on_subset [OF contk])+ |
1465 by (intro continuous_intros continuous_on_subset [OF contk])+ |
1424 using t by force |
1466 have pik: "path_image (k \<circ> Pair t) \<subseteq> S" |
1425 have pik: "path_image (k \<circ> Pair t) \<subseteq> s" |
|
1426 using ks t by (auto simp: path_image_def) |
1467 using ks t by (auto simp: path_image_def) |
1427 obtain e where "e>0" and e: |
1468 obtain e where "e>0" and e: |
1428 "\<And>g h. \<lbrakk>valid_path g; valid_path h; |
1469 "\<And>g h. \<lbrakk>valid_path g; valid_path h; |
1429 \<forall>u\<in>{0..1}. cmod (g u - (k \<circ> Pair t) u) < e \<and> cmod (h u - (k \<circ> Pair t) u) < e; |
1470 \<forall>u\<in>{0..1}. cmod (g u - (k \<circ> Pair t) u) < e \<and> cmod (h u - (k \<circ> Pair t) u) < e; |
1430 linked_paths atends g h\<rbrakk> |
1471 linked_paths atends g h\<rbrakk> |
1431 \<Longrightarrow> contour_integral h f = contour_integral g f" |
1472 \<Longrightarrow> contour_integral h f = contour_integral g f" |
1432 using contour_integral_nearby [OF \<open>open s\<close> pak pik, of atends] f by metis |
1473 using contour_integral_nearby [OF \<open>open S\<close> pak pik, of atends] f by metis |
1433 obtain d where "d>0" and d: |
1474 obtain d where "d>0" and d: |
1434 "\<And>x x'. \<lbrakk>x \<in> {0..1} \<times> {0..1}; x' \<in> {0..1} \<times> {0..1}; norm (x'-x) < d\<rbrakk> \<Longrightarrow> norm (k x' - k x) < e/4" |
1475 "\<And>x x'. \<lbrakk>x \<in> {0..1} \<times> {0..1}; x' \<in> {0..1} \<times> {0..1}; norm (x'-x) < d\<rbrakk> \<Longrightarrow> norm (k x' - k x) < e/4" |
1435 by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm \<open>e>0\<close>) |
1476 by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm \<open>e>0\<close>) |
1436 { fix t1 t2 |
1477 { fix t1 t2 |
1437 assume t1: "0 \<le> t1" "t1 \<le> 1" and t2: "0 \<le> t2" "t2 \<le> 1" and ltd: "\<bar>t1 - t\<bar> < d" "\<bar>t2 - t\<bar> < d" |
1478 assume t1: "0 \<le> t1" "t1 \<le> 1" and t2: "0 \<le> t2" "t2 \<le> 1" and ltd: "\<bar>t1 - t\<bar> < d" "\<bar>t2 - t\<bar> < d" |
1438 have no2: "\<And>g1 k1 kt. \<lbrakk>norm(g1 - k1) < e/4; norm(k1 - kt) < e/4\<rbrakk> \<Longrightarrow> norm(g1 - kt) < e" |
1479 have no2: "norm(g1 - kt) < e" if "norm(g1 - k1) < e/4" "norm(k1 - kt) < e/4" for g1 k1 kt :: complex |
1439 using \<open>e > 0\<close> |
1480 proof (rule norm_triangle_half_l) |
1440 apply (rule_tac y = k1 in norm_triangle_half_l) |
1481 show "cmod (g1 - k1) < e/2" "cmod (kt - k1) < e/2" |
1441 apply (auto simp: norm_minus_commute intro: order_less_trans) |
1482 using \<open>e > 0\<close> that by (auto simp: norm_minus_commute intro: order_less_trans) |
1442 done |
1483 qed |
1443 have "\<exists>d>0. \<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and> |
1484 have "\<exists>d>0. \<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and> |
1444 (\<forall>u\<in>{0..1}. cmod (g1 u - k (t1, u)) < d \<and> cmod (g2 u - k (t2, u)) < d) \<and> |
1485 (\<forall>u\<in>{0..1}. cmod (g1 u - k (t1, u)) < d \<and> cmod (g2 u - k (t2, u)) < d) \<and> |
1445 linked_paths atends g1 g2 \<longrightarrow> |
1486 linked_paths atends g1 g2 \<longrightarrow> |
1446 contour_integral g2 f = contour_integral g1 f" |
1487 contour_integral g2 f = contour_integral g1 f" |
1447 apply (rule_tac x="e/4" in exI) |
|
1448 using t t1 t2 ltd \<open>e > 0\<close> |
1488 using t t1 t2 ltd \<open>e > 0\<close> |
1449 apply (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1) |
1489 by (rule_tac x="e/4" in exI) (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1) |
1450 done |
|
1451 } |
1490 } |
1452 then have "\<exists>e. 0 < e \<and> |
1491 then have "\<exists>e. 0 < e \<and> |
1453 (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> \<bar>t1 - t\<bar> < e \<and> \<bar>t2 - t\<bar> < e |
1492 (\<forall>t1 t2. t1 \<in> {0..1} \<and> t2 \<in> {0..1} \<and> \<bar>t1 - t\<bar> < e \<and> \<bar>t2 - t\<bar> < e |
1454 \<longrightarrow> (\<exists>d. 0 < d \<and> |
1493 \<longrightarrow> (\<exists>d. 0 < d \<and> |
1455 (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and> |
1494 (\<forall>g1 g2. valid_path g1 \<and> valid_path g2 \<and> |
1562 then show ?thesis |
1601 then show ?thesis |
1563 by (simp add: pathsf) |
1602 by (simp add: pathsf) |
1564 qed |
1603 qed |
1565 |
1604 |
1566 proposition Cauchy_theorem_homotopic_paths: |
1605 proposition Cauchy_theorem_homotopic_paths: |
1567 assumes hom: "homotopic_paths s g h" |
1606 assumes hom: "homotopic_paths S g h" |
1568 and "open s" and f: "f holomorphic_on s" |
1607 and "open S" and f: "f holomorphic_on S" |
1569 and vpg: "valid_path g" and vph: "valid_path h" |
1608 and vpg: "valid_path g" and vph: "valid_path h" |
1570 shows "contour_integral g f = contour_integral h f" |
1609 shows "contour_integral g f = contour_integral h f" |
1571 using Cauchy_theorem_homotopic [of True s g h] assms by simp |
1610 using Cauchy_theorem_homotopic [of True S g h] assms by simp |
1572 |
1611 |
1573 proposition Cauchy_theorem_homotopic_loops: |
1612 proposition Cauchy_theorem_homotopic_loops: |
1574 assumes hom: "homotopic_loops s g h" |
1613 assumes hom: "homotopic_loops S g h" |
1575 and "open s" and f: "f holomorphic_on s" |
1614 and "open S" and f: "f holomorphic_on S" |
1576 and vpg: "valid_path g" and vph: "valid_path h" |
1615 and vpg: "valid_path g" and vph: "valid_path h" |
1577 shows "contour_integral g f = contour_integral h f" |
1616 shows "contour_integral g f = contour_integral h f" |
1578 using Cauchy_theorem_homotopic [of False s g h] assms by simp |
1617 using Cauchy_theorem_homotopic [of False S g h] assms by simp |
1579 |
1618 |
1580 lemma has_contour_integral_newpath: |
1619 lemma has_contour_integral_newpath: |
1581 "\<lbrakk>(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f\<rbrakk> |
1620 "\<lbrakk>(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f\<rbrakk> |
1582 \<Longrightarrow> (f has_contour_integral y) g" |
1621 \<Longrightarrow> (f has_contour_integral y) g" |
1583 using has_contour_integral_integral contour_integral_unique by auto |
1622 using has_contour_integral_integral contour_integral_unique by auto |
1584 |
1623 |
1585 lemma Cauchy_theorem_null_homotopic: |
1624 lemma Cauchy_theorem_null_homotopic: |
1586 "\<lbrakk>f holomorphic_on s; open s; valid_path g; homotopic_loops s g (linepath a a)\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g" |
1625 "\<lbrakk>f holomorphic_on S; open S; valid_path g; homotopic_loops S g (linepath a a)\<rbrakk> |
1587 apply (rule has_contour_integral_newpath [where h = "linepath a a"], simp) |
1626 \<Longrightarrow> (f has_contour_integral 0) g" |
1588 using contour_integrable_holomorphic_simple |
1627 by (metis Cauchy_theorem_homotopic_loops contour_integrable_holomorphic_simple valid_path_linepath |
1589 apply (blast dest: holomorphic_on_imp_continuous_on homotopic_loops_imp_subset) |
1628 contour_integral_trivial has_contour_integral_integral homotopic_loops_imp_subset) |
1590 by (simp add: Cauchy_theorem_homotopic_loops) |
|
1591 |
1629 |
1592 end |
1630 end |