# Theory Contour_Integration

```section ‹Contour integration›
theory Contour_Integration
imports "HOL-Analysis.Analysis"
begin

lemma lhopital_complex_simple:
assumes "(f has_field_derivative f') (at z)"
assumes "(g has_field_derivative g') (at z)"
assumes "f z = 0" "g z = 0" "g' ≠ 0" "f' / g' = c"
shows   "((λw. f w / g w) ⤏ c) (at z)"
proof -
have "eventually (λw. w ≠ z) (at z)"
by (auto simp: eventually_at_filter)
hence "eventually (λw. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)"
by eventually_elim (simp add: assms field_split_simps)
moreover have "((λw. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) ⤏ f' / g') (at z)"
by (intro tendsto_divide has_field_derivativeD assms)
ultimately have "((λw. f w / g w) ⤏ f' / g') (at z)"
by (blast intro: Lim_transform_eventually)
with assms show ?thesis by simp
qed

subsection‹Definition›

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

definition✐‹tag important› 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✐‹tag important› contour_integrable_on
(infixr "contour'_integrable'_on" 50)
where "f contour_integrable_on g ≡ ∃i. (f has_contour_integral i) g"

definition✐‹tag important› 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"
unfolding contour_integral_def has_contour_integral_def contour_integrable_on_def
using has_integral_unique by blast

lemma 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

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

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

lemma integrable_on_localized_vector_derivative:
"(λx. f (g x) * vector_derivative p (at x within {a..b})) integrable_on {a..b} ⟷
(λx. f (g x) * vector_derivative p (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)

lemma has_contour_integral_mirror_iff:
assumes "valid_path g"
shows   "(f has_contour_integral I) (-g) ⟷ ((λx. -f (- x)) has_contour_integral I) g"
proof -
from assms have "g piecewise_differentiable_on {0..1}"
by (auto simp: valid_path_def piecewise_C1_imp_differentiable)
then obtain S where "finite S" and S: "⋀x. x ∈ {0..1} - S ⟹ g differentiable at x within {0..1}"
unfolding piecewise_differentiable_on_def by blast
have S': "g differentiable at x" if "x ∈ {0..1} - ({0, 1} ∪ S)" for x
proof -
from that have "x ∈ interior {0..1}" by auto
with S[of x] that show ?thesis by (auto simp: at_within_interior[of _ "{0..1}"])
qed

have "(f has_contour_integral I) (-g) ⟷
((λx. f (- g x) * vector_derivative (-g) (at x)) has_integral I) {0..1}"
also have "… ⟷ ((λx. -f (- g x) * vector_derivative g (at x)) has_integral I) {0..1}"
by (intro has_integral_spike_finite_eq[of "S ∪ {0, 1}"])
(insert ‹finite S› S', auto simp: o_def fun_Compl_def)
also have "… ⟷ ((λx. -f (-x)) has_contour_integral I) g"
finally show ?thesis .
qed

lemma contour_integral_on_mirror_iff:
assumes "valid_path g"
shows   "f contour_integrable_on (-g) ⟷ (λx. -f (- x)) contour_integrable_on g"
by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff assms)

lemma contour_integral_mirror:
assumes "valid_path g"
shows   "contour_integral (-g) f = contour_integral g (λx. -f (- x))"
proof (cases "f contour_integrable_on (-g)")
case True with contour_integral_unique assms show ?thesis
by (auto simp: contour_integrable_on_def has_contour_integral_mirror_iff)
next
case False then show ?thesis
by (simp add: assms contour_integral_on_mirror_iff not_integrable_contour_integral)
qed

subsection✐‹tag unimportant› ‹Reversing a path›

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
unfolding reversepath_def has_contour_integral_def
by (rule_tac S = "(λx. 1 - x) ` S" in has_integral_spike_finite) (auto simp: *)
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✐‹tag unimportant› ‹Joining two paths together›

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: "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))"
if "0 ≤ z" "z*2 < 1" "z*2 ∉ s1" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < ¦z - 1/2¦"
using that by auto
have "((*) 2 has_vector_derivative 2) (at z)"
by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
moreover have "(g1 has_vector_derivative vector_derivative g1 (at (z * 2))) (at (2 * z))"
using s1 that by (auto simp: algebra_simps vector_derivative_works)
ultimately
show "((λx. g1 (2 * x)) has_vector_derivative 2 *⇩R vector_derivative g1 (at (z * 2))) (at z)"
by (intro vector_diff_chain_at [simplified o_def])
qed (use that in ‹simp_all add: dist_real_def abs_if split: if_split_asm›)

have g2: "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))"
if "1 < z*2" "z ≤ 1" "z*2 - 1 ∉ s2" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < ¦z - 1/2¦"
using that by auto
have "((λx. 2 * x - 1) has_vector_derivative 2) (at z)"
by (simp add: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
moreover have "(g2 has_vector_derivative vector_derivative g2 (at (z * 2 - 1))) (at (2 * z - 1))"
using s2 that by (auto simp: algebra_simps vector_derivative_works)
ultimately
show "((λx. g2 (2 * x - 1)) has_vector_derivative 2 *⇩R vector_derivative g2 (at (z * 2 - 1))) (at z)"
by (intro vector_diff_chain_at [simplified o_def])
qed (use that in ‹simp_all add: dist_real_def abs_if split: if_split_asm›)

have "((λx. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
proof (rule has_integral_spike_finite [OF _ _ i1])
show "finite (insert (1/2) ((*) 2 -` s1))"
using s1 by (force intro: finite_vimageI [where h = "(*)2"] inj_onI)
qed (auto simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
moreover have "((λx. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
proof (rule has_integral_spike_finite [OF _ _ i2])
show "finite (insert (1/2) ((λx. 2 * x - 1) -` s2))"
using s2 by (force intro: finite_vimageI [where h = "λx. 2*x-1"] inj_onI)
qed (auto simp add: joinpaths_def scaleR_conv_of_real mult_ac g2)
ultimately
show ?thesis
by (simp add: has_contour_integral has_integral_combine [where c = "1/2"])
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 integrable_affinity [of _ 0 "1/2" "1/2" 0] integrable_on_subcbox [where a=0 and b="1/2"]
by (fastforce simp: contour_integrable_on)
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: "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)"
if "0 < z" "z < 1" "z ∉ s1" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < ¦(z - 1)/2¦"
using that by auto
have §: "((λx. x * 2) has_vector_derivative 2) (at (z/2))"
using s1 by (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
have "(g1 has_vector_derivative vector_derivative g1 (at z)) (at z)"
using s1 that by (auto simp: vector_derivative_works)
then show "((λx. g1 (2 * x)) has_vector_derivative 2 *⇩R vector_derivative g1 (at z)) (at (z/2))"
using vector_diff_chain_at [OF §] by (auto simp: field_simps o_def)
qed (use that in ‹simp_all add: field_simps dist_real_def abs_if split: if_split_asm›)
have fin01: "finite ({0, 1} ∪ s1)"
show ?thesis
unfolding contour_integrable_on
by (intro integrable_spike_finite [OF fin01 _ *]) (auto simp: joinpaths_def scaleR_conv_of_real g1)
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 integrable_affinity [of _ "1/2::real" 1 "1/2" "1/2"]
integrable_on_subcbox [where a="1/2" and b=1]
by (fastforce simp: contour_integrable_on image_affinity_atLeastAtMost_diff)
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: "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)"
if "0 < z" "z < 1" "z ∉ s2" for z
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
show "0 < ¦z/2¦"
using that by auto
have §: "((λx. x * 2 - 1) has_vector_derivative 2) (at ((1 + z)/2))"
using s2 by (auto simp: has_vector_derivative_def has_derivative_def bounded_linear_mult_left)
have "(g2 has_vector_derivative vector_derivative g2 (at z)) (at z)"
using s2 that by (auto simp: vector_derivative_works)
then show "((λx. g2 (2*x - 1)) has_vector_derivative 2 *⇩R vector_derivative g2 (at z)) (at (z/2 + 1/2))"
using vector_diff_chain_at [OF §] by (auto simp: field_simps o_def)
qed (use that in ‹simp_all add: field_simps dist_real_def abs_if split: if_split_asm›)
have fin01: "finite ({0, 1} ∪ s2)"
show ?thesis
unfolding contour_integrable_on
by (intro integrable_spike_finite [OF fin01 _ *]) (auto simp: joinpaths_def scaleR_conv_of_real g2)
qed

lemma contour_integrable_join [simp]:
"⟦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]:
"⟦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✐‹tag unimportant› ‹Shifting the starting point of a (closed) path›

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))"
by (smt (verit, ccfv_threshold) Henstock_Kurzweil_Integration.integral_combine a add.commute atLeastAtMost_iff has_integral_iff)
have vd1: "vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a))"
if "0 ≤ x" "x + a < 1" "x ∉ (λx. x - a) ` S" for x
unfolding shiftpath_def
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
have "((λx. g (x + a)) has_vector_derivative vector_derivative g (at (a + x))) (at x)"
proof (rule vector_diff_chain_at [of _ 1, simplified o_def scaleR_one])
show "((λx. x + a) has_vector_derivative 1) (at x)"
by (rule derivative_eq_intros | simp)+
have "g differentiable at (x + a)"
using g a that by force
then show "(g has_vector_derivative vector_derivative g (at (a + x))) (at (x + a))"
qed
then show "((λx. g (a + x)) has_vector_derivative vector_derivative g (at (x + a))) (at x)"
by (auto simp: field_simps)
show "0 < dist (1 - a) x"
using that by auto
qed (use that in ‹auto simp: dist_real_def›)

have vd2: "vector_derivative (shiftpath a g) (at x) = vector_derivative g (at (x + a - 1))"
if "x ≤ 1" "1 < x + a" "x ∉ (λx. x - a + 1) ` S" for x
unfolding shiftpath_def
proof (rule vector_derivative_at [OF has_vector_derivative_transform_within])
have "((λx. g (x + a - 1)) has_vector_derivative vector_derivative g (at (a+x-1))) (at x)"
proof (rule vector_diff_chain_at [of _ 1, simplified o_def scaleR_one])
show "((λx. x + a - 1) has_vector_derivative 1) (at x)"
by (rule derivative_eq_intros | simp)+
have "g differentiable at (x+a-1)"
using g a that by force
then show "(g has_vector_derivative vector_derivative g (at (a+x-1))) (at (x + a - 1))"
qed
then show "((λx. g (a + x - 1)) has_vector_derivative vector_derivative g (at (x + a - 1))) (at x)"
by (auto simp: field_simps)
show "0 < dist (1 - a) x"
using that by auto
qed (use that in ‹auto simp: dist_real_def›)

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})"
using * a by (force intro: integrable_subinterval_real)
have "finite ({1 - a} ∪ (λx. x - a) ` S)"
using S by blast
then 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 f = "λx. f(g(a+x)) * vector_derivative g (at(a+x))"])
subgoal
subgoal
using has_integral_affinity [where m=1 and c=a] integrable_integral [OF va1]
done
moreover
have "finite ({1 - a} ∪ (λx. x - a + 1) ` S)"
using S by blast
then 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 f = "λx. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
subgoal
subgoal
using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]]
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 §: "shiftpath (1 - a) (shiftpath a g) differentiable at x"
using assms x
by (intro differentiable_transform_within [OF gx, of "min x (1-x)"])
(auto simp: dist_real_def shiftpath_shiftpath abs_if split: if_split_asm)
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 assms x §
apply (auto simp: finite_imp_closed open_Diff shiftpath_shiftpath
at_within_interior [of _ "{0..1}"] vector_derivative_works [symmetric])
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
unfolding has_contour_integral_def
proof (rule has_integral_spike_finite [of "{0,1} ∪ S", OF _ _  fi [unfolded has_contour_integral_def]])
show "finite ({0, 1} ∪ S)"
qed (use S assms vd in ‹auto simp: shiftpath_shiftpath›)
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)

subsection✐‹tag unimportant› ‹More about straight-line paths›

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 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 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 §: "(λt. f (g t) * vector_derivative g (at t)) integrable_on {u..v}"
using contour_integrable_on f integrable_on_subinterval uv by fastforce
then 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 uv False unfolding has_integral_integral
apply simp
apply (drule has_integral_affinity [where m="v-u" and c=u, simplified])
done

have vd: "vector_derivative (λx. g ((v-u) * x + u)) (at x) = (v-u) *⇩R vector_derivative g (at ((v-u) * x + u))"
if "x ∈ {0..1}"  "x ∉ (λt. (v-u) *⇩R t + u) -` S" for x
proof (rule vector_derivative_at [OF vector_diff_chain_at [simplified o_def]])
show "((λx. (v - u) * x + u) has_vector_derivative v - u) (at x)"
by (intro derivative_eq_intros | simp)+
qed (use S uv mult_left_le [of x "v-u"] that in ‹auto simp: vector_derivative_works›)

have fin: "finite ((λt. (v - u) *⇩R t + u) -` S)"
using fs by (auto simp: inj_on_def False finite_vimageI)
show ?thesis
unfolding subpath_def has_contour_integral
apply (rule has_integral_spike_finite [OF fin])
using has_integral_cmul [OF *, where c = "v-u"] fs assms
by (auto simp: False vd scaleR_conv_of_real)
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)"
by (smt (verit, ccfv_threshold) assms contour_integrable_on_def contour_integrable_reversepath_eq
has_contour_integral_subpath reversepath_subpath valid_path_subpath)

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}"
(is "(?fg has_integral _)_")
proof -
have "(?fg has_integral integral {u..v} ?fg) {u..v}"
using assms contour_integrable_on integrable_on_subinterval by fastforce
then show ?thesis
by (metis (full_types) assms contour_integral_unique has_contour_integral_subpath)
qed

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"
proof -
have "(λx. f (g x) * vector_derivative g (at x)) integrable_on {u..w}"
using integrable_on_subcbox [where a=u and b=w and S = "{0..1}"] assms
by (auto simp: contour_integrable_on)
with assms show ?thesis
by (auto simp: contour_integral_subcontour_integral Henstock_Kurzweil_Integration.integral_combine)
qed

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]
by (elim disjE) (auto simp: * contour_integral_reversepath contour_integrable_subpath
valid_path_subpath algebra_simps)
next
case False
with assms show ?thesis
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)

lemma contour_integral_cong:
assumes "g = g'" "⋀x. x ∈ path_image g ⟹ f x = f' x"
shows   "contour_integral g f = contour_integral g' f'"
unfolding contour_integral_integral using assms
by (intro integral_cong) (auto simp: path_image_def)

lemma contour_integral_spike_finite_simple_path:
assumes "finite A" "simple_path g" "g = g'" "⋀x. x ∈ path_image g - A ⟹ f x = f' x"
shows   "contour_integral g f = contour_integral g' f'"
unfolding contour_integral_integral
proof (rule integral_spike)
have "finite (g -` A ∩ {0<..<1})" using ‹simple_path g› ‹finite A›
by (intro finite_vimage_IntI simple_path_inj_on) auto
hence "finite ({0, 1} ∪ g -` A ∩ {0<..<1})" by auto
thus "negligible ({0, 1} ∪ g -` A ∩ {0<..<1})" by (rule negligible_finite)
next
fix x assume "x ∈ {0..1} - ({0, 1} ∪ g -` A ∩ {0<..<1})"
hence "g x ∈ path_image g - A" by (auto simp: path_image_def)
with assms show "f' (g' x) * vector_derivative g' (at x) = f (g x) * vector_derivative g (at x)"
by simp
qed

text ‹Contour integral along a segment on the real axis›

lemma has_contour_integral_linepath_Reals_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "a ∈ Reals" "b ∈ Reals" "Re a < Re b"
shows   "(f has_contour_integral I) (linepath a b) ⟷
((λx. f (of_real x)) has_integral I) {Re a..Re b}"
proof -
from assms have [simp]: "of_real (Re a) = a" "of_real (Re b) = b"
from assms have "a ≠ b" by auto
have "((λx. f (of_real x)) has_integral I) (cbox (Re a) (Re b)) ⟷
((λx. f (a + b * of_real x - a * of_real x)) has_integral I /⇩R (Re b - Re a)) {0..1}"
by (subst has_integral_affinity_iff [of "Re b - Re a" _ "Re a", symmetric])
(insert assms, simp_all add: field_simps scaleR_conv_of_real)
also have "(λx. f (a + b * of_real x - a * of_real x)) =
(λx. (f (a + b * of_real x - a * of_real x) * (b - a)) /⇩R (Re b - Re a))"
using ‹a ≠ b› by (auto simp: field_simps fun_eq_iff scaleR_conv_of_real)
also have "(… has_integral I /⇩R (Re b - Re a)) {0..1} ⟷
((λx. f (linepath a b x) * (b - a)) has_integral I) {0..1}" using assms
by (subst has_integral_cmul_iff) (auto simp: linepath_def scaleR_conv_of_real algebra_simps)
also have "… ⟷ (f has_contour_integral I) (linepath a b)" unfolding has_contour_integral_def
by (intro has_integral_cong) (simp add: vector_derivative_linepath_within)
finally show ?thesis by simp
qed

lemma contour_integrable_linepath_Reals_iff:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "a ∈ Reals" "b ∈ Reals" "Re a < Re b"
shows   "(f contour_integrable_on linepath a b) ⟷
(λx. f (of_real x)) integrable_on {Re a..Re b}"
using has_contour_integral_linepath_Reals_iff[OF assms, of f]
by (auto simp: contour_integrable_on_def integrable_on_def)

lemma contour_integral_linepath_Reals_eq:
fixes a b :: complex and f :: "complex ⇒ complex"
assumes "a ∈ Reals" "b ∈ Reals" "Re a < Re b"
shows   "contour_integral (linepath a b) f = integral {Re a..Re b} (λx. f (of_real x))"
proof (cases "f contour_integrable_on linepath a b")
case True
thus ?thesis using has_contour_integral_linepath_Reals_iff[OF assms, of f]
using has_contour_integral_integral has_contour_integral_unique by blast
next
case False
thus ?thesis using contour_integrable_linepath_Reals_iff[OF assms, of f]
qed

subsection ‹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 "finite K" and 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 "continuous_on (g ` {a..b}) f"
using assms
by (metis field_differentiable_def field_differentiable_imp_continuous_at continuous_on_eq_continuous_within continuous_on_subset image_subset_iff)
then have cfg: "continuous_on {a..b} (λx. f (g x))"
by (rule continuous_on_compose [OF cg, unfolded o_def])
{ 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)
} then show ?thesis
using assms cfg
by (force simp: at_within_Icc_at intro: fundamental_theorem_of_calculus_interior_strong [OF ‹finite K›])
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)

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 (closed_segment a b) (λx. f x * (b - a))"
by (rule continuous_intros | simp add: assms)+
then have "continuous_on {0..1} (λx. f (linepath a b x) * (b - a))"
by (metis (no_types, lifting) continuous_on_compose continuous_on_cong continuous_on_linepath linepath_image_01 o_apply)
then have "(λx. f (linepath a b x) *
vector_derivative (linepath a b)
(at x within {0..1})) integrable_on
{0..1}"
by (metis (no_types, lifting) continuous_on_cong integrable_continuous_real vector_derivative_linepath_within)
then show ?thesis
by (simp add: contour_integrable_on_def has_contour_integral_def integrable_on_def [symmetric])
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"
using contour_integral_primitive [of UNIV "λx. x^2/2" "λx. x" "linepath a b"] contour_integral_unique

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✐‹tag unimportant› ‹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"
by (simp add: has_contour_integral_def algebra_simps has_integral_mult_right)

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

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 (mono_tags, lifting) has_contour_integral_def has_integral_eq image_eqI path_image_def)

lemma has_contour_integral_bound_linepath:
assumes "(f has_contour_integral i) (linepath a b)"
"0 ≤ B" and B: "⋀x. x ∈ closed_segment a b ⟹ norm(f x) ≤ B"
shows "norm i ≤ B * norm(b - a)"
proof -
have "norm i ≤ (B * norm (b - a)) * content (cbox 0 (1::real))"
proof (rule has_integral_bound
[of _ "λx. f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1})"])
show  "cmod (f (linepath a b x) * vector_derivative (linepath a b) (at x within {0..1}))
≤ B * cmod (b - a)"
if "x ∈ cbox 0 1" for x::real
using that box_real(2) norm_mult
by (metis B linepath_in_path mult_right_mono norm_ge_zero vector_derivative_linepath_within)
qed (use assms has_contour_integral_def in auto)
then show ?thesis
by (auto simp: content_real)
qed

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✐‹tag unimportant› ‹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: "contour_integral g (λz. -f z) = -contour_integral g f"

"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 contour_integral_cong contour_integral_def by fastforce

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)"
by (meson has_contour_integral_bound_linepath has_contour_integral_integral)

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✐‹tag unimportant› ‹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)

lemma contour_integrable_neg_iff:
"(λx. -f x) contour_integrable_on g ⟷ f contour_integrable_on g"
using contour_integrable_neg[of f g] contour_integrable_neg[of "λx. -f x" g] by auto

lemma contour_integrable_lmul_iff:
"c ≠ 0 ⟹ (λx. c * f x) contour_integrable_on g ⟷ f contour_integrable_on g"
using contour_integrable_lmul[of f g c] contour_integrable_lmul[of "λx. c * f x" g "inverse c"]
by (auto simp: field_simps)

lemma contour_integrable_rmul_iff:
"c ≠ 0 ⟹ (λx. f x * c) contour_integrable_on g ⟷ f contour_integrable_on g"
using contour_integrable_rmul[of f g c] contour_integrable_rmul[of "λx. c * f x" g "inverse c"]
by (auto simp: field_simps)

lemma contour_integrable_div_iff:
"c ≠ 0 ⟹ (λx. f x / c) contour_integrable_on g ⟷ f contour_integrable_on g"
using contour_integrable_rmul_iff[of "inverse c"] by (simp add: field_simps)

subsection✐‹tag unimportant› ‹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)"
using contour_integral_reversepath by fastforce

text ‹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. (x / k) *⇩R a + ((k - x) / k) *⇩R a = a"
using False by (simp add: field_split_simps flip: real_vector.scale_left_distrib)
then have "⋀x. ((k - x) / k) *⇩R a + (x / k) *⇩R c = (1 - x) *⇩R a + x *⇩R b"
using False by (simp add: c' algebra_simps)
then 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"]
by (force dest: has_integral_cmul [where c = "inverse k"]
simp add: divide_simps mult.commute [of _ "k"] image_affinity_atLeastAtMost c)
} 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 unfolding c' scaleR_conv_of_real
apply (simp add: distrib_right distrib_left right_diff_distrib left_diff_distrib)
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
}
then show ?thesis
using f k unfolding has_contour_integral_linepath
by (simp add: linepath_def has_integral_combine [OF _ _ fi])
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])

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)

proposition 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 "continuous_on (cbox (0, 0) (1, 1::real)) ((λx. vector_derivative g (at x)) ∘ fst)"
"continuous_on (cbox (0, 0) (1::real, 1)) ((λx. vector_derivative h (at x)) ∘ snd)"
by (rule continuous_intros | simp add: gvcon hvcon)+
then have gvcon': "continuous_on (cbox (0, 0) (1, 1::real)) (λz. vector_derivative g (at (fst z)))"
and  hvcon': "continuous_on (cbox (0, 0) (1::real, 1)) (λx. vector_derivative h (at (snd x)))"
by auto
have "continuous_on ((λx. (g (fst x), h (snd x))) ` cbox (0,0) (1,1)) (λ(y1, y2). f y1 y2)"
by (auto simp: path_image_def intro: continuous_on_subset [OF fcon])
then have "continuous_on (cbox (0, 0) (1, 1)) ((λ(y1, y2). f y1 y2) ∘ (λw. ((g ∘ fst) w, (h ∘ snd) w)))"
by (intro gcon hcon continuous_intros | simp)+
then have fgh: "continuous_on (cbox (0, 0) (1, 1)) (λx. f (g (fst x)) (h (snd x)))"
by auto
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]])
have "⋀x. x ∈ {0..1} ⟹
continuous_on {0..1} (λxa. f (g x) (h xa))"
by (subst fgh1) (rule fcon_im1 hcon continuous_intros | simp)+
then show "⋀x. x ∈ {0..1} ⟹ f (g x) contour_integrable_on h"
unfolding contour_integrable_on
using continuous_on_mult hvcon integrable_continuous_real by blast
qed
also have "… = integral {0..1}
(```