Please indicate whether you will be providing relevance feedback on the first 10 results for this query by clicking on the button.

definition‹tag important› residue :: "(complex complex) complex complex" where
"residue f z = (SOME int. e>0. ε>0. ε<e
(f has_contour_integral 2*pi* 𝗂 *int) (circlepath z ε))"
lemma set_integral_complex_of_real:
"LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
unfolding set_lebesgue_integral_def
by (subst integral_complex_of_real[symmetric])
(auto intro!: Bochner_Integration.integral_cong split: split_indicator)
lemma base_residue:
assumes "open s" "zs" "r>0" and f_holo:"f holomorphic_on (s - {z})"
and r_cball:"cball z r s"
shows "(f has_contour_integral 2 * pi * 𝗂 * (residue f z)) (circlepath z r)"
proof -
obtain e where "e>0" and e_cball:"cball z e s"
using open_contains_cball[of s] ‹open s zs by auto
define c where "c 2 * pi * 𝗂"
define i where "i contour_integral (circlepath z e) f / c"
have "(f has_contour_integral c*i) (circlepath z ε)" when "ε>0" "ε<e" for ε
proof -
have "contour_integral (circlepath z e) f = contour_integral (circlepath z ε) f"
"f contour_integrable_on circlepath z ε"
"f contour_integrable_on circlepath z e"
using ε<e
by (intro contour_integral_circlepath_eq[OF ‹open s f_holo ε>0 _ e_cball],auto)+
then show ?thesis unfolding i_def c_def
by (auto intro:has_contour_integral_integral)
qed
then have "e>0. ε>0. ε<e (f has_contour_integral c * (residue f z)) (circlepath z ε)"
unfolding residue_def c_def
apply (rule_tac someI[of _ i],intro exI[where x=e])
by (auto simp add:e>0 c_def)
then obtain e' where "e'>0"
and e'_def:"ε>0. ε<e' (f has_contour_integral c * (residue f z)) (circlepath z ε)"
by auto
let ?int="λe. contour_integral (circlepath z e) f"
define ε where "ε Min {r,e'} / 2"
have "ε>0" "εr" "ε<e'" using r>0 e'>0 unfolding ε_def by auto
have "(f has_contour_integral c * (residue f z)) (circlepath z ε)"
using e'_def[rule_format,OF ε>0 ε<e'] .
then show ?thesis unfolding c_def
using contour_integral_circlepath_eq[OF ‹open s f_holo ε>0 εr r_cball]
by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z ε" "circlepath z r"])
qed
lemma residue_add:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
and g_holo:"g holomorphic_on s - {z}"
shows "residue (λz. f z + g z) z= residue f z + residue g z"
proof -
define c where "c 2 * pi * 𝗂"
define fg where "fg (λz. f z+g z)"
obtain e where "e>0" and e_cball:"cball z e s" using ‹open s zs
using open_contains_cball_eq by blast
have "(fg has_contour_integral c * residue fg z) (circlepath z e)"
unfolding fg_def using f_holo g_holo
apply (intro base_residue[OF ‹open s zs e>0 _ e_cball,folded c_def])
by (auto intro:holomorphic_intros)
moreover have "(fg has_contour_integral c*residue f z + c* residue g z) (circlepath z e)"
unfolding fg_def using f_holo g_holo
by (auto intro: has_contour_integral_add base_residue[OF ‹open s zs e>0 _ e_cball,folded c_def])
ultimately have "c*(residue f z + residue g z) = c * residue fg z"
using has_contour_integral_unique by (auto simp add:distrib_left)
thus ?thesis unfolding fg_def
by (auto simp add:c_def)
qed
lemma residue_holo:
assumes "open s" "z s" and f_holo: "f holomorphic_on s"
shows "residue f z = 0"
proof -
define c where "c 2 * pi * 𝗂"
obtain e where "e>0" and e_cball:"cball z e s" using ‹open s zs
using open_contains_cball_eq by blast
have "(f has_contour_integral c*residue f z) (circlepath z e)"
using f_holo
by (auto intro: base_residue[OF ‹open s zs e>0 _ e_cball,folded c_def])
moreover have "(f has_contour_integral 0) (circlepath z e)"
using f_holo e_cball e>0
by (auto intro: Cauchy_theorem_convex_simple[of _ "cball z e"])
ultimately have "c*residue f z =0"
using has_contour_integral_unique by blast
thus ?thesis unfolding c_def by auto
qed
lemma residue_div:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λz. (f z) / c) z= residue f z / c "
using residue_lmul[OF assms,of "1/c"] by (auto simp add:algebra_simps)
lemma residue_neg:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λz. - (f z)) z= - residue f z"
using residue_lmul[OF assms,of "-1"] by auto
lemma residue_const:"residue (λ_. c) z = 0"
by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros)
lemma residue_cong:
assumes eq: "eventually (λz. f z = g z) (at z)" and "z = z'"
shows "residue f z = residue g z'"
proof -
from assms have eq': "eventually (λz. g z = f z) (at z)"
by (simp add: eq_commute)
let ?P = "λf c e. (ε>0. ε < e
(f has_contour_integral of_real (2 * pi) * 𝗂 * c) (circlepath z ε))"

have "residue f z = residue g z" unfolding residue_def
proof (rule Eps_cong)
fix c :: complex
have "e>0. ?P g c e"
if "e>0. ?P f c e" and "eventually (λz. f z = g z) (at z)" for f g
proof -
from that(1) obtain e where e: "e > 0" "?P f c e"
by blast
from that(2) obtain e' where e': "e' > 0" "z'. z' z dist z' z < e' f z' = g z'"
unfolding eventually_at by blast
have "?P g c (min e e')"
proof (intro allI exI impI, goal_cases)
case (1 ε)
hence "(f has_contour_integral of_real (2 * pi) * 𝗂 * c) (circlepath z ε)"
using e(2) by auto
thus ?case
proof (rule has_contour_integral_eq)
fix z' assume "z' path_image (circlepath z ε)"
hence "dist z' z < e'" and "z' z"
using 1 by (auto simp: dist_commute)
with e'(2)[of z'] show "f z' = g z'" by simp
qed
qed
moreover from e and e' have "min e e' > 0" by auto
ultimately show ?thesis by blast
qed
from this[OF _ eq] and this[OF _ eq']
show "(e>0. ?P f c e) (e>0. ?P g c e)"
by blast
qed
with assms show ?thesis by simp
qed
lemma residue_rmul:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λz. (f z) * c) z= residue f z * c"
using residue_lmul[OF assms,of c] by (auto simp add:algebra_simps)
lemma residue_diff:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
and g_holo:"g holomorphic_on s - {z}"
shows "residue (λz. f z - g z) z= residue f z - residue g z"
using residue_add[OF assms(1,2,3),of "λz. - g z"] residue_neg[OF assms(1,2,4)]
by (auto intro:holomorphic_intros g_holo)
lemma residue_lmul:
assumes "open s" "z s" and f_holo: "f holomorphic_on s - {z}"
shows "residue (λz. c * (f z)) z= c * residue f z"
proof (cases "c=0")
case True
thus ?thesis using residue_const by auto
next
case False
define c' where "c' 2 * pi * 𝗂"
define f' where "f' (λz. c * (f z))"
obtain e where "e>0" and e_cball:"cball z e s" using ‹open s zs
using open_contains_cball_eq by blast
have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
unfolding f'_def using f_holo
apply (intro base_residue[OF ‹open s zs e>0 _ e_cball,folded c'_def])
by (auto intro:holomorphic_intros)
moreover have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)"
unfolding f'_def using f_holo
by (auto intro: has_contour_integral_lmul
base_residue[OF ‹open s zs e>0 _ e_cball,folded c'_def])
ultimately have "c' * residue f' z = c * (c' * residue f z)"
using has_contour_integral_unique by auto
thus ?thesis unfolding f'_def c'_def using False
by (auto simp add:field_simps)
qed
lemma residue_simple:
assumes "open s" "zs" and f_holo:"f holomorphic_on s"
shows "residue (λw. f w / (w - z)) z = f z"
proof -
define c where "c 2 * pi * 𝗂"
define f' where "f' λw. f w / (w - z)"
obtain e where "e>0" and e_cball:"cball z e s" using ‹open s zs
using open_contains_cball_eq by blast
have "(f' has_contour_integral c * f z) (circlepath z e)"
unfolding f'_def c_def using e>0 f_holo e_cball
by (auto intro!: Cauchy_integral_circlepath_simple holomorphic_intros)
moreover have "(f' has_contour_integral c * residue f' z) (circlepath z e)"
unfolding f'_def using f_holo
apply (intro base_residue[OF ‹open s zs e>0 _ e_cball,folded c_def])
by (auto intro!:holomorphic_intros)
ultimately have "c * f z = c * residue f' z"
using has_contour_integral_unique by blast
thus ?thesis unfolding c_def f'_def by auto
qed
lemma residue_simple_pole:
assumes "isolated_singularity_at f z0"
assumes "is_pole f z0" "zorder f z0 = - 1"
shows "residue f z0 = zor_poly f z0 z0"
using assms by (subst residue_pole_order) simp_all
lemma residue_pole_order:
fixes f::"complex complex" and z::complex
defines "n nat (- zorder f z)" and "h zor_poly f z"
assumes f_iso:"isolated_singularity_at f z"
and pole:"is_pole f z"
shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))"
proof -
define g where "g λx. if x=z then 0 else inverse (f x)"
obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}"
using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast
obtain r where "0 < n" "0 < r" and r_cball:"cball z r ball z e" and h_holo: "h holomorphic_on cball z r"
and h_divide:"(wcball z r. (wz f w = h w / (w - z) ^ n) h w 0)"
proof -
obtain r where r:"zorder f z < 0" "h z 0" "r>0" "cball z r ball z e" "h holomorphic_on cball z r"
"(wcball z r - {z}. f w = h w / (w - z) ^ n h w 0)"
using zorder_exist_pole[OF f_holo,simplified,OF ‹is_pole f z,folded n_def h_def] by auto
have "n>0" using ‹zorder f z < 0 unfolding n_def by simp
moreover have "(wcball z r. (wz f w = h w / (w - z) ^ n) h w 0)"
using h z0 r(6) by blast
ultimately show ?thesis using r(3,4,5) that by blast
qed
have r_nonzero:"w. w ball z r - {z} f w 0"
using h_divide by simp
define c where "c 2 * pi * 𝗂"
define der_f where "der_f ((deriv ^^ (n - 1)) h z / fact (n-1))"
define h' where "h' λu. h u / (u - z) ^ n"
have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)"
unfolding h'_def
proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1",
folded c_def Suc_pred'[OF n>0]])
show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp
show "h holomorphic_on ball z r" using h_holo by auto
show " z ball z r" using r>0 by auto
qed
then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto
then have "(f has_contour_integral c * der_f) (circlepath z r)"
proof (elim has_contour_integral_eq)
fix x assume "x path_image (circlepath z r)"
hence "xcball z r - {z}" using r>0 by auto
then show "h' x = f x" using h_divide unfolding h'_def by auto
qed
moreover have "(f has_contour_integral c * residue f z) (circlepath z r)"
using base_residue[of ‹ball z e z,simplified,OF r>0 f_holo r_cball,folded c_def]
unfolding c_def by simp
ultimately have "c * der_f = c * residue f z" using has_contour_integral_unique by blast
hence "der_f = residue f z" unfolding c_def by auto
thus ?thesis unfolding der_f_def by auto
qed
lemma residue_holomorphic_over_power:
assumes "open A" "z0 A" "f holomorphic_on A"
shows "residue (λz. f z / (z - z0) ^ Suc n) z0 = (deriv ^^ n) f z0 / fact n"
proof -
let ?f = "λz. f z / (z - z0) ^ Suc n"
from assms(1,2) obtain r where r: "r > 0" "cball z0 r A"
by (auto simp: open_contains_cball)
have "(?f has_contour_integral 2 * pi * 𝗂 * residue ?f z0) (circlepath z0 r)"
using r assms by (intro base_residue[of A]) (auto intro!: holomorphic_intros)
moreover have "(?f has_contour_integral 2 * pi * 𝗂 / fact n * (deriv ^^ n) f z0) (circlepath z0 r)"
using assms r
by (intro Cauchy_has_contour_integral_higher_derivative_circlepath)
(auto intro!: holomorphic_on_subset[OF assms(3)] holomorphic_on_imp_continuous_on)
ultimately have "2 * pi * 𝗂 * residue ?f z0 = 2 * pi * 𝗂 / fact n * (deriv ^^ n) f z0"
by (rule has_contour_integral_unique)
thus ?thesis by (simp add: field_simps)
qed
lemma residue_simple_pole_limit:
assumes "isolated_singularity_at f z0"
assumes "is_pole f z0" "zorder f z0 = - 1"
assumes "((λx. f (g x) * (g x - z0)) c) F"
assumes "filterlim g (at z0) F" "F bot"
shows "residue f z0 = c"
proof -
have "residue f z0 = zor_poly f z0 z0"
by (rule residue_simple_pole assms)+
also have " = c"
apply (rule zor_poly_pole_eqI)
using assms by auto
finally show ?thesis .
qed
theorem Residue_theorem:
fixes s pts::"complex set" and f::"complex complex"
and g::"real complex"
assumes "open s" "connected s" "finite pts" and
holo:"f holomorphic_on s-pts" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
"path_image g s-pts" and
homo:"z. (z s) winding_number g z = 0"
shows "contour_integral g f = 2 * pi * 𝗂 *(ppts. winding_number g p * residue f p)"
proof -
define c where "c 2 * pi * 𝗂"
obtain h where avoid:"ps. h p>0 (wcball p (h p). ws (wp w pts))"
using finite_cball_avoid[OF ‹open s ‹finite pts] by metis
have "contour_integral g f
= (ppts. winding_number g p * contour_integral (circlepath p (h p)) f)"

using Cauchy_theorem_singularities[OF assms avoid] .
also have "... = (ppts. c * winding_number g p * residue f p)"
proof (intro sum.cong)
show "pts = pts" by simp
next
fix x assume "x pts"
show "winding_number g x * contour_integral (circlepath x (h x)) f
= c * winding_number g x * residue f x"

proof (cases "xs")
case False
then have "winding_number g x=0" using homo by auto
thus ?thesis by auto
next
case True
have "contour_integral (circlepath x (h x)) f = c* residue f x"
using xpts ‹finite pts avoid[rule_format,OF True]
apply (intro base_residue[of "s-(pts-{x})",THEN contour_integral_unique,folded c_def])
by (auto intro:holomorphic_on_subset[OF holo] open_Diff[OF ‹open s finite_imp_closed])
then show ?thesis by auto
qed
qed
also have "... = c * (ppts. winding_number g p * residue f p)"
by (simp add: sum_distrib_left algebra_simps)
finally show ?thesis unfolding c_def .
qed
lemma series_differentiable_comparison_complex:
fixes S :: "complex set"
assumes S: "open S"
and hfd: "n x. x S f n field_differentiable (at x)"
and to_g: "x. x S d h. 0 < d summable h range h 0 (F n in sequentially. yball x d S. cmod(f n y) cmod (h n))"
obtains g where "x S. ((λn. f n x) sums g x) g field_differentiable (at x)"
proof -
have hfd': "n x. x S (f n has_field_derivative deriv (f n) x) (at x)"
using hfd field_differentiable_derivI by blast
have "g g'. x S. ((λn. f n x) sums g x) ((λn. deriv (f n) x) sums g' x) (g has_field_derivative g' x) (at x)"
by (metis series_and_derivative_comparison_complex [OF S hfd' to_g])
then show ?thesis
using field_differentiable_def that by blast
qed

text‹In particular, a power series is analytic inside circle of convergence.›
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 series_and_derivative_comparison_complex:
fixes S :: "complex set"
assumes S: "open S"
and hfd: "n x. x S (f n has_field_derivative f' n x) (at x)"
and to_g: "x. x S d h. 0 < d summable h range h 0 (F n in sequentially. yball x d S. cmod(f n y) cmod (h n))"
shows "g g'. x S. ((λn. f n x) sums g x) ((λn. f' n x) sums g' x) (g has_field_derivative g' x) (at x)"
apply (rule series_and_derivative_comparison_local [OF S hfd], assumption)
apply (rule ex_forward [OF to_g], assumption)
apply (erule exE)
apply (rule_tac x="Re h" in exI)
apply (force simp: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
done

text‹Sometimes convenient to compare with a complex series of positive reals. (?)›
theorem residue_fps_expansion_over_power_at_0:
assumes "f has_fps_expansion F"
shows "residue (λz. f z / z ^ Suc n) 0 = fps_nth F n"
proof -
from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
have "residue (λz. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
using assms s unfolding has_fps_expansion_def
by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
also from assms have " = fps_nth F n"
by (subst fps_nth_fps_expansion) auto
finally show ?thesis by simp
qed
lemma contour_integral_nearby:
assumes os: "open S" and p: "path p" "path_image p S"
shows "d. 0 < d
(g h. valid_path g valid_path h
(t {0..1}. norm(g t - p t) < d norm(h t - p t) < d)
linked_paths atends g h
path_image g S path_image h S
(f. f holomorphic_on S contour_integral h f = contour_integral g f))"

proof -
have "z. e. z path_image p 0 < e ball z e S"
using open_contains_ball os p(2) by blast
then obtain ee where ee: "z. z path_image p 0 < ee z ball z (ee z) S"
by metis
define cover where "cover = (λz. ball z (ee z/3)) ` (path_image p)"
have "compact (path_image p)"
by (metis p(1) compact_path_image)
moreover have "path_image p (cpath_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 0 < e zero_less_numeral)
then obtain N::nat where N: "N>0" "inverse N < d"
using real_arch_inverse [of d] by auto
show ?thesis
proof (intro exI conjI allI; clarify?)
show "e/3 > 0"
using 0 < e by simp
fix g h
assume g: "valid_path g" and ghp: "t{0..1}. cmod (g t - p t) < e / 3 cmod (h t - p t) < e / 3"
and h: "valid_path h"
and joins: "linked_paths atends g h"
{ fix t::real
assume t: "0 t" "t 1"
then obtain u where u: "u k" and ptu: "p t ball(p u) (ee(p u) / 3)"
using ‹path_image p D D_eq by (force simp: path_image_def)
then have ele: "e ee (p u)" using fin_eep
by (simp add: e_def)
have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3"
using ghp t by auto
with ele have "cmod (g t - p t) < ee (p u) / 3"
"cmod (h t - p t) < ee (p u) / 3"
by linarith+
then have "g t ball(p u) (ee(p u))" "h t ball(p u) (ee(p u))"
using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"]
norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u
by (force simp: dist_norm ball_def norm_minus_commute)+
then have "g t S" "h t S" using ee u k
by (auto simp: path_image_def ball_def)
}
then have ghs: "path_image g S" "path_image h S"
by (auto simp: path_image_def)
moreover
{ fix f
assume fhols: "f holomorphic_on S"
then have fpa: "f contour_integrable_on g" "f contour_integrable_on h"
using g ghs h holomorphic_on_imp_continuous_on os contour_integrable_holomorphic_simple
by blast+
have contf: "continuous_on S f"
by (simp add: fhols holomorphic_on_imp_continuous_on)
{ fix z
assume z: "z path_image p"
have "f holomorphic_on ball z (ee z)"
using fhols ee z holomorphic_on_subset by blast
then have "ff. (w ball z (ee z). (ff has_field_derivative f w) (at w))"
using holomorphic_convex_primitive [of "ball z (ee z)" "{}" f, simplified]
by (metis open_ball at_within_open holomorphic_on_def holomorphic_on_imp_continuous_on mem_ball)
}
then obtain ff where ff:
"z w. z path_image p; w ball z (ee z) (ff z has_field_derivative f w) (at w)"
by metis
{ fix n
assume n: "n N"
then have "contour_integral(subpath 0 (n/N) h) f - contour_integral(subpath 0 (n/N) g) f =
contour_integral(linepath (g(n/N)) (h(n/N))) f - contour_integral(linepath (g 0) (h 0)) f"

proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
obtain t where t: "t k" and "p (n/N) ball(p t) (ee(p t) / 3)"
using ‹path_image p D [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
by (force simp: path_image_def)
then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3"
by (simp add: dist_norm)
have e3le: "e/3 ee (p t) / 3" using fin_eep t
by (simp add: e_def)
{ fix x
assume x: "n/N x" "x (1 + n)/N"
then have nN01: "0 n/N" "(1 + n)/N 1"
using Suc.prems by auto
then have x01: "0 x" "x 1"
using x by linarith+
have "cmod (p t - p x) < ee (p t) / 3 + e/3"
proof (rule norm_diff_triangle_less [OF ptu de])
show "¦real n / real N - x¦ < d"
using x N by (auto simp: field_simps)
qed (use x01 Suc.prems in auto)
then have ptx: "cmod (p t - p x) < 2*ee (p t)/3"
using e3le eepi [OF t] by simp
have "cmod (p t - g x) < 2*ee (p t)/3 + e/3"
using ghp x01
by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx])
also have " ee (p t)"
using e3le eepi [OF t] by simp
finally have gg: "cmod (p t - g x) < ee (p t)" .
have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 "
using ghp x01
by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx])
also have " ee (p t)"
using e3le eepi [OF t] by simp
finally have "cmod (p t - g x) < ee (p t)" "cmod (p t - h x) < ee (p t)"
using gg by auto
} note ptgh_ee = this
have "closed_segment (g (n/N)) (h (n/N)) = path_image (linepath (h (n/N)) (g (n/N)))"
by (simp add: closed_segment_commute)
also have pi_hgn: " ball (p t) (ee (p t))"
using ptgh_ee [of "n/N"] Suc.prems
by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) S"
using ee pi t by blast
have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N))) ball (p t) (ee (p t))"
using ptgh_ee [of "(1+n)/N"] Suc.prems
by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) S"
using N>0 Suc.prems ee pi t
by (auto simp: Path_Connected.path_image_join field_simps)
have pi_subset_ball:
"path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
ball (p t) (ee (p t))"

proof (intro subset_path_image_join pi_hgn pi_ghn')
show "path_image (subpath (n/N) ((1+n) / N) g) ball (p t) (ee (p t))"
"path_image (subpath ((1+n) / N) (n/N) h) ball (p t) (ee (p t))"
using N>0 Suc.prems
by (auto simp: path_image_subpath dist_norm field_simps ptgh_ee)
qed
have pi0: "(f has_contour_integral 0)
(subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))"

proof (rule Cauchy_theorem_primitive)
show "x. x ball (p t) (ee (p t))
(ff (p t) has_field_derivative f x) (at x within ball (p t) (ee (p t)))"

by (metis ff open_ball at_within_open pi t)
qed (use Suc.prems pi_subset_ball in simp_all add: valid_path_subpath g h›)
have fpa1: "f contour_integrable_on subpath (n/N) (real (Suc n) / real N) g"
using Suc.prems by (simp add: contour_integrable_subpath g fpa)
have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))"
using gh_n's
by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
have fpa3: "f contour_integrable_on linepath (h (n/N)) (g (n/N))"
using gh_ns
by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f +
contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f +
contour_integral (subpath ((Suc n) / N) (n/N) h) f +
contour_integral (linepath (h (n/N)) (g (n/N))) f = 0"

using contour_integral_unique [OF pi0] Suc.prems
by (simp add: g h fpa valid_path_subpath contour_integrable_subpath
fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc)
have *: "hn he hn' gn gd gn' hgn ghn gh0 ghn'.
hn - gn = ghn - gh0;
gd + ghn' + he + hgn = (0::complex);
hn - he = hn'; gn + gd = gn'; hgn = -ghn hn' - gn' = ghn' - gh0"

by (auto simp: algebra_simps)
have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f"

unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"]
using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath)
also have " = contour_integral (subpath 0 ((Suc n) / N) h) f"
using Suc.prems by (simp add: contour_integral_subpath_combine h fpa)
finally have pi0_eq:
"contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
contour_integral (subpath 0 ((Suc n) / N) h) f"
.
show ?case
proof (rule * [OF Suc.hyps eq0 pi0_eq])
show "contour_integral (subpath 0 (n/N) g) f +
contour_integral (subpath (n/N) ((Suc n) / N) g) f =
contour_integral (subpath 0 ((Suc n) / N) g) f"

using Suc.prems contour_integral_subpath_combine fpa(1) g by auto
show "contour_integral (linepath (h (n/N)) (g (n/N))) f = - contour_integral (linepath (g (n/N)) (h (n/N))) f"
by (metis contour_integral_unique fpa3 has_contour_integral_integral has_contour_integral_reverse_linepath)
qed (use Suc.prems in auto)
qed
} note ind = this
have "contour_integral h f = contour_integral g f"
using ind [OF order_refl] N joins
by (simp add: linked_paths_def pathstart_def pathfinish_def split: if_split_asm)
}
ultimately
show "path_image g S path_image h S (f. f holomorphic_on S contour_integral h f = contour_integral g f)"
by metis
qed
qed
lemma 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›
theorem Cauchy_integral_circlepath:
assumes contf: "continuous_on (cball z r) f" and holf: "f holomorphic_on (ball z r)" and wz: "norm(w - z) < r"
shows "((λu. f u/(u - w)) has_contour_integral (2 * of_real pi * 𝗂 * f w))
(circlepath z r)"

proof -
have "r > 0"
using assms le_less_trans norm_ge_zero by blast
have "((λu. f u / (u - w)) has_contour_integral (2 * pi) * 𝗂 * winding_number (circlepath z r) w * f w)
(circlepath z r)"

proof (rule Cauchy_integral_formula_weak [where S = "cball z r" and k = "{}"])
show "x. x interior (cball z r) - {}
f field_differentiable at x"

using holf holomorphic_on_imp_differentiable_at by auto
have "w sphere z r"
by simp (metis dist_commute dist_norm not_le order_refl wz)
then show "path_image (circlepath z r) cball z r - {w}"
using r > 0 by (auto simp add: cball_def sphere_def)
qed (use wz in simp_all add: dist_norm norm_minus_commute contf›)
then show ?thesis
by (simp add: winding_number_circlepath assms)
qed
lemma contour_integral_circlepath_eq:
assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1e2"
and e2_cball:"cball z e2 s"
shows
"f contour_integrable_on circlepath z e1"
"f contour_integrable_on circlepath z e2"
"contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
proof -
define l where "l linepath (z+e2) (z+e1)"
have [simp]:"valid_path l" "pathstart l=z+e2" "pathfinish l=z+e1" unfolding l_def by auto
have "e2>0" using e1>0 e1e2 by auto
have zl_img:"zpath_image l"
proof
assume "z path_image l"
then have "e2 cmod (e2 - e1)"
using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] e1>0 e2>0 unfolding l_def
by (auto simp add:closed_segment_commute)
thus False using e2>0 e1>0 e1e2
apply (subst (asm) norm_of_real)
by auto
qed
define g where "g circlepath z e2 +++ l +++ reversepath (circlepath z e1) +++ reversepath l"
show [simp]: "f contour_integrable_on circlepath z e2" "f contour_integrable_on (circlepath z e1)"
proof -
show "f contour_integrable_on circlepath z e2"
apply (intro contour_integrable_continuous_circlepath[OF
continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
using e2>0 e2_cball by auto
show "f contour_integrable_on (circlepath z e1)"
apply (intro contour_integrable_continuous_circlepath[OF
continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
using e1>0 e1e2 e2_cball by auto
qed
have [simp]:"f contour_integrable_on l"
proof -
have "closed_segment (z + e2) (z + e1) cball z e2" using e2>0 e1>0 e1e2
by (intro closed_segment_subset,auto simp add:dist_norm)
hence "closed_segment (z + e2) (z + e1) s - {z}" using zl_img e2_cball unfolding l_def
by auto
then show "f contour_integrable_on l" unfolding l_def
apply (intro contour_integrable_continuous_linepath[OF
continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]])
by auto
qed
let ?ig="λg. contour_integral g f"
have "(f has_contour_integral 0) g"
proof (rule Cauchy_theorem_global[OF _ f_holo])
show "open (s - {z})" using ‹open s by auto
show "valid_path g" unfolding g_def l_def by auto
show "pathfinish g = pathstart g" unfolding g_def l_def by auto
next
have path_img:"path_image g cball z e2"
proof -
have "closed_segment (z + e2) (z + e1) cball z e2" using e2>0 e1>0 e1e2
by (intro closed_segment_subset,auto simp add:dist_norm)
moreover have "sphere z ¦e1¦ cball z e2" using e2>0 e1e2 e1>0 by auto
ultimately show ?thesis unfolding g_def l_def using e2>0
by (simp add: path_image_join closed_segment_commute)
qed
show "path_image g s - {z}"
proof -
have "zpath_image g" using zl_img
unfolding g_def l_def by (auto simp add: path_image_join closed_segment_commute)
moreover note ‹cball z e2 s and path_img
ultimately show ?thesis by auto
qed
show "winding_number g w = 0" when"w s - {z}" for w
proof -
have "winding_number g w = 0" when "ws" using that e2_cball
apply (intro winding_number_zero_outside[OF _ _ _ _ path_img])
by (auto simp add:g_def l_def)
moreover have "winding_number g z=0"
proof -
let ?Wz="λg. winding_number g z"
have "?Wz g = ?Wz (circlepath z e2) + ?Wz l + ?Wz (reversepath (circlepath z e1))
+ ?Wz (reversepath l)"

using e2>0 e1>0 zl_img unfolding g_def l_def
by (subst winding_number_join,auto simp add:path_image_join closed_segment_commute)+
also have "... = ?Wz (circlepath z e2) + ?Wz (reversepath (circlepath z e1))"
using zl_img
apply (subst (2) winding_number_reversepath)
by (auto simp add:l_def closed_segment_commute)
also have "... = 0"
proof -
have "?Wz (circlepath z e2) = 1" using e2>0
by (auto intro: winding_number_circlepath_centre)
moreover have "?Wz (reversepath (circlepath z e1)) = -1" using e1>0
apply (subst winding_number_reversepath)
by (auto intro: winding_number_circlepath_centre)
ultimately show ?thesis by auto
qed
finally show ?thesis .
qed
ultimately show ?thesis using that by auto
qed
qed
then have "0 = ?ig g" using contour_integral_unique by simp
also have "... = ?ig (circlepath z e2) + ?ig l + ?ig (reversepath (circlepath z e1))
+ ?ig (reversepath l)"

unfolding g_def
by (auto simp add:contour_integrable_reversepath_eq)
also have "... = ?ig (circlepath z e2) - ?ig (circlepath z e1)"
by (auto simp add:contour_integral_reversepath)
finally show "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f"
by simp
qed
lemma contour_integral_bound_exists:
assumes S: "open S"
and g: "valid_path g"
and pag: "path_image g S"
shows "L. 0 < L
(f B. f holomorphic_on S (z S. norm(f z) B)
norm(contour_integral g f) L*B)"

proof -
have "path g" using g
by (simp add: valid_path_imp_path)
then obtain d::real and p
where d: "0 < d"
and p: "polynomial_function p" "path_image p S"
and pi: "f. f holomorphic_on S contour_integral g f = contour_integral p f"
using contour_integral_nearby_ends [OF S ‹path g pag]
by (metis cancel_comm_monoid_add_class.diff_cancel g norm_zero path_approx_polynomial_function valid_path_polynomial_function)
then obtain p' where p': "polynomial_function p'"
"x. (p has_vector_derivative (p' x)) (at x)"
by (blast intro: has_vector_derivative_polynomial_function that)
then have "bounded(p' ` {0..1})"
using continuous_on_polymonial_function
by (force simp: intro!: compact_imp_bounded compact_continuous_image)
then obtain L where L: "L>0" and nop': "x. 0 x; x 1 norm (p' x) L"
by (force simp: bounded_pos)
{ fix f B
assume f: "f holomorphic_on S" and B: "z. zS cmod (f z) B"
then have "f contour_integrable_on p valid_path p"
using p S
by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
moreover have "cmod (vector_derivative p (at x)) * cmod (f (p x)) L * B" if "0 x" "x 1" for x
proof (rule mult_mono)
show "cmod (vector_derivative p (at x)) L"
by (metis nop' p'(2) that vector_derivative_at)
show "cmod (f (p x)) B"
by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that)
qed (use L>0 in auto)
ultimately
have "cmod (integral {0..1} (λx. f (p x) * vector_derivative p (at x))) L * B"
by (intro order_trans [OF integral_norm_bound_integral])
(auto simp: mult.commute norm_mult contour_integrable_on)
then have "cmod (contour_integral g f) L * B"
using contour_integral_integral f pi by presburger
} then
show ?thesis using L > 0
by (intro exI[of _ L]) auto
qed
corollary Cauchy_contour_integral_circlepath:
assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w ball z r"
shows "contour_integral(circlepath z r) (λu. f u/(u - w)^(Suc k)) = (2 * pi * 𝗂) * (deriv ^^ k) f w / (fact k)"
by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])
theorem Cauchy_integral_formula_global:
assumes S: "open S" and holf: "f holomorphic_on S"
and z: "z S" and vpg: "valid_path γ"
and pasz: "path_image γ S - {z}" and loop: "pathfinish γ = pathstart γ"
and zero: "w. w S winding_number γ w = 0"
shows "((λw. f w / (w - z)) has_contour_integral (2*pi * 𝗂 * winding_number γ z * f z)) γ"
proof -
have "path γ" using vpg by (blast intro: valid_path_imp_path)
have hols: "(λw. f w / (w - z)) holomorphic_on S - {z}" "(λw. 1 / (w - z)) holomorphic_on S - {z}"
by (rule holomorphic_intros holomorphic_on_subset [OF holf] | force)+
then have cint_fw: "(λw. f w / (w - z)) contour_integrable_on γ"
by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete S vpg pasz)
obtain d where "d>0"
and d: "g h. valid_path g; valid_path h; t{0..1}. cmod (g t - γ t) < d cmod (h t - γ t) < d;
pathstart h = pathstart g pathfinish h = pathfinish g
path_image h S - {z} (f. f holomorphic_on S - {z} contour_integral h f = contour_integral g f)"

using contour_integral_nearby_ends [OF _ ‹path γ pasz] S by (simp add: open_Diff) metis
obtain p where polyp: "polynomial_function p"
and ps: "pathstart p = pathstart γ" and pf: "pathfinish p = pathfinish γ" and led: "t{0..1}. cmod (p t - γ t) < d"
using path_approx_polynomial_function [OF ‹path γ d > 0] by metis
then have ploop: "pathfinish p = pathstart p" using loop by auto
have vpp: "valid_path p" using polyp valid_path_polynomial_function by blast
have [simp]: "z path_image γ" using pasz by blast
have paps: "path_image p S - {z}" and cint_eq: "(f. f holomorphic_on S - {z} contour_integral p f = contour_integral γ f)"
using pf ps led d [OF vpg vpp] d > 0 by auto
have wn_eq: "winding_number p z = winding_number γ z"
using vpp paps
by (simp add: subset_Diff_insert vpg valid_path_polynomial_function winding_number_valid_path cint_eq hols)
have "winding_number p w = winding_number γ w" if "w S" for w
proof -
have hol: "(λv. 1 / (v - w)) holomorphic_on S - {z}"
using that by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
have "w path_image p" "w path_image γ" using paps pasz that by auto
then show ?thesis
using vpp vpg by (simp add: subset_Diff_insert valid_path_polynomial_function winding_number_valid_path cint_eq [OF hol])
qed
then have wn0: "w. w S winding_number p w = 0"
by (simp add: zero)
show ?thesis
using Cauchy_integral_formula_global_weak [OF S holf z polyp paps ploop wn0] hols
by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
qed
lemma contour_integral_local_primitive_lemma:
fixes f :: "complexcomplex"
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 has_contour_integral_newpath:
"(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f
(f has_contour_integral y) g"

using has_contour_integral_integral contour_integral_unique by auto
lemma 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 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)
corollary‹tag unimportant› Cauchy_integral_circlepath_simple:
assumes "f holomorphic_on cball z r" "norm(w - z) < r"
shows "((λu. f u/(u - w)) has_contour_integral (2 * of_real pi * 𝗂 * f w))
(circlepath z r)"

using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)
lemma Cauchy_derivative_integral_circlepath:
assumes contf: "continuous_on (cball z r) f"
and holf: "f holomorphic_on ball z r"
and w: "w ball z r"
shows "(λu. f u/(u - w)^2) contour_integrable_on (circlepath z r)"
(is "?thes1")
and "(f has_field_derivative (1 / (2 * of_real pi * 𝗂) * contour_integral(circlepath z r) (λu. f u / (u - w)^2))) (at w)"
(is "?thes2")
proof -
have [simp]: "r 0" using w
using ball_eq_empty by fastforce
have f: "continuous_on (path_image (circlepath z r)) f"
by (rule continuous_on_subset [OF contf]) (force simp: cball_def sphere_def)
have int: "w. dist z w < r
((λu. f u / (u - w)) has_contour_integral (λx. 2 * of_real pi * 𝗂 * f x) w) (circlepath z r)"

by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
show ?thes1
apply (simp add: power2_eq_square)
apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1, simplified])
apply (blast intro: int)
done
have "((λx. 2 * of_real pi * 𝗂 * f x) has_field_derivative contour_integral (circlepath z r) (λu. f u / (u - w)^2)) (at w)"
apply (simp add: power2_eq_square)
apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "λx. 2 * of_real pi * 𝗂 * f x", simplified])
apply (blast intro: int)
done
then have fder: "(f has_field_derivative contour_integral (circlepath z r) (λu. f u / (u - w)^2) / (2 * of_real pi * 𝗂)) (at w)"
by (rule DERIV_cdivide [where f = "λx. 2 * of_real pi * 𝗂 * f x" and c = "2 * of_real pi * 𝗂", simplified])
show ?thes2
by simp (rule fder)
qed
proposition Cauchy_integral_formula_convex:
assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
and fcd: "(x. x interior S - K f field_differentiable at x)"
and z: "z interior S" and vpg: "valid_path γ"
and pasz: "path_image γ S - {z}" and loop: "pathfinish γ = pathstart γ"
shows "((λw. f w / (w - z)) has_contour_integral (2*pi * 𝗂 * winding_number γ z * f z)) γ"
proof -
have *: "x. x interior S f field_differentiable at x"
unfolding holomorphic_on_open [symmetric] field_differentiable_def
using no_isolated_singularity [where S = "interior S"]
by (meson K contf continuous_at_imp_continuous_on continuous_on_interior fcd
field_differentiable_at_within field_differentiable_def holomorphic_onI
holomorphic_on_imp_differentiable_at open_interior)
show ?thesis
by (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf]) (use * assms in auto)
qed

text‹ Formula for higher derivatives.›
lemma Cauchy_integral_formula_weak:
assumes S: "convex S" and "finite k" and conf: "continuous_on S f"
and fcd: "(x. x interior S - k f field_differentiable at x)"
and z: "z interior S - k" and vpg: "valid_path γ"
and pasz: "path_image γ S - {z}" and loop: "pathfinish γ = pathstart γ"
shows "((λw. f w / (w - z)) has_contour_integral (2*pi * 𝗂 * winding_number γ z * f z)) γ"
proof -
let ?fz = "λw. (f w - f z)/(w - z)"
obtain f' where f': "(f has_field_derivative f') (at z)"
using fcd [OF z] by (auto simp: field_differentiable_def)
have pas: "path_image γ S" and znotin: "z path_image γ" using pasz by blast+
have c: "continuous (at x within S) (λw. if w = z then f' else (f w - f z) / (w - z))" if "x S" for x
proof (cases "x = z")
case True then show ?thesis
using LIM_equal [of "z" ?fz "λw. if w = z then f' else ?fz w"] has_field_derivativeD [OF f']
by (force simp add: continuous_within Lim_at_imp_Lim_at_within)
next
case False
then have dxz: "dist x z > 0" by auto
have cf: "continuous (at x within S) f"
using conf continuous_on_eq_continuous_within that by blast
have "continuous (at x within S) (λw. (f w - f z) / (w - z))"
by (rule cf continuous_intros | simp add: False)+
then show ?thesis
apply (rule continuous_transform_within [OF _ dxz that, of ?fz])
apply (force simp: dist_commute)
done
qed
have fink': "finite (insert z k)" using ‹finite k by blast
have *: "((λw. if w = z then f' else ?fz w) has_contour_integral 0) γ"
proof (rule Cauchy_theorem_convex [OF _ S fink' _ vpg pas loop])
show "(λw. if w = z then f' else ?fz w) field_differentiable at w"
if "w interior S - insert z k" for w
proof (rule field_differentiable_transform_within)
show "(λw. ?fz w) field_differentiable at w"
using that by (intro derivative_intros fcd; simp)
qed (use that in auto simp add: dist_pos_lt dist_commute›)
qed (use c in force simp: continuous_on_eq_continuous_within›)
show ?thesis
apply (rule has_contour_integral_eq)
using znotin has_contour_integral_add [OF has_contour_integral_lmul [OF has_contour_integral_winding_number [OF vpg znotin], of "f z"] *]
apply (auto simp: ac_simps divide_simps)
done
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
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_complex_derivative_funpow_1:
"(f has_field_derivative 1) (at z); f z = z (f^^n has_field_derivative 1) (at z)"
proof (induction n)
case 0
then show ?case
by (simp add: id_def)
next
case (Suc n)
then show ?case
by (metis DERIV_chain funpow_Suc_right mult.right_neutral)
qed
lemma has_complex_derivative_uniform_sequence:
fixes S :: "complex set"
assumes S: "open S"
and hfd: "n x. x S ((f n) has_field_derivative f' n x) (at x)"
and ulim_g: "x. x S
d. 0 < d cball x d S uniform_limit (cball x d) f g sequentially"

shows "g'. x S. (g has_field_derivative g' x) (at x) ((λn. f' n x) g' x) sequentially"
proof -
have y: "y. (g has_field_derivative y) (at z) (λn. f' n z) y" if "z S" for z
proof -
obtain r where "0 < r" and r: "cball z r S"
and ul: "uniform_limit (cball z r) f g sequentially"
using ulim_g [OF z S] by blast
have *: "F n in sequentially. continuous_on (cball z r) (f n)
(w ball z r. ((f n) has_field_derivative (f' n w)) (at w))"

proof (intro eventuallyI conjI ballI)
show "continuous_on (cball z r) (f x)" for x
by (meson S continuous_on_subset hfd holomorphic_on_imp_continuous_on holomorphic_on_open r)
show "w ball z r (f x has_field_derivative f' x w) (at w)" for w x
using ball_subset_cball hfd r by blast
qed
show ?thesis
by (rule has_complex_derivative_uniform_limit [OF *, of g]) (use 0 < r ul in force+)
qed
show ?thesis
by (rule bchoice) (blast intro: y)
qed
definition
integral:: "('a real) ('a set set * ('a set real)) real" (" _ _"(*<*)[60,61] 110(*>*)) where
"integrable f M f M = (THE i. i nnfis (pp f) M) -
(THE j. j nnfis (np f) M)"


text‹So the final step is done, the integral defined. The theorems
we are already used to prove from the
earlier stages are still missing. Only now there are always two properties to be
shown: integrability and the value of the integral. Isabelle makes
it possible two have both goals in a single theorem, so that the
user may derive the statement he desires. Two useful lemmata follow. They
help lifting nonnegative function integral sets to integrals
proper. Notice how the dominated convergence theorem from above is
employed in the latter.›
proposition has_complex_derivative_uniform_limit:
fixes z::complex
assumes cont: "eventually (λn. continuous_on (cball z r) (f n)
(w ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"

and ulim: "uniform_limit (cball z r) f g F"
and F: "¬ trivial_limit F" and "0 < r"
obtains g' where
"continuous_on (cball z r) g"
"w. w ball z r (g has_field_derivative (g' w)) (at w) ((λn. f' n w) g' w) F"
proof -
let ?conint = "contour_integral (circlepath z r)"
have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] ulim F];
auto simp: holomorphic_on_open field_differentiable_def)+
then obtain g' where g': "x. x ball z r (g has_field_derivative g' x) (at x)"
using DERIV_deriv_iff_has_field_derivative
by (fastforce simp add: holomorphic_on_open)
then have derg: "x. x ball z r deriv g x = g' x"
by (simp add: DERIV_imp_deriv)
have tends_f'n_g': "((λn. f' n w) g' w) F" if w: "w ball z r" for w
proof -
have eq_f': "?conint (λx. f n x / (x - w)2) - ?conint (λx. g x / (x - w)2) = (f' n w - g' w) * (2 * of_real pi * 𝗂)"
if cont_fn: "continuous_on (cball z r) (f n)"
and fnd: "w. w ball z r (f n has_field_derivative f' n w) (at w)" for n
proof -
have hol_fn: "f n holomorphic_on ball z r"
using fnd by (force simp: holomorphic_on_open)
have "(f n has_field_derivative 1 / (2 * of_real pi * 𝗂) * ?conint (λu. f n u / (u - w)2)) (at w)"
by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w])
then have f': "f' n w = 1 / (2 * of_real pi * 𝗂) * ?conint (λu. f n u / (u - w)2)"
using DERIV_unique [OF fnd] w by blast
show ?thesis
by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] field_split_simps)
qed
define d where "d = (r - norm(w - z))^2"
have "d > 0"
using w by (simp add: dist_commute dist_norm d_def)
have dle: "d cmod ((y - w)2)" if "r = cmod (z - y)" for y
proof -
have "w ball z (cmod (z - y))"
using that w by fastforce
then have "cmod (w - z) cmod (z - y)"
by (simp add: dist_complex_def norm_minus_commute)
moreover have "cmod (z - y) - cmod (w - z) cmod (y - w)"
by (metis diff_add_cancel diff_add_eq_diff_diff_swap norm_minus_commute norm_triangle_ineq2)
ultimately show ?thesis
using that by (simp add: d_def norm_power power_mono)
qed
have 1: "F n in F. (λx. f n x / (x - w)2) contour_integrable_on circlepath z r"
by (force simp: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont])
have 2: "uniform_limit (sphere z r) (λn x. f n x / (x - w)2) (λx. g x / (x - w)2) F"
unfolding uniform_limit_iff
proof clarify
fix e::real
assume "e > 0"
with r > 0
have "F n in F. x. x w cmod (z - x) = r cmod (f n x - g x) < e * cmod ((x - w)2)"
by (force simp: 0 < d dist_norm dle intro: less_le_trans eventually_mono [OF uniform_limitD [OF ulim], of "e*d"])
with r > 0 e > 0
show "F n in F. xsphere z r. dist (f n x / (x - w)2) (g x / (x - w)2) < e"
by (simp add: norm_divide field_split_simps sphere_def dist_norm)
qed
have "((λn. contour_integral (circlepath z r) (λx. f n x / (x - w)2))
contour_integral (circlepath z r) ((λx. g x / (x - w)2))) F"

by (rule contour_integral_uniform_limit_circlepath [OF 1 2 F 0 < r])
then have tendsto_0: "((λn. 1 / (2 * of_real pi * 𝗂) * (?conint (λx. f n x / (x - w)2) - ?conint (λx. g x / (x - w)2))) 0) F"
using Lim_null by (force intro!: tendsto_mult_right_zero)
have "((λn. f' n w - g' w) 0) F"
apply (rule Lim_transform_eventually [OF tendsto_0])
apply (force simp: divide_simps intro: eq_f' eventually_mono [OF cont])
done
then show ?thesis using Lim_null by blast
qed
obtain g' where "w. w ball z r (g has_field_derivative (g' w)) (at w) ((λn. f' n w) g' w) F"
by (blast intro: tends_f'n_g' g')
then show ?thesis using g
using that by blast
qed
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 * x2 + d * x) has_field_derivative m * x + d) (at x)"
by (auto intro!: derivative_eq_intros)
qed auto
lemma complex_integrable_cnj [simp]:
"complex_integrable M (λx. cnj (f x)) complex_integrable M f"
proof
assume "complex_integrable M (λx. cnj (f x))"
then have "complex_integrable M (λx. cnj (cnj (f x)))"
by (rule integrable_cnj)
then show "complex_integrable M f"
by simp
qed simp
lemma Cauchy_contour_integral_circlepath_2:
assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w ball z r"
shows "contour_integral(circlepath z r) (λu. f u/(u - w)^2) = (2 * pi * 𝗂) * deriv f w"
using Cauchy_contour_integral_circlepath [OF assms, of 1]
by (simp add: power2_eq_square)
lemma Cauchy_higher_derivative_integral_circlepath:
assumes contf: "continuous_on (cball z r) f"
and holf: "f holomorphic_on ball z r"
and w: "w ball z r"
shows "(λu. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
(is "?thes1")
and "(deriv ^^ k) f w = (fact k) / (2 * pi * 𝗂) * contour_integral(circlepath z r) (λu. f u/(u - w)^(Suc k))"
(is "?thes2")
proof -
have *: "((λu. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * 𝗂 / (fact k) * (deriv ^^ k) f w)
(circlepath z r)"

using Cauchy_has_contour_integral_higher_derivative_circlepath [OF assms]
by simp
show ?thes1 using *
using contour_integrable_on_def by blast
show ?thes2
unfolding contour_integral_unique [OF *] by (simp add: field_split_simps)
qed
lemma contour_integral_local_primitive_lemma:
fixes f :: "complexcomplex"
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
theorem Cauchy_integral_formula_convex_simple:
assumes "convex S" and holf: "f holomorphic_on S" and "z interior S" "valid_path γ" "path_image γ S - {z}"
"pathfinish γ = pathstart γ"
shows "((λw. f w / (w - z)) has_contour_integral (2*pi * 𝗂 * winding_number γ z * f z)) γ"
proof -
have "x. x interior S f field_differentiable at x"
using holf at_within_interior holomorphic_onD interior_subset by fastforce
then show ?thesis
using assms
by (intro Cauchy_integral_formula_weak [where k = "{}"]) (auto simp: holomorphic_on_imp_continuous_on)
qed

text‹ Hence the Cauchy formula for points inside a circle.›
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 Cauchy_integral_formula_global_weak:
assumes "open U" and holf: "f holomorphic_on U"
and z: "z U" and γ: "polynomial_function γ"
and pasz: "path_image γ U - {z}" and loop: "pathfinish γ = pathstart γ"
and zero: "w. w U winding_number γ w = 0"
shows "((λw. f w / (w - z)) has_contour_integral (2*pi * 𝗂 * winding_number γ z * f z)) γ"
proof -
obtain γ' where pfγ': "polynomial_function γ'" and γ': "x. (γ has_vector_derivative (γ' x)) (at x)"
using has_vector_derivative_polynomial_function [OF γ] by blast
then have "bounded(path_image γ')"
by (simp add: path_image_def compact_imp_bounded compact_continuous_image continuous_on_polymonial_function)
then obtain B where "B>0" and B: "x. x path_image γ' norm x B"
using bounded_pos by force
define d where [abs_def]: "d z w = (if w = z then deriv f z else (f w - f z)/(w - z))" for z w
define v where "v = {w. w path_image γ winding_number γ w = 0}"
have "path γ" "valid_path γ" using γ
by (auto simp: path_polynomial_function valid_path_polynomial_function)
then have ov: "open v"
by (simp add: v_def open_winding_number_levelsets loop)
have uv_Un: "U v = UNIV"
using pasz zero by (auto simp: v_def)
have conf: "continuous_on U f"
by (metis holf holomorphic_on_imp_continuous_on)
have hol_d: "(d y) holomorphic_on U" if "y U" for y
proof -
have *: "(λc. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on U"
by (simp add: holf pole_lemma_open ‹open U)
then have "isCont (λx. if x = y then deriv f y else (f x - f y) / (x - y)) y"
using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that ‹open U by fastforce
then have "continuous_on U (d y)"
using "*" d_def holomorphic_on_imp_continuous_on by auto
moreover have "d y holomorphic_on U - {y}"
proof -
have "(λw. if w = y then deriv f y else (f w - f y) / (w - y)) field_differentiable at w"
if "w U - {y}" for w
proof (rule field_differentiable_transform_within)
show "(λw. (f w - f y) / (w - y)) field_differentiable at w"
using that ‹open U holf
by (auto intro!: holomorphic_on_imp_differentiable_at derivative_intros)
show "dist w y > 0"
using that by auto
qed (auto simp: dist_commute)
then show ?thesis
unfolding field_differentiable_def by (simp add: d_def holomorphic_on_open ‹open U open_delete)
qed
ultimately show ?thesis
by (rule no_isolated_singularity) (auto simp: ‹open U)
qed
have cint_fxy: "(λx. (f x - f y) / (x - y)) contour_integrable_on γ" if "y path_image γ" for y
proof (rule contour_integrable_holomorphic_simple [where S = "U-{y}"])
show "(λx. (f x - f y) / (x - y)) holomorphic_on U - {y}"
by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
show "path_image γ U - {y}"
using pasz that by blast
qed (auto simp: ‹open U open_delete ‹valid_path γ)
define h where
"h z = (if z U then contour_integral γ (d z) else contour_integral γ (λw. f w/(w - z)))" for z
have U: "((d z) has_contour_integral h z) γ" if "z U" for z
proof -
have "d z holomorphic_on U"
by (simp add: hol_d that)
with that show ?thesis
by (metis Diff_subset ‹valid_path γ ‹open U contour_integrable_holomorphic_simple h_def has_contour_integral_integral pasz subset_trans)
qed
have V: "((λw. f w / (w - z)) has_contour_integral h z) γ" if z: "z v" for z
proof -
have 0: "0 = (f z) * 2 * of_real (2 * pi) * 𝗂 * winding_number γ z"
using v_def z by auto
then have "((λx. 1 / (x - z)) has_contour_integral 0) γ"
using z v_def has_contour_integral_winding_number [OF ‹valid_path γ] by fastforce
then have "((λx. f z * (1 / (x - z))) has_contour_integral 0) γ"
using has_contour_integral_lmul by fastforce
then have "((λx. f z / (x - z)) has_contour_integral 0) γ"
by (simp add: field_split_simps)
moreover have "((λx. (f x - f z) / (x - z)) has_contour_integral contour_integral γ (d z)) γ"
using z
apply (simp add: v_def)
apply (metis (no_types, lifting) contour_integrable_eq d_def has_contour_integral_eq has_contour_integral_integral cint_fxy)
done
ultimately have *: "((λx. f z / (x - z) + (f x - f z) / (x - z)) has_contour_integral (0 + contour_integral γ (d z))) γ"
by (rule has_contour_integral_add)
have "((λw. f w / (w - z)) has_contour_integral contour_integral γ (d z)) γ"
if "z U"
using * by (auto simp: divide_simps has_contour_integral_eq)
moreover have "((λw. f w / (w - z)) has_contour_integral contour_integral γ (λw. f w / (w - z))) γ"
if "z U"
proof (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=U]])
show "(λw. f w / (w - z)) holomorphic_on U"
by (rule holomorphic_intros assms | use that in force)+
qed (use ‹open U pasz ‹valid_path γ in auto)
ultimately show ?thesis
using z by (simp add: h_def)
qed
have znot: "z path_image γ"
using pasz by blast
obtain d0 where "d0>0" and d0: "x y. x path_image γ y - U d0 dist x y"
using separate_compact_closed [of "path_image γ" "-U"] pasz ‹open U ‹path γ compact_path_image
by blast
obtain dd where "0 < dd" and dd: "{y + k | y k. y path_image γ k ball 0 dd} U"
proof
show "0 < d0 / 2" using 0 < d0 by auto
qed (use 0 < d0 d0 in force simp: dist_norm›)
define T where "T {y + k |y k. y path_image γ k cball 0 (dd / 2)}"
have "x x'. x path_image γ; dist x x' * 2 < dd y k. x' = y + k y path_image γ dist 0 k * 2 dd"
apply (rule_tac x=x in exI)
apply (rule_tac x="x'-x" in exI)
apply (force simp: dist_norm)
done
then have subt: "path_image γ interior T"
using 0 < dd
apply (clarsimp simp add: mem_interior T_def)
apply (rule_tac x="dd/2" in exI, auto)
done
have "compact T"
unfolding T_def
by (fastforce simp add: ‹valid_path γ compact_valid_path_image intro!: compact_sums)
have T: "T U"
unfolding T_def using 0 < dd dd by fastforce
obtain L where "L>0"
and L: "f B. f holomorphic_on interior T; z. zinterior T cmod (f z) B
cmod (contour_integral γ f) L * B"

using contour_integral_bound_exists [OF open_interior ‹valid_path γ subt]
by blast
have "bounded(f ` T)"
by (meson ‹compact T compact_continuous_image compact_imp_bounded conf continuous_on_subset T)
then obtain D where "D>0" and D: "x. x T norm (f x) D"
by (auto simp: bounded_pos)
obtain C where "C>0" and C: "x. x T norm x C"
using ‹compact T bounded_pos compact_imp_bounded by force
have "dist (h y) 0 e" if "0 < e" and le: "D * L / e + C cmod y" for e y
proof -
have "D * L / e > 0" using D>0 L>0 e>0 by simp
with le have ybig: "norm y > C" by force
with C have "y T" by force
then have ynot: "y path_image γ"
using subt interior_subset by blast
have [simp]: "winding_number γ y = 0"
proof (rule winding_number_zero_outside)
show "path_image γ cball 0 C"
by (meson C interior_subset mem_cball_0 subset_eq subt)
qed (use ybig loop ‹path γ in auto)
have [simp]: "h y = contour_integral γ (λw. f w/(w - y))"
by (rule contour_integral_unique [symmetric]) (simp add: v_def ynot V)
have holint: "(λw. f w / (w - y)) holomorphic_on interior T"
proof (intro holomorphic_intros)
show "f holomorphic_on interior T"
using holf holomorphic_on_subset interior_subset T by blast
qed (use y T interior_subset in auto)
have leD: "cmod (f z / (z - y)) D * (e / L / D)" if z: "z interior T" for z
proof -
have "D * L / e + cmod z cmod y"
using le C [of z] z using interior_subset by force
then have DL2: "D * L / e cmod (z - y)"
using norm_triangle_ineq2 [of y z] by (simp add: norm_minus_commute)
have "cmod (f z / (z - y)) = cmod (f z) * inverse (cmod (z - y))"
by (simp add: norm_mult norm_inverse Fields.field_class.field_divide_inverse)
also have " D * (e / L / D)"
proof (rule mult_mono)
show "cmod (f z) D"
using D interior_subset z by blast
show "inverse (cmod (z - y)) e / L / D" "D 0"
using L>0 e>0 D>0 DL2 by (auto simp: norm_divide field_split_simps)
qed auto
finally show ?thesis .
qed
have "dist (h y) 0 = cmod (contour_integral γ (λw. f w / (w - y)))"
by (simp add: dist_norm)
also have " L * (D * (e / L / D))"
by (rule L [OF holint leD])
also have " = e"
using L>0 0 < D by auto
finally show ?thesis .
qed
then have "(h 0) at_infinity"
by (meson Lim_at_infinityI)
moreover have "h holomorphic_on UNIV"
proof -
have con_ff: "continuous (at (x,z)) (λ(x,y). (f y - f x) / (y - x))"
if "x U" "z U" "x z" for x z
using that conf
apply (simp add: split_def continuous_on_eq_continuous_at ‹open U)
apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
done
have con_fstsnd: "continuous_on UNIV (λx. (fst x - snd x) ::complex)"
by (rule continuous_intros)+
have open_uu_Id: "open (U × U - Id)"
proof (rule open_Diff)
show "open (U × U)"
by (simp add: open_Times ‹open U)
show "closed (Id :: complex rel)"
using continuous_closed_preimage_constant [OF con_fstsnd closed_UNIV, of 0]
by (auto simp: Id_fstsnd_eq algebra_simps)
qed
have con_derf: "continuous (at z) (deriv f)" if "z U" for z
proof (rule continuous_on_interior)
show "continuous_on U (deriv f)"
by (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on ‹open U)
qed (simp add: interior_open that ‹open U)
have tendsto_f': "((λ(x,y). if y = x then deriv f (x)
else (f (y) - f (x)) / (y - x)) deriv f x)
(at (x, x) within U × U)"
if "x U" for x
proof (rule Lim_withinI)
fix e::real assume "0 < e"
obtain k1 where "k1>0" and k1: "x'. norm (x' - x) k1 norm (deriv f x' - deriv f x) < e"
using 0 < e continuous_within_E [OF con_derf [OF x U]]
by (metis UNIV_I dist_norm)
obtain k2 where "k2>0" and k2: "ball x k2 U"
by (blast intro: openE [OF ‹open U] x U)
have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) e"
if "z' x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
for x' z'
proof -
have cs_less: "w closed_segment x' z' cmod (w - x) norm (x'-x, z'-x)" for w
using segment_furthest_le [of w x' z' x]
by (metis (no_types) dist_commute dist_norm norm_fst_le norm_snd_le order_trans)
have derf_le: "w closed_segment x' z' z' x' cmod (deriv f w - deriv f x) e" for w
by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
have f_has_der: "x. x U (f has_field_derivative deriv f x) (at x within U)"
by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def ‹open U)
have "closed_segment x' z' U"
by (rule order_trans [OF _ k2]) (simp add: cs_less le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
using contour_integral_primitive [OF f_has_der valid_path_linepath] pasz by simp
then have *: "((λx. deriv f x / (z' - x')) has_contour_integral (f z' - f x') / (z' - x')) (linepath x' z')"
by (rule has_contour_integral_div)
have "norm ((f z' - f x') / (z' - x') - deriv f x) e/norm(z' - x') * norm(z' - x')"
apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_diff [OF *]])
using has_contour_integral_div [where c = "z' - x'", OF has_contour_integral_const_linepath [of "deriv f x" z' x']]
e > 0 z' x'
apply (auto simp: norm_divide divide_simps derf_le)
done
also have " e" using 0 < e by simp
finally show ?thesis .
qed
show "d>0. xaU × U.
0 < dist xa (x, x) dist xa (x, x) < d
dist (case xa of (x, y) if y = x then deriv f x else (f y - f x) / (y - x)) (deriv f x) e"

apply (rule_tac x="min k1 k2" in exI)
using k1>0 k2>0 e>0
by (force simp: dist_norm neq intro: dual_order.strict_trans2 k1 less_imp_le norm_fst_le)
qed
have con_pa_f: "continuous_on (path_image γ) f"
by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt T)
have le_B: "T. T {0..1} cmod (vector_derivative γ (at T)) B"
using γ' B by (simp add: path_image_def vector_derivative_at rev_image_eqI)
have f_has_cint: "w. w v - path_image γ ((λu. f u / (u - w) ^ 1) has_contour_integral h w) γ"
by (simp add: V)
have cond_uu: "continuous_on (U × U) (λ(x,y). d x y)"
apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
apply (simp add: tendsto_within_open_NO_MATCH open_Times ‹open U, clarify)
apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(λ(x,y). (f y - f x) / (y - x))"])
using con_ff
apply (auto simp: continuous_within)
done
have hol_dw: "(λz. d z w) holomorphic_on U" if "w U" for w
proof -
have "continuous_on U ((λ(x,y). d x y) (λz. (w,z)))"
by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
then have *: "continuous_on U (λz. if w = z then deriv f z else (f w - f z) / (w - z))"
by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
have **: "(λz. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
if "x U" "x w" for x
proof (rule_tac f = "λx. (f w - f x)/(w - x)" and d = "dist x w" in field_differentiable_transform_within)
show "(λx. (f w - f x) / (w - x)) field_differentiable at x"
using that ‹open U
by (intro derivative_intros holomorphic_on_imp_differentiable_at [OF holf]; force)
qed (use that ‹open U in auto simp: dist_commute›)
show ?thesis
unfolding d_def
proof (rule no_isolated_singularity [OF * _ ‹open U])
show "(λz. if w = z then deriv f z else (f w - f z) / (w - z)) holomorphic_on U - {w}"
by (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff ‹open U **)
qed auto
qed
{ fix a b
assume abu: "closed_segment a b U"
have cont_cint_d: "continuous_on U (λw. contour_integral (linepath a b) (λz. d z w))"
proof (rule contour_integral_continuous_on_linepath_2D [OF ‹open U _ _ abu])
show "w. w U (λz. d z w) contour_integrable_on (linepath a b)"
by (metis abu hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
show "continuous_on (U × U) (λ(x, y). d y x)"
by (auto intro: continuous_on_swap_args cond_uu)
qed
have cont_cint_dγ: "continuous_on {0..1} ((λw. contour_integral (linepath a b) (λz. d z w)) γ)"
proof (rule continuous_on_compose)
show "continuous_on {0..1} γ"
using ‹path γ path_def by blast
show "continuous_on (γ ` {0..1}) (λw. contour_integral (linepath a b) (λz. d z w))"
using pasz unfolding path_image_def
by (auto intro!: continuous_on_subset [OF cont_cint_d])
qed
have "continuous_on {0..1} (λx. vector_derivative γ (at x))"
using pfγ' by (simp add: continuous_on_polymonial_function vector_derivative_at [OF γ'])
then have cint_cint: "(λw. contour_integral (linepath a b) (λz. d z w)) contour_integrable_on γ"
apply (simp add: contour_integrable_on)
apply (rule integrable_continuous_real)
by (rule continuous_on_mult [OF cont_cint_dγ [unfolded o_def]])
have "contour_integral (linepath a b) h = contour_integral (linepath a b) (λz. contour_integral γ (d z))"
using abu by (force simp: h_def intro: contour_integral_eq)
also have " = contour_integral γ (λw. contour_integral (linepath a b) (λz. d z w))"
proof (rule contour_integral_swap)
show "continuous_on (path_image (linepath a b) × path_image γ) (λ(y1, y2). d y1 y2)"
using abu pasz by (auto intro: continuous_on_subset [OF cond_uu])
show "continuous_on {0..1} (λt. vector_derivative (linepath a b) (at t))"
by (auto intro!: continuous_intros)
show "continuous_on {0..1} (λt. vector_derivative γ (at t))"
by (metis γ' continuous_on_eq path_def path_polynomial_function pfγ' vector_derivative_at)
qed (use ‹valid_path γ in auto)
finally have cint_h_eq:
"contour_integral (linepath a b) h =
contour_integral γ (λw. contour_integral (linepath a b) (λz. d z w))"
.
note cint_cint cint_h_eq
} note cint_h = this
have conthu: "continuous_on U h"
proof (simp add: continuous_on_sequentially, clarify)
fix a x
assume x: "x U" and au: "n. a n U" and ax: "a x"
then have A1: "F n in sequentially. d (a n) contour_integrable_on γ"
by (meson U contour_integrable_on_def eventuallyI)
obtain dd where "dd>0" and dd: "cball x dd U" using open_contains_cball ‹open U x by force
have A2: "uniform_limit (path_image γ) (λn. d (a n)) (d x) sequentially"
unfolding uniform_limit_iff dist_norm
proof clarify
fix ee::real
assume "0 < ee"
show "F n in sequentially. ξpath_image γ. cmod (d (a n) ξ - d x ξ) < ee"
proof -
let ?ddpa = "{(w,z) |w z. w cball x dd z path_image γ}"
have "uniformly_continuous_on ?ddpa (λ(x,y). d x y)"
proof (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
show "compact {(w, z) |w z. w cball x dd z path_image γ}"
using ‹valid_path γ
by (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
qed (use dd pasz in auto)
then obtain kk where "kk>0"
and kk: "x x'. x ?ddpa; x' ?ddpa; dist x' x < kk
dist ((λ(x,y). d x y) x') ((λ(x,y). d x y) x) < ee"

by (rule uniformly_continuous_onE [where e = ee]) (use 0 < ee in auto)
have kk: "norm (w - x) dd; z path_image γ; norm ((w, z) - (x, z)) < kk norm (d w z - d x z) < ee"
for w z
using dd>0 kk [of "(x,z)" "(w,z)"] by (force simp: norm_minus_commute dist_norm)
obtain no where "nno. dist (a n) x < min dd kk"
using ax unfolding lim_sequentially
by (meson 0 < dd 0 < kk min_less_iff_conj)
then show ?thesis
using dd > 0 kk > 0 by (fastforce simp: eventually_sequentially kk dist_norm)
qed
qed
have "(λn. contour_integral γ (d (a n))) contour_integral γ (d x)"
by (rule contour_integral_uniform_limit [OF A1 A2 le_B]) (auto simp: ‹valid_path γ)
then have tendsto_hx: "(λn. contour_integral γ (d (a n))) h x"
by (simp add: h_def x)
then show "(h a) h x"
by (simp add: h_def x au o_def)
qed
show ?thesis
proof (simp add: holomorphic_on_open field_differentiable_def [symmetric], clarify)
fix z0
consider "z0 v" | "z0 U" using uv_Un by blast
then show "h field_differentiable at z0"
proof cases
assume "z0 v" then show ?thesis
using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint ‹valid_path γ
by (auto simp: field_differentiable_def v_def)
next
assume "z0 U" then
obtain e where "e>0" and e: "ball z0 e U" by (blast intro: openE [OF ‹open U])
have *: "contour_integral (linepath a b) h + contour_integral (linepath b c) h + contour_integral (linepath c a) h = 0"
if abc_subset: "convex hull {a, b, c} ball z0 e" for a b c
proof -
have *: "x1 x2 z. z U closed_segment x1 x2 U (λw. d w z) contour_integrable_on linepath x1 x2"
using hol_dw holomorphic_on_imp_continuous_on ‹open U
by (auto intro!: contour_integrable_holomorphic_simple)
have abc: "closed_segment a b U" "closed_segment b c U" "closed_segment c a U"
using that e segments_subset_convex_hull by fastforce+
have eq0: "w. w U contour_integral (linepath a b +++ linepath b c +++ linepath c a) (λz. d z w) = 0"
proof (rule contour_integral_unique [OF Cauchy_theorem_triangle])
show "w. w U (λz. d z w) holomorphic_on convex hull {a, b, c}"
using e abc_subset by (auto intro: holomorphic_on_subset [OF hol_dw])
qed
have "contour_integral γ
(λx. contour_integral (linepath a b) (λz. d z x) +
(contour_integral (linepath b c) (λz. d z x) +
contour_integral (linepath c a) (λz. d z x))) = 0"

apply (rule contour_integral_eq_0)
using abc pasz U
apply (subst contour_integral_join [symmetric], auto intro: eq0 *)+
done
then show ?thesis
by (simp add: cint_h abc contour_integrable_add contour_integral_add [symmetric] add_ac)
qed
show ?thesis
using e e > 0
by (auto intro!: holomorphic_on_imp_differentiable_at [OF _ open_ball] analytic_imp_holomorphic
Morera_triangle continuous_on_subset [OF conthu] *)
qed
qed
qed
ultimately have [simp]: "h z = 0" for z
by (meson Liouville_weak)
have "((λw. 1 / (w - z)) has_contour_integral complex_of_real (2 * pi) * 𝗂 * winding_number γ z) γ"
by (rule has_contour_integral_winding_number [OF ‹valid_path γ znot])
then have "((λw. f z * (1 / (w - z))) has_contour_integral complex_of_real (2 * pi) * 𝗂 * winding_number γ z * f z) γ"
by (metis mult.commute has_contour_integral_lmul)
then have 1: "((λw. f z / (w - z)) has_contour_integral complex_of_real (2 * pi) * 𝗂 * winding_number γ z * f z) γ"
by (simp add: field_split_simps)
moreover have 2: "((λw. (f w - f z) / (w - z)) has_contour_integral 0) γ"
using U [OF z] pasz d_def by (force elim: has_contour_integral_eq [where g = "λw. (f w - f z)/(w - z)"])
show ?thesis
using has_contour_integral_add [OF 1 2] by (simp add: diff_divide_distrib)
qed
lemma contour_integral_continuous_on_linepath_2D:
assumes "open U" and cont_dw: "w. w U F w contour_integrable_on (linepath a b)"
and cond_uu: "continuous_on (U × U) (λ(x,y). F x y)"
and abu: "closed_segment a b U"
shows "continuous_on U (λw. contour_integral (linepath a b) (F w))"
proof -
have *: "d>0. x'U. dist x' w < d
dist (contour_integral (linepath a b) (F x'))
(contour_integral (linepath a b) (F w)) ε"

if "w U" "0 < ε" "a b" for w ε
proof -
obtain δ where "δ>0" and δ: "cball w δ U" using open_contains_cball ‹open U w U by force
let ?TZ = "cball w δ × closed_segment a b"
have "uniformly_continuous_on ?TZ (λ(x,y). F x y)"
proof (rule compact_uniformly_continuous)
show "continuous_on ?TZ (λ(x,y). F x y)"
by (rule continuous_on_subset[OF cond_uu]) (use SigmaE δ abu in blast)
show "compact ?TZ"
by (simp add: compact_Times)
qed
then obtain η where "η>0"
and η: "x x'. x?TZ; x'?TZ; dist x' x < η
dist ((λ(x,y). F x y) x') ((λ(x,y). F x y) x) < ε/norm(b - a)"

using 0 < ε a b
by (auto elim: uniformly_continuous_onE [where e = "ε/norm(b - a)"])
have η: "norm (w - x1) δ; x2 closed_segment a b;
norm (w - x1') δ; x2' closed_segment a b; norm ((x1', x2') - (x1, x2)) < η
norm (F x1' x2' - F x1 x2) ε / cmod (b - a)"

for x1 x2 x1' x2'
using η [of "(x1,x2)" "(x1',x2')"] by (force simp: dist_norm)
have le_ee: "cmod (contour_integral (linepath a b) (λx. F x' x - F w x)) ε"
if "x' U" "cmod (x' - w) < δ" "cmod (x' - w) < η" for x'
proof -
have "(λx. F x' x - F w x) contour_integrable_on linepath a b"
by (simp add: w U cont_dw contour_integrable_diff that)
then have "cmod (contour_integral (linepath a b) (λx. F x' x - F w x)) ε/norm(b - a) * norm(b - a)"
apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ η])
using 0 < ε 0 < δ that by (auto simp: norm_minus_commute)
also have " = ε" using a b by simp
finally show ?thesis .
qed
show ?thesis
apply (rule_tac x="min δ η" in exI)
using 0 < δ 0 < η
by (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] w U intro: le_ee)
qed
show ?thesis
proof (cases "a=b")
case False
show ?thesis
by (rule continuous_onI) (use False in auto intro: *›)
qed auto
qed

text‹This version has term‹polynomial_function γ as an additional assumption.›
corollary card_residue_primroots:
assumes "g. residue_primroot m g"
shows "card {gtotatives m. residue_primroot m g} = totient (totient m)"
proof (cases "m = 1")
case [simp]: True
have "{g totatives m. residue_primroot m g} = {1}"
by (auto simp: residue_primroot_def)
thus ?thesis by simp
next
case False
from assms obtain g where g: "residue_primroot m g" by auto
hence "m 0" by (intro notI) auto
with m 1 have "m > 1" by linarith
from this g have "bij_betw (λi. g ^ i mod m) (totatives (totient m))
{gtotatives m. residue_primroot m g}"

by (rule residue_primroot_bij_betw_primroots)
hence "card (totatives (totient m)) = card {gtotatives m. residue_primroot m g}"
by (rule bij_betw_same_card)
thus ?thesis by (simp add: totient_def)
qed
corollary fps_coeff_residues_bigo:
fixes f :: "complex complex" and r :: real
assumes "open A" "connected A" "cball 0 r A" "r > 0"
assumes "f holomorphic_on A - S" "S ball 0 r" "finite S" "0 S"
assumes g: "eventually (λn. g n = -(zS. residue (λz. f z / z ^ Suc n) z)) sequentially"
(is "eventually (λn. _ = -?g' n) _")
shows "(λn. (deriv ^^ n) f 0 / fact n - g n) O(λn. 1 / r ^ n)" (is "(λn. ?c n - _) O(_)")
proof -
from assms have "compact (f ` sphere 0 r)"
by (intro compact_continuous_image holomorphic_on_imp_continuous_on
holomorphic_on_subset[OF f holomorphic_on A - S]) auto
hence "bounded (f ` sphere 0 r)" by (rule compact_imp_bounded)
then obtain C where C: "z. z sphere 0 r norm (f z) C"
by (auto simp: bounded_iff sphere_def)
have "0 norm (f (of_real r))" by simp
also from C[of "of_real r"] and r > 0 have " C" by simp
finally have C_nonneg: "C 0" .

have "(λn. ?c n + ?g' n) O(λn. of_real (1 / r ^ n))"
proof (intro bigoI[of _ C] always_eventually allI )
fix n :: nat
from assms and C and C_nonneg have "norm (?c n + ?g' n) C / r ^ n"
by (intro fps_coeff_residues_bound[where A = A and k = "{}"]) auto
also have " = C * norm (complex_of_real (1 / r ^ n))"
using r > 0 by (simp add: norm_divide norm_power)
finally show "norm (?c n + ?g' n) " .
qed
also have "?this (λn. ?c n - g n) O(λn. of_real (1 / r ^ n))"
by (intro landau_o.big.in_cong eventually_mono[OF g]) simp_all
finally show ?thesis .
qed
lemma residue_primroot_def [code]:
"residue_primroot n x n > 0 coprime n x ord n x = totient n"
by (simp add: residue_primroot.simps)
lemma residue_primroot_cong:
assumes "[x = x'] (mod n)"
shows "residue_primroot n x = residue_primroot n x'"
proof -
have "residue_primroot n x = residue_primroot n (x mod n)"
by simp
also have "x mod n = x' mod n"
using assms by (simp add: cong_def)
also have "residue_primroot n (x' mod n) = residue_primroot n x'"
by simp
finally show ?thesis .
qed
lemma residue_primroot_Carmichael:
assumes "residue_primroot n g"
shows "Carmichael n = totient n"
proof (cases "n = 1")
case False
show ?thesis
proof (intro dvd_antisym Carmichael_dvd_totient)
have "ord n g dvd Carmichael n"
using assms False by (intro ord_dvd_Carmichael) (auto simp: residue_primroot_def)
thus "totient n dvd Carmichael n"
using assms by (auto simp: residue_primroot_def)
qed
qed auto
lemma residue_primroot_mod [simp]: "residue_primroot n (x mod n) = residue_primroot n x"
by (cases "n = 0") (simp_all add: residue_primroot_def)
lemma Cauchy_has_contour_integral_higher_derivative_circlepath:
assumes contf: "continuous_on (cball z r) f"
and holf: "f holomorphic_on ball z r"
and w: "w ball z r"
shows "((λu. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * 𝗂) / (fact k) * (deriv ^^ k) f w))
(circlepath z r)"

using w
proof (induction k arbitrary: w)
case 0 then show ?case
using assms by (auto simp: Cauchy_integral_circlepath dist_commute dist_norm)
next
case (Suc k)
have [simp]: "r > 0" using w
using ball_eq_empty by fastforce
have f: "continuous_on (path_image (circlepath z r)) f"
by (rule continuous_on_subset [OF contf]) (force simp: cball_def sphere_def less_imp_le)
obtain X where X: "((λu. f u / (u - w) ^ Suc (Suc k)) has_contour_integral X) (circlepath z r)"
using Cauchy_next_derivative_circlepath(1) [OF f Suc.IH _ Suc.prems]
by (auto simp: contour_integrable_on_def)
then have con: "contour_integral (circlepath z r) ((λu. f u / (u - w) ^ Suc (Suc k))) = X"
by (rule contour_integral_unique)
have "n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
using Suc.prems assms has_field_derivative_higher_deriv by auto
then have dnf_diff: "n. (deriv ^^ n) f field_differentiable (at w)"
by (force simp: field_differentiable_def)
have "deriv (λw. complex_of_real (2 * pi) * 𝗂 / (fact k) * (deriv ^^ k) f w) w =
of_nat (Suc k) * contour_integral (circlepath z r) (λu. f u / (u - w) ^ Suc (Suc k))"

by (force intro!: DERIV_imp_deriv Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
also have " = of_nat (Suc k) * X"
by (simp only: con)
finally have "deriv (λw. ((2 * pi) * 𝗂 / (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
then have "((2 * pi) * 𝗂 / (fact k)) * deriv (λw. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
by (metis deriv_cmult dnf_diff)
then have "deriv (λw. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * 𝗂 / (fact k))"
by (simp add: field_simps)
then show ?case
using of_nat_eq_0_iff X by fastforce
qed
theorem argument_principle:
fixes f::"complex complex" and poles s:: "complex set"
defines "pz {w. f w = 0 w poles}" ― ‹termpz is the set of poles and zeros›
assumes "open s" and
"connected s" and
f_holo:"f holomorphic_on s-poles" and
h_holo:"h holomorphic_on s" and
"valid_path g" and
loop:"pathfinish g = pathstart g" and
path_img:"path_image g s - pz" and
homo:"z. (z s) winding_number g z = 0" and
finite:"finite pz" and
poles:"ppoles. is_pole f p"
shows "contour_integral g (λx. deriv f x * h x / f x) = 2 * pi * 𝗂 *
(ppz. winding_number g p * h p * zorder f p)"

(is "?L=?R")
proof -
define c where "c 2 * complex_of_real pi * 𝗂 "
define ff where "ff (λx. deriv f x * h x / f x)"
define cont where "cont λff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
define avoid where "avoid λp e. wcball p e. w s (w p w pz)"

have "e>0. avoid p e (ppz cont ff p e)" when "ps" for p
proof -
obtain e1 where "e1>0" and e1_avoid:"avoid p e1"
using finite_cball_avoid[OF ‹open s finite] ps unfolding avoid_def by auto
have "e2>0. cball p e2 ball p e1 cont ff p e2" when "ppz"
proof -
define po where "po zorder f p"
define pp where "pp zor_poly f p"
define f' where "f' λw. pp w * (w - p) powr po"
define ff' where "ff' (λx. deriv f' x * h x / f' x)"
obtain r where "pp p0" "r>0" and
"r<e1" and
pp_holo:"pp holomorphic_on cball p r" and
pp_po:"(wcball p r-{p}. f w = pp w * (w - p) powr po pp w 0)"
proof -
have "isolated_singularity_at f p"
proof -
have "f holomorphic_on ball p e1 - {p}"
apply (intro holomorphic_on_subset[OF f_holo])
using e1_avoid ppz unfolding avoid_def pz_def by force
then show ?thesis unfolding isolated_singularity_at_def
using e1>0 analytic_on_open open_delete by blast
qed
moreover have "not_essential f p"
proof (cases "is_pole f p")
case True
then show ?thesis unfolding not_essential_def by auto
next
case False
then have "ps-poles" using ps poles unfolding pz_def by auto
moreover have "open (s-poles)"
using ‹open s
apply (elim open_Diff)
apply (rule finite_imp_closed)
using finite unfolding pz_def by simp
ultimately have "isCont f p"
using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at
by auto
then show ?thesis unfolding isCont_def not_essential_def by auto
qed
moreover have "F w in at p. f w 0 "
proof (rule ccontr)
assume "¬ (F w in at p. f w 0)"
then have "F w in at p. f w= 0" unfolding frequently_def by auto
then obtain rr where "rr>0" "wball p rr - {p}. f w =0"
unfolding eventually_at by (auto simp add:dist_commute)
then have "ball p rr - {p} {wball p rr-{p}. f w=0}" by blast
moreover have "infinite (ball p rr - {p})" using rr>0 using finite_imp_not_open by fastforce
ultimately have "infinite {wball p rr-{p}. f w=0}" using infinite_super by blast
then have "infinite pz"
unfolding pz_def infinite_super by auto
then show False using ‹finite pz by auto
qed
ultimately obtain r where "pp p 0" and r:"r>0" "pp holomorphic_on cball p r"
"(wcball p r - {p}. f w = pp w * (w - p) powr of_int po pp w 0)"
using zorder_exist[of f p,folded po_def pp_def] by auto
define r1 where "r1=min r e1 / 2"
have "r1<e1" unfolding r1_def using e1>0 r>0 by auto
moreover have "r1>0" "pp holomorphic_on cball p r1"
"(wcball p r1 - {p}. f w = pp w * (w - p) powr of_int po pp w 0)"
unfolding r1_def using e1>0 r by auto
ultimately show ?thesis using that pp p0 by auto
qed

define e2 where "e2 r/2"
have "e2>0" using r>0 unfolding e2_def by auto
define anal where "anal λw. deriv pp w * h w / pp w"
define prin where "prin λw. po * h w / (w - p)"
have "((λw. prin w + anal w) has_contour_integral c * po * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r s"
using r<e1 avoid_def ball_subset_cball e1_avoid by (simp add: subset_eq)
then have "cball p e2 s"
using r>0 unfolding e2_def by auto
then have "(λw. po * h w) holomorphic_on cball p e2"
using h_holo by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral c * po * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "λw. po * h w"] e2>0
unfolding prin_def by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
using pp_holo h_holo pp_po ‹ball p r s pp p0
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
using e2_def r>0
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont ff' p e2" unfolding cont_def po_def
proof (elim has_contour_integral_eq)
fix w assume "w path_image (circlepath p e2)"
then have "wball p r" and "wp" unfolding e2_def using r>0 by auto
define wp where "wp w-p"
have "wp0" and "pp w 0"
unfolding wp_def using wp wball p r pp_po by auto
moreover have der_f':"deriv f' w = po * pp w * (w-p) powr (po - 1) + deriv pp w * (w-p) powr po"
proof (rule DERIV_imp_deriv)
have "(pp has_field_derivative (deriv pp w)) (at w)"
using DERIV_deriv_iff_has_field_derivative pp_holo wp
by (meson open_ball w ball p r ball_subset_cball holomorphic_derivI holomorphic_on_subset)
then show " (f' has_field_derivative of_i