Theory Cauchy_Integral_Theorem
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 (- ℝ⇩≤⇩0) x *⇩R Ln x) ∈ borel_measurable borel"
by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
have "(λx. if x ∈ ℝ⇩≤⇩0 then ln (-Re x) + 𝗂 * pi else indicator (-ℝ⇩≤⇩0) x *⇩R Ln x) ∈ borel →⇩M borel"
(is "?f ∈ _") by (rule measurable_If_set[OF _ cont]) auto
hence "(λx. if x = 0 then Ln 0 else ?f x) ∈ borel →⇩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)"
proof (rule has_contour_integral_split)
show "midpoint a b - a = (1/2) *⇩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) *⇩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)"
proof (rule Cauchy_theorem_primitive)
show "⋀x. x ∈ UNIV ⟹ ((λx. m / 2 * x⇧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 ‹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)+
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⇧2 / 4 ≤ cmod (pathint a c' + pathint c' b' + pathint b' a)" |
"e * K⇧2 / 4 ≤ cmod (pathint a' c' + pathint c' b + pathint b a')" |
"e * K⇧2 / 4 ≤ cmod (pathint a' c + pathint c b' + pathint b' a')" |
"e * K⇧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 ‹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))"
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‹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"
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 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}"
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')⇧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))⇧2
≤ (3 * K / 2 ^ n)⇧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))⇧2 ≤ e * (3 * K / 2 ^ n)⇧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 ‹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 *⇩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) *⇩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 *⇩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) *⇩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 *⇩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⟧
⟹ 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 *⇩R (x - d)" for x
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)
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 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 *⇩R (b - d)) - (a - e *⇩R (a - d)) - (b - a) = e *⇩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: "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<C›)
{ 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) *⇩R u - (1 - x) *⇩R d) + cmod (x *⇩R v - x *⇩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) *⇩R (u - d) + x *⇩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 ‹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)"
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)"
by (simp add: algebra_simps)
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 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))
≤ 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))
≤ 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 ‹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 ‹Version allowing finite number of exceptional points›
proposition 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 ‹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"
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 *⇩R a + v *⇩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"
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)) /⇩R cmod (y - x)) ─x→ 0"
by (simp add: Lim_at dist_norm inverse_eq_divide)
then have "(λy. (1 / cmod (y - x)) *⇩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
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;
⋀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"
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. (?pathint x y - f x * (y - x)) /⇩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)) *⇩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 ‹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 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:
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 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 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 ‹Generalize integrability to local primitives›
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
⟹ ∃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"
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) ⟶
(λ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
⟹ ∃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"
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"
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 ‹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: "