# Theory Cauchy_Integral_Theorem

theory Cauchy_Integral_Theorem
imports Complex_Transcendental Weierstrass_Theorems
```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 Complex_Transcendental Weierstrass_Theorems Ordered_Euclidean_Space
begin

subsection‹Homeomorphisms of arc images›

lemma homeomorphism_arc:
fixes g :: "real ⇒ 'a::t2_space"
assumes "arc g"
obtains h where "homeomorphism {0..1} (path_image g) g h"
using assms by (force simp: arc_def homeomorphism_compact path_def path_image_def)

lemma homeomorphic_arc_image_interval:
fixes g :: "real ⇒ 'a::t2_space" and a::real
assumes "arc g" "a < b"
shows "(path_image g) homeomorphic {a..b}"
proof -
have "(path_image g) homeomorphic {0..1::real}"
by (meson assms(1) homeomorphic_def homeomorphic_sym homeomorphism_arc)
also have "… homeomorphic {a..b}"
using assms by (force intro: homeomorphic_closed_intervals_real)
finally show ?thesis .
qed

lemma homeomorphic_arc_images:
fixes g :: "real ⇒ 'a::t2_space" and h :: "real ⇒ 'b::t2_space"
assumes "arc g" "arc h"
shows "(path_image g) homeomorphic (path_image h)"
proof -
have "(path_image g) homeomorphic {0..1::real}"
by (meson assms homeomorphic_def homeomorphic_sym homeomorphism_arc)
also have "… homeomorphic (path_image h)"
by (meson assms homeomorphic_def homeomorphism_arc)
finally show ?thesis .
qed

lemma path_connected_arc_complement:
fixes γ :: "real ⇒ 'a::euclidean_space"
assumes "arc γ" "2 ≤ DIM('a)"
shows "path_connected(- path_image γ)"
proof -
have "path_image γ homeomorphic {0..1::real}"
then
show ?thesis
apply (rule path_connected_complement_homeomorphic_convex_compact)
apply (auto simp: assms)
done
qed

lemma connected_arc_complement:
fixes γ :: "real ⇒ 'a::euclidean_space"
assumes "arc γ" "2 ≤ DIM('a)"
shows "connected(- path_image γ)"
by (simp add: assms path_connected_arc_complement path_connected_imp_connected)

lemma inside_arc_empty:
fixes γ :: "real ⇒ 'a::euclidean_space"
assumes "arc γ"
shows "inside(path_image γ) = {}"
proof (cases "DIM('a) = 1")
case True
then show ?thesis
using assms connected_arc_image connected_convex_1_gen inside_convex by blast
next
case False
show ?thesis
proof (rule inside_bounded_complement_connected_empty)
show "connected (- path_image γ)"
apply (rule connected_arc_complement [OF assms])
using False
by (metis DIM_ge_Suc0 One_nat_def Suc_1 not_less_eq_eq order_class.order.antisym)
show "bounded (path_image γ)"
qed
qed

lemma inside_simple_curve_imp_closed:
fixes γ :: "real ⇒ 'a::euclidean_space"
shows "⟦simple_path γ; x ∈ inside(path_image γ)⟧ ⟹ pathfinish γ = pathstart γ"
using arc_simple_path  inside_arc_empty by blast

subsection ‹Piecewise differentiable functions›

definition piecewise_differentiable_on
(infixr "piecewise'_differentiable'_on" 50)
where "f piecewise_differentiable_on i  ≡
continuous_on i f ∧
(∃S. finite S ∧ (∀x ∈ i - S. f differentiable (at x within i)))"

lemma piecewise_differentiable_on_imp_continuous_on:
"f piecewise_differentiable_on S ⟹ continuous_on S f"

lemma piecewise_differentiable_on_subset:
"f piecewise_differentiable_on S ⟹ T ≤ S ⟹ f piecewise_differentiable_on T"
using continuous_on_subset
unfolding piecewise_differentiable_on_def
apply safe
apply (blast elim: continuous_on_subset)
by (meson Diff_iff differentiable_within_subset subsetCE)

lemma differentiable_on_imp_piecewise_differentiable:
fixes a:: "'a::{linorder_topology,real_normed_vector}"
shows "f differentiable_on {a..b} ⟹ f piecewise_differentiable_on {a..b}"
apply (rule_tac x="{a,b}" in exI, simp add: differentiable_on_def)
done

lemma differentiable_imp_piecewise_differentiable:
"(⋀x. x ∈ S ⟹ f differentiable (at x within S))
⟹ f piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def differentiable_imp_continuous_on differentiable_on_def
intro: differentiable_within_subset)

lemma piecewise_differentiable_const [iff]: "(λx. z) piecewise_differentiable_on S"

lemma piecewise_differentiable_compose:
"⟦f piecewise_differentiable_on S; g piecewise_differentiable_on (f ` S);
⋀x. finite (S ∩ f-`{x})⟧
⟹ (g ∘ f) piecewise_differentiable_on S"
apply (blast intro: continuous_on_compose2)
apply (rename_tac A B)
apply (rule_tac x="A ∪ (⋃x∈B. S ∩ f-`{x})" in exI)
apply (blast intro!: differentiable_chain_within)
done

lemma piecewise_differentiable_affine:
fixes m::real
assumes "f piecewise_differentiable_on ((λx. m *⇩R x + c) ` S)"
shows "(f ∘ (λx. m *⇩R x + c)) piecewise_differentiable_on S"
proof (cases "m = 0")
case True
then show ?thesis
unfolding o_def
by (force intro: differentiable_imp_piecewise_differentiable differentiable_const)
next
case False
show ?thesis
apply (rule piecewise_differentiable_compose [OF differentiable_imp_piecewise_differentiable])
apply (rule assms derivative_intros | simp add: False vimage_def real_vector_affinity_eq)+
done
qed

lemma piecewise_differentiable_cases:
fixes c::real
assumes "f piecewise_differentiable_on {a..c}"
"g piecewise_differentiable_on {c..b}"
"a ≤ c" "c ≤ b" "f c = g c"
shows "(λx. if x ≤ c then f x else g x) piecewise_differentiable_on {a..b}"
proof -
obtain S T where st: "finite S" "finite T"
and fd: "⋀x. x ∈ {a..c} - S ⟹ f differentiable at x within {a..c}"
and gd: "⋀x. x ∈ {c..b} - T ⟹ g differentiable at x within {c..b}"
using assms
by (auto simp: piecewise_differentiable_on_def)
have finabc: "finite ({a,b,c} ∪ (S ∪ T))"
by (metis ‹finite S› ‹finite T› finite_Un finite_insert finite.emptyI)
have "continuous_on {a..c} f" "continuous_on {c..b} g"
using assms piecewise_differentiable_on_def by auto
then have "continuous_on {a..b} (λx. if x ≤ c then f x else g x)"
using continuous_on_cases [OF closed_real_atLeastAtMost [of a c],
OF closed_real_atLeastAtMost [of c b],
of f g "λx. x≤c"]  assms
by (force simp: ivl_disj_un_two_touch)
moreover
{ fix x
assume x: "x ∈ {a..b} - ({a,b,c} ∪ (S ∪ T))"
have "(λx. if x ≤ c then f x else g x) differentiable at x within {a..b}" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
proof (rule differentiable_transform_within [where d = "dist x c"])
have "f differentiable at x"
using x le fd [of x] at_within_interior [of x "{a..c}"] by simp
then show "f differentiable at x within {a..b}"
qed (use x le st dist_real_def in auto)
next
case ge show ?diff_fg
proof (rule differentiable_transform_within [where d = "dist x c"])
have "g differentiable at x"
using x ge gd [of x] at_within_interior [of x "{c..b}"] by simp
then show "g differentiable at x within {a..b}"
qed (use x ge st dist_real_def in auto)
qed
}
then have "∃S. finite S ∧
(∀x∈{a..b} - S. (λx. if x ≤ c then f x else g x) differentiable at x within {a..b})"
by (meson finabc)
ultimately show ?thesis
qed

lemma piecewise_differentiable_neg:
"f piecewise_differentiable_on S ⟹ (λx. -(f x)) piecewise_differentiable_on S"
by (auto simp: piecewise_differentiable_on_def continuous_on_minus)

assumes "f piecewise_differentiable_on i"
"g piecewise_differentiable_on i"
shows "(λx. f x + g x) piecewise_differentiable_on i"
proof -
obtain S T where st: "finite S" "finite T"
"∀x∈i - S. f differentiable at x within i"
"∀x∈i - T. g differentiable at x within i"
using assms by (auto simp: piecewise_differentiable_on_def)
then have "finite (S ∪ T) ∧ (∀x∈i - (S ∪ T). (λx. f x + g x) differentiable at x within i)"
by auto
moreover have "continuous_on i f" "continuous_on i g"
using assms piecewise_differentiable_on_def by auto
ultimately show ?thesis
qed

lemma piecewise_differentiable_diff:
"⟦f piecewise_differentiable_on S;  g piecewise_differentiable_on S⟧
⟹ (λx. f x - g x) piecewise_differentiable_on S"

lemma continuous_on_joinpaths_D1:
"continuous_on {0..1} (g1 +++ g2) ⟹ continuous_on {0..1} g1"
apply (rule continuous_on_eq [of _ "(g1 +++ g2) ∘ (( *)(inverse 2))"])
apply (rule continuous_intros | simp)+
apply (auto elim!: continuous_on_subset simp: joinpaths_def)
done

lemma continuous_on_joinpaths_D2:
"⟦continuous_on {0..1} (g1 +++ g2); pathfinish g1 = pathstart g2⟧ ⟹ continuous_on {0..1} g2"
apply (rule continuous_on_eq [of _ "(g1 +++ g2) ∘ (λx. inverse 2*x + 1/2)"])
apply (rule continuous_intros | simp)+
apply (auto elim!: continuous_on_subset simp add: joinpaths_def pathfinish_def pathstart_def Ball_def)
done

lemma piecewise_differentiable_D1:
assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}"
shows "g1 piecewise_differentiable_on {0..1}"
proof -
obtain S where cont: "continuous_on {0..1} g1" and "finite S"
and S: "⋀x. x ∈ {0..1} - S ⟹ g1 +++ g2 differentiable at x within {0..1}"
using assms unfolding piecewise_differentiable_on_def
by (blast dest!: continuous_on_joinpaths_D1)
show ?thesis
unfolding piecewise_differentiable_on_def
proof (intro exI conjI ballI cont)
show "finite (insert 1 ((( *)2) ` S))"
show "g1 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 1 (( *) 2 ` S)" for x
proof (rule_tac d="dist (x/2) (1/2)" in differentiable_transform_within)
have "g1 +++ g2 differentiable at (x / 2) within {0..1/2}"
by (rule differentiable_subset [OF S [of "x/2"]] | use that in force)+
then show "g1 +++ g2 ∘ ( *) (inverse 2) differentiable at x within {0..1}"
by (auto intro: differentiable_chain_within)
qed (use that in ‹auto simp: joinpaths_def›)
qed
qed

lemma piecewise_differentiable_D2:
assumes "(g1 +++ g2) piecewise_differentiable_on {0..1}" and eq: "pathfinish g1 = pathstart g2"
shows "g2 piecewise_differentiable_on {0..1}"
proof -
have [simp]: "g1 1 = g2 0"
using eq by (simp add: pathfinish_def pathstart_def)
obtain S where cont: "continuous_on {0..1} g2" and "finite S"
and S: "⋀x. x ∈ {0..1} - S ⟹ g1 +++ g2 differentiable at x within {0..1}"
using assms unfolding piecewise_differentiable_on_def
by (blast dest!: continuous_on_joinpaths_D2)
show ?thesis
unfolding piecewise_differentiable_on_def
proof (intro exI conjI ballI cont)
show "finite (insert 0 ((λx. 2*x-1)`S))"
show "g2 differentiable at x within {0..1}" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1)`S)" for x
proof (rule_tac d="dist ((x+1)/2) (1/2)" in differentiable_transform_within)
have x2: "(x + 1) / 2 ∉ S"
using that
apply (clarsimp simp: image_iff)
have "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}"
by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
then show "g1 +++ g2 ∘ (λx. (x+1) / 2) differentiable at x within {0..1}"
by (auto intro: differentiable_chain_within)
show "(g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'" if "x' ∈ {0..1}" "dist x' x < dist ((x + 1) / 2) (1/2)" for x'
proof -
have [simp]: "(2*x'+2)/2 = x'+1"
show ?thesis
using that by (auto simp: joinpaths_def)
qed
qed (use that in ‹auto simp: joinpaths_def›)
qed
qed

subsubsection‹The concept of continuously differentiable›

text ‹
John Harrison writes as follows:

``The usual assumption in complex analysis texts is that a path ‹γ› should be piecewise
continuously differentiable, which ensures that the path integral exists at least for any continuous
f, since all piecewise continuous functions are integrable. However, our notion of validity is
weaker, just piecewise differentiability\ldots{} [namely] continuity plus differentiability except on a
finite set\ldots{} [Our] underlying theory of integration is the Kurzweil-Henstock theory. In contrast to
the Riemann or Lebesgue theory (but in common with a simple notion based on antiderivatives), this
can integrate all derivatives.''

"Formalizing basic complex analysis." From Insight to Proof: Festschrift in Honour of Andrzej Trybulec.
Studies in Logic, Grammar and Rhetoric 10.23 (2007): 151-165.

And indeed he does not assume that his derivatives are continuous, but the penalty is unreasonably
difficult proofs concerning winding numbers. We need a self-contained and straightforward theorem
asserting that all derivatives can be integrated before we can adopt Harrison's choice.›

definition C1_differentiable_on :: "(real ⇒ 'a::real_normed_vector) ⇒ real set ⇒ bool"
(infix "C1'_differentiable'_on" 50)
where
"f C1_differentiable_on S ⟷
(∃D. (∀x ∈ S. (f has_vector_derivative (D x)) (at x)) ∧ continuous_on S D)"

lemma C1_differentiable_on_eq:
"f C1_differentiable_on S ⟷
(∀x ∈ S. f differentiable at x) ∧ continuous_on S (λx. vector_derivative f (at x))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
unfolding C1_differentiable_on_def
by (metis (no_types, lifting) continuous_on_eq  differentiableI_vector vector_derivative_at)
next
assume ?rhs
then show ?lhs
using C1_differentiable_on_def vector_derivative_works by fastforce
qed

lemma C1_differentiable_on_subset:
"f C1_differentiable_on T ⟹ S ⊆ T ⟹ f C1_differentiable_on S"
unfolding C1_differentiable_on_def  continuous_on_eq_continuous_within
by (blast intro:  continuous_within_subset)

lemma C1_differentiable_compose:
assumes fg: "f C1_differentiable_on S" "g C1_differentiable_on (f ` S)" and fin: "⋀x. finite (S ∩ f-`{x})"
shows "(g ∘ f) C1_differentiable_on S"
proof -
have "⋀x. x ∈ S ⟹ g ∘ f differentiable at x"
by (meson C1_differentiable_on_eq assms differentiable_chain_at imageI)
moreover have "continuous_on S (λx. vector_derivative (g ∘ f) (at x))"
proof (rule continuous_on_eq [of _ "λx. vector_derivative f (at x) *⇩R vector_derivative g (at (f x))"])
show "continuous_on S (λx. vector_derivative f (at x) *⇩R vector_derivative g (at (f x)))"
using fg
apply (rule Limits.continuous_on_scaleR, assumption)
by (metis (mono_tags, lifting) continuous_at_imp_continuous_on continuous_on_compose continuous_on_cong differentiable_imp_continuous_within o_def)
show "⋀x. x ∈ S ⟹ vector_derivative f (at x) *⇩R vector_derivative g (at (f x)) = vector_derivative (g ∘ f) (at x)"
by (metis (mono_tags, hide_lams) C1_differentiable_on_eq fg imageI vector_derivative_chain_at)
qed
ultimately show ?thesis
qed

lemma C1_diff_imp_diff: "f C1_differentiable_on S ⟹ f differentiable_on S"

lemma C1_differentiable_on_ident [simp, derivative_intros]: "(λx. x) C1_differentiable_on S"
by (auto simp: C1_differentiable_on_eq continuous_on_const)

lemma C1_differentiable_on_const [simp, derivative_intros]: "(λz. a) C1_differentiable_on S"
by (auto simp: C1_differentiable_on_eq continuous_on_const)

"f C1_differentiable_on S ⟹ g C1_differentiable_on S ⟹ (λx. f x + g x) C1_differentiable_on S"
unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)

lemma C1_differentiable_on_minus [simp, derivative_intros]:
"f C1_differentiable_on S ⟹ (λx. - f x) C1_differentiable_on S"
unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)

lemma C1_differentiable_on_diff [simp, derivative_intros]:
"f C1_differentiable_on S ⟹ g C1_differentiable_on S ⟹ (λx. f x - g x) C1_differentiable_on S"
unfolding C1_differentiable_on_eq  by (auto intro: continuous_intros)

lemma C1_differentiable_on_mult [simp, derivative_intros]:
fixes f g :: "real ⇒ 'a :: real_normed_algebra"
shows "f C1_differentiable_on S ⟹ g C1_differentiable_on S ⟹ (λx. f x * g x) C1_differentiable_on S"
unfolding C1_differentiable_on_eq
by (auto simp: continuous_on_add continuous_on_mult continuous_at_imp_continuous_on differentiable_imp_continuous_within)

lemma C1_differentiable_on_scaleR [simp, derivative_intros]:
"f C1_differentiable_on S ⟹ g C1_differentiable_on S ⟹ (λx. f x *⇩R g x) C1_differentiable_on S"
unfolding C1_differentiable_on_eq
by (rule continuous_intros | simp add: continuous_at_imp_continuous_on differentiable_imp_continuous_within)+

definition piecewise_C1_differentiable_on
(infixr "piecewise'_C1'_differentiable'_on" 50)
where "f piecewise_C1_differentiable_on i  ≡
continuous_on i f ∧
(∃S. finite S ∧ (f C1_differentiable_on (i - S)))"

lemma C1_differentiable_imp_piecewise:
"f C1_differentiable_on S ⟹ f piecewise_C1_differentiable_on S"
by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_at_imp_continuous_on differentiable_imp_continuous_within)

lemma piecewise_C1_imp_differentiable:
"f piecewise_C1_differentiable_on i ⟹ f piecewise_differentiable_on i"
by (auto simp: piecewise_C1_differentiable_on_def piecewise_differentiable_on_def
C1_differentiable_on_def differentiable_def has_vector_derivative_def
intro: has_derivative_at_withinI)

lemma piecewise_C1_differentiable_compose:
assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "⋀x. finite (S ∩ f-`{x})"
shows "(g ∘ f) piecewise_C1_differentiable_on S"
proof -
have "continuous_on S (λx. g (f x))"
by (metis continuous_on_compose2 fg order_refl piecewise_C1_differentiable_on_def)
moreover have "∃T. finite T ∧ g ∘ f C1_differentiable_on S - T"
proof -
obtain F where "finite F" and F: "f C1_differentiable_on S - F" and f: "f piecewise_C1_differentiable_on S"
using fg by (auto simp: piecewise_C1_differentiable_on_def)
obtain G where "finite G" and G: "g C1_differentiable_on f ` S - G" and g: "g piecewise_C1_differentiable_on f ` S"
using fg by (auto simp: piecewise_C1_differentiable_on_def)
show ?thesis
proof (intro exI conjI)
show "finite (F ∪ (⋃x∈G. S ∩ f-`{x}))"
using fin by (auto simp only: Int_Union ‹finite F› ‹finite G› finite_UN finite_imageI)
show "g ∘ f C1_differentiable_on S - (F ∪ (⋃x∈G. S ∩ f -` {x}))"
apply (rule C1_differentiable_compose)
apply (blast intro: C1_differentiable_on_subset [OF F])
apply (blast intro: C1_differentiable_on_subset [OF G])
by (simp add:  C1_differentiable_on_subset G Diff_Int_distrib2 fin)
qed
qed
ultimately show ?thesis
qed

lemma piecewise_C1_differentiable_on_subset:
"f piecewise_C1_differentiable_on S ⟹ T ≤ S ⟹ f piecewise_C1_differentiable_on T"
by (auto simp: piecewise_C1_differentiable_on_def elim!: continuous_on_subset C1_differentiable_on_subset)

lemma C1_differentiable_imp_continuous_on:
"f C1_differentiable_on S ⟹ continuous_on S f"
unfolding C1_differentiable_on_eq continuous_on_eq_continuous_within
using differentiable_at_withinI differentiable_imp_continuous_within by blast

lemma C1_differentiable_on_empty [iff]: "f C1_differentiable_on {}"
unfolding C1_differentiable_on_def
by auto

lemma piecewise_C1_differentiable_affine:
fixes m::real
assumes "f piecewise_C1_differentiable_on ((λx. m * x + c) ` S)"
shows "(f ∘ (λx. m *⇩R x + c)) piecewise_C1_differentiable_on S"
proof (cases "m = 0")
case True
then show ?thesis
unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const)
next
case False
have *: "⋀x. finite (S ∩ {y. m * y + c = x})"
using False not_finite_existsD by fastforce
show ?thesis
apply (rule piecewise_C1_differentiable_compose [OF C1_differentiable_imp_piecewise])
apply (rule * assms derivative_intros | simp add: False vimage_def)+
done
qed

lemma piecewise_C1_differentiable_cases:
fixes c::real
assumes "f piecewise_C1_differentiable_on {a..c}"
"g piecewise_C1_differentiable_on {c..b}"
"a ≤ c" "c ≤ b" "f c = g c"
shows "(λx. if x ≤ c then f x else g x) piecewise_C1_differentiable_on {a..b}"
proof -
obtain S T where st: "f C1_differentiable_on ({a..c} - S)"
"g C1_differentiable_on ({c..b} - T)"
"finite S" "finite T"
using assms
by (force simp: piecewise_C1_differentiable_on_def)
then have f_diff: "f differentiable_on {a..<c} - S"
and g_diff: "g differentiable_on {c<..b} - T"
by (simp_all add: C1_differentiable_on_eq differentiable_at_withinI differentiable_on_def)
have "continuous_on {a..c} f" "continuous_on {c..b} g"
using assms piecewise_C1_differentiable_on_def by auto
then have cab: "continuous_on {a..b} (λx. if x ≤ c then f x else g x)"
using continuous_on_cases [OF closed_real_atLeastAtMost [of a c],
OF closed_real_atLeastAtMost [of c b],
of f g "λx. x≤c"]  assms
by (force simp: ivl_disj_un_two_touch)
{ fix x
assume x: "x ∈ {a..b} - insert c (S ∪ T)"
have "(λx. if x ≤ c then f x else g x) differentiable at x" (is "?diff_fg")
proof (cases x c rule: le_cases)
case le show ?diff_fg
apply (rule differentiable_transform_within [where f=f and d = "dist x c"])
using x dist_real_def le st by (auto simp: C1_differentiable_on_eq)
next
case ge show ?diff_fg
apply (rule differentiable_transform_within [where f=g and d = "dist x c"])
using dist_nz x dist_real_def ge st x by (auto simp: C1_differentiable_on_eq)
qed
}
then have "(∀x ∈ {a..b} - insert c (S ∪ T). (λx. if x ≤ c then f x else g x) differentiable at x)"
by auto
moreover
{ assume fcon: "continuous_on ({a<..<c} - S) (λx. vector_derivative f (at x))"
and gcon: "continuous_on ({c<..<b} - T) (λx. vector_derivative g (at x))"
have "open ({a<..<c} - S)"  "open ({c<..<b} - T)"
using st by (simp_all add: open_Diff finite_imp_closed)
moreover have "continuous_on ({a<..<c} - S) (λx. vector_derivative (λx. if x ≤ c then f x else g x) (at x))"
proof -
have "((λx. if x ≤ c then f x else g x) has_vector_derivative vector_derivative f (at x))            (at x)"
if "a < x" "x < c" "x ∉ S" for x
proof -
have f: "f differentiable at x"
by (meson C1_differentiable_on_eq Diff_iff atLeastAtMost_iff less_eq_real_def st(1) that)
show ?thesis
using that
apply (rule_tac f=f and d="dist x c" in has_vector_derivative_transform_within)
apply (auto simp: dist_norm vector_derivative_works [symmetric] f)
done
qed
then show ?thesis
by (metis (no_types, lifting) continuous_on_eq [OF fcon] DiffE greaterThanLessThan_iff vector_derivative_at)
qed
moreover have "continuous_on ({c<..<b} - T) (λx. vector_derivative (λx. if x ≤ c then f x else g x) (at x))"
proof -
have "((λx. if x ≤ c then f x else g x) has_vector_derivative vector_derivative g (at x))            (at x)"
if "c < x" "x < b" "x ∉ T" for x
proof -
have g: "g differentiable at x"
by (metis C1_differentiable_on_eq DiffD1 DiffI atLeastAtMost_diff_ends greaterThanLessThan_iff st(2) that)
show ?thesis
using that
apply (rule_tac f=g and d="dist x c" in has_vector_derivative_transform_within)
apply (auto simp: dist_norm vector_derivative_works [symmetric] g)
done
qed
then show ?thesis
by (metis (no_types, lifting) continuous_on_eq [OF gcon] DiffE greaterThanLessThan_iff vector_derivative_at)
qed
ultimately have "continuous_on ({a<..<b} - insert c (S ∪ T))
(λx. vector_derivative (λx. if x ≤ c then f x else g x) (at x))"
by (rule continuous_on_subset [OF continuous_on_open_Un], auto)
} note * = this
have "continuous_on ({a<..<b} - insert c (S ∪ T)) (λx. vector_derivative (λx. if x ≤ c then f x else g x) (at x))"
using st
by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset intro: *)
ultimately have "∃S. finite S ∧ ((λx. if x ≤ c then f x else g x) C1_differentiable_on {a..b} - S)"
apply (rule_tac x="{a,b,c} ∪ S ∪ T" in exI)
using st  by (auto simp: C1_differentiable_on_eq elim!: continuous_on_subset)
with cab show ?thesis
qed

lemma piecewise_C1_differentiable_neg:
"f piecewise_C1_differentiable_on S ⟹ (λx. -(f x)) piecewise_C1_differentiable_on S"
unfolding piecewise_C1_differentiable_on_def
by (auto intro!: continuous_on_minus C1_differentiable_on_minus)

assumes "f piecewise_C1_differentiable_on i"
"g piecewise_C1_differentiable_on i"
shows "(λx. f x + g x) piecewise_C1_differentiable_on i"
proof -
obtain S t where st: "finite S" "finite t"
"f C1_differentiable_on (i-S)"
"g C1_differentiable_on (i-t)"
using assms by (auto simp: piecewise_C1_differentiable_on_def)
then have "finite (S ∪ t) ∧ (λx. f x + g x) C1_differentiable_on i - (S ∪ t)"
by (auto intro: C1_differentiable_on_add elim!: C1_differentiable_on_subset)
moreover have "continuous_on i f" "continuous_on i g"
using assms piecewise_C1_differentiable_on_def by auto
ultimately show ?thesis
qed

lemma piecewise_C1_differentiable_diff:
"⟦f piecewise_C1_differentiable_on S;  g piecewise_C1_differentiable_on S⟧
⟹ (λx. f x - g x) piecewise_C1_differentiable_on S"

lemma piecewise_C1_differentiable_D1:
fixes g1 :: "real ⇒ 'a::real_normed_field"
assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}"
shows "g1 piecewise_C1_differentiable_on {0..1}"
proof -
obtain S where "finite S"
and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))"
and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x"
using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have g1D: "g1 differentiable at x" if "x ∈ {0..1} - insert 1 (( *) 2 ` S)" for x
proof (rule differentiable_transform_within)
show "g1 +++ g2 ∘ ( *) (inverse 2) differentiable at x"
using that g12D
apply (simp only: joinpaths_def)
by (rule differentiable_chain_at derivative_intros | force)+
show "⋀x'. ⟦dist x' x < dist (x/2) (1/2)⟧
⟹ (g1 +++ g2 ∘ ( *) (inverse 2)) x' = g1 x'"
using that by (auto simp: dist_real_def joinpaths_def)
qed (use that in ‹auto simp: dist_real_def›)
have [simp]: "vector_derivative (g1 ∘ ( *) 2) (at (x/2)) = 2 *⇩R vector_derivative g1 (at x)"
if "x ∈ {0..1} - insert 1 (( *) 2 ` S)" for x
apply (subst vector_derivative_chain_at)
using that
apply (rule derivative_eq_intros g1D | simp)+
done
have "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))"
using co12 by (rule continuous_on_subset) force
then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) S) (λx. vector_derivative (g1 ∘ ( *)2) (at x))"
proof (rule continuous_on_eq [OF _ vector_derivative_at])
show "(g1 +++ g2 has_vector_derivative vector_derivative (g1 ∘ ( *) 2) (at x)) (at x)"
if "x ∈ {0..1/2} - insert (1/2) S" for x
proof (rule has_vector_derivative_transform_within)
show "(g1 ∘ ( *) 2 has_vector_derivative vector_derivative (g1 ∘ ( *) 2) (at x)) (at x)"
using that
by (force intro: g1D differentiable_chain_at simp: vector_derivative_works [symmetric])
show "⋀x'. ⟦dist x' x < dist x (1/2)⟧ ⟹ (g1 ∘ ( *) 2) x' = (g1 +++ g2) x'"
using that by (auto simp: dist_norm joinpaths_def)
qed (use that in ‹auto simp: dist_norm›)
qed
have "continuous_on ({0..1} - insert 1 (( *) 2 ` S))
((λx. 1/2 * vector_derivative (g1 ∘ ( *)2) (at x)) ∘ ( *)(1/2))"
apply (rule continuous_intros)+
using coDhalf
apply (simp add: scaleR_conv_of_real image_set_diff image_image)
done
then have con_g1: "continuous_on ({0..1} - insert 1 (( *) 2 ` S)) (λx. vector_derivative g1 (at x))"
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g1"
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
with ‹finite S› show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
apply (rule_tac x="insert 1 ((( *)2)`S)" in exI)
done
qed

lemma piecewise_C1_differentiable_D2:
fixes g2 :: "real ⇒ 'a::real_normed_field"
assumes "(g1 +++ g2) piecewise_C1_differentiable_on {0..1}" "pathfinish g1 = pathstart g2"
shows "g2 piecewise_C1_differentiable_on {0..1}"
proof -
obtain S where "finite S"
and co12: "continuous_on ({0..1} - S) (λx. vector_derivative (g1 +++ g2) (at x))"
and g12D: "∀x∈{0..1} - S. g1 +++ g2 differentiable at x"
using assms  by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have g2D: "g2 differentiable at x" if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x
proof (rule differentiable_transform_within)
show "g1 +++ g2 ∘ (λx. (x + 1) / 2) differentiable at x"
using g12D that
apply (simp only: joinpaths_def)
apply (drule_tac x= "(x+1) / 2" in bspec, force simp: divide_simps)
apply (rule differentiable_chain_at derivative_intros | force)+
done
show "⋀x'. dist x' x < dist ((x + 1) / 2) (1/2) ⟹ (g1 +++ g2 ∘ (λx. (x + 1) / 2)) x' = g2 x'"
using that by (auto simp: dist_real_def joinpaths_def field_simps)
qed (use that in ‹auto simp: dist_norm›)
have [simp]: "vector_derivative (g2 ∘ (λx. 2*x-1)) (at ((x+1)/2)) = 2 *⇩R vector_derivative g2 (at x)"
if "x ∈ {0..1} - insert 0 ((λx. 2*x-1) ` S)" for x
using that  by (auto simp: vector_derivative_chain_at divide_simps g2D)
have "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g1 +++ g2) (at x))"
using co12 by (rule continuous_on_subset) force
then have coDhalf: "continuous_on ({1/2..1} - insert (1/2) S) (λx. vector_derivative (g2 ∘ (λx. 2*x-1)) (at x))"
proof (rule continuous_on_eq [OF _ vector_derivative_at])
show "(g1 +++ g2 has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x))
(at x)"
if "x ∈ {1 / 2..1} - insert (1 / 2) S" for x
proof (rule_tac f="g2 ∘ (λx. 2*x-1)" and d="dist (3/4) ((x+1)/2)" in has_vector_derivative_transform_within)
show "(g2 ∘ (λx. 2 * x - 1) has_vector_derivative vector_derivative (g2 ∘ (λx. 2 * x - 1)) (at x))
(at x)"
using that by (force intro: g2D differentiable_chain_at simp: vector_derivative_works [symmetric])
show "⋀x'. ⟦dist x' x < dist (3 / 4) ((x + 1) / 2)⟧ ⟹ (g2 ∘ (λx. 2 * x - 1)) x' = (g1 +++ g2) x'"
using that by (auto simp: dist_norm joinpaths_def add_divide_distrib)
qed (use that in ‹auto simp: dist_norm›)
qed
have [simp]: "((λx. (x+1) / 2) ` ({0..1} - insert 0 ((λx. 2 * x - 1) ` S))) = ({1/2..1} - insert (1/2) S)"
apply (simp add: image_set_diff inj_on_def image_image)
done
have "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S))
((λx. 1/2 * vector_derivative (g2 ∘ (λx. 2*x-1)) (at x)) ∘ (λx. (x+1)/2))"
by (rule continuous_intros | simp add:  coDhalf)+
then have con_g2: "continuous_on ({0..1} - insert 0 ((λx. 2*x-1) ` S)) (λx. vector_derivative g2 (at x))"
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g2"
using continuous_on_joinpaths_D2 assms piecewise_C1_differentiable_on_def by blast
with ‹finite S› show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
apply (rule_tac x="insert 0 ((λx. 2 * x - 1) ` S)" in exI)
done
qed

subsection ‹Valid paths, and their start and finish›

definition valid_path :: "(real ⇒ 'a :: real_normed_vector) ⇒ bool"
where "valid_path f ≡ f piecewise_C1_differentiable_on {0..1::real}"

definition closed_path :: "(real ⇒ 'a :: real_normed_vector) ⇒ bool"
where "closed_path g ≡ g 0 = g 1"

subsubsection‹In particular, all results for paths apply›

lemma valid_path_imp_path: "valid_path g ⟹ path g"
by (simp add: path_def piecewise_C1_differentiable_on_def valid_path_def)

lemma connected_valid_path_image: "valid_path g ⟹ connected(path_image g)"
by (metis connected_path_image valid_path_imp_path)

lemma compact_valid_path_image: "valid_path g ⟹ compact(path_image g)"
by (metis compact_path_image valid_path_imp_path)

lemma bounded_valid_path_image: "valid_path g ⟹ bounded(path_image g)"
by (metis bounded_path_image valid_path_imp_path)

lemma closed_valid_path_image: "valid_path g ⟹ closed(path_image g)"
by (metis closed_path_image valid_path_imp_path)

proposition valid_path_compose:
assumes "valid_path g"
and der: "⋀x. x ∈ path_image g ⟹ f field_differentiable (at x)"
and con: "continuous_on (path_image g) (deriv f)"
shows "valid_path (f ∘ g)"
proof -
obtain S where "finite S" and g_diff: "g C1_differentiable_on {0..1} - S"
using ‹valid_path g› unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
have "f ∘ g differentiable at t" when "t∈{0..1} - S" for t
proof (rule differentiable_chain_at)
show "g differentiable at t" using ‹valid_path g›
by (meson C1_differentiable_on_eq ‹g C1_differentiable_on {0..1} - S› that)
next
have "g t∈path_image g" using that DiffD1 image_eqI path_image_def by metis
then show "f differentiable at (g t)"
using der[THEN field_differentiable_imp_differentiable] by auto
qed
moreover have "continuous_on ({0..1} - S) (λx. vector_derivative (f ∘ g) (at x))"
proof (rule continuous_on_eq [where f = "λx. vector_derivative g (at x) * deriv f (g x)"],
rule continuous_intros)
show "continuous_on ({0..1} - S) (λx. vector_derivative g (at x))"
using g_diff C1_differentiable_on_eq by auto
next
have "continuous_on {0..1} (λx. deriv f (g x))"
using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
‹valid_path g› piecewise_C1_differentiable_on_def valid_path_def
by blast
then show "continuous_on ({0..1} - S) (λx. deriv f (g x))"
using continuous_on_subset by blast
next
show "vector_derivative g (at t) * deriv f (g t) = vector_derivative (f ∘ g) (at t)"
when "t ∈ {0..1} - S" for t
proof (rule vector_derivative_chain_at_general[symmetric])
show "g differentiable at t" by (meson C1_differentiable_on_eq g_diff that)
next
have "g t∈path_image g" using that DiffD1 image_eqI path_image_def by metis
then show "f field_differentiable at (g t)" using der by auto
qed
qed
ultimately have "f ∘ g C1_differentiable_on {0..1} - S"
using C1_differentiable_on_eq by blast
moreover have "path (f ∘ g)"
apply (rule path_continuous_image[OF valid_path_imp_path[OF ‹valid_path g›]])
using der
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using ‹finite S› by auto
qed

lemma valid_path_uminus_comp[simp]:
fixes g::"real ⇒ 'a ::real_normed_field"
shows "valid_path (uminus ∘ g) ⟷ valid_path g"
proof
show "valid_path g ⟹ valid_path (uminus ∘ g)" for g::"real ⇒ 'a"
by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])
then show "valid_path g" when "valid_path (uminus ∘ g)"
by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
qed

lemma valid_path_offset[simp]:
shows "valid_path (λt. g t - z) ⟷ valid_path g"
proof
show *: "valid_path (g::real⇒'a) ⟹ valid_path (λt. g t - z)" for g z
unfolding valid_path_def
by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
show "valid_path (λt. g t - z) ⟹ valid_path g"
using *[of "λt. g t - z" "-z",simplified] .
qed

subsection‹Contour Integrals along a path›

text‹This definition is for complex numbers only, and does not generalise to line integrals in a vector field›

text‹piecewise differentiable function on [0,1]›

definition has_contour_integral :: "(complex ⇒ complex) ⇒ complex ⇒ (real ⇒ complex) ⇒ bool"
(infixr "has'_contour'_integral" 50)
where "(f has_contour_integral i) g ≡
((λx. f(g x) * vector_derivative g (at x within {0..1}))
has_integral i) {0..1}"

definition contour_integrable_on
(infixr "contour'_integrable'_on" 50)
where "f contour_integrable_on g ≡ ∃i. (f has_contour_integral i) g"

definition contour_integral
where "contour_integral g f ≡ SOME i. (f has_contour_integral i) g ∨ ¬ f contour_integrable_on g ∧ i=0"

lemma not_integrable_contour_integral: "¬ f contour_integrable_on g ⟹ contour_integral g f = 0"
unfolding contour_integrable_on_def contour_integral_def by blast

lemma contour_integral_unique: "(f has_contour_integral i) g ⟹ contour_integral g f = i"
apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
using has_integral_unique by blast

corollary has_contour_integral_eqpath:
"⟦(f has_contour_integral y) p; f contour_integrable_on γ;
contour_integral p f = contour_integral γ f⟧
⟹ (f has_contour_integral y) γ"
using contour_integrable_on_def contour_integral_unique by auto

lemma has_contour_integral_integral:
"f contour_integrable_on i ⟹ (f has_contour_integral (contour_integral i f)) i"
by (metis contour_integral_unique contour_integrable_on_def)

lemma has_contour_integral_unique:
"(f has_contour_integral i) g ⟹ (f has_contour_integral j) g ⟹ i = j"
using has_integral_unique
by (auto simp: has_contour_integral_def)

lemma has_contour_integral_integrable: "(f has_contour_integral i) g ⟹ f contour_integrable_on g"
using contour_integrable_on_def by blast

subsubsection‹Show that we can forget about the localized derivative.›

lemma has_integral_localized_vector_derivative:
"((λx. f (g x) * vector_derivative g (at x within {a..b})) has_integral i) {a..b} ⟷
((λx. f (g x) * vector_derivative g (at x)) has_integral i) {a..b}"
proof -
have *: "{a..b} - {a,b} = interior {a..b}"
show ?thesis
apply (rule has_integral_spike_eq [of "{a,b}"])
apply (auto simp: at_within_interior [of _ "{a..b}"])
done
qed

lemma integrable_on_localized_vector_derivative:
"(λx. f (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b} ⟷
(λx. f (g x) * vector_derivative g (at x)) integrable_on {a..b}"

lemma has_contour_integral:
"(f has_contour_integral i) g ⟷
((λx. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"

lemma contour_integrable_on:
"f contour_integrable_on g ⟷
(λt. f(g t) * vector_derivative g (at t)) integrable_on {0..1}"
by (simp add: has_contour_integral integrable_on_def contour_integrable_on_def)

subsection‹Reversing a path›

lemma valid_path_imp_reverse:
assumes "valid_path g"
shows "valid_path(reversepath g)"
proof -
obtain S where "finite S" and S: "g C1_differentiable_on ({0..1} - S)"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
then have "finite ((-) 1 ` S)"
by auto
moreover have "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` S))"
unfolding reversepath_def
apply (rule C1_differentiable_compose [of "λx::real. 1-x" _ g, unfolded o_def])
using S
by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+
ultimately show ?thesis using assms
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
qed

lemma valid_path_reversepath [simp]: "valid_path(reversepath g) ⟷ valid_path g"
using valid_path_imp_reverse by force

lemma has_contour_integral_reversepath:
assumes "valid_path g" and f: "(f has_contour_integral i) g"
shows "(f has_contour_integral (-i)) (reversepath g)"
proof -
{ fix S x
assume xs: "g C1_differentiable_on ({0..1} - S)" "x ∉ (-) 1 ` S" "0 ≤ x" "x ≤ 1"
have "vector_derivative (λx. g (1 - x)) (at x within {0..1}) =
- vector_derivative g (at (1 - x) within {0..1})"
proof -
obtain f' where f': "(g has_vector_derivative f') (at (1 - x))"
using xs
by (force simp: has_vector_derivative_def C1_differentiable_on_def)
have "(g ∘ (λx. 1 - x) has_vector_derivative -1 *⇩R f') (at x)"
by (intro vector_diff_chain_within has_vector_derivative_at_within [OF f'] derivative_eq_intros | simp)+
then have mf': "((λx. g (1 - x)) has_vector_derivative -f') (at x)"
show ?thesis
using xs
by (auto simp: vector_derivative_at_within_ivl [OF mf'] vector_derivative_at_within_ivl [OF f'])
qed
} note * = this
obtain S where S: "continuous_on {0..1} g" "finite S" "g C1_differentiable_on {0..1} - S"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
have "((λx. - (f (g (1 - x)) * vector_derivative g (at (1 - x) within {0..1}))) has_integral -i)
{0..1}"
using has_integral_affinity01 [where m= "-1" and c=1, OF f [unfolded has_contour_integral_def]]
then show ?thesis
using S
apply (clarsimp simp: reversepath_def has_contour_integral_def)
apply (rule_tac S = "(λx. 1 - x) ` S" in has_integral_spike_finite)
apply (auto simp: *)
done
qed

lemma contour_integrable_reversepath:
"valid_path g ⟹ f contour_integrable_on g ⟹ f contour_integrable_on (reversepath g)"
using has_contour_integral_reversepath contour_integrable_on_def by blast

lemma contour_integrable_reversepath_eq:
"valid_path g ⟹ (f contour_integrable_on (reversepath g) ⟷ f contour_integrable_on g)"
using contour_integrable_reversepath valid_path_reversepath by fastforce

lemma contour_integral_reversepath:
assumes "valid_path g"
shows "contour_integral (reversepath g) f = - (contour_integral g f)"
proof (cases "f contour_integrable_on g")
case True then show ?thesis
by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
next
case False then have "~ f contour_integrable_on (reversepath g)"
with False show ?thesis by (simp add: not_integrable_contour_integral)
qed

subsection‹Joining two paths together›

lemma valid_path_join:
assumes "valid_path g1" "valid_path g2" "pathfinish g1 = pathstart g2"
shows "valid_path(g1 +++ g2)"
proof -
have "g1 1 = g2 0"
using assms by (auto simp: pathfinish_def pathstart_def)
moreover have "(g1 ∘ (λx. 2*x)) piecewise_C1_differentiable_on {0..1/2}"
apply (rule piecewise_C1_differentiable_compose)
using assms
apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
done
moreover have "(g2 ∘ (λx. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
apply (rule piecewise_C1_differentiable_compose)
using assms unfolding valid_path_def piecewise_C1_differentiable_on_def
by (auto intro!: continuous_intros finite_vimageI [where h = "(λx. 2*x - 1)"] inj_onI
simp: image_affinity_atLeastAtMost_diff continuous_on_joinpaths)
ultimately show ?thesis
apply (simp only: valid_path_def continuous_on_joinpaths joinpaths_def)
apply (rule piecewise_C1_differentiable_cases)
apply (auto simp: o_def)
done
qed

lemma valid_path_join_D1:
fixes g1 :: "real ⇒ 'a::real_normed_field"
shows "valid_path (g1 +++ g2) ⟹ valid_path g1"
unfolding valid_path_def
by (rule piecewise_C1_differentiable_D1)

lemma valid_path_join_D2:
fixes g2 :: "real ⇒ 'a::real_normed_field"
shows "⟦valid_path (g1 +++ g2); pathfinish g1 = pathstart g2⟧ ⟹ valid_path g2"
unfolding valid_path_def
by (rule piecewise_C1_differentiable_D2)

lemma valid_path_join_eq [simp]:
fixes g2 :: "real ⇒ 'a::real_normed_field"
shows "pathfinish g1 = pathstart g2 ⟹ (valid_path(g1 +++ g2) ⟷ valid_path g1 ∧ valid_path g2)"
using valid_path_join_D1 valid_path_join_D2 valid_path_join by blast

lemma has_contour_integral_join:
assumes "(f has_contour_integral i1) g1" "(f has_contour_integral i2) g2"
"valid_path g1" "valid_path g2"
shows "(f has_contour_integral (i1 + i2)) (g1 +++ g2)"
proof -
obtain s1 s2
where s1: "finite s1" "∀x∈{0..1} - s1. g1 differentiable at x"
and s2: "finite s2" "∀x∈{0..1} - s2. g2 differentiable at x"
using assms
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have 1: "((λx. f (g1 x) * vector_derivative g1 (at x)) has_integral i1) {0..1}"
and 2: "((λx. f (g2 x) * vector_derivative g2 (at x)) has_integral i2) {0..1}"
using assms
by (auto simp: has_contour_integral)
have i1: "((λx. (2*f (g1 (2*x))) * vector_derivative g1 (at (2*x))) has_integral i1) {0..1/2}"
and i2: "((λx. (2*f (g2 (2*x - 1))) * vector_derivative g2 (at (2*x - 1))) has_integral i2) {1/2..1}"
using has_integral_affinity01 [OF 1, where m= 2 and c=0, THEN has_integral_cmul [where c=2]]
has_integral_affinity01 [OF 2, where m= 2 and c="-1", THEN has_integral_cmul [where c=2]]
by (simp_all only: image_affinity_atLeastAtMost_div_diff, simp_all add: scaleR_conv_of_real mult_ac)
have g1: "⟦0 ≤ z; z*2 < 1; z*2 ∉ s1⟧ ⟹
vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *⇩R vector_derivative g1 (at (z*2))" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g1(2*x))" and d = "¦z - 1/2¦"]])
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. 2*x" 2 _ g1, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
using s1
apply (auto simp: algebra_simps vector_derivative_works)
done
have g2: "⟦1 < z*2; z ≤ 1; z*2 - 1 ∉ s2⟧ ⟹
vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at z) =
2 *⇩R vector_derivative g2 (at (z*2 - 1))" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g2 (2*x - 1))" and d = "¦z - 1/2¦"]])
apply (simp_all add: dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. 2*x - 1" 2 _ g2, simplified o_def])
apply (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
using s2
apply (auto simp: algebra_simps vector_derivative_works)
done
have "((λx. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (( *)2 -` s1)"])
using s1
apply (force intro: finite_vimageI [where h = "( *)2"] inj_onI)
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
done
moreover have "((λx. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
apply (rule has_integral_spike_finite [OF _ _ i2, of "insert (1/2) ((λx. 2*x-1) -` s2)"])
using s2
apply (force intro: finite_vimageI [where h = "λx. 2*x-1"] inj_onI)
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
done
ultimately
show ?thesis
apply (rule has_integral_combine [where c = "1/2"], auto)
done
qed

lemma contour_integrable_joinI:
assumes "f contour_integrable_on g1" "f contour_integrable_on g2"
"valid_path g1" "valid_path g2"
shows "f contour_integrable_on (g1 +++ g2)"
using assms
by (meson has_contour_integral_join contour_integrable_on_def)

lemma contour_integrable_joinD1:
assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g1"
shows "f contour_integrable_on g1"
proof -
obtain s1
where s1: "finite s1" "∀x∈{0..1} - s1. g1 differentiable at x"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have "(λx. f ((g1 +++ g2) (x/2)) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
using assms
apply (auto simp: contour_integrable_on)
apply (drule integrable_on_subcbox [where a=0 and b="1/2"])
apply (auto intro: integrable_affinity [of _ 0 "1/2::real" "1/2" 0, simplified])
done
then have *: "(λx. (f ((g1 +++ g2) (x/2))/2) * vector_derivative (g1 +++ g2) (at (x/2))) integrable_on {0..1}"
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
have g1: "⟦0 < z; z < 1; z ∉ s1⟧ ⟹
vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2)) =
2 *⇩R vector_derivative g1 (at z)"  for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g1(2*x))" and d = "¦(z-1)/2¦"]])
apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. x*2" 2 _ g1, simplified o_def])
using s1
apply (auto simp: vector_derivative_works has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
done
show ?thesis
using s1
apply (auto simp: contour_integrable_on)
apply (rule integrable_spike_finite [of "{0,1} ∪ s1", OF _ _ *])
apply (auto simp: joinpaths_def scaleR_conv_of_real g1)
done
qed

lemma contour_integrable_joinD2:
assumes "f contour_integrable_on (g1 +++ g2)" "valid_path g2"
shows "f contour_integrable_on g2"
proof -
obtain s2
where s2: "finite s2" "∀x∈{0..1} - s2. g2 differentiable at x"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have "(λx. f ((g1 +++ g2) (x/2 + 1/2)) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2))) integrable_on {0..1}"
using assms
apply (auto simp: contour_integrable_on)
apply (drule integrable_on_subcbox [where a="1/2" and b=1], auto)
apply (drule integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2", simplified])
done
then have *: "(λx. (f ((g1 +++ g2) (x/2 + 1/2))/2) * vector_derivative (g1 +++ g2) (at (x/2 + 1/2)))
integrable_on {0..1}"
by (auto dest: integrable_cmul [where c="1/2"] simp: scaleR_conv_of_real)
have g2: "⟦0 < z; z < 1; z ∉ s2⟧ ⟹
vector_derivative (λx. if x*2 ≤ 1 then g1 (2*x) else g2 (2*x - 1)) (at (z/2+1/2)) =
2 *⇩R vector_derivative g2 (at z)" for z
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g2(2*x-1))" and d = "¦z/2¦"]])
apply (simp_all add: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. x*2-1" 2 _ g2, simplified o_def])
using s2
apply (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left
done
show ?thesis
using s2
apply (auto simp: contour_integrable_on)
apply (rule integrable_spike_finite [of "{0,1} ∪ s2", OF _ _ *])
apply (auto simp: joinpaths_def scaleR_conv_of_real g2)
done
qed

lemma contour_integrable_join [simp]:
shows
"⟦valid_path g1; valid_path g2⟧
⟹ f contour_integrable_on (g1 +++ g2) ⟷ f contour_integrable_on g1 ∧ f contour_integrable_on g2"
using contour_integrable_joinD1 contour_integrable_joinD2 contour_integrable_joinI by blast

lemma contour_integral_join [simp]:
shows
"⟦f contour_integrable_on g1; f contour_integrable_on g2; valid_path g1; valid_path g2⟧
⟹ contour_integral (g1 +++ g2) f = contour_integral g1 f + contour_integral g2 f"
by (simp add: has_contour_integral_integral has_contour_integral_join contour_integral_unique)

subsection‹Shifting the starting point of a (closed) path›

lemma shiftpath_alt_def: "shiftpath a f = (λx. if x ≤ 1-a then f (a + x) else f (a + x - 1))"
by (auto simp: shiftpath_def)

lemma valid_path_shiftpath [intro]:
assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
shows "valid_path(shiftpath a g)"
using assms
apply (auto simp: valid_path_def shiftpath_alt_def)
apply (rule piecewise_C1_differentiable_cases)
apply (auto simp: algebra_simps)
apply (rule piecewise_C1_differentiable_affine [of g 1 a, simplified o_def scaleR_one])
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
apply (rule piecewise_C1_differentiable_affine [of g 1 "a-1", simplified o_def scaleR_one algebra_simps])
apply (auto simp: pathfinish_def pathstart_def elim: piecewise_C1_differentiable_on_subset)
done

lemma has_contour_integral_shiftpath:
assumes f: "(f has_contour_integral i) g" "valid_path g"
and a: "a ∈ {0..1}"
shows "(f has_contour_integral i) (shiftpath a g)"
proof -
obtain s
where s: "finite s" and g: "∀x∈{0..1} - s. g differentiable at x"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have *: "((λx. f (g x) * vector_derivative g (at x)) has_integral i) {0..1}"
using assms by (auto simp: has_contour_integral)
then have i: "i = integral {a..1} (λx. f (g x) * vector_derivative g (at x)) +
integral {0..a} (λx. f (g x) * vector_derivative g (at x))"
apply (rule has_integral_unique)
apply (subst integral_combine)
using assms * integral_unique by auto
{ fix x
have "0 ≤ x ⟹ x + a < 1 ⟹ x ∉ (λx. x - a) ` s ⟹
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
unfolding shiftpath_def
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g(a+x))" and d = "dist(1-a) x"]])
apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. x+a" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
using g
apply (drule_tac x="x+a" in bspec)
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute)
done
} note vd1 = this
{ fix x
have "1 < x + a ⟹ x ≤ 1 ⟹ x ∉ (λx. x - a + 1) ` s ⟹
vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
unfolding shiftpath_def
apply (rule vector_derivative_at [OF has_vector_derivative_transform_within [where f = "(λx. g(a+x-1))" and d = "dist (1-a) x"]])
apply (auto simp: field_simps dist_real_def abs_if split: if_split_asm)
apply (rule vector_diff_chain_at [of "λx. x+a-1" 1 _ g, simplified o_def scaleR_one])
apply (intro derivative_eq_intros | simp)+
using g
apply (drule_tac x="x+a-1" in bspec)
using a apply (auto simp: has_vector_derivative_def vector_derivative_works image_def add.commute)
done
} note vd2 = this
have va1: "(λx. f (g x) * vector_derivative g (at x)) integrable_on ({a..1})"
using * a   by (fastforce intro: integrable_subinterval_real)
have v0a: "(λx. f (g x) * vector_derivative g (at x)) integrable_on ({0..a})"
apply (rule integrable_subinterval_real)
using * a by auto
have "((λx. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
has_integral  integral {a..1} (λx. f (g x) * vector_derivative g (at x)))  {0..1 - a}"
apply (rule has_integral_spike_finite
[where S = "{1-a} ∪ (λx. x-a) ` s" and f = "λx. f(g(a+x)) * vector_derivative g (at(a+x))"])
using s apply blast
using a apply (auto simp: algebra_simps vd1)
using has_integral_affinity [where m=1 and c=a, simplified, OF integrable_integral [OF va1]]
done
moreover
have "((λx. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
has_integral  integral {0..a} (λx. f (g x) * vector_derivative g (at x)))  {1 - a..1}"
apply (rule has_integral_spike_finite
[where S = "{1-a} ∪ (λx. x-a+1) ` s" and f = "λx. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
using s apply blast
using a apply (auto simp: algebra_simps vd2)
using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]]
apply (simp add: image_affinity_atLeastAtMost [where m=1 and c="1-a", simplified])
done
ultimately show ?thesis
using a
by (auto simp: i has_contour_integral intro: has_integral_combine [where c = "1-a"])
qed

lemma has_contour_integral_shiftpath_D:
assumes "(f has_contour_integral i) (shiftpath a g)"
"valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
shows "(f has_contour_integral i) g"
proof -
obtain s
where s: "finite s" and g: "∀x∈{0..1} - s. g differentiable at x"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
{ fix x
assume x: "0 < x" "x < 1" "x ∉ s"
then have gx: "g differentiable at x"
using g by auto
have "vector_derivative g (at x within {0..1}) =
vector_derivative (shiftpath (1 - a) (shiftpath a g)) (at x within {0..1})"
apply (rule vector_derivative_at_within_ivl
[OF has_vector_derivative_transform_within_open
[where f = "(shiftpath (1 - a) (shiftpath a g))" and S = "{0<..<1}-s"]])
using s g assms x
apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric])
apply (rule differentiable_transform_within [OF gx, of "min x (1-x)"])
apply (auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)
done
} note vd = this
have fi: "(f has_contour_integral i) (shiftpath (1 - a) (shiftpath a g))"
using assms  by (auto intro!: has_contour_integral_shiftpath)
show ?thesis
apply (rule has_integral_spike_finite [of "{0,1} ∪ s", OF _ _  fi [unfolded has_contour_integral_def]])
using s assms vd
apply (auto simp: Path_Connected.shiftpath_shiftpath)
done
qed

lemma has_contour_integral_shiftpath_eq:
assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
shows "(f has_contour_integral i) (shiftpath a g) ⟷ (f has_contour_integral i) g"
using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast

lemma contour_integrable_on_shiftpath_eq:
assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
shows "f contour_integrable_on (shiftpath a g) ⟷ f contour_integrable_on g"
using assms contour_integrable_on_def has_contour_integral_shiftpath_eq by auto

lemma contour_integral_shiftpath:
assumes "valid_path g" "pathfinish g = pathstart g" "a ∈ {0..1}"
shows "contour_integral (shiftpath a g) f = contour_integral g f"
using assms
by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq)

lemma has_vector_derivative_linepath_within:
"(linepath a b has_vector_derivative (b - a)) (at x within s)"
apply (simp add: linepath_def has_vector_derivative_def algebra_simps)
apply (rule derivative_eq_intros | simp)+
done

lemma vector_derivative_linepath_within:
"x ∈ {0..1} ⟹ vector_derivative (linepath a b) (at x within {0..1}) = b - a"
apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
apply (auto simp: has_vector_derivative_linepath_within)
done

lemma vector_derivative_linepath_at [simp]: "vector_derivative (linepath a b) (at x) = b - a"

lemma valid_path_linepath [iff]: "valid_path (linepath a b)"
apply (simp add: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq continuous_on_linepath)
apply (rule_tac x="{}" in exI)
using has_vector_derivative_def has_vector_derivative_linepath_within
done

lemma has_contour_integral_linepath:
shows "(f has_contour_integral i) (linepath a b) ⟷
((λx. f(linepath a b x) * (b - a)) has_integral i) {0..1}"

lemma linepath_in_path:
shows "x ∈ {0..1} ⟹ linepath a b x ∈ closed_segment a b"
by (auto simp: segment linepath_def)

lemma linepath_image_01: "linepath a b ` {0..1} = closed_segment a b"
by (auto simp: segment linepath_def)

lemma linepath_in_convex_hull:
fixes x::real
assumes a: "a ∈ convex hull s"
and b: "b ∈ convex hull s"
and x: "0≤x" "x≤1"
shows "linepath a b x ∈ convex hull s"
apply (rule closed_segment_subset_convex_hull [OF a b, THEN subsetD])
using x
apply (auto simp: linepath_image_01 [symmetric])
done

lemma Re_linepath: "Re(linepath (of_real a) (of_real b) x) = (1 - x)*a + x*b"

lemma Im_linepath: "Im(linepath (of_real a) (of_real b) x) = 0"

lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"

lemma has_contour_integral_trivial_iff [simp]: "(f has_contour_integral i) (linepath a a) ⟷ i=0"
using has_contour_integral_unique by blast

lemma contour_integral_trivial [simp]: "contour_integral (linepath a a) f = 0"
using has_contour_integral_trivial contour_integral_unique by blast

subsection‹Relation to subpath construction›

lemma valid_path_subpath:
fixes g :: "real ⇒ 'a :: real_normed_vector"
assumes "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}"
shows "valid_path(subpath u v g)"
proof (cases "v=u")
case True
then show ?thesis
unfolding valid_path_def subpath_def
by (force intro: C1_differentiable_on_const C1_differentiable_imp_piecewise)
next
case False
have "(g ∘ (λx. ((v-u) * x + u))) piecewise_C1_differentiable_on {0..1}"
apply (rule piecewise_C1_differentiable_compose)
using assms False
apply (auto simp: algebra_simps valid_path_def piecewise_C1_differentiable_on_subset)
apply (subst Int_commute)
apply (auto simp: inj_on_def algebra_simps crossproduct_eq finite_vimage_IntI)
done
then show ?thesis
by (auto simp: o_def valid_path_def subpath_def)
qed

lemma has_contour_integral_subpath_refl [iff]: "(f has_contour_integral 0) (subpath u u g)"

lemma contour_integrable_subpath_refl [iff]: "f contour_integrable_on (subpath u u g)"
using has_contour_integral_subpath_refl contour_integrable_on_def by blast

lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0"

lemma has_contour_integral_subpath:
assumes f: "f contour_integrable_on g" and g: "valid_path g"
and uv: "u ∈ {0..1}" "v ∈ {0..1}" "u ≤ v"
shows "(f has_contour_integral  integral {u..v} (λx. f(g x) * vector_derivative g (at x)))
(subpath u v g)"
proof (cases "v=u")
case True
then show ?thesis
using f   by (simp add: contour_integrable_on_def subpath_def has_contour_integral)
next
case False
obtain s where s: "⋀x. x ∈ {0..1} - s ⟹ g differentiable at x" and fs: "finite s"
using g unfolding piecewise_C1_differentiable_on_def C1_differentiable_on_eq valid_path_def by blast
have *: "((λx. f (g ((v - u) * x + u)) * vector_derivative g (at ((v - u) * x + u)))
has_integral (1 / (v - u)) * integral {u..v} (λt. f (g t) * vector_derivative g (at t)))
{0..1}"
using f uv
apply (simp add: contour_integrable_on subpath_def has_contour_integral)
apply (drule integrable_on_subcbox [where a=u and b=v, simplified])
apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
apply (simp_all add: False image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
done
{ fix x
have "x ∈ {0..1} ⟹
x ∉ (λt. (v-u) *⇩R t + u) -` s ⟹
vector_derivative (λx. g ((v-u) * x + u)) (at x) = (v-u) *⇩R vector_derivative g (at ((v-u) * x + u))"
apply (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]])
apply (intro derivative_eq_intros | simp)+
apply (cut_tac s [of "(v - u) * x + u"])
using uv mult_left_le [of x "v-u"]
apply (auto simp:  vector_derivative_works)
done
} note vd = this
show ?thesis
apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
using fs assms
apply (simp add: False subpath_def has_contour_integral)
apply (rule_tac S = "(λt. ((v-u) *⇩R t + u)) -` s" in has_integral_spike_finite)
apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
done
qed

lemma contour_integrable_subpath:
assumes "f contour_integrable_on g" "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}"
shows "f contour_integrable_on (subpath u v g)"
apply (cases u v rule: linorder_class.le_cases)
apply (metis contour_integrable_on_def has_contour_integral_subpath [OF assms])
apply (subst reversepath_subpath [symmetric])
apply (rule contour_integrable_reversepath)
using assms apply (blast intro: valid_path_subpath)
using assms apply (blast intro: has_contour_integral_subpath)
done

lemma has_integral_contour_integral_subpath:
assumes "f contour_integrable_on g" "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}" "u ≤ v"
shows "(((λx. f(g x) * vector_derivative g (at x)))
has_integral  contour_integral (subpath u v g) f) {u..v}"
using assms
apply (auto simp: has_integral_integrable_integral)
apply (rule integrable_on_subcbox [where a=u and b=v and S = "{0..1}", simplified])
apply (auto simp: contour_integral_unique [OF has_contour_integral_subpath] contour_integrable_on)
done

lemma contour_integral_subcontour_integral:
assumes "f contour_integrable_on g" "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}" "u ≤ v"
shows "contour_integral (subpath u v g) f =
integral {u..v} (λx. f(g x) * vector_derivative g (at x))"
using assms has_contour_integral_subpath contour_integral_unique by blast

lemma contour_integral_subpath_combine_less:
assumes "f contour_integrable_on g" "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}" "w ∈ {0..1}"
"u<v" "v<w"
shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
contour_integral (subpath u w g) f"
using assms apply (auto simp: contour_integral_subcontour_integral)
apply (rule integral_combine, auto)
apply (rule integrable_on_subcbox [where a=u and b=w and S = "{0..1}", simplified])
apply (auto simp: contour_integrable_on)
done

lemma contour_integral_subpath_combine:
assumes "f contour_integrable_on g" "valid_path g" "u ∈ {0..1}" "v ∈ {0..1}" "w ∈ {0..1}"
shows "contour_integral (subpath u v g) f + contour_integral (subpath v w g) f =
contour_integral (subpath u w g) f"
proof (cases "u≠v ∧ v≠w ∧ u≠w")
case True
have *: "subpath v u g = reversepath(subpath u v g) ∧
subpath w u g = reversepath(subpath u w g) ∧
subpath w v g = reversepath(subpath v w g)"
by (auto simp: reversepath_subpath)
have "u < v ∧ v < w ∨
u < w ∧ w < v ∨
v < u ∧ u < w ∨
v < w ∧ w < u ∨
w < u ∧ u < v ∨
w < v ∧ v < u"
using True assms by linarith
with assms show ?thesis
using contour_integral_subpath_combine_less [of f g u v w]
contour_integral_subpath_combine_less [of f g u w v]
contour_integral_subpath_combine_less [of f g v u w]
contour_integral_subpath_combine_less [of f g v w u]
contour_integral_subpath_combine_less [of f g w u v]
contour_integral_subpath_combine_less [of f g w v u]
apply simp
apply (elim disjE)
apply (auto simp: * contour_integral_reversepath contour_integrable_subpath
valid_path_reversepath valid_path_subpath algebra_simps)
done
next
case False
then show ?thesis
apply (auto simp: contour_integral_subpath_refl)
using assms
by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath)
qed

lemma contour_integral_integral:
"contour_integral g f = integral {0..1} (λx. f (g x) * vector_derivative g (at x))"
by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)

text‹Cauchy's theorem where there's a primitive›

lemma contour_integral_primitive_lemma:
fixes f :: "complex ⇒ complex" and g :: "real ⇒ complex"
assumes "a ≤ b"
and "⋀x. x ∈ s ⟹ (f has_field_derivative f' x) (at x within s)"
and "g piecewise_differentiable_on {a..b}"  "⋀x. x ∈ {a..b} ⟹ g x ∈ s"
shows "((λx. f'(g x) * vector_derivative g (at x within {a..b}))
has_integral (f(g b) - f(g a))) {a..b}"
proof -
obtain k where k: "finite k" "∀x∈{a..b} - k. g differentiable (at x within {a..b})" and cg: "continuous_on {a..b} g"
using assms by (auto simp: piecewise_differentiable_on_def)
have cfg: "continuous_on {a..b} (λx. f (g x))"
apply (rule continuous_on_compose [OF cg, unfolded o_def])
using assms
apply (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
done
{ fix x::real
assume a: "a < x" and b: "x < b" and xk: "x ∉ k"
then have "g differentiable at x within {a..b}"
using k by (simp add: differentiable_at_withinI)
then have "(g has_vector_derivative vector_derivative g (at x within {a..b})) (at x within {a..b})"
by (simp add: vector_derivative_works has_field_derivative_def scaleR_conv_of_real)
then have gdiff: "(g has_derivative (λu. u * vector_derivative g (at x within {a..b}))) (at x within {a..b})"
have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
then have fdiff: "(f has_derivative ( *) (f' (g x))) (at (g x) within g ` {a..b})"
have "((λx. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
using diff_chain_within [OF gdiff fdiff]
by (simp add: has_vector_derivative_def scaleR_conv_of_real o_def mult_ac)
} note * = this
show ?thesis
apply (rule fundamental_theorem_of_calculus_interior_strong)
using k assms cfg *
apply (auto simp: at_within_Icc_at)
done
qed

lemma contour_integral_primitive:
assumes "⋀x. x ∈ s ⟹ (f has_field_derivative f' x) (at x within s)"
and "valid_path g" "path_image g ⊆ s"
shows "(f' has_contour_integral (f(pathfinish g) - f(pathstart g))) g"
using assms
apply (simp add: valid_path_def path_image_def pathfinish_def pathstart_def has_contour_integral_def)
apply (auto intro!: piecewise_C1_imp_differentiable contour_integral_primitive_lemma [of 0 1 s])
done

corollary Cauchy_theorem_primitive:
assumes "⋀x. x ∈ s ⟹ (f has_field_derivative f' x) (at x within s)"
and "valid_path g"  "path_image g ⊆ s" "pathfinish g = pathstart g"
shows "(f' has_contour_integral 0) g"
using assms
by (metis diff_self contour_integral_primitive)

text‹Existence of path integral for continuous function›
lemma contour_integrable_continuous_linepath:
assumes "continuous_on (closed_segment a b) f"
shows "f contour_integrable_on (linepath a b)"
proof -
have "continuous_on {0..1} ((λx. f x * (b - a)) ∘ linepath a b)"
apply (rule continuous_on_compose [OF continuous_on_linepath], simp add: linepath_image_01)
apply (rule continuous_intros | simp add: assms)+
done
then show ?thesis
apply (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric])
apply (rule integrable_continuous [of 0 "1::real", simplified])
apply (rule continuous_on_eq [where f = "λx. f(linepath a b x)*(b - a)"])
apply (auto simp: vector_derivative_linepath_within)
done
qed

lemma has_field_der_id: "((λx. x⇧2 / 2) has_field_derivative x) (at x)"
by (rule has_derivative_imp_has_field_derivative)
(rule derivative_intros | simp)+

lemma contour_integral_id [simp]: "contour_integral (linepath a b) (λy. y) = (b^2 - a^2)/2"
apply (rule contour_integral_unique)
using contour_integral_primitive [of UNIV "λx. x^2/2" "λx. x" "linepath a b"]
apply (auto simp: field_simps has_field_der_id)
done

lemma contour_integrable_on_const [iff]: "(λx. c) contour_integrable_on (linepath a b)"

lemma contour_integrable_on_id [iff]: "(λx. x) contour_integrable_on (linepath a b)"

subsection‹Arithmetical combining theorems›

lemma has_contour_integral_neg:
"(f has_contour_integral i) g ⟹ ((λx. -(f x)) has_contour_integral (-i)) g"

"⟦(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g⟧
⟹ ((λx. f1 x + f2 x) has_contour_integral (i1 + i2)) g"

lemma has_contour_integral_diff:
"⟦(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g⟧
⟹ ((λx. f1 x - f2 x) has_contour_integral (i1 - i2)) g"
by (simp add: has_integral_diff has_contour_integral_def algebra_simps)

lemma has_contour_integral_lmul:
"(f has_contour_integral i) g ⟹ ((λx. c * (f x)) has_contour_integral (c*i)) g"
apply (drule has_integral_mult_right)
done

lemma has_contour_integral_rmul:
"(f has_contour_integral i) g ⟹ ((λx. (f x) * c) has_contour_integral (i*c)) g"
apply (drule has_contour_integral_lmul)
done

lemma has_contour_integral_div:
"(f has_contour_integral i) g ⟹ ((λx. f x/c) has_contour_integral (i/c)) g"
by (simp add: field_class.field_divide_inverse) (metis has_contour_integral_rmul)

lemma has_contour_integral_eq:
"⟦(f has_contour_integral y) p; ⋀x. x ∈ path_image p ⟹ f x = g x⟧ ⟹ (g has_contour_integral y) p"
by (metis (no_types, lifting) image_eqI has_integral_eq)

lemma has_contour_integral_bound_linepath:
assumes "(f has_contour_integral i) (linepath a b)"
"0 ≤ B" "⋀x. x ∈ closed_segment a b ⟹ norm(f x) ≤ B"
shows "norm i ≤ B * norm(b - a)"
proof -
{ fix x::real
assume x: "0 ≤ x" "x ≤ 1"
have "norm (f (linepath a b x)) *
norm (vector_derivative (linepath a b) (at x within {0..1})) ≤ B * norm (b - a)"
by (auto intro: mult_mono simp: assms linepath_in_path of_real_linepath vector_derivative_linepath_within x)
} note * = this
have "norm i ≤ (B * norm (b - a)) * content (cbox 0 (1::real))"
apply (rule has_integral_bound
[of _ "λx. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
using assms * unfolding has_contour_integral_def
apply (auto simp: norm_mult)
done
then show ?thesis
by (auto simp: content_real)
qed

(*UNUSED
lemma has_contour_integral_bound_linepath_strong:
fixes a :: real and f :: "complex ⇒ real"
assumes "(f has_contour_integral i) (linepath a b)"
"finite k"
"0 ≤ B" "⋀x::real. x ∈ closed_segment a b - k ⟹ norm(f x) ≤ B"
shows "norm i ≤ B*norm(b - a)"
*)

lemma has_contour_integral_const_linepath: "((λx. c) has_contour_integral c*(b - a))(linepath a b)"
unfolding has_contour_integral_linepath
by (metis content_real diff_0_right has_integral_const_real lambda_one of_real_1 scaleR_conv_of_real zero_le_one)

lemma has_contour_integral_0: "((λx. 0) has_contour_integral 0) g"

lemma has_contour_integral_is_0:
"(⋀z. z ∈ path_image g ⟹ f z = 0) ⟹ (f has_contour_integral 0) g"
by (rule has_contour_integral_eq [OF has_contour_integral_0]) auto

lemma has_contour_integral_sum:
"⟦finite s; ⋀a. a ∈ s ⟹ (f a has_contour_integral i a) p⟧
⟹ ((λx. sum (λa. f a x) s) has_contour_integral sum i s) p"
by (induction s rule: finite_induct) (auto simp: has_contour_integral_0 has_contour_integral_add)

subsection ‹Operations on path integrals›

lemma contour_integral_const_linepath [simp]: "contour_integral (linepath a b) (λx. c) = c*(b - a)"
by (rule contour_integral_unique [OF has_contour_integral_const_linepath])

lemma contour_integral_neg:
"f contour_integrable_on g ⟹ contour_integral g (λx. -(f x)) = -(contour_integral g f)"
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_neg)

"f1 contour_integrable_on g ⟹ f2 contour_integrable_on g ⟹ contour_integral g (λx. f1 x + f2 x) =
contour_integral g f1 + contour_integral g f2"

lemma contour_integral_diff:
"f1 contour_integrable_on g ⟹ f2 contour_integrable_on g ⟹ contour_integral g (λx. f1 x - f2 x) =
contour_integral g f1 - contour_integral g f2"
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_diff)

lemma contour_integral_lmul:
shows "f contour_integrable_on g
⟹ contour_integral g (λx. c * f x) = c*contour_integral g f"
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_lmul)

lemma contour_integral_rmul:
shows "f contour_integrable_on g
⟹ contour_integral g (λx. f x * c) = contour_integral g f * c"
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_rmul)

lemma contour_integral_div:
shows "f contour_integrable_on g
⟹ contour_integral g (λx. f x / c) = contour_integral g f / c"
by (simp add: contour_integral_unique has_contour_integral_integral has_contour_integral_div)

lemma contour_integral_eq:
"(⋀x. x ∈ path_image p ⟹ f x = g x) ⟹ contour_integral p f = contour_integral p g"
using has_contour_integral_eq
by (metis contour_integral_unique has_contour_integral_integrable has_contour_integral_integral)

lemma contour_integral_eq_0:
"(⋀z. z ∈ path_image g ⟹ f z = 0) ⟹ contour_integral g f = 0"

lemma contour_integral_bound_linepath:
shows
"⟦f contour_integrable_on (linepath a b);
0 ≤ B; ⋀x. x ∈ closed_segment a b ⟹ norm(f x) ≤ B⟧
⟹ norm(contour_integral (linepath a b) f) ≤ B*norm(b - a)"
apply (rule has_contour_integral_bound_linepath [of f])
apply (auto simp: has_contour_integral_integral)
done

lemma contour_integral_0 [simp]: "contour_integral g (λx. 0) = 0"

lemma contour_integral_sum:
"⟦finite s; ⋀a. a ∈ s ⟹ (f a) contour_integrable_on p⟧
⟹ contour_integral p (λx. sum (λa. f a x) s) = sum (λa. contour_integral p (f a)) s"
by (auto simp: contour_integral_unique has_contour_integral_sum has_contour_integral_integral)

lemma contour_integrable_eq:
"⟦f contour_integrable_on p; ⋀x. x ∈ path_image p ⟹ f x = g x⟧ ⟹ g contour_integrable_on p"
unfolding contour_integrable_on_def
by (metis has_contour_integral_eq)

subsection ‹Arithmetic theorems for path integrability›

lemma contour_integrable_neg:
"f contour_integrable_on g ⟹ (λx. -(f x)) contour_integrable_on g"
using has_contour_integral_neg contour_integrable_on_def by blast

"⟦f1 contour_integrable_on g; f2 contour_integrable_on g⟧ ⟹ (λx. f1 x + f2 x) contour_integrable_on g"
by fastforce

lemma contour_integrable_diff:
"⟦f1 contour_integrable_on g; f2 contour_integrable_on g⟧ ⟹ (λx. f1 x - f2 x) contour_integrable_on g"
using has_contour_integral_diff contour_integrable_on_def
by fastforce

lemma contour_integrable_lmul:
"f contour_integrable_on g ⟹ (λx. c * f x) contour_integrable_on g"
using has_contour_integral_lmul contour_integrable_on_def
by fastforce

lemma contour_integrable_rmul:
"f contour_integrable_on g ⟹ (λx. f x * c) contour_integrable_on g"
using has_contour_integral_rmul contour_integrable_on_def
by fastforce

lemma contour_integrable_div:
"f contour_integrable_on g ⟹ (λx. f x / c) contour_integrable_on g"
using has_contour_integral_div contour_integrable_on_def
by fastforce

lemma contour_integrable_sum:
"⟦finite s; ⋀a. a ∈ s ⟹ (f a) contour_integrable_on p⟧
⟹ (λx. sum (λa. f a x) s) contour_integrable_on p"
unfolding contour_integrable_on_def
by (metis has_contour_integral_sum)

subsection‹Reversing a path integral›

lemma has_contour_integral_reverse_linepath:
"(f has_contour_integral i) (linepath a b)
⟹ (f has_contour_integral (-i)) (linepath b a)"
using has_contour_integral_reversepath valid_path_linepath by fastforce

lemma contour_integral_reverse_linepath:
"continuous_on (closed_segment a b) f
⟹ contour_integral (linepath a b) f = - (contour_integral(linepath b a) f)"
apply (rule contour_integral_unique)
apply (rule has_contour_integral_reverse_linepath)
by (simp add: closed_segment_commute contour_integrable_continuous_linepath has_contour_integral_integral)

(* Splitting a path integral in a flat way.*)

lemma has_contour_integral_split:
assumes f: "(f has_contour_integral i) (linepath a c)" "(f has_contour_integral j) (linepath c b)"
and k: "0 ≤ k" "k ≤ 1"
and c: "c - a = k *⇩R (b - a)"
shows "(f has_contour_integral (i + j)) (linepath a b)"
proof (cases "k = 0 ∨ k = 1")
case True
then show ?thesis
using assms by auto
next
case False
then have k: "0 < k" "k < 1" "complex_of_real k ≠ 1"
using assms by auto
have c': "c = k *⇩R (b - a) + a"
have bc: "(b - c) = (1 - k) *⇩R (b - a)"
{ assume *: "((λx. f ((1 - x) *⇩R a + x *⇩R c) * (c - a)) has_integral i) {0..1}"
have **: "⋀x. ((k - x) / k) *⇩R a + (x / k) *⇩R c = (1 - x) *⇩R a + x *⇩R b"
using False apply (simp add: c' algebra_simps)
apply (simp add: real_vector.scale_left_distrib [symmetric] divide_simps)
done
have "((λx. f ((1 - x) *⇩R a + x *⇩R b) * (b - a)) has_integral i) {0..k}"
using k has_integral_affinity01 [OF *, of "inverse k" "0"]
apply (simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost ** c)
apply (auto dest: has_integral_cmul [where c = "inverse k"])
done
} note fi = this
{ assume *: "((λx. f ((1 - x) *⇩R c + x *⇩R b) * (b - c)) has_integral j) {0..1}"
have **: "⋀x. (((1 - x) / (1 - k)) *⇩R c + ((x - k) / (1 - k)) *⇩R b) = ((1 - x) *⇩R a + x *⇩R b)"
using k
done
have "((λx. f ((1 - x) *⇩R a + x *⇩R b) * (b - a)) has_integral j) {k..1}"
using k has_integral_affinity01 [OF *, of "inverse(1 - k)" "-(k/(1 - k))"]
apply (simp add: divide_simps mult.commute [of _ "1-k"] image_affinity_atLeastAtMost ** bc)
apply (auto dest: has_integral_cmul [where k = "(1 - k) *⇩R j" and c = "inverse (1 - k)"])
done
} note fj = this
show ?thesis
using f k
apply (rule has_integral_combine [OF _ _ fi fj], simp_all)
done
qed

lemma continuous_on_closed_segment_transform:
assumes f: "continuous_on (closed_segment a b) f"
and k: "0 ≤ k" "k ≤ 1"
and c: "c - a = k *⇩R (b - a)"
shows "continuous_on (closed_segment a c) f"
proof -
have c': "c = (1 - k) *⇩R a + k *⇩R b"
using c by (simp add: algebra_simps)
have "closed_segment a c ⊆ closed_segment a b"
by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
then show "continuous_on (closed_segment a c) f"
by (rule continuous_on_subset [OF f])
qed

lemma contour_integral_split:
assumes f: "continuous_on (closed_segment a b) f"
and k: "0 ≤ k" "k ≤ 1"
and c: "c - a = k *⇩R (b - a)"
shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
proof -
have c': "c = (1 - k) *⇩R a + k *⇩R b"
using c by (simp add: algebra_simps)
have "closed_segment a c ⊆ closed_segment a b"
by (metis c' ends_in_segment(1) in_segment(1) k subset_closed_segment)
moreover have "closed_segment c b ⊆ closed_segment a b"
by (metis c' ends_in_segment(2) in_segment(1) k subset_closed_segment)
ultimately
have *: "continuous_on (closed_segment a c) f" "continuous_on (closed_segment c b) f"
by (auto intro: continuous_on_subset [OF f])
show ?thesis
by (rule contour_integral_unique) (meson "*" c contour_integrable_continuous_linepath has_contour_integral_integral has_contour_integral_split k)
qed

lemma contour_integral_split_linepath:
assumes f: "continuous_on (closed_segment a b) f"
and c: "c ∈ closed_segment a b"
shows "contour_integral(linepath a b) f = contour_integral(linepath a c) f + contour_integral(linepath c b) f"
using c by (auto simp: closed_segment_def algebra_simps intro!: contour_integral_split [OF f])

text‹The special case of midpoints used in the main quadrisection›

lemma has_contour_integral_midpoint:
assumes "(f has_contour_integral i) (linepath a (midpoint a b))"
"(f has_contour_integral j) (linepath (midpoint a b) b)"
shows "(f has_contour_integral (i + j)) (linepath a b)"
apply (rule has_contour_integral_split [where c = "midpoint a b" and k = "1/2"])
using assms
apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
done

lemma contour_integral_midpoint:
"continuous_on (closed_segment a b) f
⟹ contour_integral (linepath a b) f =
contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
apply (rule contour_integral_split [where c = "midpoint a b" and k = "1/2"])
apply (auto simp: midpoint_def algebra_simps scaleR_conv_of_real)
done

text‹A couple of special case lemmas that are useful below›

lemma triangle_linear_has_chain_integral:
"((λx. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
apply (rule Cauchy_theorem_primitive [of UNIV "λx. m/2 * x^2 + d*x"])
apply (auto intro!: derivative_eq_intros)
done

lemma has_chain_integral_chain_integral3:
"(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d)
⟹ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i"
apply (subst contour_integral_unique [symmetric], assumption)
apply (drule has_contour_integral_integrable)
done

lemma has_chain_integral_chain_integral4:
"(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e)
⟹ contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i"
apply (subst contour_integral_unique [symmetric], assumption)
apply (drule has_contour_integral_integrable)
done

subsection‹Reversing the order in a double path integral›

text‹The condition is stronger than needed but it's often true in typical situations›

lemma fst_im_cbox [simp]: "cbox c d ≠ {} ⟹ (fst ` cbox (a,c) (b,d)) = cbox a b"
by (auto simp: cbox_Pair_eq)

lemma snd_im_cbox [simp]: "cbox a b ≠ {} ⟹ (snd ` cbox (a,c) (b,d)) = cbox c d"
by (auto simp: cbox_Pair_eq)

lemma contour_integral_swap:
assumes fcon:  "continuous_on (path_image g × path_image h) (λ(y1,y2). f y1 y2)"
and vp:    "valid_path g" "valid_path h"
and gvcon: "continuous_on {0..1} (λt. vector_derivative g (at t))"
and hvcon: "continuous_on {0..1} (λt. vector_derivative h (at t))"
shows "contour_integral g (λw. contour_integral h (f w)) =
contour_integral h (λz. contour_integral g (λw. f w z))"
proof -
have gcon: "continuous_on {0..1} g" and hcon: "continuous_on {0..1} h"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
have fgh1: "⋀x. (λt. f (g x) (h t)) = (λ(y1,y2). f y1 y2) ∘ (λt. (g x, h t))"
by (rule ext) simp
have fgh2: "⋀x. (λt. f (g t) (h x)) = (λ(y1,y2). f y1 y2) ∘ (λt. (g t, h x))"
by (rule ext) simp
have fcon_im1: "⋀x. 0 ≤ x ⟹ x ≤ 1 ⟹ continuous_on ((λt. (g x, h t)) ` {0..1}) (λ(x, y). f x y)"
by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def)
have fcon_im2: "⋀x. 0 ≤ x ⟹ x ≤ 1 ⟹ continuous_on ((λt. (g t, h x)) ` {0..1}) (λ(x, y). f x y)"
by (rule continuous_on_subset [OF fcon]) (auto simp: path_image_def)
have "⋀y. y ∈ {0..1} ⟹ continuous_on {0..1} (λx. f (g x) (h y))"
by (subst fgh2) (rule fcon_im2 gcon continuous_intros | simp)+
then have vdg: "⋀y. y ∈ {0..1} ⟹ (λx. f (g x) (h y) * vector_derivative g (at x)) integrable_on {0..1}"
using continuous_on_mult gvcon integrable_continuous_real by blast
have "(λz. vector_derivative g (at (fst z))) = (λx. vector_derivative g (at x)) ∘ fst"
by auto
then have gvcon': "continuous_on (cbox (0, 0) (1, 1::real)) (λx. vector_derivative g (at (fst x)))"
apply (rule ssubst)
apply (rule continuous_intros | simp add: gvcon)+
done
have "(λz. vector_derivative h (at (snd z))) = (λx. vector_derivative h (at x)) ∘ snd"
by auto
then have hvcon': "continuous_on (cbox (0, 0) (1::real, 1)) (λx. vector_derivative h (at (snd x)))"
apply (rule ssubst)
apply (rule continuous_intros | simp add: hvcon)+
done
have "(λx. f (g (fst x)) (h (snd x))) = (λ(y1,y2). f y1 y2) ∘ (λw. ((g ∘ fst) w, (h ∘ snd) w))"
by auto
then have fgh: "continuous_on (cbox (0, 0) (1, 1)) (λx. f (g (fst x)) (h (snd x)))"
apply (rule ssubst)
apply (rule gcon hcon continuous_intros | simp)+
apply (auto simp: path_image_def intro: continuous_on_subset [OF fcon])
done
have "integral {0..1} (λx. contour_integral h (f (g x)) * vector_derivative g (at x)) =
integral {0..1} (λx. contour_integral h (λy. f (g x) y * vector_derivative g (at x)))"
proof (rule integral_cong [OF contour_integral_rmul [symmetric]])
show "⋀x. x ∈ {0..1} ⟹ f (g x) contour_integrable_on h"
unfolding contour_integrable_on
apply (rule integrable_continuous_real)
apply (rule continuous_on_mult [OF _ hvcon])
apply (subst fgh1)
apply (rule fcon_im1 hcon continuous_intros | simp)+
done
qed
also have "… = integral {0..1}
(λy. contour_integral g (λx. f x (h y) * vector_derivative h (at y)))"
unfolding contour_integral_integral
apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified])
apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
unfolding integral_mult_left [symmetric]
apply (simp only: mult_ac)
done
also have "… = contour_integral h (λz. contour_integral g (λw. f w z))"
unfolding contour_integral_integral
apply (rule integral_cong)
unfolding integral_mult_left [symmetric]
done
finally show ?thesis
qed

lemma norm_sum_half:
assumes "norm(a + b) ≥ e"
shows "norm a ≥ e/2 ∨ norm b ≥ e/2"
proof -
have "e ≤ norm (- a - b)"
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
then show ?thesis
by (auto dest!: norm_sum_half)
qed

assumes f: "continuous_on (convex hull {a,b,c}) f"
and dist: "dist a b ≤ K" "dist b c ≤ K" "dist c a ≤ K"
and e: "e * K^2 ≤
norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)"
shows "∃a' b' c'.
a' ∈ convex hull {a,b,c} ∧ b' ∈ convex hull {a,b,c} ∧ c' ∈ convex hull {a,b,c} ∧
dist a' b' ≤ K/2  ∧  dist b' c' ≤ K/2  ∧  dist c' a' ≤ K/2  ∧
e * (K/2)^2 ≤ norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)"
(is "∃x y z. ?Φ x y z")
proof -
note divide_le_eq_numeral1 [simp del]
define a' where "a' = midpoint b c"
define b' where "b' = midpoint c a"
define c' where "c' = midpoint a b"
have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
using f continuous_on_subset segments_subset_convex_hull by metis+
have fcont': "continuous_on (closed_segment c' b') f"
"continuous_on (closed_segment a' c') f"
"continuous_on (closed_segment b' a') f"
unfolding a'_def b'_def c'_def
by (rule continuous_on_subset [OF f],
metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+
let ?pathint = "λx y. contour_integral(linepath x y) f"
have *: "?pathint a b + ?pathint b c + ?pathint c a =
(?pathint a c' + ?pathint c' b' + ?pathint b' a) +
(?pathint a' c' + ?pathint c' b + ?pathint b a') +
(?pathint a' c + ?pathint c b' + ?pathint b' a') +
(?pathint a' b' + ?pathint b' c' + ?pathint c' a')"
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)"
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 unfolding * by (blast intro: that dest!: norm_sum_lemma)
then show ?thesis
proof cases
case 1 then have "?Φ a c' b'"
using assms
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 divide_simps)
done
then show ?thesis by blast
next
case 2 then  have "?Φ a' c' b"
using assms
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 divide_simps)
done
then show ?thesis by blast
next
case 3 then have "?Φ a' c b'"
using assms
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 divide_simps)
done
then show ?thesis by blast
next
case 4 then have "?Φ a' b' c'"
using assms
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 divide_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"
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])
done
{ fix y
assume yc: "y ∈ convex hull {a,b,c}"
have "cmod (f y - f x - f' * (y - x)) ≤ e*norm(y - x)"
proof (rule f')
show "cmod (y - x) ≤ d"
by (metis triangle_points_closer [OF xc yc] le norm_minus_commute order_trans)
qed (use S yc in blast)
also have "… ≤ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))"
by (simp add: yc e xc disj_le [OF triangle_points_closer])
finally have "cmod (f y - f x - f' * (y - x)) ≤ e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" .
} note cm_le = this
have "?normle a b c"
unfolding dist_norm pa
apply (rule le_of_3)
using f' xc S e
apply simp_all
apply (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
next
case (Suc n) show ?case
by (metis (no_types, lifting) AtSuc [OF Suc] f.simps(2) someI_ex)
qed

lemma Follows: "Follows (f(Suc n)) (f n)"
by (metis (no_types, lifting) AtSuc [OF At [of n]] f.simps(2) someI_ex)

declare f.simps(2) [simp del]
end

lemma Chain3:
assumes At0: "At x0 y0 z0 0"
and AtSuc: "⋀x y z n. At x y z n ⟹ ∃x' y' z'. At x' y' z' (Suc n) ∧ Follows x' y' z' x y z"
obtains f g h where
"f 0 = x0" "g 0 = y0" "h 0 = z0"
"⋀n. At (f n) (g n) (h n) n"
"⋀n. Follows (f(Suc n)) (g(Suc n)) (h(Suc n)) (f n) (g n) (h n)"
proof -
interpret three: Chain "(x0,y0,z0)" "λ(x,y,z). At x y z" "λ(x',y',z'). λ(x,y,z). Follows x' y' z' x y z"
apply unfold_locales
using At0 AtSuc by auto
show ?thesis
apply (rule that [of "λn. fst (three.f n)"  "λn. fst (snd (three.f n))" "λn. snd (snd (three.f n))"])
using three.At three.Follows
apply simp_all
done
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"
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 (meson convex_hull_subset empty_subsetI insert_subset subsetCE)
done
} note AtSuc = this
obtain fa fb fc
where f0 [simp]: "fa 0 = a" "fb 0 = b" "fc 0 = c"
and cosb: "⋀n. convex hull {fa n, fb n, fc n} ⊆ convex hull {a,b,c}"
and dist: "⋀n. dist (fa n) (fb n) ≤ K/2^n"
"⋀n. dist (fb n) (fc n) ≤ K/2^n"
"⋀n. dist (fc n) (fa n) ≤ K/2^n"
and no: "⋀n. norm(?pathint (fa n) (fb n) +
?pathint (fb n) (fc n) +
?pathint (fc n) (fa n)) ≥ e * (K/2^n)^2"
and conv_le: "⋀n. convex hull {fa(Suc n), fb(Suc n), fc(Suc n)} ⊆ convex hull {fa n, fb n, fc n}"
apply (rule Chain3 [of At, OF At0 AtSuc])
apply (auto simp: At_def)
done
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})"
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
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
apply (simp only: zero_less_norm_iff [symmetric])
done
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 then show ?thesis
using fabc c
apply (subst contour_integral_split [of a c f "1/k" b, symmetric])
apply (metis closed_segment_commute fabc(3))
apply (auto simp: k contour_integral_reverse_linepath)
done
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"
apply (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"])
using False c
apply (auto simp: f insert_commute scaleR_conv_of_real algebra_simps)
done
ultimately show ?thesis
apply (auto simp: contour_integral_reverse_linepath)
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 -
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})"
then obtain C where C: "0 < C" and Cno: "⋀y. y ∈ convex hull {a,b,c} ⟹ norm y < C"
using bounded_pos_less by blast
then have diff_2C: "norm(x - y) ≤ 2*C"
if x: "x ∈ convex hull {a, b, c}" and y: "y ∈ convex hull {a, b, c}" for x y
proof -
have "cmod x ≤ C"
using x by (meson Cno not_le not_less_iff_gr_or_eq)
hence "cmod (x - y) ≤ C + C"
using y by (meson Cno add_mono_thms_linordered_field(4) less_eq_real_def norm_triangle_ineq4 order_trans)
thus "cmod (x - y) ≤ 2 * C"
by (metis mult_2)
qed
have contf': "continuous_on (convex hull {b,a,c}) f"
using contf by (simp add: insert_commute)
{ fix y::complex
assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
and ynz: "y ≠ 0"
have pi_eq_y: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = y"
by (rule has_chain_integral_chain_integral3 [OF fy])
have ?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]
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
}
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
let ?pathint = "λx y. contour_integral(linepath x y) f"
have e: "0 < e" "e ≤ 1" "e ≤ d1 / (4 * C)" "e ≤ cmod y / 24 / C / B"
using d1_pos ‹C>0› ‹B>0› ynz by (simp_all add: e_def)
then have eCB: "24 * e * C * B ≤ cmod y"
using ‹C>0› ‹B>0›  by (simp add: field_simps)
have e_le_d1: "e * (4 * C) ≤ d1"
using e ‹C>0› by (simp add: field_simps)
have "shrink a ∈ interior(convex hull {a,b,c})"
"shrink b ∈ interior(convex hull {a,b,c})"
"shrink c ∈ interior(convex hull {a,b,c})"
using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
then have fhp0: "(f has_contour_integral 0)
(linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))"
by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal)
then have f_0_shrink: "?pathint (shrink a) (shrink b) + ?pathint (shrink b) (shrink c) + ?pathint (shrink c) (shrink a) = 0"
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)"
have "cmod y / (24 * C) ≤ cmod y / cmod (b - a) / 12"
using False ‹C>0› diff_2C [of b a] ynz
by (auto simp: divide_simps hull_inc)
have less_C: "⟦u ∈ convex hull {a, b, c}; 0 ≤ x; x ≤ 1⟧ ⟹ x * cmod u < C" for x u
apply (cases "x=0", simp add: ‹0<C›)
using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
{ fix u v
assume uv: "u ∈ convex hull {a, b, c}" "v ∈ convex hull {a, b, c}" "u≠v"
and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)"
have shr_uv: "shrink u ∈ interior(convex hull {a,b,c})"
"shrink v ∈ interior(convex hull {a,b,c})"
using d e uv
by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
have cmod_fuv: "⋀x. 0≤x ⟹ x≤1 ⟹ cmod (f (linepath (shrink u) (shrink v) x)) ≤ B"
using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
have By_uv: "B * (12 * (e * cmod (u - v))) ≤ cmod y"
apply (rule order_trans [OF _ eCB])
using e ‹B>0› diff_2C [of u v] uv
by (auto simp: field_simps)
{ fix x::real   assume x: "0≤x" "x≤1"
have cmod_less_4C: "cmod ((1 - x) *⇩R u - (1 - x) *⇩R d) + cmod (x *⇩R v - x *⇩R d) < (C+C) + (C+C)"
apply (rule add_strict_mono; rule norm_triangle_half_l [of _ 0])
using uv x d interior_subset
apply (auto simp: hull_inc intro!: less_C)
done
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"
apply (simp only: ll norm_mult scaleR_diff_right)
using ‹e>0› cmod_less_4C apply (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1])
done
have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)"
using x uv shr_uv cmod_less_dt
by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull)
also have "… ≤ cmod y / cmod (v - u) / 12"
using False uv ‹C>0› diff_2C [of v u] ynz
by (auto simp: divide_simps hull_inc)
finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) ≤ cmod y / cmod (v - u) / 12"
by simp
then have cmod_12_le: "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) * 12 ≤ cmod y"
using uv False by (auto simp: field_simps)
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)"
using By_uv e ‹0 < B› ‹0 < C› x apply (simp_all add: cmod_fuv cmod_shr cmod_12_le)
done
also have "… ≤ cmod y / 6"
by simp
finally have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) +
cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x))
≤ cmod y / 6" .
} note cmod_diff_le = this
have f_uv: "continuous_on (closed_segment u v) f"
by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull])
have **: "⋀f' x' f x::complex. f'*x' - f*x = f'*(x' - x) + x*(f' - f)"
have "norm (?pathint (shrink u) (shrink v) - ?pathint u v)
≤ (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
apply (rule has_integral_bound
[of _ "λx. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
_ 0 1])
using ynz ‹0 < B› ‹0 < C›
apply (simp_all del: le_divide_eq_numeral1)
apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral
fpi_uv f_uv contour_integrable_continuous_linepath)
apply (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"
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"
then
have "norm(?pathint a b + ?pathint b c + ?pathint c a) ≤ norm y / 2"
then have "False"
using pi_eq_y ynz by auto
}
moreover have "uniformly_continuous_on (convex hull {a,b,c}) f"
by (simp add: contf compact_convex_hull compact_uniformly_continuous)
ultimately have "False"
unfolding uniformly_continuous_on_def
by (force simp: ynz ‹0 < C› 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]
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"
using S
apply (clarsimp simp add: convex_hull_insert [of "{b,c}" a] segment_convex_hull)
apply (meson subs convexD convex_closed_segment ends_in_segment(1) ends_in_segment(2) subsetCE)
done

lemma triangle_contour_integrals_starlike_primitive:
assumes contf: "continuous_on S f"
and S: "a ∈ S" "open S"
and x: "x ∈ S"
and subs: "⋀y. y ∈ S ⟹ closed_segment a y ⊆ S"
and zer: "⋀b c. closed_segment b c ⊆ S
⟹ contour_integral (linepath a b) f + contour_integral (linepath b c) f +
contour_integral (linepath c a) f = 0"
shows "((λx. contour_integral(linepath a x) f) has_field_derivative f x) (at x)"
proof -
let ?pathint = "λx y. contour_integral(linepath x y) f"
{ fix e y
assume e: "0 < e" and bxe: "ball x e ⊆ S" and close: "cmod (y - x) < e"
have y: "y ∈ S"
using bxe close  by (force simp: dist_norm norm_minus_commute)
have cont_ayf: "continuous_on (closed_segment a y) f"
using contf continuous_on_subset subs y by blast
have xys: "closed_segment x y ⊆ S"
apply (rule order_trans [OF _ bxe])
using close
by (auto simp: dist_norm ball_def norm_minus_commute dest: segment_bound)
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)"
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)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
apply (rule Lim_transform [OF * Lim_eventually])
using ‹open S› x apply (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at)
done
qed

(** Existence of a primitive.*)

lemma holomorphic_starlike_primitive:
fixes f :: "complex ⇒ complex"
assumes contf: "continuous_on S f"
and S: "starlike S" and os: "open S"
and k: "finite k"
and fcd: "⋀x. x ∈ S - k ⟹ f field_differentiable at x"
shows "∃g. ∀x ∈ S. (g has_field_derivative f x) (at x)"
proof -
obtain a where a: "a∈S" and a_cs: "⋀x. x∈S ⟹ closed_segment a x ⊆ S"
using S by (auto simp: starlike_def)
{ fix x b c
assume "x ∈ S" "closed_segment b c ⊆ S"
then have abcs: "convex hull {a, b, c} ⊆ S"
by (simp add: a a_cs starlike_convex_subset)
then have "continuous_on (convex hull {a, b, c}) f"
by (simp add: continuous_on_subset [OF contf])
then have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
using abcs interior_subset by (force intro: fcd Cauchy_theorem_triangle_cofinite [OF _ k])
} note 0 = this
show ?thesis
apply (intro exI ballI)
apply (rule triangle_contour_integrals_starlike_primitive [OF contf a os], assumption)
apply (metis a_cs)
apply (metis has_chain_integral_chain_integral3 0)
done
qed

corollary 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)

corollary Cauchy_theorem_starlike_simple:
"⟦open S; starlike S; f holomorphic_on S; valid_path g; path_image g ⊆ S; pathfinish g = pathstart g⟧
⟹ (f has_contour_integral 0) g"
apply (rule Cauchy_theorem_starlike [OF _ _ finite.emptyI])
apply (metis at_within_open holomorphic_on_def)
done

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)"
finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
using i yx  by (simp add: contour_integral_unique divide_less_eq)
}
then have "∃d>0. ∀y∈S. y ≠ x ∧ cmod (y-x) < d ⟶ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
using d1 by blast
}
then have *: "((λy. (contour_integral (linepath x y) f - f x * (y - x)) /⇩R cmod (y - x)) ⤏ 0) (at x within S)"
by (simp add: Lim_within dist_norm inverse_eq_divide)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
apply (rule Lim_transform [OF * Lim_eventually])
using linordered_field_no_ub
apply (force simp: inverse_eq_divide [symmetric] eventually_at)
done
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:
"⟦f holomorphic_on S; convex S;
valid_path g; path_image g ⊆ S;
pathfinish g = pathstart g⟧ ⟹ (f has_contour_integral 0) g"
apply (rule Cauchy_theorem_convex [where K = "{}"])
using at_within_interior holomorphic_on_def interior_subset by fastforce

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"

subsection‹Generalize integrability to local primitives›

lemma contour_integral_local_primitive_lemma:
fixes f :: "complex⇒complex"
shows
"⟦g piecewise_differentiable_on {a..b};
⋀x. x ∈ s ⟹ (f has_field_derivative f' x) (at x within s);
⋀x. x ∈ {a..b} ⟹ g x ∈ s⟧
⟹ (λx. f' (g x) * vector_derivative g (at x within {a..b}))
integrable_on {a..b}"
apply (cases "cbox a b = {}", force)
apply (rule exI)
apply (rule contour_integral_primitive_lemma, assumption+)
using atLeastAtMost_iff by blast

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
apply (auto simp: dist_norm continuous_on_iff)
apply (drule_tac x=x in bspec)
using x apply simp
apply (drule_tac x=d in spec, auto)
done
have "∃d>0. ∀u v. u ≤ x ∧ x ≤ v ∧ {u..v} ⊆ ball x d ∧ (u ≤ v ⟶ a ≤ u ∧ v ≤ b) ⟶
(λx. f (g x) * vector_derivative g (at x)) integrable_on {u..v}"
apply (rule_tac x=e in exI)
using e
apply (simp add: integrable_on_localized_vector_derivative [symmetric], clarify)
apply (rule_tac f = h and s = "g ` {u..v}" in contour_integral_local_primitive_lemma)
apply (meson atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset)
apply (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h], force)
done
} 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"
using g
apply (simp add: valid_path_def path_image_def contour_integrable_on_def has_contour_integral_def
has_integral_localized_vector_derivative integrable_on_def [symmetric])
using contour_integral_local_primitive_any [OF _ dh]
by (meson image_subset_iff piecewise_C1_imp_differentiable)

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 set_mp)
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: "open S"
and g: "valid_path g" "path_image g ⊆ S"
shows "f contour_integrable_on g"
apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g])
using fh  by (simp add: field_differentiable_def holomorphic_on_open os)

lemma continuous_on_inversediff:
fixes z:: "'a::real_normed_field" shows "z ∉ S ⟹ continuous_on S (λw. 1 / (w - z))"
by (rule continuous_intros | force)+

corollary contour_integrable_inversediff:
"⟦valid_path g; z ∉ path_image g⟧ ⟹ (λw. 1 / (w-z)) contour_integrable_on g"
apply (rule contour_integrable_holomorphic_simple [of _ "UNIV-{z}"])
apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
done

text‹Key fact that path integral is the same for a "nearby" path. This is the
main lemma for the homotopy form of Cauchy's theorem and is also useful
if we want "without loss of generality" to assume some nice properties of a
path (e.g. smoothness). It can also be used to define the integrals of
analytic functions over arbitrary continuous paths. This is just done for
winding numbers now.
›

text‹A technical definition to avoid duplication of similar proofs,
for paths joined at the ends versus looping paths›
definition linked_paths :: "bool ⇒ (real ⇒ 'a) ⇒ (real ⇒ 'a::topological_space) ⇒ bool"
where "linked_paths atends g h ==
(if atends then pathstart h = pathstart g ∧ pathfinish h = pathfinish g
else pathfinish g = pathstart g ∧ pathfinish h = pathstart h)"

text‹This formulation covers two cases: @{term g} and @{term h} share their
start and end points; @{term g} and @{term h} both loop upon themselves.›
lemma contour_integral_nearby:
assumes os: "open S" and p: "path p" "path_image p ⊆ S"
shows "∃d. 0 < d ∧
(∀g h. valid_path g ∧ valid_path h ∧
(∀t ∈ {0..1}. norm(g t - p t) < d ∧ norm(h t - p t) < d) ∧
⟶ path_image g ⊆ S ∧ path_image h ⊆ S ∧
(∀f. f holomorphic_on S ⟶ contour_integral h f = contour_integral g f))"
proof -
have "∀z. ∃e. z ∈ path_image p ⟶ 0 < e ∧ ball z e ⊆ S"
using open_contains_ball os p(2) by blast
then obtain ee where ee: "⋀z. z ∈ path_image p ⟹ 0 < ee z ∧ ball z (ee z) ⊆ S"
by metis
define cover where "cover = (λz. ball z (ee z/3)) ` (path_image p)"
have "compact (path_image p)"
by (metis p(1) compact_path_image)
moreover have "path_image p ⊆ (⋃c∈path_image p. ball c (ee c / 3))"
using ee by auto
ultimately have "∃D ⊆ cover. finite D ∧ path_image p ⊆ ⋃D"
then obtain D where D: "D ⊆ cover" "finite D" "path_image p ⊆ ⋃D"
by blast
then obtain k where k: "k ⊆ {0..1}" "finite k" and D_eq: "D = ((λz. ball z (ee z / 3)) ∘ p) ` k"
apply (simp add: cover_def path_image_def image_comp)
apply (blast dest!: finite_subset_image [OF ‹finite D›])
done
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
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"
{ 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"
have e3le: "e/3 ≤ ee (p t) / 3"  using fin_eep t
{ fix x
assume x: "n/N ≤ x" "x ≤ (1 + n)/N"
then have nN01: "0 ≤ n/N" "(1 + n)/N ≤ 1"
using Suc.prems by auto
then have x01: "0 ≤ x" "x ≤ 1"
using x by linarith+
have "cmod (p t - p x)  < ee (p t) / 3 + e/3"
proof (rule norm_diff_triangle_less [OF ptu de])
show "¦real n / real N - x¦ < d"
using x N by (auto simp: field_simps)
qed (use x01 Suc.prems in auto)
then have ptx: "cmod (p t - p x) < 2*ee (p t)/3"
using e3le eepi [OF t] by simp
have "cmod (p t - g x) < 2*ee (p t)/3 + e/3 "
apply (rule norm_diff_triangle_less [OF ptx])
using ghp x01 by (simp add: norm_minus_commute)
also have "… ≤ ee (p t)"
using e3le eepi [OF t] by simp
finally have gg: "cmod (p t - g x) < ee (p t)" .
have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 "
apply (rule norm_diff_triangle_less [OF ptx])
using ghp x01 by (simp add: norm_minus_commute)
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 (real n / real N)) (h (real n / real N)) = path_image (linepath (h (n/N)) (g (n/N)))"
also have pi_hgn: "… ⊆ ball (p t) (ee (p t))"
using ptgh_ee [of "n/N"] Suc.prems
by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
finally have gh_ns: "closed_segment (g (n/N)) (h (n/N)) ⊆ S"
using ee pi t by blast
have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N))) ⊆ ball (p t) (ee (p t))"
using ptgh_ee [of "(1+n)/N"] Suc.prems
by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N)) ⊆ S"
using ‹N>0› Suc.prems ee pi t
by (auto simp: Path_Connected.path_image_join field_simps)
have pi_subset_ball:
"path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
⊆ ball (p t) (ee (p t))"
apply (intro subset_path_image_join pi_hgn pi_ghn')
using ‹N>0› Suc.prems
apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
done
have pi0: "(f has_contour_integral 0)
(subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))"
apply (rule Cauchy_theorem_primitive [of "ball(p t) (ee(p t))" "ff (p t)" "f"])
apply (metis ff open_ball at_within_open pi t)
using Suc.prems pi_subset_ball apply (simp_all add: valid_path_join valid_path_subpath g h)
done
have fpa1: "f contour_integrable_on subpath (real n / real N) (real (Suc n) / real N) g"
using Suc.prems by (simp add: contour_integrable_subpath g fpa)
have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))"
using gh_n's
by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
have fpa3: "f contour_integrable_on linepath (h (real n / real N)) (g (real n / real N))"
using gh_ns
by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f +
contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f +
contour_integral (subpath ((Suc n) / N) (n/N) h) f +
contour_integral (linepath (h (n/N)) (g (n/N))) f = 0"
using contour_integral_unique [OF pi0] Suc.prems
by (simp add: g h fpa valid_path_subpath contour_integrable_subpath
fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc)
have *: "⋀hn he hn' gn gd gn' hgn ghn gh0 ghn'.
⟦hn - gn = ghn - gh0;
gd + ghn' + he + hgn = (0::complex);
hn - he = hn'; gn + gd = gn'; hgn = -ghn⟧ ⟹ hn' - gn' = ghn' - gh0"
by (auto simp: algebra_simps)
have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f"
unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"]
using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath)
also have "… = contour_integral (subpath 0 ((Suc n) / N) h) f"
using Suc.prems by (simp add: contour_integral_subpath_combine h fpa)
finally have pi0_eq:
"contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
contour_integral (subpath 0 ((Suc n) / N) h) f" .
show ?case
apply (rule * [OF Suc.hyps eq0 pi0_eq])
using Suc.prems
apply (simp_all add: g h fpa contour_integral_subpath_combine
contour_integral_reversepath [symmetric] contour_integrable_continuous_linepath
continuous_on_subset [OF contf gh_ns])
done
qed
} note ind = this
have "contour_integral h f = contour_integral g f"
using ind [OF order_refl] N joins
}
ultimately
show "path_image g ⊆ S ∧ path_image h ⊆ S ∧ (∀f. f holomorphic_on S ⟶ contour_integral h f = contour_integral g f)"
by metis
qed
qed

lemma
assumes "open S" "path p" "path_image p ⊆ S"
shows contour_integral_nearby_ends:
"∃d. 0 < d ∧
(∀g h. valid_path g ∧ valid_path h ∧
(∀t ∈ {0..1}. norm(g t - p t) < d ∧ norm(h t - p t) < d) ∧
pathstart h = pathstart g ∧ pathfinish h = pathfinish g
⟶ path_image g ⊆ S ∧
path_image h ⊆ S ∧
(∀f. f holomorphic_on S
⟶ contour_integral h f = contour_integral g f))"
and contour_integral_nearby_loops:
"∃d. 0 < d ∧
(∀g h. valid_path g ∧ valid_path h ∧
(∀t ∈ {0..1}. norm(g t - p t) < d ∧ norm(h t - p t) < d) ∧
pathfinish g = pathstart g ∧ pathfinish h = pathstart h
⟶ path_image g ⊆ S ∧
path_image h ⊆ S ∧
(∀f. f holomorphic_on S
⟶ contour_integral h f = contour_integral g f))"
using contour_integral_nearby [OF assms, where atends=True]
using contour_integral_nearby [OF assms, where atends=False]

lemma C1_differentiable_polynomial_function:
fixes p :: "real ⇒ 'a::euclidean_space"
shows "polynomial_function p ⟹ p C1_differentiable_on S"
by (metis continuous_on_polymonial_function C1_differentiable_on_def  has_vector_derivative_polynomial_function)

lemma valid_path_polynomial_function:
fixes p :: "real ⇒ 'a::euclidean_space"
shows "polynomial_function p ⟹ valid_path p"
by (force simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_polymonial_function C1_differentiable_polynomial_function)

lemma valid_path_subpath_trivial [simp]:
fixes g :: "real ⇒ 'a::euclidean_space"
shows "z ≠ g x ⟹ valid_path (subpath x x g)"

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
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]
apply clarify
apply (drule_tac x=g in spec)
apply (simp only: assms)
apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
done
then obtain p' where p': "polynomial_function p'"
"⋀x. (p has_vector_derivative (p' x)) (at x)"
by (blast intro: has_vector_derivative_polynomial_function that)
then have "bounded(p' ` {0..1})"
using continuous_on_polymonial_function
by (force simp: intro!: compact_imp_bounded compact_continuous_image)
then obtain L where L: "L>0" and nop': "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ norm (p' x) ≤ L"
by (force simp: bounded_pos)
{ fix f B
assume f: "f holomorphic_on S" and B: "⋀z. z∈S ⟹ cmod (f z) ≤ B"
then have "f contour_integrable_on p ∧ valid_path p"
using p S
by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
moreover have "cmod (vector_derivative p (at x)) * cmod (f (p x)) ≤ L * B" if "0 ≤ x" "x ≤ 1" for x
proof (rule mult_mono)
show "cmod (vector_derivative p (at x)) ≤ L"
by (metis nop' p'(2) that vector_derivative_at)
show "cmod (f (p x)) ≤ B"
by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that)
qed (use ‹L>0› in auto)
ultimately have "cmod (contour_integral g f) ≤ L * B"
apply (simp only: pi [OF f])
apply (simp only: contour_integral_integral)
apply (rule order_trans [OF integral_norm_bound_integral])
apply (auto simp: mult.commute integral_norm_bound_integral contour_integrable_on [symmetric] norm_mult)
done
} then
show ?thesis
by (force simp: L contour_integral_integral)
qed

text‹We can treat even non-rectifiable paths as having a "length" for bounds on analytic functions in open sets.›

subsection‹Winding Numbers›

definition winding_number_prop :: "[real ⇒ complex, complex, real, real ⇒ complex, complex] ⇒ bool" where
"winding_number_prop γ z e p n ≡
valid_path p ∧ z ∉ path_image p ∧
pathstart p = pathstart γ ∧
pathfinish p = pathfinish γ ∧
(∀t ∈ {0..1}. norm(γ t - p t) < e) ∧
contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n"

definition winding_number:: "[real ⇒ complex, complex] ⇒ complex" where
"winding_number γ z ≡ SOME n. ∀e > 0. ∃p. winding_number_prop γ z e p n"

lemma winding_number:
assumes "path γ" "z ∉ path_image γ" "0 < e"
shows "∃p. winding_number_prop γ z e p (winding_number γ z)"
proof -
have "path_image γ ⊆ UNIV - {z}"
using assms by blast
then obtain d
where d: "d>0"
and pi_eq: "⋀h1 h2. valid_path h1 ∧ valid_path h2 ∧
(∀t∈{0..1}. cmod (h1 t - γ t) < d ∧ cmod (h2 t - γ t) < d) ∧
pathstart h2 = pathstart h1 ∧ pathfinish h2 = pathfinish h1 ⟶
path_image h1 ⊆ UNIV - {z} ∧ path_image h2 ⊆ UNIV - {z} ∧
(∀f. f holomorphic_on UNIV - {z} ⟶ contour_integral h2 f = contour_integral h1 f)"
using contour_integral_nearby_ends [of "UNIV - {z}" γ] assms by (auto simp: open_delete)
then obtain h where h: "polynomial_function h ∧ pathstart h = pathstart γ ∧ pathfinish h = pathfinish γ ∧
(∀t ∈ {0..1}. norm(h t - γ t) < d/2)"
using path_approx_polynomial_function [OF ‹path γ›, of "d/2"] d by auto
define nn where "nn = 1/(2* pi*𝗂) * contour_integral h (λw. 1/(w - z))"
have "∃n. ∀e > 0. ∃p. winding_number_prop γ z e p n"
proof (rule_tac x=nn in exI, clarify)
fix e::real
assume e: "e>0"
obtain p where p: "polynomial_function p ∧
pathstart p = pathstart γ ∧ pathfinish p = pathfinish γ ∧ (∀t∈{0..1}. cmod (p t - γ t) < min e (d/2))"
using path_approx_polynomial_function [OF ‹path γ›, of "min e (d/2)"] d ‹0<e› by auto
have "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto simp: intro!: holomorphic_intros)
then show "∃p. winding_number_prop γ z e p nn"
apply (rule_tac x=p in exI)
using pi_eq [of h p] h p d
apply (auto simp: valid_path_polynomial_function norm_minus_commute nn_def winding_number_prop_def)
done
qed
then show ?thesis
unfolding winding_number_def by (rule someI2_ex) (blast intro: ‹0<e›)
qed

lemma winding_number_unique:
assumes γ: "path γ" "z ∉ path_image γ"
and pi: "⋀e. e>0 ⟹ ∃p. winding_number_prop γ z e p n"
shows "winding_number γ z = n"
proof -
have "path_image γ ⊆ UNIV - {z}"
using assms by blast
then obtain e
where e: "e>0"
and pi_eq: "⋀h1 h2 f. ⟦valid_path h1; valid_path h2;
(∀t∈{0..1}. cmod (h1 t - γ t) < e ∧ cmod (h2 t - γ t) < e);
pathstart h2 = pathstart h1; pathfinish h2 = pathfinish h1; f holomorphic_on UNIV - {z}⟧ ⟹
contour_integral h2 f = contour_integral h1 f"
using contour_integral_nearby_ends [of "UNIV - {z}" γ] assms  by (auto simp: open_delete)
obtain p where p: "winding_number_prop γ z e p n"
using pi [OF e] by blast
obtain q where q: "winding_number_prop γ z e q (winding_number γ z)"
using winding_number [OF γ e] by blast
have "2 * complex_of_real pi * 𝗂 * n = contour_integral p (λw. 1 / (w - z))"
using p by (auto simp: winding_number_prop_def)
also have "… = contour_integral q (λw. 1 / (w - z))"
proof (rule pi_eq)
show "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto intro!: holomorphic_intros)
qed (use p q in ‹auto simp: winding_number_prop_def norm_minus_commute›)
also have "… = 2 * complex_of_real pi * 𝗂 * winding_number γ z"
using q by (auto simp: winding_number_prop_def)
finally have "2 * complex_of_real pi * 𝗂 * n = 2 * complex_of_real pi * 𝗂 * winding_number γ z" .
then show ?thesis
by simp
qed

(*NB not winding_number_prop here due to the loop in p*)
lemma winding_number_unique_loop:
assumes γ: "path γ" "z ∉ path_image γ"
and loop: "pathfinish γ = pathstart γ"
and pi:
"⋀e. e>0 ⟹ ∃p. valid_path p ∧ z ∉ path_image p ∧
pathfinish p = pathstart p ∧
(∀t ∈ {0..1}. norm (γ t - p t) < e) ∧
contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n"
shows "winding_number γ z = n"
proof -
have "path_image γ ⊆ UNIV - {z}"
using assms by blast
then obtain e
where e: "e>0"
and pi_eq: "⋀h1 h2 f. ⟦valid_path h1; valid_path h2;
(∀t∈{0..1}. cmod (h1 t - γ t) < e ∧ cmod (h2 t - γ t) < e);
pathfinish h1 = pathstart h1; pathfinish h2 = pathstart h2; f holomorphic_on UNIV - {z}⟧ ⟹
contour_integral h2 f = contour_integral h1 f"
using contour_integral_nearby_loops [of "UNIV - {z}" γ] assms  by (auto simp: open_delete)
obtain p where p:
"valid_path p ∧ z ∉ path_image p ∧ pathfinish p = pathstart p ∧
(∀t ∈ {0..1}. norm (γ t - p t) < e) ∧
contour_integral p (λw. 1/(w - z)) = 2 * pi * 𝗂 * n"
using pi [OF e] by blast
obtain q where q: "winding_number_prop γ z e q (winding_number γ z)"
using winding_number [OF γ e] by blast
have "2 * complex_of_real pi * 𝗂 * n = contour_integral p (λw. 1 / (w - z))"
using p by auto
also have "… = contour_integral q (λw. 1 / (w - z))"
proof (rule pi_eq)
show "(λw. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto intro!: holomorphic_intros)
qed (use p q loop in ‹auto simp: winding_number_prop_def norm_minus_commute›)
also have "… = 2 * complex_of_real pi * 𝗂 * winding_number γ z"
using q by (auto simp: winding_number_prop_def)
finally have "2 * complex_of_real pi * 𝗂 * n = 2 * complex_of_real pi * 𝗂 * winding_number γ z" .
then show ?thesis
by simp
qed

lemma winding_number_valid_path:
assumes "valid_path γ" "z ∉ path_image γ"
shows "winding_number γ z = 1/(2*pi*𝗂) * contour_integral γ (λw. 1/(w - z))"
by (rule winding_number_unique)
(use assms in ‹auto simp: valid_path_imp_path winding_number_prop_def›)

lemma has_contour_integral_winding_number:
assumes γ: "valid_path γ" "z ∉ path_image γ"
shows "((λw. 1/(w - z)) has_contour_integral (2*pi*𝗂*winding_number γ z)) γ"
by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms)

lemma winding_number_trivial [simp]: "z ≠ a ⟹ winding_number(linepath a a) z = 0"

lemma winding_number_subpath_trivial [simp]: "z ≠ g x ⟹ winding_number (subpath x x g) z = 0"

lemma winding_number_join:
assumes γ1: "path γ1" "z ∉ path_image γ1"
and γ2: "path γ2" "z ∉ path_image γ2"
and "pathfinish γ1 = pathstart γ2"
shows "winding_number(γ1 +++ γ2) z = winding_number γ1 z + winding_number γ2 z"
proof (rule winding_number_unique)
show "∃p. winding_number_prop (γ1 +++ γ2) z e p
(winding_number γ1 z + winding_number γ2 z)" if "e > 0" for e
proof -
obtain p1 where "winding_number_prop γ1 z e p1 (winding_number γ1 z)"
using ‹0 < e› γ1 winding_number by blast
moreover
obtain p2 where "winding_number_prop γ2 z e p2 (winding_number γ2 z)"
using ‹0 < e› γ2 winding_number by blast
ultimately
have "winding_number_prop (γ1+++γ2) z e (p1+++p2) (winding_number γ1 z + winding_number γ2 z)"
using assms
apply (simp add: winding_number_prop_def not_in_path_image_join contour_integrable_inversediff algebra_simps)
apply (auto simp: joinpaths_def)
done
then show ?thesis
by blast
qed
qed (use assms in ‹auto simp: not_in_path_image_join›)

lemma winding_number_reversepath:
assumes "path γ" "z ∉ path_image γ"
shows "winding_number(reversepath γ) z = - (winding_number γ z)"
proof (rule winding_number_unique)
show "∃p. winding_number_prop (reversepath γ) z e p (- winding_number γ z)" if "e > 0" for e
proof -
obtain p where "winding_number_prop γ z e p (winding_number γ z)"
using ‹0 < e› assms winding_number by blast
then have "winding_number_prop (reversepath γ) z e (reversepath p) (- winding_number γ z)"
using assms
apply (simp add: winding_number_prop_def contour_integral_reversepath contour_integrable_inversediff valid_path_imp_reverse)
apply (auto simp: reversepath_def)
done
then show ?thesis
by blast
qed
qed (use assms in auto)

lemma winding_number_shiftpath:
assumes γ: "path γ" "z ∉ path_image γ"
and "pathfinish γ = pathstart γ" "a ∈ {0..1}"
shows "winding_number(shiftpath a γ) z = winding_number γ z"
proof (rule winding_number_unique_loop)
show "∃p. valid_path p ∧ z ∉ path_image p ∧ pathfinish p = pathstart p ∧
(∀t∈{0..1}. cmod (shiftpath a γ t - p t) < e) ∧
contour_integral p (λw. 1 / (w - z)) =
complex_of_real (2 * pi) * 𝗂 * winding_number γ z"
if "e > 0" for e
proof -
obtain p where "winding_number_prop γ z e p (winding_number γ z)"
using ‹0 < e› assms winding_number by blast
then show ?thesis
apply (rule_tac x="shiftpath a p" in exI)
using assms that
apply (auto simp: winding_number_prop_def path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath contour_integral_shiftpath)
done
qed
qed (use assms in ‹auto simp: path_shiftpath path_image_shiftpath pathfinish_shiftpath pathstart_shiftpath›)

lemma winding_number_split_linepath:
assumes "c ∈ closed_segment a b" "z ∉ closed_segment a b"
shows "winding_number(linepath a b) z = winding_number(linepath a c) z + winding_number(linepath c b) z"
proof -
have "z ∉ closed_segment a c" "z ∉ closed_segment c b"
using assms  by (meson convex_contains_segment convex_segment ends_in_segment subsetCE)+
then show ?thesis
using assms
by (simp add: winding_number_valid_path contour_integral_split_linepath [symmetric] continuous_on_inversediff field_simps)
qed

lemma winding_number_cong:
"(⋀t. ⟦0 ≤ t; t ≤ 1⟧ ⟹ p t = q t) ⟹ winding_number p z = winding_number q z"
by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)

lemma winding_number_constI:
assumes "c≠z" "⋀t. ⟦0≤t; t≤1⟧ ⟹ g t = c"
shows "winding_number g z = 0"
proof -
have "winding_number g z = winding_number (linepath c c) z"
apply (rule winding_number_cong)
using assms unfolding linepath_def by auto
moreover have "winding_number (linepath c c) z =0"
apply (rule winding_number_trivial)
using assms by auto
ultimately show ?thesis by auto
qed

lemma winding_number_offset: "winding_number p z = winding_number (λw. p w - z) 0"
unfolding winding_number_def
proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
fix n e g
assume "0 < e" and g: "winding_number_prop p z e g n"
then show "∃r. winding_number_prop (λw. p w - z) 0 e r n"
by (rule_tac x="λt. g t - z" in exI)
(force simp: winding_number_prop_def contour_integral_integral valid_path_def path_defs
vector_derivative_def has_vector_derivative_diff_const piecewise_C1_differentiable_diff C1_differentiable_imp_piecewise)
next
fix n e g
assume "0 < e" and g: "winding_number_prop (λw. p w - z) 0 e g n"
then show "∃r. winding_number_prop p z e r n"
apply (rule_tac x="λt. g t + z" in exI)
apply (simp add: winding_number_prop_def contour_integral_integral valid_path_def path_defs
apply (force simp: algebra_simps)
done
qed

subsubsection‹Some lemmas about negating a path›

lemma valid_path_negatepath: "valid_path γ ⟹ valid_path (uminus ∘ γ)"
unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast

lemma has_contour_integral_negatepath:
assumes γ: "valid_path γ" and cint: "((λz. f (- z)) has_contour_integral - i) γ"
shows "(f has_contour_integral i) (uminus ∘ γ)"
proof -
obtain S where cont: "continuous_on {0..1} γ" and "finite S" and diff: "γ C1_differentiable_on {0..1} - S"
using γ by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
have "((λx. - (f (- γ x) * vector_derivative γ (at x within {0..1}))) has_integral i) {0..1}"
using cint by (auto simp: has_contour_integral_def dest: has_integral_neg)
then
have "((λx. f (- γ x) * vector_derivative (uminus ∘ γ) (at x within {0..1})) has_integral i) {0..1}"
proof (rule rev_iffD1 [OF _ has_integral_spike_eq])
show "negligible S"
by (simp add: ‹finite S› negligible_finite)
show "f (- γ x) * vector_derivative (uminus ∘ γ) (at x within {0..1}) =
- (f (- γ x) * vector_derivative γ (at x within {0..1}))"
if "x ∈ {0..1} - S" for x
proof -
have "vector_derivative (uminus ∘ γ) (at x within cbox 0 1) = - vector_derivative γ (at x within cbox 0 1)"
proof (rule vector_derivative_within_cbox)
show "(uminus ∘ γ has_vector_derivative - vector_derivative γ (at x within cbox 0 1)) (at x within cbox 0 1)"
using that unfolding o_def
by (metis C1_differentiable_on_eq UNIV_I diff differentiable_subset has_vector_derivative_minus subsetI that vector_derivative_works)
qed (use that in auto)
then show ?thesis
by simp
qed
qed
then show ?thesis by (simp add: has_contour_integral_def)
qed

lemma winding_number_negatepath:
assumes γ: "valid_path γ" and 0: "0 ∉ path_image γ"
shows "winding_number(uminus ∘ γ) 0 = winding_number γ 0"
proof -
have "(/) 1 contour_integrable_on γ"
using "0" γ contour_integrable_inversediff by fastforce
then have "((λz. 1/z) has_contour_integral contour_integral γ ((/) 1)) γ"
by (rule has_contour_integral_integral)
then have "((λz. 1 / - z) has_contour_integral - contour_integral γ ((/) 1)) γ"
using has_contour_integral_neg by auto
then show ?thesis
using assms
apply (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs)
done
qed

lemma contour_integrable_negatepath:
assumes γ: "valid_path γ" and pi: "(λz. f (- z)) contour_integrable_on γ"
shows "f contour_integrable_on (uminus ∘ γ)"
by (metis γ add.inverse_inverse contour_integrable_on_def has_contour_integral_negatepath pi)

(* A combined theorem deducing several things piecewise.*)
lemma winding_number_join_pos_combined:
"⟦valid_path γ1; z ∉ path_image γ1; 0 < Re(winding_number γ1 z);
valid_path γ2; z ∉ path_image γ2; 0 < Re(winding_number γ2 z); pathfinish γ1 = pathstart γ2⟧
⟹ valid_path(γ1 +++ γ2) ∧ z ∉ path_image(γ1 +++ γ2) ∧ 0 < Re(winding_number(γ1 +++ γ2) z)"
by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)

subsubsection‹Useful sufficient conditions for the winding number to be positive›

lemma Re_winding_number:
"⟦valid_path γ; z ∉ path_image γ⟧
⟹ Re(winding_number γ z) = Im(contour_integral γ (λw. 1/(w - z))) / (2*pi)"
by (simp add: winding_number_valid_path field_simps Re_divide power2_eq_square)

lemma winding_number_pos_le:
assumes γ: "valid_path γ" "z ∉ path_image γ"
and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ 0 ≤ Im (vector_derivative γ (at x) * cnj(γ x - z))"
shows "0 ≤ Re(winding_number γ z)"
proof -
have ge0: "0 ≤ Im (vector_derivative γ (at x) / (γ x - z))" if x: "0 < x" "x < 1" for x
using ge by (simp add: Complex.Im_divide algebra_simps x)
let ?vd = "λx. 1 / (γ x - z) * vector_derivative γ (at x)"
let ?int = "λz. contour_integral γ (λw. 1 / (w - z))"
have hi: "(?vd has_integral ?int z) (cbox 0 1)"
unfolding box_real
apply (subst has_contour_integral [symmetric])
using γ by (simp add: contour_integrable_inversediff has_contour_integral_integral)
have "0 ≤ Im (?int z)"
proof (rule has_integral_component_nonneg [of 𝗂, simplified])
show "⋀x. x ∈ cbox 0 1 ⟹ 0 ≤ Im (if 0 < x ∧ x < 1 then ?vd x else 0)"
by (force simp: ge0)
show "((λx. if 0 < x ∧ x < 1 then ?vd x else 0) has_integral ?int z) (cbox 0 1)"
by (rule has_integral_spike_interior [OF hi]) simp
qed
then show ?thesis
by (simp add: Re_winding_number [OF γ] field_simps)
qed

lemma winding_number_pos_lt_lemma:
assumes γ: "valid_path γ" "z ∉ path_image γ"
and e: "0 < e"
and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ e ≤ Im (vector_derivative γ (at x) / (γ x - z))"
shows "0 < Re(winding_number γ z)"
proof -
let ?vd = "λx. 1 / (γ x - z) * vector_derivative γ (at x)"
let ?int = "λz. contour_integral γ (λw. 1 / (w - z))"
have hi: "(?vd has_integral ?int z) (cbox 0 1)"
unfolding box_real
apply (subst has_contour_integral [symmetric])
using γ by (simp add: contour_integrable_inversediff has_contour_integral_integral)
have "e ≤ Im (contour_integral γ (λw. 1 / (w - z)))"
proof (rule has_integral_component_le [of 𝗂 "λx. 𝗂*e" "𝗂*e" "{0..1}", simplified])
show "((λx. if 0 < x ∧ x < 1 then ?vd x else 𝗂 * complex_of_real e) has_integral ?int z) {0..1}"
by (rule has_integral_spike_interior [OF hi, simplified box_real]) (use e in simp)
show "⋀x. 0 ≤ x ∧ x ≤ 1 ⟹
e ≤ Im (if 0 < x ∧ x < 1 then ?vd x else 𝗂 * complex_of_real e)"
qed (use has_integral_const_real [of _ 0 1] in auto)
with e show ?thesis
by (simp add: Re_winding_number [OF γ] field_simps)
qed

lemma winding_number_pos_lt:
assumes γ: "valid_path γ" "z ∉ path_image γ"
and e: "0 < e"
and ge: "⋀x. ⟦0 < x; x < 1⟧ ⟹ e ≤ Im (vector_derivative γ (at x) * cnj(γ x - z))"
shows "0 < Re (winding_number γ z)"
proof -
have bm: "bounded ((λw. w - z) ` (path_image γ))"
using bounded_translation [of _ "-z"] γ by (simp add: bounded_valid_path_image)
then obtain B where B: "B > 0" and Bno: "⋀x. x ∈ (λw. w - z) ` (path_image γ) ⟹ norm x ≤ B"
using bounded_pos [THEN iffD1, OF bm] by blast
{ fix x::real  assume x: "0 < x" "x < 1"
then have B2: "cmod (γ x - z)^2 ≤ B^2" using Bno [of "γ x - z"]
by (simp add: path_image_def power2_eq_square mult_mono')
with x have "γ x ≠ z" using γ
using path_image_def by fastforce
then have "e / B⇧2 ≤ Im (vector_derivative γ (at x) * cnj (γ x - z)) / (cmod (γ x - z))⇧2"
using B ge [OF x] B2 e
apply (rule_tac y="e / (cmod (γ x - z))⇧2" in order_trans)
apply (auto simp: divide_left_mono divide_right_mono)
done
then have "e / B⇧2 ≤ Im (vector_derivative γ (at x) / (γ x - z))"
by (simp add: complex_div_cnj [of _ "γ x - z" for x] del: complex_cnj_diff times_complex.sel)
} note * = this
show ?thesis
using e B by (simp add: * winding_number_pos_lt_lemma [OF γ, of "e/B^2"])
qed

subsection‹The winding number is an integer›

text‹Proof from the book Complex Analysis by Lars V. Ahlfors, Chapter 4, section 2.1,
Also on page 134 of Serge Lang's book with the name title, etc.›

lemma exp_fg:
fixes z::complex
assumes g: "(g has_vector_derivative g') (at x within s)"
and f: "(f has_vector_derivative (g' / (g x - z))) (at x within s)"
and z: "g x ≠ z"
shows "((λx. exp(-f x) * (g x - z)) has_vector_derivative 0) (at x within s)"
proof -
have *: "(exp ∘ (λx. (- f x)) has_vector_derivative - (g' / (g x - z)) * exp (- f x)) (at x within s)"
using assms unfolding has_vector_derivative_def scaleR_conv_of_real
by (auto intro!: derivative_eq_intros)
show ?thesis
apply (rule has_vector_derivative_eq_rhs)
using z
apply (auto intro!: derivative_eq_intros * [unfolded o_def] g)
done
qed

lemma winding_number_exp_integral:
fixes z::complex
assumes γ: "γ piecewise_C1_differentiable_on {a..b}"
and ab: "a ≤ b"
and z: "z ∉ γ ` {a..b}"
shows "(λx. vector_derivative γ (at x) / (γ x - z)) integrable_on {a..b}"
(is "?thesis1")
"exp (- (integral {a..b} (λx. vector_derivative γ (at x) / (γ x - z)))) * (γ b - z) = γ a - z"
(is "?thesis2")
proof -
let ?Dγ = "λx. vector_derivative γ (at x)"
have [simp]: "⋀x. a ≤ x ⟹ x ≤ b ⟹ γ x ≠ z"
using z by force
have cong: "continuous_on {a..b} γ"
using γ by (simp add: piecewise_C1_differentiable_on_def)
obtain k where fink: "finite k" and g_C1_diff: "γ C1_differentiable_on ({a..b} - k)"
using γ by (force simp: piecewise_C1_differentiable_on_def)
have ∘: "open ({a<..<b} - k)"
using ‹finite k› by (simp add: finite_imp_closed open_Diff)
moreover have "{a<..<b} - k ⊆ {a..b} - k"
by force
ultimately have g_diff_at: "⋀x. ⟦x ∉ k; x ∈ {a<..<b}⟧ ⟹ γ differentiable at x"
by (metis Diff_iff differentiable_on_subset C1_diff_imp_diff [OF g_C1_diff] differentiable_on_def at_within_open)
{ fix w
assume "w ≠ z"
have "continuous_on (ball w (cmod (w - z))) (λw. 1 / (w - z))"
by (auto simp: dist_norm intro!: continuous_intros)
moreover have "⋀x. cmod (w - x) < cmod (w - z) ⟹ ∃f'. ((λw. 1 / (w - z)) has_field_derivative f') (at x)"
by (auto simp: intro!: derivative_eq_intros)
ultimately have "W```