section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close>
text\<open>By John Harrison et al. Ported from HOL Light by L C Paulson (2015)\<close>
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\<open>The special case of midpoints used in the main quadrisection\<close>
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)"
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:
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\<open>A couple of special case lemmas that are useful below\<close>
lemma triangle_linear_has_chain_integral:
"((\x. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
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:
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:
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>\<open>tag unimportant\<close> \<open>The key quadrisection step\<close>
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' \<le> K/2 \<and> dist b' c' \<le> K/2 \<and> dist c' a' \<le> K/2 \<and>
e * (K/2)^2 \<le> 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)+
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 by (metis "*" norm_sum_lemma pathint_def)
then show ?thesis
proof cases
case 1 then have "?\ a c' b'"
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 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 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 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>\<open>tag unimportant\<close> \<open>Cauchy's theorem for triangles\<close>
lemma triangle_points_closer:
fixes a::complex
shows "\x \ convex hull {a,b,c}; y \ convex hull {a,b,c}\
\<Longrightarrow> norm(x - y) \<le> norm(a - b) \<or>
norm(x - y) \<le> norm(b - c) \<or>
norm(x - y) \<le> 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 \<in> convex hull {a,b,c} \<and> convex hull {a,b,c} \<subseteq> S
\<longrightarrow> norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f +
contour_integral(linepath c a) f)
\<le> 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\
\<Longrightarrow> a \<le> 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) (\<lambda>y. f y - f x - f' * (y-x)) +
contour_integral (linepath b c) (\<lambda>y. f y - f x - f' * (y-x)) +
contour_integral (linepath c a) (\<lambda>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
using f' xc S e
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\<open>Hence the most basic theorem for a triangle.\<close>
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"
proof qed (use At0 AtSuc in auto)
show ?thesis
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>\<open>tag unimportant\<close> 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} \<subseteq> convex hull {a,b,c} \<and>
dist x y \<le> K/2^n \<and> dist y z \<le> K/2^n \<and> dist z x \<le> K/2^n \<and>
norm(?pathint x y + ?pathint y z + ?pathint z x) \<ge> 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)) \<ge> 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}"
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'.
\<lbrakk>dist x' y' \<le> k; dist y' z' \<le> k; dist z' x' \<le> k;
x \<in> convex hull {x',y',z'};
convex hull {x',y',z'} \ convex hull {a,b,c}\
\<Longrightarrow>
cmod (?pathint x' y' + ?pathint y' z' + ?pathint z' x') * 10
\<le> 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
\<le> (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
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>\<open>tag unimportant\<close> \<open>Version needing function holomorphic in interior only\<close>
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
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"
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
by (metis (no_types, lifting) contour_integral_reverse_linepath eq_neg_iff_add_eq_0 minus_add_cancel)
qed
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: "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 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\
\<Longrightarrow> 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
have e: "0 < e" "e \ 1" "e \ d1 / (4 * C)" "e \ cmod y / 24 / C / B"
using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
have e_le_d1: "e * (4 * C) \ d1"
using e \<open>C>0\<close> 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 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 \<open>C>0\<close> diff_2C [of b a] ynz
by (auto simp: field_split_simps hull_inc)
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: \<open>0<C\<close>)
{ 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])
{ 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)"
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"
unfolding ll norm_mult scaleR_diff_right
using \<open>e>0\<close> 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))
\<le> B * (cmod y / 24 / C / B * 2 * C) + 2 * C * (cmod y / 24 / C)"
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 \<open>B>0\<close> diff_2C [of u v] uv by (auto simp: field_simps)
also have "\ \ cmod y"
using \<open>C>0\<close> \<open>B>0\<close> e by (simp add: field_simps)
finally show "cmod (shrink v - shrink u - (v - u)) \ cmod y / 24 / C / B * 2 * C"
using \<open>0 < B\<close> \<open>0 < C\<close> 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 \<open>C>0\<close> 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))
\<le> 2 * C * (cmod y / 24 / C)"
using uv C by (simp add: field_simps)
qed (use \<open>0 < B\<close> 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))
\<le> 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)"
by (simp add: algebra_simps)
have "norm (pathint (shrink u) (shrink v) - pathint u v)
\<le> (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 \<open>0 < B\<close> \<open>0 < C\<close>
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" .
} note * = this
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"
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"
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))
\<le> 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))
\<le> norm y / 2"
by (simp add: algebra_simps)
then
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 \<open>C > 0\<close> by auto
ultimately obtain \<delta> where "\<delta> > 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 \<open>C > 0\<close> ynz unfolding uniformly_continuous_on_def dist_norm by blast
hence False using *[of \<delta>] 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>\<open>tag unimportant\<close> \<open>Version allowing finite number of exceptional points\<close>
proposition\<^marker>\<open>tag unimportant\<close> 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 \<notin> 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>\<open>tag unimportant\<close> \<open>Cauchy's theorem for an open starlike set\<close>
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"
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
\<Longrightarrow> 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"
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"
by (simp add: Lim_at dist_norm inverse_eq_divide)
then have "(\y. (1 / cmod (y - x)) *\<^sub>R (?pathint a y - (?pathint a x + f x * (y - x)))) \x\ 0"
using \<open>open S\<close> 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
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;
\<And>x. x \<in> S - k \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
\<Longrightarrow> (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\
\<Longrightarrow> (f has_contour_integral 0) g"
using Cauchy_theorem_starlike [OF _ _ finite.emptyI]
by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at)
subsection\<open>Cauchy's theorem for a convex set\<close>
text\<open>For a convex set we can avoid assuming openness and boundary analyticity\<close>
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\
\<Longrightarrow> 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. (?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)
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
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 \<open>convex S\<close> 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: \<open>convex S\<close> 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 \<open>force+\<close>)
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 \<open>auto intro: holomorphic_on_imp_continuous_on\<close>)
corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_convex:
"\continuous_on S f; convex S; finite K;
\<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
\<Longrightarrow> (f has_contour_integral 0) g"
by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)
corollary Cauchy_theorem_convex_simple:
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\<open>In particular for a disc\<close>
corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_disc:
"\finite K; continuous_on (cball a e) f;
\<And>x. x \<in> ball a e - K \<Longrightarrow> f field_differentiable at x;
valid_path g; path_image g \<subseteq> cball a e;
pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
by (auto intro: Cauchy_theorem_convex)
corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_disc_simple:
"\f holomorphic_on (ball a e); valid_path g; path_image g \ ball a e;
pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
by (simp add: Cauchy_theorem_convex_simple)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Generalize integrability to local primitives\<close>
lemma contour_integral_local_primitive_lemma:
fixes f :: "complex\complex"
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
\<Longrightarrow> \<exists>d h. 0 < d \<and>
(\<forall>y. norm(y - x) < d \<longrightarrow> (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))"
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 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) \
(\<lambda>x. f (g x) * vector_derivative g (at x)) integrable_on {u..v}"
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
\<Longrightarrow> \<exists>d h. 0 < d \<and>
(\<forall>y. norm(y - x) < d \<longrightarrow> (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\<open>In particular if a function is holomorphic\<close>
lemma contour_integrable_holomorphic:
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"
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
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)"
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))"
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))"
using \<open>0 < d\<close> 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"
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:
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\<open>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.
\<close>
text\<open>A technical definition to avoid duplication of similar proofs,
for paths joined at the ends versus looping paths\<close>
definition linked_paths :: "bool \ (real \ 'a) \ (real \ 'a::topological_space) \ bool"
where "linked_paths atends g h ==
(if atends then pathstart h = pathstart g \<and> pathfinish h = pathfinish g
else pathfinish g = pathstart g \<and> pathfinish h = pathstart h)"
text\<open>This formulation covers two cases: \<^term>\<open>g\<close> and \<^term>\<open>h\<close> share their
start and end points; \<^term>\<open>g\<close> and \<^term>\<open>h\<close> both loop upon themselves.\<close>
lemma contour_integral_nearby:
assumes os: "open S" and p: "path p" "path_image p \ S"
shows "\d. 0 < d \
(\<forall>g h. valid_path g \<and> valid_path h \<and>
(\<forall>t \<in> {0..1}. norm(g t - p t) < d \<and> norm(h t - p t) < d) \<and>
linked_paths atends g h
\<longrightarrow> path_image g \<subseteq> S \<and> path_image h \<subseteq> S \<and>
(\<forall>f. f holomorphic_on S \<longrightarrow> 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"
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 \<open>0 < e\<close> zero_less_numeral)
then obtain N::nat where N: "N>0" "inverse N < d"
using real_arch_inverse [of d] by auto
show ?thesis
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.76 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
