diff --git a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy --- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy +++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy @@ -1,1592 +1,1630 @@ section \Complex Path Integrals and Cauchy's Integral Theorem\ text\By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\ theory Cauchy_Integral_Theorem imports "HOL-Analysis.Analysis" Contour_Integration begin lemma leibniz_rule_holomorphic: fixes f::"complex \ 'b::euclidean_space \ complex" assumes "\x t. x \ U \ t \ cbox a b \ ((\x. f x t) has_field_derivative fx x t) (at x within U)" assumes "\x. x \ U \ (f x) integrable_on cbox a b" assumes "continuous_on (U \ (cbox a b)) (\(x, t). fx x t)" assumes "convex U" shows "(\x. integral (cbox a b) (f x)) holomorphic_on U" using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)] by (auto simp: holomorphic_on_def) lemma Ln_measurable [measurable]: "Ln \ measurable borel borel" proof - have *: "Ln (-of_real x) = of_real (ln x) + \ * pi" if "x > 0" for x using that by (subst Ln_minus) (auto simp: Ln_of_real) have **: "Ln (of_real x) = of_real (ln (-x)) + \ * pi" if "x < 0" for x using *[of "-x"] that by simp have cont: "(\x. indicat_real (- \\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel_measurable borel" by (intro borel_measurable_continuous_on_indicator continuous_intros) auto have "(\x. if x \ \\<^sub>\\<^sub>0 then ln (-Re x) + \ * pi else indicator (-\\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel \\<^sub>M borel" (is "?f \ _") by (rule measurable_If_set[OF _ cont]) auto hence "(\x. if x = 0 then Ln 0 else ?f x) \ borel \\<^sub>M borel" by measurable also have "(\x. if x = 0 then Ln 0 else ?f x) = Ln" by (auto simp: fun_eq_iff ** nonpos_Reals_def) finally show ?thesis . qed lemma powr_complex_measurable [measurable]: assumes [measurable]: "f \ measurable M borel" "g \ measurable M borel" shows "(\x. f x powr g x :: complex) \ measurable M borel" using assms by (simp add: powr_def) text\The special case of midpoints used in the main quadrisection\ lemma has_contour_integral_midpoint: assumes "(f has_contour_integral i) (linepath a (midpoint a b))" "(f has_contour_integral j) (linepath (midpoint a b) b)" shows "(f has_contour_integral (i + j)) (linepath a b)" - apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"]) - using assms - apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) - done +proof (rule has_contour_integral_split) + show "midpoint a b - a = (1/2) *\<^sub>R (b - a)" + using assms by (auto simp: midpoint_def scaleR_conv_of_real) +qed (use assms in auto) lemma contour_integral_midpoint: - "continuous_on (closed_segment a b) f - \ contour_integral (linepath a b) f = - contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" - apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"]) - apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real) - done + assumes "continuous_on (closed_segment a b) f" + shows "contour_integral (linepath a b) f = + contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f" +proof (rule contour_integral_split) + show "midpoint a b - a = (1/2) *\<^sub>R (b - a)" + using assms by (auto simp: midpoint_def scaleR_conv_of_real) +qed (use assms in auto) text\A couple of special case lemmas that are useful below\ lemma triangle_linear_has_chain_integral: "((\x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" - apply (rule Cauchy_theorem_primitive [of UNIV "\x. m/2 * x^2 + d*x"]) - apply (auto intro!: derivative_eq_intros) - done +proof (rule Cauchy_theorem_primitive) + show "\x. x \ UNIV \ ((\x. m / 2 * x\<^sup>2 + d * x) has_field_derivative m * x + d) (at x)" + by (auto intro!: derivative_eq_intros) +qed auto lemma has_chain_integral_chain_integral3: - "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d) - \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" - apply (subst contour_integral_unique [symmetric], assumption) - apply (drule has_contour_integral_integrable) - apply (simp add: valid_path_join) - done + assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d)" + (is "(f has_contour_integral i) ?g") + shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i" + (is "?lhs = _") +proof - + have "f contour_integrable_on ?g" + using assms contour_integrable_on_def by blast + then have "?lhs = contour_integral ?g f" + by (simp add: valid_path_join has_contour_integral_integrable) + then show ?thesis + using assms contour_integral_unique by blast +qed lemma has_chain_integral_chain_integral4: - "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e) - \ 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" - apply (subst contour_integral_unique [symmetric], assumption) - apply (drule has_contour_integral_integrable) - apply (simp add: valid_path_join) - done + assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e)" + (is "(f has_contour_integral i) ?g") + 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" + (is "?lhs = _") +proof - + have "f contour_integrable_on ?g" + using assms contour_integrable_on_def by blast + then have "?lhs = contour_integral ?g f" + by (simp add: valid_path_join has_contour_integral_integrable) + then show ?thesis + using assms contour_integral_unique by blast +qed subsection\<^marker>\tag unimportant\ \The key quadrisection step\ lemma norm_sum_half: assumes "norm(a + b) \ e" shows "norm a \ e/2 \ norm b \ e/2" proof - have "e \ norm (- a - b)" by (simp add: add.commute assms norm_minus_commute) thus ?thesis using norm_triangle_ineq4 order_trans by fastforce qed lemma norm_sum_lemma: assumes "e \ norm (a + b + c + d)" shows "e / 4 \ norm a \ e / 4 \ norm b \ e / 4 \ norm c \ e / 4 \ norm d" proof - have "e \ norm ((a + b) + (c + d))" using assms by (simp add: algebra_simps) then show ?thesis by (auto dest!: norm_sum_half) qed lemma Cauchy_theorem_quadrisection: assumes f: "continuous_on (convex hull {a,b,c}) f" and dist: "dist a b \ K" "dist b c \ K" "dist c a \ K" and e: "e * K^2 \ norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)" shows "\a' b' c'. a' \ convex hull {a,b,c} \ b' \ convex hull {a,b,c} \ c' \ convex hull {a,b,c} \ dist a' b' \ K/2 \ dist b' c' \ K/2 \ dist c' a' \ K/2 \ e * (K/2)^2 \ norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)" (is "\x y z. ?\ x y z") proof - note divide_le_eq_numeral1 [simp del] define a' where "a' = midpoint b c" define b' where "b' = midpoint c a" define c' where "c' = midpoint a b" have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using f continuous_on_subset segments_subset_convex_hull by metis+ have fcont': "continuous_on (closed_segment c' b') f" "continuous_on (closed_segment a' c') f" "continuous_on (closed_segment b' a') f" unfolding a'_def b'_def c'_def by (rule continuous_on_subset [OF f], metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+ - let ?pathint = "\x y. contour_integral(linepath x y) f" - have *: "?pathint a b + ?pathint b c + ?pathint c a = - (?pathint a c' + ?pathint c' b' + ?pathint b' a) + - (?pathint a' c' + ?pathint c' b + ?pathint b a') + - (?pathint a' c + ?pathint c b' + ?pathint b' a') + - (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" + define pathint where "pathint x y \ contour_integral(linepath x y) f" for x y + have *: "pathint a b + pathint b c + pathint c a = + (pathint a c' + pathint c' b' + pathint b' a) + + (pathint a' c' + pathint c' b + pathint b a') + + (pathint a' c + pathint c b' + pathint b' a') + + (pathint a' b' + pathint b' c' + pathint c' a')" + unfolding pathint_def by (simp add: fcont' contour_integral_reverse_linepath) (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc) have [simp]: "\x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2" by (metis left_diff_distrib mult.commute norm_mult_numeral1) have [simp]: "\x y. cmod (x - y) = cmod (y - x)" by (simp add: norm_minus_commute) - consider "e * K\<^sup>2 / 4 \ cmod (?pathint a c' + ?pathint c' b' + ?pathint b' a)" | - "e * K\<^sup>2 / 4 \ cmod (?pathint a' c' + ?pathint c' b + ?pathint b a')" | - "e * K\<^sup>2 / 4 \ cmod (?pathint a' c + ?pathint c b' + ?pathint b' a')" | - "e * K\<^sup>2 / 4 \ cmod (?pathint a' b' + ?pathint b' c' + ?pathint c' a')" - using assms unfolding * by (blast intro: that dest!: norm_sum_lemma) + consider "e * K\<^sup>2 / 4 \ cmod (pathint a c' + pathint c' b' + pathint b' a)" | + "e * K\<^sup>2 / 4 \ cmod (pathint a' c' + pathint c' b + pathint b a')" | + "e * K\<^sup>2 / 4 \ cmod (pathint a' c + pathint c b' + pathint b' a')" | + "e * K\<^sup>2 / 4 \ cmod (pathint a' b' + pathint b' c' + pathint c' a')" + using assms by (metis "*" norm_sum_lemma pathint_def) then show ?thesis proof cases case 1 then have "?\ a c' b'" - using assms + using assms unfolding pathint_def [symmetric] apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 2 then have "?\ a' c' b" - using assms + using assms unfolding pathint_def [symmetric] apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 3 then have "?\ a' c b'" - using assms + using assms unfolding pathint_def [symmetric] apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast next case 4 then have "?\ a' b' c'" - using assms + using assms unfolding pathint_def [symmetric] apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD]) apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps) done then show ?thesis by blast qed qed subsection\<^marker>\tag unimportant\ \Cauchy's theorem for triangles\ lemma triangle_points_closer: fixes a::complex shows "\x \ convex hull {a,b,c}; y \ convex hull {a,b,c}\ \ norm(x - y) \ norm(a - b) \ norm(x - y) \ norm(b - c) \ norm(x - y) \ norm(c - a)" using simplex_extremal_le [of "{a,b,c}"] by (auto simp: norm_minus_commute) + lemma holomorphic_point_small_triangle: assumes x: "x \ S" and f: "continuous_on S f" and cd: "f field_differentiable (at x within S)" and e: "0 < e" shows "\k>0. \a b c. dist a b \ k \ dist b c \ k \ dist c a \ k \ x \ convex hull {a,b,c} \ convex hull {a,b,c} \ S \ norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f) \ e*(dist a b + dist b c + dist c a)^2" (is "\k>0. \a b c. _ \ ?normle a b c") proof - have le_of_3: "\a x y z. \0 \ x*y; 0 \ x*z; 0 \ y*z; a \ (e*(x + y + z))*x + (e*(x + y + z))*y + (e*(x + y + z))*z\ \ a \ e*(x + y + z)^2" by (simp add: algebra_simps power2_eq_square) have disj_le: "\x \ a \ x \ b \ x \ c; 0 \ a; 0 \ b; 0 \ c\ \ x \ a + b + c" for x::real and a b c by linarith have fabc: "f contour_integrable_on linepath a b" "f contour_integrable_on linepath b c" "f contour_integrable_on linepath c a" if "convex hull {a, b, c} \ S" for a b c using segments_subset_convex_hull that by (metis continuous_on_subset f contour_integrable_continuous_linepath)+ note path_bound = has_contour_integral_bound_linepath [simplified norm_minus_commute, OF has_contour_integral_integral] { fix f' a b c d assume d: "0 < d" and f': "\y. \cmod (y - x) \ d; y \ S\ \ cmod (f y - f x - f' * (y - x)) \ e * cmod (y - x)" and le: "cmod (a - b) \ d" "cmod (b - c) \ d" "cmod (c - a) \ d" and xc: "x \ convex hull {a, b, c}" and S: "convex hull {a, b, c} \ S" have pa: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = - contour_integral (linepath a b) (\y. f y - f x - f'*(y - x)) + - contour_integral (linepath b c) (\y. f y - f x - f'*(y - x)) + - contour_integral (linepath c a) (\y. f y - f x - f'*(y - x))" + contour_integral (linepath a b) (\y. f y - f x - f' * (y-x)) + + contour_integral (linepath b c) (\y. f y - f x - f' * (y-x)) + + contour_integral (linepath c a) (\y. f y - f x - f' * (y-x))" apply (simp add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc [OF S]) apply (simp add: field_simps) done { fix y assume yc: "y \ convex hull {a,b,c}" have "cmod (f y - f x - f' * (y - x)) \ e*norm(y - x)" proof (rule f') show "cmod (y - x) \ d" by (metis triangle_points_closer [OF xc yc] le norm_minus_commute order_trans) qed (use S yc in blast) also have "\ \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" by (simp add: yc e xc disj_le [OF triangle_points_closer]) finally have "cmod (f y - f x - f' * (y - x)) \ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" . } note cm_le = this have "?normle a b c" unfolding dist_norm pa - apply (rule le_of_3) using f' xc S e - apply simp_all - apply (intro norm_triangle_le add_mono path_bound) + apply (intro le_of_3 norm_triangle_le add_mono path_bound) apply (simp_all add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc) apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+ done } note * = this show ?thesis using cd e apply (simp add: field_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def) apply (clarify dest!: spec mp) using * unfolding dist_norm apply blast done qed text\Hence the most basic theorem for a triangle.\ locale Chain = fixes x0 At Follows assumes At0: "At x0 0" and AtSuc: "\x n. At x n \ \x'. At x' (Suc n) \ Follows x' x" begin primrec f where "f 0 = x0" | "f (Suc n) = (SOME x. At x (Suc n) \ Follows x (f n))" lemma At: "At (f n) n" proof (induct n) case 0 show ?case by (simp add: At0) next case (Suc n) show ?case by (metis (no_types, lifting) AtSuc [OF Suc] f.simps(2) someI_ex) qed lemma Follows: "Follows (f(Suc n)) (f n)" by (metis (no_types, lifting) AtSuc [OF At [of n]] f.simps(2) someI_ex) declare f.simps(2) [simp del] end lemma Chain3: assumes At0: "At x0 y0 z0 0" and AtSuc: "\x y z n. At x y z n \ \x' y' z'. At x' y' z' (Suc n) \ Follows x' y' z' x y z" obtains f g h where "f 0 = x0" "g 0 = y0" "h 0 = z0" "\n. At (f n) (g n) (h n) n" "\n. Follows (f(Suc n)) (g(Suc n)) (h(Suc n)) (f n) (g n) (h n)" proof - interpret three: Chain "(x0,y0,z0)" "\(x,y,z). At x y z" "\(x',y',z'). \(x,y,z). Follows x' y' z' x y z" - apply unfold_locales - using At0 AtSuc by auto + proof qed (use At0 AtSuc in auto) show ?thesis - apply (rule that [of "\n. fst (three.f n)" "\n. fst (snd (three.f n))" "\n. snd (snd (three.f n))"]) - using three.At three.Follows - apply simp_all - apply (simp_all add: split_beta') - done + proof + show "\n. Follows (fst (three.f (Suc n))) (fst (snd (three.f (Suc n)))) + (snd (snd (three.f (Suc n)))) (fst (three.f n)) + (fst (snd (three.f n))) (snd (snd (three.f n)))" + "\n. At (fst (three.f n)) (fst (snd (three.f n))) (snd (snd (three.f n))) n" + using three.At three.Follows + by (simp_all add: split_beta') + qed auto qed + proposition\<^marker>\tag unimportant\ Cauchy_theorem_triangle: assumes "f holomorphic_on (convex hull {a,b,c})" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof - have contf: "continuous_on (convex hull {a,b,c}) f" by (metis assms holomorphic_on_imp_continuous_on) let ?pathint = "\x y. contour_integral(linepath x y) f" { fix y::complex assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" define K where "K = 1 + max (dist a b) (max (dist b c) (dist c a))" define e where "e = norm y / K^2" have K1: "K \ 1" by (simp add: K_def max.coboundedI1) then have K: "K > 0" by linarith have [iff]: "dist a b \ K" "dist b c \ K" "dist c a \ K" by (simp_all add: K_def) have e: "e > 0" unfolding e_def using ynz K1 by simp define At where "At x y z n \ convex hull {x,y,z} \ convex hull {a,b,c} \ dist x y \ K/2^n \ dist y z \ K/2^n \ dist z x \ K/2^n \ norm(?pathint x y + ?pathint y z + ?pathint z x) \ e*(K/2^n)^2" for x y z n have At0: "At a b c 0" using fy by (simp add: At_def e_def has_chain_integral_chain_integral3) { fix x y z n assume At: "At x y z n" then have contf': "continuous_on (convex hull {x,y,z}) f" using contf At_def continuous_on_subset by metis have "\x' y' z'. At x' y' z' (Suc n) \ convex hull {x',y',z'} \ convex hull {x,y,z}" using At Cauchy_theorem_quadrisection [OF contf', of "K/2^n" e] apply (simp add: At_def algebra_simps) apply (meson convex_hull_subset empty_subsetI insert_subset subsetCE) done } note AtSuc = this obtain fa fb fc where f0 [simp]: "fa 0 = a" "fb 0 = b" "fc 0 = c" and cosb: "\n. convex hull {fa n, fb n, fc n} \ convex hull {a,b,c}" and dist: "\n. dist (fa n) (fb n) \ K/2^n" "\n. dist (fb n) (fc n) \ K/2^n" "\n. dist (fc n) (fa n) \ K/2^n" and no: "\n. norm(?pathint (fa n) (fb n) + ?pathint (fb n) (fc n) + ?pathint (fc n) (fa n)) \ e * (K/2^n)^2" and conv_le: "\n. convex hull {fa(Suc n), fb(Suc n), fc(Suc n)} \ convex hull {fa n, fb n, fc n}" - apply (rule Chain3 [of At, OF At0 AtSuc]) - apply (auto simp: At_def) - done + by (rule Chain3 [of At, OF At0 AtSuc]) (auto simp: At_def) obtain x where x: "\n. x \ convex hull {fa n, fb n, fc n}" proof (rule bounded_closed_nest) show "\n. closed (convex hull {fa n, fb n, fc n})" by (simp add: compact_imp_closed finite_imp_compact_convex_hull) show "\m n. m \ n \ convex hull {fa n, fb n, fc n} \ convex hull {fa m, fb m, fc m}" by (erule transitive_stepwise_le) (auto simp: conv_le) qed (fastforce intro: finite_imp_bounded_convex_hull)+ then have xin: "x \ convex hull {a,b,c}" using assms f0 by blast then have fx: "f field_differentiable at x within (convex hull {a,b,c})" using assms holomorphic_on_def by blast { fix k n assume k: "0 < k" and le: "\x' y' z'. \dist x' y' \ k; dist y' z' \ k; dist z' x' \ k; x \ convex hull {x',y',z'}; convex hull {x',y',z'} \ convex hull {a,b,c}\ \ cmod (?pathint x' y' + ?pathint y' z' + ?pathint z' x') * 10 \ e * (dist x' y' + dist y' z' + dist z' x')\<^sup>2" and Kk: "K / k < 2 ^ n" have "K / 2 ^ n < k" using Kk k by (auto simp: field_simps) then have DD: "dist (fa n) (fb n) \ k" "dist (fb n) (fc n) \ k" "dist (fc n) (fa n) \ k" using dist [of n] k by linarith+ have dle: "(dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))\<^sup>2 \ (3 * K / 2 ^ n)\<^sup>2" using dist [of n] e K by (simp add: abs_le_square_iff [symmetric]) have less10: "\x y::real. 0 < x \ y \ 9*x \ y < x*10" by linarith have "e * (dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))\<^sup>2 \ e * (3 * K / 2 ^ n)\<^sup>2" using ynz dle e mult_le_cancel_left_pos by blast also have "\ < cmod (?pathint (fa n) (fb n) + ?pathint (fb n) (fc n) + ?pathint (fc n) (fa n)) * 10" using no [of n] e K - apply (simp add: e_def field_simps) - apply (simp only: zero_less_norm_iff [symmetric]) - done + by (simp add: e_def field_simps) (simp only: zero_less_norm_iff [symmetric]) finally have False using le [OF DD x cosb] by auto } then have ?thesis using holomorphic_point_small_triangle [OF xin contf fx, of "e/10"] e apply clarsimp apply (rule_tac y1="K/k" in exE [OF real_arch_pow[of 2]], force+) done } moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" by simp (meson contf continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(1) segments_subset_convex_hull(3) segments_subset_convex_hull(5)) ultimately show ?thesis using has_contour_integral_integral by fastforce qed subsection\<^marker>\tag unimportant\ \Version needing function holomorphic in interior only\ lemma Cauchy_theorem_flat_lemma: assumes f: "continuous_on (convex hull {a,b,c}) f" and c: "c - a = k *\<^sub>R (b - a)" and k: "0 \ k" shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" proof - have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using f continuous_on_subset segments_subset_convex_hull by metis+ show ?thesis proof (cases "k \ 1") case True show ?thesis by (simp add: contour_integral_split [OF fabc(1) k True c] contour_integral_reverse_linepath fabc) next - case False then show ?thesis - using fabc c - apply (subst contour_integral_split [of a c f "1/k" b, symmetric]) - apply (metis closed_segment_commute fabc(3)) - apply (auto simp: k contour_integral_reverse_linepath) - done + case False + show ?thesis + proof (subst contour_integral_split [symmetric]) + show "b - a = (1/k) *\<^sub>R (c - a)" + using False c by force + show "contour_integral (linepath a c) f + contour_integral (linepath c a) f = 0" + by (simp add: contour_integral_reverse_linepath fabc(3)) + show "continuous_on (closed_segment a c) f" + by (metis closed_segment_commute fabc(3)) + qed (use False in auto) qed qed lemma Cauchy_theorem_flat: assumes f: "continuous_on (convex hull {a,b,c}) f" and c: "c - a = k *\<^sub>R (b - a)" shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" proof (cases "0 \ k") case True with assms show ?thesis by (blast intro: Cauchy_theorem_flat_lemma) next case False have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using f continuous_on_subset segments_subset_convex_hull by metis+ moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f + - contour_integral (linepath c b) f = 0" - apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) - using False c - apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps) - done + contour_integral (linepath c b) f = 0" + proof (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"]) + show "continuous_on (convex hull {b, a, c}) f" + by (simp add: f insert_commute) + show "c - b = (1 - k) *\<^sub>R (a - b)" + using c by (auto simp: algebra_simps) + qed (use False in auto) ultimately show ?thesis - apply (auto simp: contour_integral_reverse_linepath) - using add_eq_0_iff by force + by (metis (no_types, lifting) contour_integral_reverse_linepath eq_neg_iff_add_eq_0 minus_add_cancel) qed -lemma Cauchy_theorem_triangle_interior: + +proposition Cauchy_theorem_triangle_interior: assumes contf: "continuous_on (convex hull {a,b,c}) f" and holf: "f holomorphic_on interior (convex hull {a,b,c})" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof - + define pathint where "pathint \ \x y. contour_integral(linepath x y) f" have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f" using contf continuous_on_subset segments_subset_convex_hull by metis+ have "bounded (f ` (convex hull {a,b,c}))" by (simp add: compact_continuous_image compact_convex_hull compact_imp_bounded contf) then obtain B where "0 < B" and Bnf: "\x. x \ convex hull {a,b,c} \ norm (f x) \ B" by (auto simp: dest!: bounded_pos [THEN iffD1]) have "bounded (convex hull {a,b,c})" by (simp add: bounded_convex_hull) then obtain C where C: "0 < C" and Cno: "\y. y \ convex hull {a,b,c} \ norm y < C" using bounded_pos_less by blast then have diff_2C: "norm(x - y) \ 2*C" if x: "x \ convex hull {a, b, c}" and y: "y \ convex hull {a, b, c}" for x y proof - have "cmod x \ C" using x by (meson Cno not_le not_less_iff_gr_or_eq) hence "cmod (x - y) \ C + C" using y by (meson Cno add_mono_thms_linordered_field(4) less_eq_real_def norm_triangle_ineq4 order_trans) thus "cmod (x - y) \ 2 * C" by (metis mult_2) qed have contf': "continuous_on (convex hull {b,a,c}) f" using contf by (simp add: insert_commute) { fix y::complex assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" - have pi_eq_y: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = y" - by (rule has_chain_integral_chain_integral3 [OF fy]) + have pi_eq_y: "pathint a b + pathint b c + pathint c a= y" + unfolding pathint_def by (rule has_chain_integral_chain_integral3 [OF fy]) have ?thesis proof (cases "c=a \ a=b \ b=c") case True then show ?thesis using Cauchy_theorem_flat [OF contf, of 0] using has_chain_integral_chain_integral3 [OF fy] ynz by (force simp: fabc contour_integral_reverse_linepath) next case False then have car3: "card {a, b, c} = Suc (DIM(complex))" by auto { assume "interior(convex hull {a,b,c}) = {}" then have "collinear{a,b,c}" using interior_convex_hull_eq_empty [OF car3] by (simp add: collinear_3_eq_affine_dependent) with False obtain d where "c \ a" "a \ b" "b \ c" "c - b = d *\<^sub>R (a - b)" by (auto simp: collinear_3 collinear_lemma) then have "False" using False Cauchy_theorem_flat [OF contf'] pi_eq_y ynz - by (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath) + by (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath pathint_def) } then obtain d where d: "d \ interior (convex hull {a, b, c})" by blast { fix d1 assume d1_pos: "0 < d1" and d1: "\x x'. \x\convex hull {a, b, c}; x'\convex hull {a, b, c}; cmod (x' - x) < d1\ \ cmod (f x' - f x) < cmod y / (24 * C)" define e where "e = min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))" define shrink where "shrink x = x - e *\<^sub>R (x - d)" for x - let ?pathint = "\x y. contour_integral(linepath x y) f" have e: "0 < e" "e \ 1" "e \ d1 / (4 * C)" "e \ cmod y / 24 / C / B" using d1_pos \C>0\ \B>0\ ynz by (simp_all add: e_def) - then have eCB: "24 * e * C * B \ cmod y" - using \C>0\ \B>0\ by (simp add: field_simps) have e_le_d1: "e * (4 * C) \ d1" using e \C>0\ by (simp add: field_simps) have "shrink a \ interior(convex hull {a,b,c})" "shrink b \ interior(convex hull {a,b,c})" "shrink c \ interior(convex hull {a,b,c})" using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) then have fhp0: "(f has_contour_integral 0) (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))" by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal) - then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0" - by (simp add: has_chain_integral_chain_integral3) + then have f_0_shrink: "pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a) = 0" + by (simp add: has_chain_integral_chain_integral3 pathint_def) have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)" "f contour_integrable_on linepath (shrink b) (shrink c)" "f contour_integrable_on linepath (shrink c) (shrink a)" using fhp0 by (auto simp: valid_path_join dest: has_contour_integral_integrable) have cmod_shr: "\x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)" using e by (simp add: shrink_def real_vector.scale_right_diff_distrib [symmetric]) have sh_eq: "\a b d::complex. (b - e *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)" by (simp add: algebra_simps) have "cmod y / (24 * C) \ cmod y / cmod (b - a) / 12" using False \C>0\ diff_2C [of b a] ynz by (auto simp: field_split_simps hull_inc) - have less_C: "\u \ convex hull {a, b, c}; 0 \ x; x \ 1\ \ x * cmod u < C" for x u - apply (cases "x=0", simp add: \0) - using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast + have less_C: "x * cmod u < C" if "u \ convex hull {a,b,c}" "0 \ x" "x \ 1" for x u + proof (cases "x=0") + case False + with that show ?thesis + using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast + qed (simp add: \0) { fix u v assume uv: "u \ convex hull {a, b, c}" "v \ convex hull {a, b, c}" "u\v" and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)" have shr_uv: "shrink u \ interior(convex hull {a,b,c})" "shrink v \ interior(convex hull {a,b,c})" using d e uv by (auto simp: hull_inc mem_interior_convex_shrink shrink_def) have cmod_fuv: "\x. 0\x \ x\1 \ cmod (f (linepath (shrink u) (shrink v) x)) \ B" using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD]) - have By_uv: "B * (12 * (e * cmod (u - v))) \ cmod y" - apply (rule order_trans [OF _ eCB]) - using e \B>0\ diff_2C [of u v] uv - by (auto simp: field_simps) { fix x::real assume x: "0\x" "x\1" + have "\1 - x\ * cmod u < C" "\x\ * cmod v < C" + using uv x by (auto intro!: less_C) + moreover have "\x\ * cmod d < C" "\1 - x\ * cmod d < C" + using x d interior_subset by (auto intro!: less_C) + ultimately 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)" - apply (rule add_strict_mono; rule norm_triangle_half_l [of _ 0]) - using uv x d interior_subset - apply (auto simp: hull_inc intro!: less_C) - done + by (metis add_strict_mono le_less_trans norm_scaleR norm_triangle_ineq4) have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *\<^sub>R (u - d) + x *\<^sub>R (v - d))" by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real) have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1" - apply (simp only: ll norm_mult scaleR_diff_right) - using \e>0\ cmod_less_4C apply (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1]) - done - have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" - using x uv shr_uv cmod_less_dt - by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) - also have "\ \ cmod y / cmod (v - u) / 12" - using False uv \C>0\ diff_2C [of v u] ynz - by (auto simp: field_split_simps hull_inc) - finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ cmod y / cmod (v - u) / 12" - by simp - then have cmod_12_le: "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) * 12 \ cmod y" - using uv False by (auto simp: field_simps) + unfolding ll norm_mult scaleR_diff_right + using \e>0\ cmod_less_4C by (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1]) have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ B * (cmod y / 24 / C / B * 2 * C) + 2 * C * (cmod y / 24 / C)" - apply (rule add_mono [OF mult_mono]) - using By_uv e \0 < B\ \0 < C\ x apply (simp_all add: cmod_fuv cmod_shr cmod_12_le) - apply (simp add: field_simps) - done + proof (intro add_mono [OF mult_mono]) + show "cmod (f (linepath (shrink u) (shrink v) x)) \ B" + using cmod_fuv x by blast + have "B * (12 * (e * cmod (u - v))) \ 24 * e * C * B" + using e \B>0\ diff_2C [of u v] uv by (auto simp: field_simps) + also have "\ \ cmod y" + using \C>0\ \B>0\ e by (simp add: field_simps) + finally show "cmod (shrink v - shrink u - (v - u)) \ cmod y / 24 / C / B * 2 * C" + using \0 < B\ \0 < C\ by (simp add: cmod_shr mult_ac divide_simps) + have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)" + using x uv shr_uv cmod_less_dt + by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull) + also have "\ \ cmod y / cmod (v - u) / 12" + using False uv \C>0\ diff_2C [of v u] ynz + by (auto simp: field_split_simps hull_inc) + finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ cmod y / cmod (v - u) / 12" + by simp + then show "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) + \ 2 * C * (cmod y / 24 / C)" + using uv C by (simp add: field_simps) + qed (use \0 < B\ in auto) also have "\ \ cmod y / 6" by simp finally have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) + cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) \ cmod y / 6" . } note cmod_diff_le = this have f_uv: "continuous_on (closed_segment u v) f" by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull]) - have **: "\f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)" + have **: "\f' x' f x::complex. f'*x' - f*x = f' * (x' - x) + x * (f' - f)" by (simp add: algebra_simps) - have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) + have "norm (pathint (shrink u) (shrink v) - pathint u v) \ (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))" apply (rule has_integral_bound [of _ "\x. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)" _ 0 1]) using ynz \0 < B\ \0 < C\ - apply (simp_all del: le_divide_eq_numeral1) - apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral - fpi_uv f_uv contour_integrable_continuous_linepath) + apply (simp_all add: pathint_def has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral + fpi_uv f_uv contour_integrable_continuous_linepath del: le_divide_eq_numeral1) apply (auto simp: ** norm_triangle_le norm_mult cmod_diff_le simp del: le_divide_eq_numeral1) done also have "\ \ norm y / 6" by simp - finally have "norm (?pathint (shrink u) (shrink v) - ?pathint u v) \ norm y / 6" . + finally have "norm (pathint (shrink u) (shrink v) - pathint u v) \ norm y / 6" . } note * = this - have "norm (?pathint (shrink a) (shrink b) - ?pathint a b) \ norm y / 6" + have "norm (pathint (shrink a) (shrink b) - pathint a b) \ norm y / 6" using False fpi_abc by (rule_tac *) (auto simp: hull_inc) moreover - have "norm (?pathint (shrink b) (shrink c) - ?pathint b c) \ norm y / 6" + have "norm (pathint (shrink b) (shrink c) - pathint b c) \ norm y / 6" using False fpi_abc by (rule_tac *) (auto simp: hull_inc) moreover - have "norm (?pathint (shrink c) (shrink a) - ?pathint c a) \ norm y / 6" + have "norm (pathint (shrink c) (shrink a) - pathint c a) \ norm y / 6" using False fpi_abc by (rule_tac *) (auto simp: hull_inc) ultimately - have "norm((?pathint (shrink a) (shrink b) - ?pathint a b) + - (?pathint (shrink b) (shrink c) - ?pathint b c) + (?pathint (shrink c) (shrink a) - ?pathint c a)) + have "norm((pathint (shrink a) (shrink b) - pathint a b) + + (pathint (shrink b) (shrink c) - pathint b c) + (pathint (shrink c) (shrink a) - pathint c a)) \ norm y / 6 + norm y / 6 + norm y / 6" by (metis norm_triangle_le add_mono) also have "\ = norm y / 2" by simp - finally have "norm((?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a)) - - (?pathint a b + ?pathint b c + ?pathint c a)) + finally have "norm((pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a)) - + (pathint a b + pathint b c + pathint c a)) \ norm y / 2" by (simp add: algebra_simps) then - have "norm(?pathint a b + ?pathint b c + ?pathint c a) \ norm y / 2" + have "norm(pathint a b + pathint b c + pathint c a) \ norm y / 2" by (simp add: f_0_shrink) (metis (mono_tags) add.commute minus_add_distrib norm_minus_cancel uminus_add_conv_diff) then have "False" using pi_eq_y ynz by auto } note * = this have "uniformly_continuous_on (convex hull {a,b,c}) f" by (simp add: contf compact_convex_hull compact_uniformly_continuous) moreover have "norm y / (24 * C) > 0" using ynz \C > 0\ by auto ultimately obtain \ where "\ > 0" and "\x\convex hull {a, b, c}. \x'\convex hull {a, b, c}. dist x' x < \ \ dist (f x') (f x) < cmod y / (24 * C)" using \C > 0\ ynz unfolding uniformly_continuous_on_def dist_norm by blast hence False using *[of \] by (auto simp: dist_norm) then show ?thesis .. qed } moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" using fabc contour_integrable_continuous_linepath by auto ultimately show ?thesis using has_contour_integral_integral by fastforce qed subsection\<^marker>\tag unimportant\ \Version allowing finite number of exceptional points\ proposition\<^marker>\tag unimportant\ Cauchy_theorem_triangle_cofinite: assumes "continuous_on (convex hull {a,b,c}) f" and "finite S" and "(\x. x \ interior(convex hull {a,b,c}) - S \ f field_differentiable (at x))" shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" using assms proof (induction "card S" arbitrary: a b c S rule: less_induct) case (less S a b c) show ?case proof (cases "S={}") case True with less show ?thesis by (fastforce simp: holomorphic_on_def field_differentiable_at_within Cauchy_theorem_triangle_interior) next case False then obtain d S' where d: "S = insert d S'" "d \ S'" by (meson Set.set_insert all_not_in_conv) then show ?thesis proof (cases "d \ convex hull {a,b,c}") case False show "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" proof (rule less.hyps) show "\x. x \ interior (convex hull {a, b, c}) - S' \ f field_differentiable at x" using False d interior_subset by (auto intro!: less.prems) qed (use d less.prems in auto) next case True have *: "convex hull {a, b, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have abd: "(f has_contour_integral 0) (linepath a b +++ linepath b d +++ linepath d a)" proof (rule less.hyps) show "\x. x \ interior (convex hull {a, b, d}) - S' \ f field_differentiable at x" using d not_in_interior_convex_hull_3 by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) qed (use d continuous_on_subset [OF _ *] less.prems in auto) have *: "convex hull {b, c, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have bcd: "(f has_contour_integral 0) (linepath b c +++ linepath c d +++ linepath d b)" proof (rule less.hyps) show "\x. x \ interior (convex hull {b, c, d}) - S' \ f field_differentiable at x" using d not_in_interior_convex_hull_3 by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) qed (use d continuous_on_subset [OF _ *] less.prems in auto) have *: "convex hull {c, a, d} \ convex hull {a, b, c}" by (meson True hull_subset insert_subset convex_hull_subset) have cad: "(f has_contour_integral 0) (linepath c a +++ linepath a d +++ linepath d c)" proof (rule less.hyps) show "\x. x \ interior (convex hull {c, a, d}) - S' \ f field_differentiable at x" using d not_in_interior_convex_hull_3 by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono) qed (use d continuous_on_subset [OF _ *] less.prems in auto) have "f contour_integrable_on linepath a b" using less.prems abd contour_integrable_joinD1 contour_integrable_on_def by blast moreover have "f contour_integrable_on linepath b c" using less.prems bcd contour_integrable_joinD1 contour_integrable_on_def by blast moreover have "f contour_integrable_on linepath c a" using less.prems cad contour_integrable_joinD1 contour_integrable_on_def by blast ultimately have fpi: "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)" by auto { fix y::complex assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)" and ynz: "y \ 0" have cont_ad: "continuous_on (closed_segment a d) f" by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(3)) have cont_bd: "continuous_on (closed_segment b d) f" by (meson True closed_segment_subset_convex_hull continuous_on_subset hull_subset insert_subset less.prems(1)) have cont_cd: "continuous_on (closed_segment c d) f" by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2)) have "contour_integral (linepath a b) f = - (contour_integral (linepath b d) f + (contour_integral (linepath d a) f))" "contour_integral (linepath b c) f = - (contour_integral (linepath c d) f + (contour_integral (linepath d b) f))" "contour_integral (linepath c a) f = - (contour_integral (linepath a d) f + contour_integral (linepath d c) f)" using has_chain_integral_chain_integral3 [OF abd] has_chain_integral_chain_integral3 [OF bcd] has_chain_integral_chain_integral3 [OF cad] by (simp_all add: algebra_simps add_eq_0_iff) then have ?thesis using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 contour_integral_reverse_linepath by fastforce } then show ?thesis using fpi contour_integrable_on_def by blast qed qed qed subsection\<^marker>\tag unimportant\ \Cauchy's theorem for an open starlike set\ lemma starlike_convex_subset: assumes S: "a \ S" "closed_segment b c \ S" and subs: "\x. x \ S \ closed_segment a x \ S" - shows "convex hull {a,b,c} \ S" - using S - apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull) - apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE) - done + shows "convex hull {a,b,c} \ S" +proof - + have "convex hull {b, c} \ S" + using assms(2) segment_convex_hull by auto + then have "\u v d. \0 \ u; 0 \ v; u + v = 1; d \ convex hull {b, c}\ \ u *\<^sub>R a + v *\<^sub>R d \ S" + by (meson subs convexD convex_closed_segment ends_in_segment subsetCE) + then show ?thesis + by (auto simp add: convex_hull_insert [of "{b,c}" a]) +qed lemma triangle_contour_integrals_starlike_primitive: assumes contf: "continuous_on S f" and S: "a \ S" "open S" and x: "x \ S" and subs: "\y. y \ S \ closed_segment a y \ S" and zer: "\b c. closed_segment b c \ S \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" shows "((\x. contour_integral(linepath a x) f) has_field_derivative f x) (at x)" proof - let ?pathint = "\x y. contour_integral(linepath x y) f" { fix e y assume e: "0 < e" and bxe: "ball x e \ S" and close: "cmod (y - x) < e" have y: "y \ S" using bxe close by (force simp: dist_norm norm_minus_commute) have cont_ayf: "continuous_on (closed_segment a y) f" using contf continuous_on_subset subs y by blast have xys: "closed_segment x y \ S" - apply (rule order_trans [OF _ bxe]) - using close - by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound) + by (metis bxe centre_in_ball close closed_segment_subset convex_ball dist_norm dual_order.trans e mem_ball norm_minus_commute) have "?pathint a y - ?pathint a x = ?pathint x y" using zer [OF xys] contour_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force } note [simp] = this { fix e::real assume e: "0 < e" have cont_atx: "continuous (at x) f" using x S contf continuous_on_eq_continuous_at by blast then obtain d1 where d1: "d1>0" and d1_less: "\y. cmod (y - x) < d1 \ cmod (f y - f x) < e/2" unfolding continuous_at Lim_at dist_norm using e by (drule_tac x="e/2" in spec) force obtain d2 where d2: "d2>0" "ball x d2 \ S" using \open S\ x by (auto simp: open_contains_ball) have dpos: "min d1 d2 > 0" using d1 d2 by simp { fix y assume yx: "y \ x" and close: "cmod (y - x) < min d1 d2" have y: "y \ S" using d2 close by (force simp: dist_norm norm_minus_commute) have "closed_segment x y \ S" using close d2 by (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1)) then have fxy: "f contour_integrable_on linepath x y" by (metis contour_integrable_continuous_linepath continuous_on_subset [OF contf]) then obtain i where i: "(f has_contour_integral i) (linepath x y)" by (auto simp: contour_integrable_on_def) then have "((\w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)" by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath]) then have "cmod (i - f x * (y - x)) \ e / 2 * cmod (y - x)" proof (rule has_contour_integral_bound_linepath) show "\u. u \ closed_segment x y \ cmod (f u - f x) \ e / 2" by (meson close d1_less le_less_trans less_imp_le min.strict_boundedE segment_bound1) qed (use e in simp) also have "\ < e * cmod (y - x)" by (simp add: e yx) finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using i yx by (simp add: contour_integral_unique divide_less_eq) } then have "\d>0. \y. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using dpos by blast } - then have *: "(\y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \x\ 0" + then have "(\y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \x\ 0" by (simp add: Lim_at dist_norm inverse_eq_divide) - show ?thesis - apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right) - apply (rule Lim_transform [OF * tendsto_eventually]) - using \open S\ x apply (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at) - done + then have "(\y. (1 / cmod (y - x)) *\<^sub>R (?pathint a y - (?pathint a x + f x * (y - x)))) \x\ 0" + using \open S\ x + by (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at intro: Lim_transform [OF _ tendsto_eventually]) + then show ?thesis + by (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right) qed (** Existence of a primitive.*) lemma holomorphic_starlike_primitive: fixes f :: "complex \ complex" assumes contf: "continuous_on S f" and S: "starlike S" and os: "open S" and k: "finite k" and fcd: "\x. x \ S - k \ f field_differentiable at x" shows "\g. \x \ S. (g has_field_derivative f x) (at x)" proof - obtain a where a: "a\S" and a_cs: "\x. x\S \ closed_segment a x \ S" using S by (auto simp: starlike_def) { fix x b c assume "x \ S" "closed_segment b c \ S" then have abcs: "convex hull {a, b, c} \ S" by (simp add: a a_cs starlike_convex_subset) then have "continuous_on (convex hull {a, b, c}) f" by (simp add: continuous_on_subset [OF contf]) then have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" using abcs interior_subset by (force intro: fcd Cauchy_theorem_triangle_cofinite [OF _ k]) } note 0 = this show ?thesis - apply (intro exI ballI) - apply (rule triangle_contour_integrals_starlike_primitive [OF contf a os], assumption) - apply (metis a_cs) - apply (metis has_chain_integral_chain_integral3 0) - done + proof (intro exI ballI) + show "\x. x \ S \ ((\x. contour_integral (linepath a x) f) has_field_derivative f x) (at x)" + using "0" a a_cs contf has_chain_integral_chain_integral3 os triangle_contour_integrals_starlike_primitive by force + qed qed lemma Cauchy_theorem_starlike: "\open S; starlike S; finite k; continuous_on S f; \x. x \ S - k \ f field_differentiable at x; valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open) lemma Cauchy_theorem_starlike_simple: "\open S; starlike S; f holomorphic_on S; valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" -apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI]) -apply (simp_all add: holomorphic_on_imp_continuous_on) -apply (metis at_within_open holomorphic_on_def) -done + using Cauchy_theorem_starlike [OF _ _ finite.emptyI] + by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at) subsection\Cauchy's theorem for a convex set\ text\For a convex set we can avoid assuming openness and boundary analyticity\ lemma triangle_contour_integrals_convex_primitive: assumes contf: "continuous_on S f" and S: "a \ S" "convex S" and x: "x \ S" and zer: "\b c. \b \ S; c \ S\ \ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0" shows "((\x. contour_integral(linepath a x) f) has_field_derivative f x) (at x within S)" proof - let ?pathint = "\x y. contour_integral(linepath x y) f" { fix y assume y: "y \ S" have cont_ayf: "continuous_on (closed_segment a y) f" using S y by (meson contf continuous_on_subset convex_contains_segment) have xys: "closed_segment x y \ S" (*?*) using convex_contains_segment S x y by auto have "?pathint a y - ?pathint a x = ?pathint x y" using zer [OF x y] contour_integral_reverse_linepath [OF cont_ayf] add_eq_0_iff by force } note [simp] = this { fix e::real assume e: "0 < e" have cont_atx: "continuous (at x within S) f" using x S contf by (simp add: continuous_on_eq_continuous_within) then obtain d1 where d1: "d1>0" and d1_less: "\y. \y \ S; cmod (y - x) < d1\ \ cmod (f y - f x) < e/2" unfolding continuous_within Lim_within dist_norm using e by (drule_tac x="e/2" in spec) force { fix y assume yx: "y \ x" and close: "cmod (y - x) < d1" and y: "y \ S" have fxy: "f contour_integrable_on linepath x y" using convex_contains_segment S x y by (blast intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) then obtain i where i: "(f has_contour_integral i) (linepath x y)" by (auto simp: contour_integrable_on_def) then have "((\w. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)" by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath]) then have "cmod (i - f x * (y - x)) \ e / 2 * cmod (y - x)" proof (rule has_contour_integral_bound_linepath) show "\u. u \ closed_segment x y \ cmod (f u - f x) \ e / 2" by (meson assms(3) close convex_contains_segment d1_less le_less_trans less_imp_le segment_bound1 subset_iff x y) qed (use e in simp) also have "\ < e * cmod (y - x)" by (simp add: e yx) finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using i yx by (simp add: contour_integral_unique divide_less_eq) } then have "\d>0. \y\S. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e" using d1 by blast } - then have *: "((\y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \ 0) (at x within S)" + then have "((\y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \ 0) (at x within S)" by (simp add: Lim_within dist_norm inverse_eq_divide) - show ?thesis - apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right) - apply (rule Lim_transform [OF * tendsto_eventually]) + then have "((\y. (1 / cmod (y - x)) *\<^sub>R (?pathint a y - (?pathint a x + f x * (y - x)))) \ 0) + (at x within S)" using linordered_field_no_ub - apply (force simp: inverse_eq_divide [symmetric] eventually_at) - done + by (force simp: inverse_eq_divide [symmetric] eventually_at intro: Lim_transform [OF _ tendsto_eventually]) + then show ?thesis + by (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right) qed lemma contour_integral_convex_primitive: assumes "convex S" "continuous_on S f" "\a b c. \a \ S; b \ S; c \ S\ \ (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)" obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" proof (cases "S={}") case False with assms that show ?thesis by (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3) qed auto lemma holomorphic_convex_primitive: fixes f :: "complex \ complex" assumes "convex S" "finite K" and contf: "continuous_on S f" and fd: "\x. x \ interior S - K \ f field_differentiable at x" obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" proof (rule contour_integral_convex_primitive [OF \convex S\ contf Cauchy_theorem_triangle_cofinite]) have *: "convex hull {a, b, c} \ S" if "a \ S" "b \ S" "c \ S" for a b c by (simp add: \convex S\ hull_minimal that) show "continuous_on (convex hull {a, b, c}) f" if "a \ S" "b \ S" "c \ S" for a b c by (meson "*" contf continuous_on_subset that) show "f field_differentiable at x" if "a \ S" "b \ S" "c \ S" "x \ interior (convex hull {a, b, c}) - K" for a b c x by (metis "*" DiffD1 DiffD2 DiffI fd interior_mono subsetCE that) qed (use assms in \force+\) lemma holomorphic_convex_primitive': fixes f :: "complex \ complex" assumes "convex S" and "open S" and "f holomorphic_on S" obtains g where "\x. x \ S \ (g has_field_derivative f x) (at x within S)" proof (rule holomorphic_convex_primitive) fix x assume "x \ interior S - {}" with assms show "f field_differentiable at x" by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open) qed (use assms in \auto intro: holomorphic_on_imp_continuous_on\) corollary\<^marker>\tag unimportant\ Cauchy_theorem_convex: "\continuous_on S f; convex S; finite K; \x. x \ interior S - K \ f field_differentiable at x; valid_path g; path_image g \ S; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (metis holomorphic_convex_primitive Cauchy_theorem_primitive) corollary Cauchy_theorem_convex_simple: - "\f holomorphic_on S; convex S; - valid_path g; path_image g \ S; - pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" - apply (rule Cauchy_theorem_convex [where K = "{}"]) - apply (simp_all add: holomorphic_on_imp_continuous_on) - using at_within_interior holomorphic_on_def interior_subset by fastforce + assumes holf: "f holomorphic_on S" + and "convex S" "valid_path g" "path_image g \ S" "pathfinish g = pathstart g" + shows "(f has_contour_integral 0) g" +proof - + have "f holomorphic_on interior S" + by (meson holf holomorphic_on_subset interior_subset) + with Cauchy_theorem_convex [where K = "{}"] show ?thesis + using assms + by (metis Diff_empty finite.emptyI holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at open_interior) +qed text\In particular for a disc\ corollary\<^marker>\tag unimportant\ Cauchy_theorem_disc: "\finite K; continuous_on (cball a e) f; \x. x \ ball a e - K \ f field_differentiable at x; valid_path g; path_image g \ cball a e; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (auto intro: Cauchy_theorem_convex) corollary\<^marker>\tag unimportant\ Cauchy_theorem_disc_simple: "\f holomorphic_on (ball a e); valid_path g; path_image g \ ball a e; pathfinish g = pathstart g\ \ (f has_contour_integral 0) g" by (simp add: Cauchy_theorem_convex_simple) subsection\<^marker>\tag unimportant\ \Generalize integrability to local primitives\ lemma contour_integral_local_primitive_lemma: fixes f :: "complex\complex" - shows - "\g piecewise_differentiable_on {a..b}; - \x. x \ s \ (f has_field_derivative f' x) (at x within s); - \x. x \ {a..b} \ g x \ s\ - \ (\x. f' (g x) * vector_derivative g (at x within {a..b})) - integrable_on {a..b}" - apply (cases "cbox a b = {}", force) - apply (simp add: integrable_on_def) - apply (rule exI) - apply (rule contour_integral_primitive_lemma, assumption+) - using atLeastAtMost_iff by blast + assumes gpd: "g piecewise_differentiable_on {a..b}" + and dh: "\x. x \ S \ (f has_field_derivative f' x) (at x within S)" + and gs: "\x. x \ {a..b} \ g x \ S" + shows + "(\x. f' (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b}" +proof (cases "cbox a b = {}") + case False + then show ?thesis + unfolding integrable_on_def by (auto intro: assms contour_integral_primitive_lemma) +qed auto lemma contour_integral_local_primitive_any: fixes f :: "complex \ complex" assumes gpd: "g piecewise_differentiable_on {a..b}" - and dh: "\x. x \ s + and dh: "\x. x \ S \ \d h. 0 < d \ - (\y. norm(y - x) < d \ (h has_field_derivative f y) (at y within s))" - and gs: "\x. x \ {a..b} \ g x \ s" + (\y. norm(y - x) < d \ (h has_field_derivative f y) (at y within S))" + and gs: "\x. x \ {a..b} \ g x \ S" shows "(\x. f(g x) * vector_derivative g (at x)) integrable_on {a..b}" proof - { fix x assume x: "a \ x" "x \ b" obtain d h where d: "0 < d" - and h: "(\y. norm(y - g x) < d \ (h has_field_derivative f y) (at y within s))" + and h: "(\y. norm(y - g x) < d \ (h has_field_derivative f y) (at y within S))" using x gs dh by (metis atLeastAtMost_iff) have "continuous_on {a..b} g" using gpd piecewise_differentiable_on_def by blast then obtain e where e: "e>0" and lessd: "\x'. x' \ {a..b} \ \x' - x\ < e \ cmod (g x' - g x) < d" - using x d - apply (auto simp: dist_norm continuous_on_iff) - apply (drule_tac x=x in bspec) - using x apply simp - apply (drule_tac x=d in spec, auto) - done - have "\d>0. \u v. u \ x \ x \ v \ {u..v} \ ball x d \ (u \ v \ a \ u \ v \ b) \ + using x d by (fastforce simp: dist_norm continuous_on_iff) + have "\e>0. \u v. u \ x \ x \ v \ {u..v} \ ball x e \ (u \ v \ a \ u \ v \ b) \ (\x. f (g x) * vector_derivative g (at x)) integrable_on {u..v}" - apply (rule_tac x=e in exI) - using e - apply (simp add: integrable_on_localized_vector_derivative [symmetric], clarify) - apply (rule_tac f = h and s = "g ` {u..v}" in contour_integral_local_primitive_lemma) - apply (meson atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset) - apply (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h], force) - done + proof - + have "(\x. f (g x) * vector_derivative g (at x within {u..v})) integrable_on {u..v}" + if "u \ x" "x \ v" and ball: "{u..v} \ ball x e" and auvb: "u \ v \ a \ u \ v \ b" + for u v + proof (rule contour_integral_local_primitive_lemma) + show "g piecewise_differentiable_on {u..v}" + by (metis atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset auvb) + show "\x. x \ g ` {u..v} \ (h has_field_derivative f x) (at x within g ` {u..v})" + using that by (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h]) + qed auto + then show ?thesis + using e integrable_on_localized_vector_derivative by blast + qed } then show ?thesis by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified]) qed lemma contour_integral_local_primitive: fixes f :: "complex \ complex" - assumes g: "valid_path g" "path_image g \ s" - and dh: "\x. x \ s + assumes g: "valid_path g" "path_image g \ S" + and dh: "\x. x \ S \ \d h. 0 < d \ - (\y. norm(y - x) < d \ (h has_field_derivative f y) (at y within s))" - shows "f contour_integrable_on g" - using g - apply (simp add: valid_path_def path_image_def contour_integrable_on_def has_contour_integral_def - has_integral_localized_vector_derivative integrable_on_def [symmetric]) - using contour_integral_local_primitive_any [OF _ dh] - by (meson image_subset_iff piecewise_C1_imp_differentiable) + (\y. norm(y - x) < d \ (h has_field_derivative f y) (at y within S))" + shows "f contour_integrable_on g" +proof - + have "(\x. f (g x) * vector_derivative g (at x)) integrable_on {0..1}" + using contour_integral_local_primitive_any [OF _ dh] g + unfolding path_image_def valid_path_def + by (metis (no_types, lifting) image_subset_iff piecewise_C1_imp_differentiable) + then show ?thesis + using contour_integrable_on by presburger +qed text\In particular if a function is holomorphic\ lemma contour_integrable_holomorphic: - assumes contf: "continuous_on s f" - and os: "open s" + assumes contf: "continuous_on S f" + and os: "open S" and k: "finite k" - and g: "valid_path g" "path_image g \ s" - and fcd: "\x. x \ s - k \ f field_differentiable at x" + and g: "valid_path g" "path_image g \ S" + and fcd: "\x. x \ S - k \ f field_differentiable at x" shows "f contour_integrable_on g" proof - { fix z - assume z: "z \ s" - obtain d where "d>0" and d: "ball z d \ s" using \open s\ z + assume z: "z \ S" + obtain d where "d>0" and d: "ball z d \ S" using \open S\ z by (auto simp: open_contains_ball) then have contfb: "continuous_on (ball z d) f" using contf continuous_on_subset by blast obtain h where "\y\ball z d. (h has_field_derivative f y) (at y within ball z d)" by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD) - then have "\y\ball z d. (h has_field_derivative f y) (at y within s)" + then have "\y\ball z d. (h has_field_derivative f y) (at y within S)" by (metis open_ball at_within_open d os subsetCE) - then have "\h. (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within s))" + then have "\h. (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within S))" by (force simp: dist_norm norm_minus_commute) - then have "\d h. 0 < d \ (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within s))" + then have "\d h. 0 < d \ (\y. cmod (y - z) < d \ (h has_field_derivative f y) (at y within S))" using \0 < d\ by blast } then show ?thesis by (rule contour_integral_local_primitive [OF g]) qed lemma contour_integrable_holomorphic_simple: assumes fh: "f holomorphic_on S" and os: "open S" and g: "valid_path g" "path_image g \ S" shows "f contour_integrable_on g" - apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g]) - apply (simp add: fh holomorphic_on_imp_continuous_on) - using fh by (simp add: field_differentiable_def holomorphic_on_open os) +proof - + have "\x. x \ S \ f field_differentiable at x" + using fh holomorphic_on_imp_differentiable_at os by blast + moreover have "continuous_on S f" + by (simp add: fh holomorphic_on_imp_continuous_on) + ultimately show ?thesis + by (metis Diff_empty contour_integrable_holomorphic finite.emptyI g os) +qed lemma continuous_on_inversediff: fixes z:: "'a::real_normed_field" shows "z \ S \ continuous_on S (\w. 1 / (w - z))" by (rule continuous_intros | force)+ lemma contour_integrable_inversediff: - "\valid_path g; z \ path_image g\ \ (\w. 1 / (w-z)) contour_integrable_on g" -apply (rule contour_integrable_holomorphic_simple [of _ "UNIV-{z}"]) -apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros) -done + assumes g: "valid_path g" + and notin: "z \ path_image g" + shows "(\w. 1 / (w-z)) contour_integrable_on g" +proof (rule contour_integrable_holomorphic_simple) + show "(\w. 1 / (w-z)) holomorphic_on UNIV - {z}" + by (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros) +qed (use assms in auto) text\Key fact that path integral is the same for a "nearby" path. This is the main lemma for the homotopy form of Cauchy's theorem and is also useful if we want "without loss of generality" to assume some nice properties of a path (e.g. smoothness). It can also be used to define the integrals of analytic functions over arbitrary continuous paths. This is just done for winding numbers now. \ text\A technical definition to avoid duplication of similar proofs, for paths joined at the ends versus looping paths\ definition linked_paths :: "bool \ (real \ 'a) \ (real \ 'a::topological_space) \ bool" where "linked_paths atends g h == (if atends then pathstart h = pathstart g \ pathfinish h = pathfinish g else pathfinish g = pathstart g \ pathfinish h = pathstart h)" text\This formulation covers two cases: \<^term>\g\ and \<^term>\h\ share their start and end points; \<^term>\g\ and \<^term>\h\ both loop upon themselves.\ lemma contour_integral_nearby: assumes os: "open S" and p: "path p" "path_image p \ S" shows "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ linked_paths atends g h \ path_image g \ S \ path_image h \ S \ (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" proof - have "\z. \e. z \ path_image p \ 0 < e \ ball z e \ S" using open_contains_ball os p(2) by blast then obtain ee where ee: "\z. z \ path_image p \ 0 < ee z \ ball z (ee z) \ S" by metis define cover where "cover = (\z. ball z (ee z/3)) ` (path_image p)" have "compact (path_image p)" by (metis p(1) compact_path_image) moreover have "path_image p \ (\c\path_image p. ball c (ee c / 3))" using ee by auto ultimately have "\D \ cover. finite D \ path_image p \ \D" by (simp add: compact_eq_Heine_Borel cover_def) then obtain D where D: "D \ cover" "finite D" "path_image p \ \D" by blast then obtain k where k: "k \ {0..1}" "finite k" and D_eq: "D = ((\z. ball z (ee z / 3)) \ p) ` k" - apply (simp add: cover_def path_image_def image_comp) - apply (blast dest!: finite_subset_image [OF \finite D\]) - done + unfolding cover_def path_image_def image_comp + by (meson finite_subset_image) then have kne: "k \ {}" using D by auto have pi: "\i. i \ k \ p i \ path_image p" using k by (auto simp: path_image_def) then have eepi: "\i. i \ k \ 0 < ee((p i))" by (metis ee) define e where "e = Min((ee \ p) ` k)" have fin_eep: "finite ((ee \ p) ` k)" using k by blast have "0 < e" using ee k by (simp add: kne e_def Min_gr_iff [OF fin_eep] eepi) have "uniformly_continuous_on {0..1} p" using p by (simp add: path_def compact_uniformly_continuous) then obtain d::real where d: "d>0" and de: "\x x'. \x' - x\ < d \ x\{0..1} \ x'\{0..1} \ cmod (p x' - p x) < e/3" unfolding uniformly_continuous_on_def dist_norm real_norm_def by (metis divide_pos_pos \0 < e\ zero_less_numeral) then obtain N::nat where N: "N>0" "inverse N < d" using real_arch_inverse [of d] by auto show ?thesis proof (intro exI conjI allI; clarify?) show "e/3 > 0" using \0 < e\ by simp fix g h assume g: "valid_path g" and ghp: "\t\{0..1}. cmod (g t - p t) < e / 3 \ cmod (h t - p t) < e / 3" and h: "valid_path h" and joins: "linked_paths atends g h" { fix t::real assume t: "0 \ t" "t \ 1" then obtain u where u: "u \ k" and ptu: "p t \ ball(p u) (ee(p u) / 3)" using \path_image p \ \D\ D_eq by (force simp: path_image_def) then have ele: "e \ ee (p u)" using fin_eep by (simp add: e_def) have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3" using ghp t by auto with ele have "cmod (g t - p t) < ee (p u) / 3" "cmod (h t - p t) < ee (p u) / 3" by linarith+ then have "g t \ ball(p u) (ee(p u))" "h t \ ball(p u) (ee(p u))" using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"] norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u by (force simp: dist_norm ball_def norm_minus_commute)+ then have "g t \ S" "h t \ S" using ee u k by (auto simp: path_image_def ball_def) } then have ghs: "path_image g \ S" "path_image h \ S" by (auto simp: path_image_def) moreover { fix f assume fhols: "f holomorphic_on S" then have fpa: "f contour_integrable_on g" "f contour_integrable_on h" using g ghs h holomorphic_on_imp_continuous_on os contour_integrable_holomorphic_simple by blast+ have contf: "continuous_on S f" by (simp add: fhols holomorphic_on_imp_continuous_on) { fix z assume z: "z \ path_image p" have "f holomorphic_on ball z (ee z)" using fhols ee z holomorphic_on_subset by blast then have "\ff. (\w \ ball z (ee z). (ff has_field_derivative f w) (at w))" using holomorphic_convex_primitive [of "ball z (ee z)" "{}" f, simplified] by (metis open_ball at_within_open holomorphic_on_def holomorphic_on_imp_continuous_on mem_ball) } then obtain ff where ff: "\z w. \z \ path_image p; w \ ball z (ee z)\ \ (ff z has_field_derivative f w) (at w)" by metis { fix n assume n: "n \ N" then have "contour_integral(subpath 0 (n/N) h) f - contour_integral(subpath 0 (n/N) g) f = contour_integral(linepath (g(n/N)) (h(n/N))) f - contour_integral(linepath (g 0) (h 0)) f" proof (induct n) case 0 show ?case by simp next case (Suc n) obtain t where t: "t \ k" and "p (n/N) \ ball(p t) (ee(p t) / 3)" using \path_image p \ \D\ [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems by (force simp: path_image_def) then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3" by (simp add: dist_norm) have e3le: "e/3 \ ee (p t) / 3" using fin_eep t by (simp add: e_def) { fix x assume x: "n/N \ x" "x \ (1 + n)/N" then have nN01: "0 \ n/N" "(1 + n)/N \ 1" using Suc.prems by auto then have x01: "0 \ x" "x \ 1" using x by linarith+ have "cmod (p t - p x) < ee (p t) / 3 + e/3" proof (rule norm_diff_triangle_less [OF ptu de]) show "\real n / real N - x\ < d" using x N by (auto simp: field_simps) qed (use x01 Suc.prems in auto) then have ptx: "cmod (p t - p x) < 2*ee (p t)/3" using e3le eepi [OF t] by simp - have "cmod (p t - g x) < 2*ee (p t)/3 + e/3 " - apply (rule norm_diff_triangle_less [OF ptx]) - using ghp x01 by (simp add: norm_minus_commute) + have "cmod (p t - g x) < 2*ee (p t)/3 + e/3" + using ghp x01 + by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx]) also have "\ \ ee (p t)" using e3le eepi [OF t] by simp finally have gg: "cmod (p t - g x) < ee (p t)" . have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 " - apply (rule norm_diff_triangle_less [OF ptx]) - using ghp x01 by (simp add: norm_minus_commute) + using ghp x01 + by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx]) also have "\ \ ee (p t)" using e3le eepi [OF t] by simp - finally have "cmod (p t - g x) < ee (p t)" - "cmod (p t - h x) < ee (p t)" + finally have "cmod (p t - g x) < ee (p t)" "cmod (p t - h x) < ee (p t)" using gg by auto } note ptgh_ee = this - have "closed_segment (g (real n / real N)) (h (real n / real N)) = path_image (linepath (h (n/N)) (g (n/N)))" + have "closed_segment (g (n/N)) (h (n/N)) = path_image (linepath (h (n/N)) (g (n/N)))" by (simp add: closed_segment_commute) also have pi_hgn: "\ \ ball (p t) (ee (p t))" using ptgh_ee [of "n/N"] Suc.prems by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) \ S" using ee pi t by blast have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N))) \ ball (p t) (ee (p t))" using ptgh_ee [of "(1+n)/N"] Suc.prems by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"]) then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) \ S" using \N>0\ Suc.prems ee pi t by (auto simp: Path_Connected.path_image_join field_simps) have pi_subset_ball: "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++ subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N))) \ ball (p t) (ee (p t))" - apply (intro subset_path_image_join pi_hgn pi_ghn') - using \N>0\ Suc.prems - apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee) - done + proof (intro subset_path_image_join pi_hgn pi_ghn') + show "path_image (subpath (n/N) ((1+n) / N) g) \ ball (p t) (ee (p t))" + "path_image (subpath ((1+n) / N) (n/N) h) \ ball (p t) (ee (p t))" + using \N>0\ Suc.prems + by (auto simp: path_image_subpath dist_norm field_simps ptgh_ee) + qed have pi0: "(f has_contour_integral 0) (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++ subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))" - apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"]) - apply (metis ff open_ball at_within_open pi t) - using Suc.prems pi_subset_ball apply (simp_all add: valid_path_join valid_path_subpath g h) - done - have fpa1: "f contour_integrable_on subpath (real n / real N) (real (Suc n) / real N) g" + proof (rule Cauchy_theorem_primitive) + show "\x. x \ ball (p t) (ee (p t)) + \ (ff (p t) has_field_derivative f x) (at x within ball (p t) (ee (p t)))" + by (metis ff open_ball at_within_open pi t) + qed (use Suc.prems pi_subset_ball in \simp_all add: valid_path_subpath g h\) + have fpa1: "f contour_integrable_on subpath (n/N) (real (Suc n) / real N) g" using Suc.prems by (simp add: contour_integrable_subpath g fpa) have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))" using gh_n's by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) - have fpa3: "f contour_integrable_on linepath (h (real n / real N)) (g (real n / real N))" + have fpa3: "f contour_integrable_on linepath (h (n/N)) (g (n/N))" using gh_ns by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf]) have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f + contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f + contour_integral (subpath ((Suc n) / N) (n/N) h) f + contour_integral (linepath (h (n/N)) (g (n/N))) f = 0" using contour_integral_unique [OF pi0] Suc.prems by (simp add: g h fpa valid_path_subpath contour_integrable_subpath fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc) have *: "\hn he hn' gn gd gn' hgn ghn gh0 ghn'. \hn - gn = ghn - gh0; gd + ghn' + he + hgn = (0::complex); hn - he = hn'; gn + gd = gn'; hgn = -ghn\ \ hn' - gn' = ghn' - gh0" by (auto simp: algebra_simps) have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f = contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f" unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"] using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath) also have "\ = contour_integral (subpath 0 ((Suc n) / N) h) f" using Suc.prems by (simp add: contour_integral_subpath_combine h fpa) finally have pi0_eq: "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f = contour_integral (subpath 0 ((Suc n) / N) h) f" . show ?case - apply (rule * [OF Suc.hyps eq0 pi0_eq]) - using Suc.prems - apply (simp_all add: g h fpa contour_integral_subpath_combine - contour_integral_reversepath [symmetric] contour_integrable_continuous_linepath - continuous_on_subset [OF contf gh_ns]) - done + proof (rule * [OF Suc.hyps eq0 pi0_eq]) + show "contour_integral (subpath 0 (n/N) g) f + + contour_integral (subpath (n/N) ((Suc n) / N) g) f = + contour_integral (subpath 0 ((Suc n) / N) g) f" + using Suc.prems contour_integral_subpath_combine fpa(1) g by auto + show "contour_integral (linepath (h (n/N)) (g (n/N))) f = - contour_integral (linepath (g (n/N)) (h (n/N))) f" + by (metis contour_integral_unique fpa3 has_contour_integral_integral has_contour_integral_reverse_linepath) + qed (use Suc.prems in auto) qed } note ind = this have "contour_integral h f = contour_integral g f" using ind [OF order_refl] N joins by (simp add: linked_paths_def pathstart_def pathfinish_def split: if_split_asm) } ultimately show "path_image g \ S \ path_image h \ S \ (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f)" by metis qed qed lemma assumes "open S" "path p" "path_image p \ S" shows contour_integral_nearby_ends: "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ pathstart h = pathstart g \ pathfinish h = pathfinish g \ path_image g \ S \ path_image h \ S \ (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" and contour_integral_nearby_loops: "\d. 0 < d \ (\g h. valid_path g \ valid_path h \ (\t \ {0..1}. norm(g t - p t) < d \ norm(h t - p t) < d) \ pathfinish g = pathstart g \ pathfinish h = pathstart h \ path_image g \ S \ path_image h \ S \ (\f. f holomorphic_on S \ contour_integral h f = contour_integral g f))" using contour_integral_nearby [OF assms, where atends=True] using contour_integral_nearby [OF assms, where atends=False] unfolding linked_paths_def by simp_all lemma contour_integral_bound_exists: assumes S: "open S" and g: "valid_path g" and pag: "path_image g \ S" shows "\L. 0 < L \ (\f B. f holomorphic_on S \ (\z \ S. norm(f z) \ B) \ norm(contour_integral g f) \ L*B)" proof - have "path g" using g by (simp add: valid_path_imp_path) then obtain d::real and p where d: "0 < d" and p: "polynomial_function p" "path_image p \ S" and pi: "\f. f holomorphic_on S \ contour_integral g f = contour_integral p f" using contour_integral_nearby_ends [OF S \path g\ pag] by (metis cancel_comm_monoid_add_class.diff_cancel g norm_zero path_approx_polynomial_function valid_path_polynomial_function) then obtain p' where p': "polynomial_function p'" "\x. (p has_vector_derivative (p' x)) (at x)" by (blast intro: has_vector_derivative_polynomial_function that) then have "bounded(p' ` {0..1})" using continuous_on_polymonial_function by (force simp: intro!: compact_imp_bounded compact_continuous_image) then obtain L where L: "L>0" and nop': "\x. \0 \ x; x \ 1\ \ norm (p' x) \ L" by (force simp: bounded_pos) { fix f B assume f: "f holomorphic_on S" and B: "\z. z\S \ cmod (f z) \ B" then have "f contour_integrable_on p \ valid_path p" using p S by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on) moreover have "cmod (vector_derivative p (at x)) * cmod (f (p x)) \ L * B" if "0 \ x" "x \ 1" for x proof (rule mult_mono) show "cmod (vector_derivative p (at x)) \ L" by (metis nop' p'(2) that vector_derivative_at) show "cmod (f (p x)) \ B" by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that) qed (use \L>0\ in auto) - ultimately have "cmod (contour_integral g f) \ L * B" - apply (simp only: pi [OF f]) - apply (simp only: contour_integral_integral) - apply (rule order_trans [OF integral_norm_bound_integral]) - apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult) - done + ultimately + have "cmod (integral {0..1} (\x. f (p x) * vector_derivative p (at x))) \ L * B" + by (intro order_trans [OF integral_norm_bound_integral]) + (auto simp: mult.commute norm_mult contour_integrable_on) + then have "cmod (contour_integral g f) \ L * B" + using contour_integral_integral f pi by presburger } then show ?thesis using \L > 0\ by (intro exI[of _ L]) auto qed subsection\Homotopy forms of Cauchy's theorem\ lemma Cauchy_theorem_homotopic: - assumes hom: "if atends then homotopic_paths s g h else homotopic_loops s g h" - and "open s" and f: "f holomorphic_on s" + assumes hom: "if atends then homotopic_paths S g h else homotopic_loops S g h" + and "open S" and f: "f holomorphic_on S" and vpg: "valid_path g" and vph: "valid_path h" shows "contour_integral g f = contour_integral h f" proof - have pathsf: "linked_paths atends g h" using hom by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop) obtain k :: "real \ real \ complex" where contk: "continuous_on ({0..1} \ {0..1}) k" - and ks: "k ` ({0..1} \ {0..1}) \ s" + and ks: "k ` ({0..1} \ {0..1}) \ S" and k [simp]: "\x. k (0, x) = g x" "\x. k (1, x) = h x" and ksf: "\t\{0..1}. linked_paths atends g (\x. k (t, x))" using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: if_split_asm) have ucontk: "uniformly_continuous_on ({0..1} \ {0..1}) k" by (blast intro: compact_Times compact_uniformly_continuous [OF contk]) { fix t::real assume t: "t \ {0..1}" - have pak: "path (k \ (\u. (t, u)))" + have "Pair t ` {0..1} \ {0..1} \ {0..1}" + using t by force + then have pak: "path (k \ (\u. (t, u)))" unfolding path_def - apply (rule continuous_intros continuous_on_subset [OF contk])+ - using t by force - have pik: "path_image (k \ Pair t) \ s" + by (intro continuous_intros continuous_on_subset [OF contk])+ + have pik: "path_image (k \ Pair t) \ S" using ks t by (auto simp: path_image_def) obtain e where "e>0" and e: "\g h. \valid_path g; valid_path h; \u\{0..1}. cmod (g u - (k \ Pair t) u) < e \ cmod (h u - (k \ Pair t) u) < e; linked_paths atends g h\ \ contour_integral h f = contour_integral g f" - using contour_integral_nearby [OF \open s\ pak pik, of atends] f by metis + using contour_integral_nearby [OF \open S\ pak pik, of atends] f by metis obtain d where "d>0" and d: "\x x'. \x \ {0..1} \ {0..1}; x' \ {0..1} \ {0..1}; norm (x'-x) < d\ \ norm (k x' - k x) < e/4" by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm \e>0\) { fix t1 t2 assume t1: "0 \ t1" "t1 \ 1" and t2: "0 \ t2" "t2 \ 1" and ltd: "\t1 - t\ < d" "\t2 - t\ < d" - have no2: "\g1 k1 kt. \norm(g1 - k1) < e/4; norm(k1 - kt) < e/4\ \ norm(g1 - kt) < e" - using \e > 0\ - apply (rule_tac y = k1 in norm_triangle_half_l) - apply (auto simp: norm_minus_commute intro: order_less_trans) - done + have no2: "norm(g1 - kt) < e" if "norm(g1 - k1) < e/4" "norm(k1 - kt) < e/4" for g1 k1 kt :: complex + proof (rule norm_triangle_half_l) + show "cmod (g1 - k1) < e/2" "cmod (kt - k1) < e/2" + using \e > 0\ that by (auto simp: norm_minus_commute intro: order_less_trans) + qed have "\d>0. \g1 g2. valid_path g1 \ valid_path g2 \ (\u\{0..1}. cmod (g1 u - k (t1, u)) < d \ cmod (g2 u - k (t2, u)) < d) \ linked_paths atends g1 g2 \ contour_integral g2 f = contour_integral g1 f" - apply (rule_tac x="e/4" in exI) using t t1 t2 ltd \e > 0\ - apply (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1) - done + by (rule_tac x="e/4" in exI) (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1) } then have "\e. 0 < e \ (\t1 t2. t1 \ {0..1} \ t2 \ {0..1} \ \t1 - t\ < e \ \t2 - t\ < e \ (\d. 0 < d \ (\g1 g2. valid_path g1 \ valid_path g2 \ (\u \ {0..1}. norm(g1 u - k((t1,u))) < d \ norm(g2 u - k((t2,u))) < d) \ linked_paths atends g1 g2 \ contour_integral g2 f = contour_integral g1 f)))" by (rule_tac x=d in exI) (simp add: \d > 0\) } then obtain ee where ee: "\t. t \ {0..1} \ ee t > 0 \ (\t1 t2. t1 \ {0..1} \ t2 \ {0..1} \ \t1 - t\ < ee t \ \t2 - t\ < ee t \ (\d. 0 < d \ (\g1 g2. valid_path g1 \ valid_path g2 \ (\u \ {0..1}. norm(g1 u - k((t1,u))) < d \ norm(g2 u - k((t2,u))) < d) \ linked_paths atends g1 g2 \ contour_integral g2 f = contour_integral g1 f)))" by metis - note ee_rule = ee [THEN conjunct2, rule_format] + note ee_rule = ee [THEN conjunct2, rule_format, of 0 0 0] define C where "C = (\t. ball t (ee t / 3)) ` {0..1}" obtain C' where C': "C' \ C" "finite C'" and C'01: "{0..1} \ \C'" proof (rule compactE [OF compact_interval]) show "{0..1} \ \C" using ee [THEN conjunct1] by (auto simp: C_def dist_norm) qed (use C_def in auto) define kk where "kk = {t \ {0..1}. ball t (ee t / 3) \ C'}" have kk01: "kk \ {0..1}" by (auto simp: kk_def) define e where "e = Min (ee ` kk)" have C'_eq: "C' = (\t. ball t (ee t / 3)) ` kk" using C' by (auto simp: kk_def C_def) have ee_pos[simp]: "\t. t \ {0..1} \ ee t > 0" by (simp add: kk_def ee) moreover have "finite kk" using \finite C'\ kk01 by (force simp: C'_eq inj_on_def ball_eq_ball_iff dest: ee_pos finite_imageD) moreover have "kk \ {}" using \{0..1} \ \C'\ C'_eq by force ultimately have "e > 0" using finite_less_Inf_iff [of "ee ` kk" 0] kk01 by (force simp: e_def) then obtain N::nat where "N > 0" and N: "1/N < e/3" by (meson divide_pos_pos nat_approx_posE zero_less_Suc zero_less_numeral) have e_le_ee: "\i. i \ kk \ e \ ee i" using \finite kk\ by (simp add: e_def Min_le_iff [of "ee ` kk"]) have plus: "\t \ kk. x \ ball t (ee t / 3)" if "x \ {0..1}" for x using C' subsetD [OF C'01 that] unfolding C'_eq by blast have [OF order_refl]: "\d. 0 < d \ (\j. valid_path j \ (\u \ {0..1}. norm(j u - k (n/N, u)) < d) \ linked_paths atends g j \ contour_integral j f = contour_integral g f)" if "n \ N" for n using that proof (induct n) - case 0 show ?case using ee_rule [of 0 0 0] - apply clarsimp - apply (rule_tac x=d in exI, safe) - by (metis diff_self vpg norm_zero) + case 0 show ?case + using ee_rule + by clarsimp (metis diff_self norm_eq_zero vpg) next case (Suc n) then have N01: "n/N \ {0..1}" "(Suc n)/N \ {0..1}" by auto then obtain t where t: "t \ kk" "n/N \ ball t (ee t / 3)" using plus [of "n/N"] by blast then have nN_less: "\n/N - t\ < ee t" by (simp add: dist_norm del: less_divide_eq_numeral1) have n'N_less: "\real (Suc n) / real N - t\ < ee t" using t N \N > 0\ e_le_ee [of t] by (simp add: dist_norm add_divide_distrib abs_diff_less_iff del: less_divide_eq_numeral1) (simp add: field_simps) have t01: "t \ {0..1}" using \kk \ {0..1}\ \t \ kk\ by blast obtain d1 where "d1 > 0" and d1: "\g1 g2. \valid_path g1; valid_path g2; \u\{0..1}. cmod (g1 u - k (n/N, u)) < d1 \ cmod (g2 u - k ((Suc n) / N, u)) < d1; linked_paths atends g1 g2\ \ contour_integral g2 f = contour_integral g1 f" using ee [THEN conjunct2, rule_format, OF t01 N01 nN_less n'N_less] by fastforce have "n \ N" using Suc.prems by auto with Suc.hyps obtain d2 where "d2 > 0" and d2: "\j. \valid_path j; \u\{0..1}. cmod (j u - k (n/N, u)) < d2; linked_paths atends g j\ \ contour_integral j f = contour_integral g f" - by auto - have "continuous_on {0..1} (k \ (\u. (n/N, u)))" - apply (rule continuous_intros continuous_on_subset [OF contk])+ + by auto + have "Pair (n/ N) ` {0..1} \ {0..1} \ {0..1}" using N01 by auto + then have "continuous_on {0..1} (k \ (\u. (n/N, u)))" + by (intro continuous_intros continuous_on_subset [OF contk]) then have pkn: "path (\u. k (n/N, u))" by (simp add: path_def) have min12: "min d1 d2 > 0" by (simp add: \0 < d1\ \0 < d2\) obtain p where "polynomial_function p" and psf: "pathstart p = pathstart (\u. k (n/N, u))" "pathfinish p = pathfinish (\u. k (n/N, u))" and pk_le: "\t. t\{0..1} \ cmod (p t - k (n/N, t)) < min d1 d2" using path_approx_polynomial_function [OF pkn min12] by blast then have vpp: "valid_path p" using valid_path_polynomial_function by blast have lpa: "linked_paths atends g p" by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf) show ?case proof (intro exI; safe) fix j assume "valid_path j" "linked_paths atends g j" and "\u\{0..1}. cmod (j u - k (real (Suc n) / real N, u)) < min d1 d2" then have "contour_integral j f = contour_integral p f" using pk_le N01(1) ksf by (force intro!: vpp d1 simp add: linked_paths_def psf) also have "... = contour_integral g f" using pk_le by (force intro!: vpp d2 lpa) finally show "contour_integral j f = contour_integral g f" . qed (simp add: \0 < d1\ \0 < d2\) qed then obtain d where "0 < d" "\j. valid_path j \ (\u \ {0..1}. norm(j u - k (1,u)) < d) \ linked_paths atends g j \ contour_integral j f = contour_integral g f" using \N>0\ by auto then have "linked_paths atends g h \ contour_integral h f = contour_integral g f" using \N>0\ vph by fastforce then show ?thesis by (simp add: pathsf) qed proposition Cauchy_theorem_homotopic_paths: - assumes hom: "homotopic_paths s g h" - and "open s" and f: "f holomorphic_on s" + assumes hom: "homotopic_paths S g h" + and "open S" and f: "f holomorphic_on S" and vpg: "valid_path g" and vph: "valid_path h" shows "contour_integral g f = contour_integral h f" - using Cauchy_theorem_homotopic [of True s g h] assms by simp + using Cauchy_theorem_homotopic [of True S g h] assms by simp proposition Cauchy_theorem_homotopic_loops: - assumes hom: "homotopic_loops s g h" - and "open s" and f: "f holomorphic_on s" + assumes hom: "homotopic_loops S g h" + and "open S" and f: "f holomorphic_on S" and vpg: "valid_path g" and vph: "valid_path h" shows "contour_integral g f = contour_integral h f" - using Cauchy_theorem_homotopic [of False s g h] assms by simp + using Cauchy_theorem_homotopic [of False S g h] assms by simp lemma has_contour_integral_newpath: "\(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f\ \ (f has_contour_integral y) g" using has_contour_integral_integral contour_integral_unique by auto lemma Cauchy_theorem_null_homotopic: - "\f holomorphic_on s; open s; valid_path g; homotopic_loops s g (linepath a a)\ \ (f has_contour_integral 0) g" - apply (rule has_contour_integral_newpath [where h = "linepath a a"], simp) - using contour_integrable_holomorphic_simple - apply (blast dest: holomorphic_on_imp_continuous_on homotopic_loops_imp_subset) - by (simp add: Cauchy_theorem_homotopic_loops) + "\f holomorphic_on S; open S; valid_path g; homotopic_loops S g (linepath a a)\ + \ (f has_contour_integral 0) g" + by (metis Cauchy_theorem_homotopic_loops contour_integrable_holomorphic_simple valid_path_linepath + contour_integral_trivial has_contour_integral_integral homotopic_loops_imp_subset) end \ No newline at end of file