Quelle  Contour_Integration.thy

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_cong:
  assumes "∧z. z ∈ path_image g ==> f z = f' z" "g = g'" "c = c'"
  shows   "(f has_contour_integral c) g ⟷ (f' has_contour_integral c') g'"
  unfolding has_contour_integral_def assms(2,3)
  by (intro has_integral_cong) (auto simp: assms path_image_def intro!: assms(1))

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_translate:
  "(f has_contour_integral I) ((+) z ∘ g) ⟷ ((λx. f (x + z)) has_contour_integral I) g"
  by (simp add: has_contour_integral_def add_ac)

lemma contour_integrable_translate:
  "f contour_integrable_on ((+) z ∘ g) ⟷ (λx. f (x + z)) contour_integrable_on g"
  by (simp add: contour_integrable_on_def has_contour_integral_translate)

lemma contour_integral_translate:
  "contour_integral ((+) z ∘ g) f = contour_integral g (λx. f (x + z))"
  by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)

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}"
    by (simp add: atLeastAtMost_diff_ends)
  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}"
  by (simp add: integrable_on_def has_integral_localized_vector_derivative)

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

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}"
    by (simp add: has_contour_integral)
  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"
    by (simp add: has_contour_integral)
  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)"
        by (simp add: o_def)
      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]]
    by (simp add: has_integral_neg)
  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)"
    by (simp add: assms contour_integrable_reversepath_eq)
  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)"
    by (simp add: 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)"
    by (simp add: 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))"
        by (metis add.commute vector_derivative_works)
    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))"
        by (metis add.commute vector_derivative_works)
    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
      using a by (simp add: vd1) (force simp: shiftpath_def add.commute)
    subgoal
      using has_integral_affinity [where m=1 and c=a] integrable_integral [OF va1]
      by (force simp add: add.commute)
    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
      using a by (simp add: vd2) (force simp: shiftpath_def add.commute)
    subgoal
      using has_integral_affinity [where m=1 and c="a-1", simplified, OF integrable_integral [OF v0a]]
      by (force simp add: algebra_simps)
    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)"
      by (simp add: 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}"
  by (simp add: has_contour_integral)

lemma has_contour_integral_trivial [iff]: "(f has_contour_integral 0) (linepath a a)"
  by (simp add: has_contour_integral_linepath)

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)"
  by (simp add: has_contour_integral subpath_def)

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"
  by (simp add: contour_integral_unique)

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])
    apply (simp_all add: image_affinity_atLeastAtMost_div_diff scaleR_conv_of_real)
    apply (simp add: divide_simps)
    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"
  by (smt (verit) Henstock_Kurzweil_Integration.integral_combine assms
      has_integral_contour_integral_subpath has_integral_iff)

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
    by (metis add.right_neutral contour_integral_reversepath contour_integral_subpath_refl
        diff_0 eq_diff_eq add_0 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)

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 -
  have [simp]: "of_real (Re a) = a" "of_real (Re b) = b" and "a ≠ b"
    using assms by (simp_all add: complex_eq_iff)
  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
    using has_contour_integral_def has_contour_integral_linepath by presburger
  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
    by (metis assms has_contour_integral_integral
        has_contour_integral_linepath_Reals_iff integral_unique)
next
  case False
  thus ?thesis
    by (simp add: assms contour_integrable_linepath_Reals_iff
        not_integrable_contour_integral not_integrable_integral)
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 DERIV_continuous_on continuous_on_subset image_subsetI)
  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})"
      by (simp add: has_vector_derivative_def scaleR_conv_of_real)
    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})"
      by (simp add: has_field_derivative_def)
    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
  by (simp add: has_field_der_id)

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

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

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"
  by (simp add: has_integral_neg has_contour_integral_def)

lemma has_contour_integral_add:
    "[(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_add has_contour_integral_def algebra_simps)

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"
  by (simp add: mult.commute has_contour_integral_lmul)

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)) * measure lborel (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"
  by (simp add: has_contour_integral_def)

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"
  by (simp add: contour_integral_integral)

lemma contour_integral_add:
    "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_add)

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"
  by (simp add: has_contour_integral_is_0 contour_integral_unique)

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"
  by (simp add: contour_integral_unique has_contour_integral_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

lemma contour_integrable_add:
    "[f1 contour_integrable_on g; f2 contour_integrable_on g] ==> (λx. f1 x + f2 x) contour_integrable_on g"
  using has_contour_integral_add contour_integrable_on_def
  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)

(* TODO: generalise to any path *)
lemma uniform_limit_contour_integral_linepath:
  assumes u: "uniform_limit (path_image (linepath a b)) f g F"
  assumes c: "∧n. continuous_on (path_image (linepath a b)) (f n)"
  assumes [simp]: "F ≠ bot"
  obtains I J where
    "∧n. (f n has_contour_integral I n) (linepath a b)"
    "(g has_contour_integral J) (linepath a b)"
    "(I ---> J) F"
proof (rule uniform_limit_integral)
  note [continuous_intros] = continuous_on_compose2[OF c]

  show "uniform_limit {0..1} (λx t. f x (linepath a b t) * (b - a))
          (λt. g (linepath a b t) * (b - a)) F"
  proof (rule uniform_limit_intros)
    show "uniform_limit {0..1} (λx t. f x (linepath a b t))
            (λt. g (linepath a b t)) F"
      using u unfolding path_image_def by (rule uniform_limit_compose') auto
  qed

  show "continuous_on {0..1} (λt. f n (linepath a b t) * (b - a))" for n
    by (intro continuous_intros; unfold path_image_def) auto

  fix I J
  assume I: "∧n. ((λt. f n (linepath a b t) * (b - a)) has_integral I n) {0..1}"
     and J: "((λt. g (linepath a b t) * (b - a)) has_integral J) {0..1}"
     and lim: "(I ---> J) F"
  show ?thesis
   by (rule that[of I J]) (use I J lim in ‹auto simp: has_contour_integral›)
qed auto

(* TODO: generalise to any path *)
lemma contour_integral_sums_linepath:
  assumes u: "uniform_limit (closed_segment a b) (λN w. ∑n
  assumes c: "∧n. continuous_on (closed_segment a b) (f n)"
  obtains J where
    "(g has_contour_integral J) (linepath a b)"
    "(λn. contour_integral (linepath a b) (f n)) sums J"
proof (rule uniform_limit_contour_integral_linepath)
  show "uniform_limit (path_image (linepath a b)) (λN w. ∑n
    using u by simp
next
  show "continuous_on (path_image (linepath a b)) (λw. ∑n for N
    by (intro continuous_intros continuous_on_subset[OF c]) simp_all
next
  fix I J
  assume 1: "∧N. ((λw. ∑n
  assume 2: "(g has_contour_integral J) (linepath a b)" and 3: "(I ---> J) sequentially"
  have 4: "I = (λN. (∑n
  proof
    fix N :: nat
    have "f n contour_integrable_on (linepath a b)" for n
      by (intro contour_integrable_continuous_linepath assms)
    hence "((λw. ∑n
             (∑n
      using c by (intro has_contour_integral_sum) (simp_all add: has_contour_integral_integral)
    with 1[of N] show "I N = (∑n
      using contour_integral_unique by metis
  qed
  have 5: "(λn. contour_integral (linepath a b) (f n)) sums J"
    using 1 2 3 4 unfolding sums_def by blast
  from that[OF 2 5] show ?thesis .
qed auto


lemma contour_integral_linepath_same_Re:
  assumes "Re z = c" "Re z' = c" "Im z = a" "Im z' = b" "a < b"
  shows   "contour_integral (linepath z z') f =
           i * integral {a..b} (λx. f (Complex c x))"
proof -
  have zz': "z = Complex c a" "z' = Complex c b"
    using assms by (auto simp: complex_eq_iff)
  have "contour_integral (linepath z z') f =
         (z' - z) * integral {0..1} (λx. f (linepath z z' x))"
    by (simp add: contour_integral_integral)
  also have "z' - z = i * of_real (b - a)"
    by (simp add: zz' Complex_eq algebra_simps)
  also have "integral {0..1} (λx. f (linepath z z' x)) =
             integral {0..1} (λx. f (Complex c (linepath a b x)))"
    by (simp add: linepath_def Complex_eq scaleR_conv_of_real algebra_simps zz')
  also have "… = integral {0..(b - a) / (b - a)} (λx. f (Complex c (a + (b - a) * x)))"
    using ‹a 🚫› by (simp add: algebra_simps linepath_def)
  also have "{0..(b - a) / (b - a)} = (λx. x / (b - a)) ` {0..b - a}"
    using ‹a 🚫› by simp
  also have "integral … (λx. f (Complex c (a + (b - a) * x))) =
             integral {a-a..b-a} (λx. f (Complex c (x + a))) / of_real (b - a)"
    using ‹a 🚫› by (subst integral_stretch_real) (auto simp: scaleR_conv_of_real add_ac)
  also have "… = integral {a..b} (λx. f (Complex c x)) / of_real (b - a)"
    by (subst integral_shift_real_ivl) (rule refl)
  finally show ?thesis
    using ‹a 🚫› by simp
qed

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"
    using assms by auto
  have c': "c = k *🪙R (b - a) + a"
    by (metis diff_add_cancel c)
  have bc: "(b - c) = (1 - k) *🪙R (b - a)"
    by (simp add: algebra_simps c')
  { 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 
      apply (simp add: c' scaleR_conv_of_real divide_simps)
      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])
  then have "(f has_contour_integral
                contour_integral (linepath a c) f + contour_integral (linepath c b) f) (linepath a b)"
    by (meson c contour_integrable_continuous_linepath
        has_contour_integral_integral has_contour_integral_split k)
  then show ?thesis
    by (metis contour_integral_unique)
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}
                     (λ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])
    subgoal
      by (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
    by (simp add: mult.commute mult.left_commute)
  also have "… = contour_integral h (λz. contour_integral g (λw. f w z))"
    unfolding contour_integral_integral integral_mult_left [symmetric]
    by (simp add: algebra_simps)
  finally show ?thesis
    by (simp add: contour_integral_integral)
qed

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

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)"
  by (simp add: subpath_def valid_path_polynomial_function)

subsection‹Partial circle path›

definition🍋‹tag important› part_circlepath :: "[complex, real, real, real, real] ==> complex"
  where "part_circlepath z r s t ≡ λx. z + of_real r * exp (i * of_real (linepath s t x))"

lemma pathstart_part_circlepath [simp]:
  "pathstart(part_circlepath z r s t) = z + r*exp(i * s)"
  by (metis part_circlepath_def pathstart_def pathstart_linepath)

lemma pathfinish_part_circlepath [simp]:
  "pathfinish(part_circlepath z r s t) = z + r*exp(i*t)"
  by (metis part_circlepath_def pathfinish_def pathfinish_linepath)

lemma reversepath_part_circlepath[simp]:
  "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
  unfolding part_circlepath_def reversepath_def linepath_def
  by (auto simp:algebra_simps)

lemma has_vector_derivative_part_circlepath [derivative_intros]:
    "((part_circlepath z r s t) has_vector_derivative
      (i * r * (of_real t - of_real s) * exp(i * linepath s t x)))
     (at x within X)"
  unfolding part_circlepath_def linepath_def scaleR_conv_of_real
  by (rule has_vector_derivative_real_field derivative_eq_intros | simp)+

lemma differentiable_part_circlepath:
  "part_circlepath c r a b differentiable at x within A"
  using has_vector_derivative_part_circlepath[of c r a b x A] differentiableI_vector by blast

lemma vector_derivative_part_circlepath:
    "vector_derivative (part_circlepath z r s t) (at x) =
       i * r * (of_real t - of_real s) * exp(i * linepath s t x)"
  using has_vector_derivative_part_circlepath vector_derivative_at by blast

lemma vector_derivative_part_circlepath01:
    "[0 ≤ x; x ≤ 1]
     ==> vector_derivative (part_circlepath z r s t) (at x within {0..1}) =
          i * r * (of_real t - of_real s) * exp(i * linepath s t x)"
  using has_vector_derivative_part_circlepath
  by (auto simp: vector_derivative_at_within_ivl)

lemma valid_path_part_circlepath [simp]: "valid_path (part_circlepath z r s t)"
  unfolding valid_path_def
  by (auto simp: C1_differentiable_on_eq vector_derivative_works vector_derivative_part_circlepath has_vector_derivative_part_circlepath
              intro!: C1_differentiable_imp_piecewise continuous_intros)

lemma path_part_circlepath [simp]: "path (part_circlepath z r s t)"
  by (simp add: valid_path_imp_path)

proposition path_image_part_circlepath:
  assumes "s ≤ t"
    shows "path_image (part_circlepath z r s t) = {z + r * exp(i * of_real x) | x. s ≤ x ∧ x ≤ t}"
proof -
  { fix z::real
    assume "0 ≤ z" "z ≤ 1"
    with ‹s ≤ t› have "∃x. (exp (i * linepath s t z) = exp (i * of_real x)) ∧ s ≤ x ∧ x ≤ t"
      apply (rule_tac x="(1 - z) * s + z * t" in exI)
      apply (simp add: linepath_def scaleR_conv_of_real algebra_simps)
      by (metis (no_types) affine_ineq mult.commute mult_left_mono)
  }
  moreover
  { fix z
    assume "s ≤ z" "z ≤ t"
    then have "z + of_real r * exp (i * of_real z) ∈ (λx. z + of_real r * exp (i * linepath s t x)) ` {0..1}"
      apply (rule_tac x="(z - s)/(t - s)" in image_eqI)
      apply (simp add: linepath_def scaleR_conv_of_real divide_simps exp_eq)
      apply (auto simp: field_split_simps)
      done
  }
  ultimately show ?thesis
    by (fastforce simp add: path_image_def part_circlepath_def)
qed

lemma path_image_part_circlepath':
  "path_image (part_circlepath z r s t) = (λx. z + r * cis x) ` closed_segment s t"
  by (metis (no_types, lifting) ext cis_conv_exp image_image linepath_image_01
      part_circlepath_def path_image_def)

lemma path_image_part_circlepath_subset:
    "[s ≤ t; 0 ≤ r] ==> path_image(part_circlepath z r s t) ⊆ sphere z r"
by (auto simp: path_image_part_circlepath sphere_def dist_norm algebra_simps norm_mult)

lemma in_path_image_part_circlepath:
  assumes "w ∈ path_image(part_circlepath z r s t)" "s ≤ t" "0 ≤ r"
    shows "norm(w - z) = r"
  by (smt (verit) assms dist_norm mem_Collect_eq norm_minus_commute path_image_part_circlepath_subset sphere_def subsetD)

lemma path_image_part_circlepath_subset':
  assumes "r ≥ 0"
  shows   "path_image (part_circlepath z r s t) ⊆ sphere z r"
  by (smt (verit) assms path_image_part_circlepath_subset reversepath_part_circlepath reversepath_simps(2))

lemma part_circlepath_cnj: "cnj (part_circlepath c r a b x) = part_circlepath (cnj c) r (-a) (-b) x"
  by (simp add: part_circlepath_def exp_cnj linepath_def algebra_simps)

lemma contour_integrable_on_compose_cnj_iff:
  assumes "valid_path γ"
  shows   "f contour_integrable_on (cnj ∘ γ) ⟷ (cnj ∘ f ∘ cnj) contour_integrable_on γ"
proof -
  from assms obtain S where S: "finite S" "γ C1_differentiable_on {0..1} - S"
    unfolding valid_path_def piecewise_C1_differentiable_on_def by blast
  have "f contour_integrable_on (cnj ∘ γ) ⟷
        ((λt. cnj (cnj (f (cnj (γ t))) * vector_derivative γ (at t))) integrable_on {0..1})"
    unfolding contour_integrable_on o_def
  proof (intro integrable_spike_finite_eq [OF S(1)])
    fix t :: real assume "t ∈ {0..1} - S"
    hence "γ differentiable at t"
      using S(2) by (meson C1_differentiable_on_eq)
    hence "vector_derivative (λx. cnj (γ x)) (at t) = cnj (vector_derivative γ (at t))"
      by (rule vector_derivative_cnj)
    thus "f (cnj (γ t)) * vector_derivative (λx. cnj (γ x)) (at t) =
          cnj (cnj (f (cnj (γ t))) * vector_derivative γ (at t))"
      by simp
  qed
  also have "… ⟷ ((λt. cnj (f (cnj (γ t))) * vector_derivative γ (at t)) integrable_on {0..1})"
    by (rule integrable_on_cnj_iff)
  also have "… ⟷ (cnj ∘ f ∘ cnj) contour_integrable_on γ"
    by (simp add: contour_integrable_on o_def)
  finally show ?thesis .
qed

lemma contour_integral_cnj:
  assumes "valid_path γ"
  shows   "contour_integral (cnj ∘ γ) f = cnj (contour_integral γ (cnj ∘ f ∘ cnj))"
proof -
  from assms obtain S where S: "finite S" "γ C1_differentiable_on {0..1} - S"
    unfolding valid_path_def piecewise_C1_differentiable_on_def by blast
  have "contour_integral (cnj ∘ γ) f =
          integral {0..1} (λt. cnj (cnj (f (cnj (γ t))) * vector_derivative γ (at t)))"
    unfolding contour_integral_integral
  proof (intro integral_spike)
    fix t assume "t ∈ {0..1} - S"
    hence "γ differentiable at t"
      using S(2) by (meson C1_differentiable_on_eq)
    hence "vector_derivative (λx. cnj (γ x)) (at t) = cnj (vector_derivative γ (at t))"
      by (rule vector_derivative_cnj)
    thus "cnj (cnj (f (cnj (γ t))) * vector_derivative γ (at t)) =
            f ((cnj ∘ γ) t) * vector_derivative (cnj ∘ γ) (at t)"
      by (simp add: o_def)
  qed (use S(1) in auto)
  also have "… = cnj (integral {0..1} (λt. cnj (f (cnj (γ t))) * vector_derivative γ (at t)))"
    by (subst integral_cnj [symmetric]) auto
  also have "… = cnj (contour_integral γ (cnj ∘ f ∘ cnj))"
    by (simp add: contour_integral_integral)
  finally show ?thesis .
qed

lemma contour_integral_negatepath:
  assumes "valid_path γ"
  shows   "contour_integral (uminus ∘ γ) f = -(contour_integral γ (λx. f (-x)))" (is "?lhs = ?rhs")
proof (cases "f contour_integrable_on (uminus ∘ γ)")
  case True
  hence *: "(f has_contour_integral ?lhs) (uminus ∘ γ)"
    using has_contour_integral_integral by blast
  have "((λz. f (-z)) has_contour_integral - contour_integral (uminus ∘ γ) f)
            (uminus ∘ (uminus ∘ γ))"
    by (rule has_contour_integral_negatepath) (use * assms in auto)
  hence "((λx. f (-x)) has_contour_integral -?lhs) γ"
    by (simp add: o_def)
  thus ?thesis
    by (simp add: contour_integral_unique)
next
  case False
  hence "¬(λz. f (- z)) contour_integrable_on γ"
    using contour_integrable_negatepath[of γ f] assms by auto
  with False show ?thesis
    by (simp add: not_integrable_contour_integral)
qed

lemma contour_integral_bound_part_circlepath:
  assumes "f contour_integrable_on part_circlepath c r a b"
  assumes "B ≥ 0" "r ≥ 0" "∧x. x ∈ path_image (part_circlepath c r a b) ==> norm (f x) ≤ B"
  shows   "norm (contour_integral (part_circlepath c r a b) f) ≤ B * r * ∣b - a∣"
proof -
  let ?I = "integral {0..1} (λx. f (part_circlepath c r a b x) * i * of_real (r * (b - a)) *
              exp (i * linepath a b x))"
  have "norm ?I ≤ integral {0..1} (λx::real. B * 1 * (r * ∣b - a∣) * 1)"
  proof (rule integral_norm_bound_integral, goal_cases)
    case 1
    with assms(1) show ?case
      by (simp add: contour_integrable_on vector_derivative_part_circlepath mult_ac)
  next
    case (3 x)
    with assms(2-) show ?case unfolding norm_mult norm_of_real abs_mult
      by (intro mult_mono) (auto simp: path_image_def)
  qed auto
  also have "?I = contour_integral (part_circlepath c r a b) f"
    by (simp add: contour_integral_integral vector_derivative_part_circlepath mult_ac)
  finally show ?thesis by simp
qed

lemma has_contour_integral_part_circlepath_iff:
  assumes "a < b"
  shows "(f has_contour_integral I) (part_circlepath c r a b) ⟷
           ((λt. f (c + r * cis t) * r * i * cis t) has_integral I) {a..b}"
proof -
  have "(f has_contour_integral I) (part_circlepath c r a b) ⟷
          ((λx. f (part_circlepath c r a b x) * vector_derivative (part_circlepath c r a b)
           (at x within {0..1})) has_integral I) {0..1}"
    unfolding has_contour_integral_def ..
  also have "… ⟷ ((λx. f (part_circlepath c r a b x) * r * (b - a) * i *
                            cis (linepath a b x)) has_integral I) {0..1}"
    by (intro has_integral_cong, subst vector_derivative_part_circlepath01)
       (simp_all add: cis_conv_exp)
  also have "… ⟷ ((λx. f (c + r * exp (i * linepath (of_real a) (of_real b) x)) *
                       r * i * exp (i * linepath (of_real a) (of_real b) x) *
                       vector_derivative (linepath (of_real a) (of_real b))
                         (at x within {0..1})) has_integral I) {0..1}"
    by (intro has_integral_cong, subst vector_derivative_linepath_within)
       (auto simp: part_circlepath_def cis_conv_exp of_real_linepath [symmetric])
  also have "… ⟷ ((λz. f (c + r * exp (i * z)) * r * i * exp (i * z)) has_contour_integral I)
                      (linepath (of_real a) (of_real b))"
    by (simp add: has_contour_integral_def)
  also have "… ⟷ ((λt. f (c + r * cis t) * r * i * cis t) has_integral I) {a..b}" using assms
    by (subst has_contour_integral_linepath_Reals_iff) (simp_all add: cis_conv_exp)
  finally show ?thesis .
qed

lemma contour_integrable_part_circlepath_iff:
  assumes "a < b"
  shows "f contour_integrable_on (part_circlepath c r a b) ⟷
           (λt. f (c + r * cis t) * r * i * cis t) integrable_on {a..b}"
  using assms by (auto simp: contour_integrable_on_def integrable_on_def
                             has_contour_integral_part_circlepath_iff)

lemma contour_integral_part_circlepath_eq:
  assumes "a < b"
  shows "contour_integral (part_circlepath c r a b) f =
           integral {a..b} (λt. f (c + r * cis t) * r * i * cis t)"
proof (cases "f contour_integrable_on part_circlepath c r a b")
  case True
  hence "(λt. f (c + r * cis t) * r * i * cis t) integrable_on {a..b}"
    using assms by (simp add: contour_integrable_part_circlepath_iff)
  with True show ?thesis
    using has_contour_integral_part_circlepath_iff[OF assms]
          contour_integral_unique has_integral_integrable_integral by blast
next
  case False
  hence "¬(λt. f (c + r * cis t) * r * i * cis t) integrable_on {a..b}"
    using assms by (simp add: contour_integrable_part_circlepath_iff)
  with False show ?thesis
    by (simp add: not_integrable_contour_integral not_integrable_integral)
qed

lemma contour_integral_part_circlepath_reverse:
  "contour_integral (part_circlepath c r a b) f = -contour_integral (part_circlepath c r b a) f"
  by (metis contour_integral_reversepath reversepath_part_circlepath valid_path_part_circlepath)

lemma contour_integral_part_circlepath_reverse':
  "b < a ==> contour_integral (part_circlepath c r a b) f =
               -contour_integral (part_circlepath c r b a) f"
  by (rule contour_integral_part_circlepath_reverse)

lemma finite_bounded_log: "finite {z::complex. norm z ≤ b ∧ exp z = w}"
proof (cases "w = 0")
  case True then show ?thesis by auto
next
  case False
  have *: "finite {x. cmod ((2 * real_of_int x * pi) * i) ≤ b + cmod (Ln w)}"
  proof (simp add: norm_mult finite_int_iff_bounded_le)
    have "abs ` {x. 2 * ∣real_of_int x∣ * pi ≤ b + cmod (Ln w)}
    ⊆ {..⌊(b + cmod (Ln w)) / (2 * pi)⌋}"
      by (auto simp: field_split_simps le_floor_iff)
    then show "∃k. abs ` {x. 2 * ∣of_int x∣ * pi ≤ b + cmod (Ln w)} ⊆ {..k}"
      by blast
  qed
  have [simp]: "∧P f. {z. P z ∧ (∃n. z = f n)} = f ` {n. P (f n)}"
    by blast
  have "finite {z. cmod z ≤ b ∧ exp z = exp (Ln w)}"
    using norm_add_leD by (fastforce intro: finite_subset [OF _ *] simp: exp_eq)
  then show ?thesis
    using False by auto
qed

lemma finite_bounded_log2:
  fixes a::complex
    assumes "a ≠ 0"
    shows "finite {z. norm z ≤ b ∧ exp(a*z) = w}"
proof -
  have *: "finite ((λz. z / a) ` {z. cmod z ≤ b * cmod a ∧ exp z = w})"
    by (rule finite_imageI [OF finite_bounded_log])
  show ?thesis
    by (rule finite_subset [OF _ *]) (force simp: assms norm_mult)
qed

lemma has_contour_integral_bound_part_circlepath_strong:
  assumes fi: "(f has_contour_integral i) (part_circlepath z r s t)"
      and "finite k" and le: "0 ≤ B" "0 < r" "s ≤ t"
      and B: "∧x. x ∈ path_image(part_circlepath z r s t) - k ==> norm(f x) ≤ B"
    shows "cmod i ≤ B * r * (t - s)"
proof -
  consider "s = t" | "s < t" using ‹s ≤ t› by linarith
  then show ?thesis
  proof cases
    case 1 with fi [unfolded has_contour_integral]
    have "i = 0"  by (simp add: vector_derivative_part_circlepath)
    with assms show ?thesis by simp
  next
    case 2
    have [simp]: "∣r∣ = r" using ‹r > 0› by linarith
    have [simp]: "cmod (of_real t - of_real s) = t-s"
      by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff)
    have "finite (part_circlepath z r s t -` {y} ∩ {0..1})" if "y ∈ k" for y
    proof -
      let ?w = "(y - z)/of_real r / exp(i * of_real s)"
      have fin: "finite (of_real -` {z. cmod z ≤ 1 ∧ exp (i * of_real (t - s) * z) = ?w})"
        using ‹s 🚫›
        by (intro finite_vimageI [OF finite_bounded_log2]) (auto simp: inj_of_real)
      show ?thesis
        unfolding part_circlepath_def linepath_def vimage_def
        using le
        by (intro finite_subset [OF _ fin]) (auto simp: algebra_simps scaleR_conv_of_real exp_add exp_diff)
    qed
    then have fin01: "finite ((part_circlepath z r s t) -` k ∩ {0..1})"
      by (rule finite_finite_vimage_IntI [OF ‹finite k›])
    have **: "((λx. if (part_circlepath z r s t x) ∈ k then 0
                    else f(part_circlepath z r s t x) *
                       vector_derivative (part_circlepath z r s t) (at x)) has_integral i) {0..1}"
      by (rule has_integral_spike [OF negligible_finite [OF fin01]])  (use fi has_contour_integral in auto)
    have *: "∧x. [0 ≤ x; x ≤ 1; part_circlepath z r s t x ∉ k] ==> cmod (f (part_circlepath z r s t x)) ≤ B"
      by (auto intro!: B [unfolded path_image_def image_def])
    show ?thesis
      using has_integral_bound [where 'a=real, simplified, OF _ **]
      using assms le * "2" ‹r > 0› by (auto simp add: norm_mult vector_derivative_part_circlepath)
  qed
qed

corollary contour_integral_bound_part_circlepath_strong:
  assumes "f contour_integrable_on part_circlepath z r s t"
      and "finite k" and "0 ≤ B" "0 < r" "s ≤ t"
      and "∧x. x ∈ path_image(part_circlepath z r s t) - k ==> norm(f x) ≤ B"
    shows "cmod (contour_integral (part_circlepath z r s t) f) ≤ B * r * (t - s)"
  using assms has_contour_integral_bound_part_circlepath_strong has_contour_integral_integral by blast

lemma has_contour_integral_bound_part_circlepath:
      "[(f has_contour_integral i) (part_circlepath z r s t);
        0 ≤ B; 0 < r; s ≤ t;
        ∧x. x ∈ path_image(part_circlepath z r s t) ==> norm(f x) ≤ B]
       ==> norm i ≤ B*r*(t - s)"
  by (auto intro: has_contour_integral_bound_part_circlepath_strong)

lemma contour_integrable_continuous_part_circlepath:
     "continuous_on (path_image (part_circlepath z r s t)) f
      ==> f contour_integrable_on (part_circlepath z r s t)"
  unfolding contour_integrable_on has_contour_integral_def vector_derivative_part_circlepath path_image_def
  by (best intro: integrable_continuous_real path_part_circlepath [unfolded path_def] continuous_intros 
      continuous_on_compose2 [where g=f, OF _ _ order_refl])

lemma simple_path_part_circlepath:
    "simple_path(part_circlepath z r s t) ⟷ (r ≠ 0 ∧ s ≠ t ∧ ∣s - t∣ ≤ 2*pi)"
proof (cases "r = 0 ∨ s = t")
  case True
  then show ?thesis
    unfolding part_circlepath_def simple_path_def loop_free_def
    by (rule disjE) (force intro: bexI [where x = "1/4"] bexI [where x = "1/3"])+
next
  case False then have "r ≠ 0" "s ≠ t" by auto
  have *: "∧x y z s t. i*((1 - x) * s + x * t) = i*(((1 - y) * s + y * t)) + z ⟷ i*(x - y) * (t - s) = z"
    by (simp add: algebra_simps)
  have abs01: "∧x y::real. 0 ≤ x ∧ x ≤ 1 ∧ 0 ≤ y ∧ y ≤ 1
                      ==> (x = y ∨ x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0 ⟷ ∣x - y∣ ∈ {0,1})"
    by auto
  have **: "∧x y. (∃n. (complex_of_real x - of_real y) * (of_real t - of_real s) = 2 * (of_int n * of_real pi)) ⟷
                  (∃n. ∣x - y∣ * (t - s) = 2 * (of_int n * pi))"
    by (force simp: algebra_simps abs_if dest: arg_cong [where f=Re] arg_cong [where f=complex_of_real]
                    intro: exI [where x = "-n" for n])
  have 1: "∣s - t∣ ≤ 2 * pi"
    if "∧x. 0 ≤ x ∧ x ≤ 1 ==> (∃n. x * (t - s) = 2 * (real_of_int n * pi)) ⟶ x = 0 ∨ x = 1"
  proof (rule ccontr)
    assume "¬ ∣s - t∣ ≤ 2 * pi"
    then have *: "∧n. t - s ≠ of_int n * ∣s - t∣"
      using False that [of "2*pi / ∣t - s∣"]
      by (simp add: abs_minus_commute divide_simps)
    show False
      using * [of 1] * [of "-1"] by auto
  qed
  have 2: "∣s - t∣ = ∣2 * (real_of_int n * pi) / x∣" if "x ≠ 0" "x * (t - s) = 2 * (real_of_int n * pi)" for x n
  proof -
    have "t-s = 2 * (real_of_int n * pi)/x"
      using that by (simp add: field_simps)
    then show ?thesis by (metis abs_minus_commute)
  qed
  have abs_away: "∧P. (∀x∈{0..1}. ∀y∈{0..1}. P ∣x - y∣) ⟷ (∀x::real. 0 ≤ x ∧ x ≤ 1 ⟶ P x)"
    by force
  have "∧x n. [s ≠ t; ∣s - t∣ ≤ 2 * pi; 0 ≤ x; x < 1;
            x * (t - s) = 2 * (real_of_int n * pi)]
           ==> x = 0"
    by (rule ccontr) (auto simp: 2 field_split_simps abs_mult dest: of_int_leD)
  then
  show ?thesis using False
    apply (simp add: simple_path_def loop_free_def)
    apply (simp add: part_circlepath_def linepath_def exp_eq  * ** abs01 del: Set.insert_iff)
    apply (subst abs_away)
    apply (auto simp: 1)
    done
qed

lemma arc_part_circlepath:
  assumes "r ≠ 0" "s ≠ t" "∣s - t∣ < 2*pi"
    shows "arc (part_circlepath z r s t)"
proof -
  have *: "x = y" if eq: "i * (linepath s t x) = i * (linepath s t y) + 2 * of_int n * of_real pi * i"
    and x: "x ∈ {0..1}" and y: "y ∈ {0..1}" for x y n
  proof (rule ccontr)
    assume "x ≠ y"
    have "(linepath s t x) = (linepath s t y) + 2 * of_int n * complex_of_real pi"
      by (metis add_divide_eq_iff complex_i_not_zero mult.commute nonzero_mult_div_cancel_left eq)
    then have "s*y + t*x = s*x + (t*y + of_int n * (pi * 2))"
      by (force simp: algebra_simps linepath_def dest: arg_cong [where f=Re])
    with ‹x ≠ y› have st: "s-t = (of_int n * (pi * 2) / (y-x))"
      by (force simp: field_simps)
    have "∣real_of_int n∣ < ∣y - x∣"
      using assms ‹x ≠ y› by (simp add: st abs_mult field_simps)
    then show False
      using assms x y st by (auto dest: of_int_lessD)
  qed
  then have "inj_on (part_circlepath z r s t) {0..1}"
    using assms by (force simp add: part_circlepath_def inj_on_def exp_eq)
  then show ?thesis
    by (simp add: arc_def)
qed

subsection‹Special case of one complete circle›

definition🍋‹tag important› circlepath :: "[complex, real, real] ==> complex"
  where "circlepath z r ≡ part_circlepath z r 0 (2*pi)"

lemma circlepath: "circlepath z r = (λx. z + r * exp(2 * of_real pi * i * of_real x))"
  by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps)

lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r"
  by (simp add: circlepath_def)

lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r"
  by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute)

lemma circlepath_minus: "circlepath z (-r) x = circlepath z r (x + 1/2)"
proof -
  have "z + of_real r * exp (2 * pi * i * (x + 1/2)) =
        z + of_real r * exp (2 * pi * i * x + pi * i)"
    by (simp add: divide_simps) (simp add: algebra_simps)
  also have "… = z - r * exp (2 * pi * i * x)"
    by (simp add: exp_add)
  finally show ?thesis
    by (simp add: circlepath path_image_def sphere_def dist_norm)
qed

lemma circlepath_add1: "circlepath z r (x+1) = circlepath z r x"
  using circlepath_minus [of z r "x+1/2"] circlepath_minus [of z "-r" x]
  by (simp add: add.commute)

lemma circlepath_add_half: "circlepath z r (x + 1/2) = circlepath z r (x - 1/2)"
  using circlepath_add1 [of z r "x-1/2"]
  by (simp add: add.commute)

lemma path_image_circlepath_minus_subset:
     "path_image (circlepath z (-r)) ⊆ path_image (circlepath z r)"
proof -
  have "∃x∈{0..1}. circlepath z r (y + 1/2) = circlepath z r x"
    if "0 ≤ y" "y ≤ 1" for y
  proof (cases "y ≤ 1/2")
    case False
    with that show ?thesis
      by (force simp: circlepath_add_half)
  qed (use that in force)
  then show ?thesis
    by (auto simp add: path_image_def image_def circlepath_minus)
qed

lemma path_image_circlepath_minus: "path_image (circlepath z (-r)) = path_image (circlepath z r)"
  using path_image_circlepath_minus_subset by fastforce

lemma has_vector_derivative_circlepath [derivative_intros]:
 "((circlepath z r) has_vector_derivative (2 * pi * i * r * exp (2 * of_real pi * i * x)))
   (at x within X)"
  unfolding circlepath_def scaleR_conv_of_real
  by (rule derivative_eq_intros) (simp add: algebra_simps)

lemma vector_derivative_circlepath:
  "vector_derivative (circlepath z r) (at x) =
    2 * pi * i * r * exp(2 * of_real pi * i * x)"
  using has_vector_derivative_circlepath vector_derivative_at by blast

lemma vector_derivative_circlepath01:
    "[0 ≤ x; x ≤ 1]
     ==> vector_derivative (circlepath z r) (at x within {0..1}) =
          2 * pi * i * r * exp(2 * of_real pi * i * x)"
  using has_vector_derivative_circlepath
  by (auto simp: vector_derivative_at_within_ivl)

lemma valid_path_circlepath [simp]: "valid_path (circlepath z r)"
  by (simp add: circlepath_def)

lemma path_circlepath [simp]: "path (circlepath z r)"
  by (simp add: valid_path_imp_path)

lemma path_image_circlepath_nonneg:
  assumes "0 ≤ r" shows "path_image (circlepath z r) = sphere z r"
proof -
  have *: "x ∈ (λu. z + (cmod (x - z)) * exp (i * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
  proof (cases "x = z")
    case True then show ?thesis by force
  next
    case False
    define w where "w = x - z"
    then have "w ≠ 0" by (simp add: False)
    have **: "∧t. [Re w = cos t * cmod w; Im w = sin t * cmod w] ==> w = of_real (cmod w) * exp (i * t)"
      using cis_conv_exp complex_eq_iff by auto
    obtain t where "0 ≤ t" "t < 2*pi" "Re(w/norm w) = cos t" "Im(w/norm w) = sin t"
      apply (rule sincos_total_2pi [of "Re(w/(norm w))" "Im(w/(norm w))"])
      by (auto simp add: divide_simps ‹w ≠ 0› cmod_power2 [symmetric])
    then
    show ?thesis
      using False ** w_def ‹w ≠ 0›
      by (rule_tac x="t / (2*pi)" in image_eqI) (auto simp add: field_simps)
  qed
  show ?thesis
    unfolding circlepath path_image_def sphere_def dist_norm
    by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *)
qed

lemma path_image_circlepath [simp]:
    "path_image (circlepath z r) = sphere z ∣r∣"
  using path_image_circlepath_minus
  by (force simp: path_image_circlepath_nonneg abs_if)

lemma has_contour_integral_bound_circlepath_strong:
      "[(f has_contour_integral i) (circlepath z r);
        finite k; 0 ≤ B; 0 < r;
        ∧x. [norm(x - z) = r; x ∉ k] ==> norm(f x) ≤ B]
        ==> norm i ≤ B*(2*pi*r)"
  unfolding circlepath_def
  by (auto simp: algebra_simps in_path_image_part_circlepath dest!: has_contour_integral_bound_part_circlepath_strong)

lemma has_contour_integral_bound_circlepath:
      "[(f has_contour_integral i) (circlepath z r);
        0 ≤ B; 0 < r; ∧x. norm(x - z) = r ==> norm(f x) ≤ B]
        ==> norm i ≤ B*(2*pi*r)"
  by (auto intro: has_contour_integral_bound_circlepath_strong)

lemma contour_integrable_continuous_circlepath:
    "continuous_on (path_image (circlepath z r)) f
     ==> f contour_integrable_on (circlepath z r)"
  by (simp add: circlepath_def contour_integrable_continuous_part_circlepath)

lemma simple_path_circlepath: "simple_path(circlepath z r) ⟷ (r ≠ 0)"
  by (simp add: circlepath_def simple_path_part_circlepath)

lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r ==> w ∉ path_image (circlepath z r)"
  by (simp add: sphere_def dist_norm norm_minus_commute)

lemma contour_integral_circlepath:
  assumes "r > 0"
  shows "contour_integral (circlepath z r) (λw. 1 / (w - z)) = 2 * of_real pi * i"
proof (rule contour_integral_unique)
  show "((λw. 1 / (w - z)) has_contour_integral 2 * of_real pi * i) (circlepath z r)"
    unfolding has_contour_integral_def using assms has_integral_const_real [of _ 0 1]
    apply (subst has_integral_cong)
     apply (simp add: vector_derivative_circlepath01)
    apply (force simp: circlepath)
    done
qed

subsection‹ Uniform convergence of path integral›

text‹Uniform convergence when the derivative of the path is bounded, and in particular for the special case of a circle.›

proposition contour_integral_uniform_limit:
  assumes ev_fint: "eventually (λn::'a. (f n) contour_integrable_on γ) F"
      and ul_f: "uniform_limit (path_image γ) f l F"
      and noleB: "∧t. t ∈ {0..1} ==> norm (vector_derivative γ (at t)) ≤ B"
      and γ: "valid_path γ"
      and [simp]: "¬ trivial_limit F"
  shows "l contour_integrable_on γ" "((λn. contour_integral γ (f n)) ---> contour_integral γ l) F"
proof -
  have "0 ≤ B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
  { fix e::real
    assume "0 < e"
    then have "0 < e / (∣B∣ + 1)" by simp
    then have 🍋: "∀🪙F n in F. ∀x∈path_image γ. cmod (f n x - l x) < e / (∣B∣ + 1)"
      using ul_f [unfolded uniform_limit_iff dist_norm] by auto
    obtain a where fga: "∧x. x ∈ {0..1} ==> cmod (f a (γ x) - l (γ x)) < e / (∣B∣ + 1)"
               and inta: "(λt. f a (γ t) * vector_derivative γ (at t)) integrable_on {0..1}"
      using eventually_happens [OF eventually_conj [OF ev_fint 🍋]]
      by (fastforce simp: contour_integrable_on path_image_def)
    have "∃h. (∀x∈{0..1}. cmod (l (γ x) * vector_derivative γ (at x) - h x) ≤ e) ∧ h integrable_on {0..1}"
    proof (intro exI conjI ballI)
      show "cmod (l (γ x) * vector_derivative γ (at x) - f a (γ x) * vector_derivative γ (at x)) ≤ e"
        if "x ∈ {0..1}" for x
      proof -
        have "cmod (l (γ x) * vector_derivative γ (at x) - f a (γ x) * vector_derivative γ (at x)) ≤ B * e / (∣B∣ + 1)"
          using noleB [OF that] fga [OF that] ‹0 ≤ B› ‹0 🚫›
          by (fastforce simp: mult_ac dest: mult_mono [OF less_imp_le] simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
        also have "… ≤ e"
          using ‹0 ≤ B›  ‹0 🚫› by (simp add: field_split_simps)
        finally show ?thesis .
      qed
    qed (rule inta)
  }
  then show lintg: "l contour_integrable_on γ"
    unfolding contour_integrable_on by (metis (mono_tags, lifting)integrable_uniform_limit_real)
  { fix e::real
    define B' where "B' = B + 1"
    have B': "B' > 0" "B' > B" using  ‹0 ≤ B› by (auto simp: B'_def)
    assume "0 < e"
    then have ev_no': "∀🪙F n in F. ∀x∈path_image γ. 2 * cmod (f n x - l x) < e / B'"
      using ul_f [unfolded uniform_limit_iff dist_norm, rule_format, of "e / B'/2"] B'
        by (simp add: field_simps)
    have ie: "integral {0..1::real} (λx. e/2) < e" using ‹0 🚫› by simp
    have *: "cmod (f x (γ t) * vector_derivative γ (at t) - l (γ t) * vector_derivative γ (at t)) ≤ e/2"
             if t: "t∈{0..1}" and leB': "2 * cmod (f x (γ t) - l (γ t)) < e / B'" for x t
    proof -
      have "2 * cmod (f x (γ t) - l (γ t)) * cmod (vector_derivative γ (at t)) ≤ e * (B/ B')"
        using mult_mono [OF less_imp_le [OF leB'] noleB] B' ‹0 🚫› t by auto
      also have "… < e"
        by (simp add: B' ‹0 🚫› mult_imp_div_pos_less)
      finally have "2 * cmod (f x (γ t) - l (γ t)) * cmod (vector_derivative γ (at t)) < e" .
      then show ?thesis
        by (simp add: left_diff_distrib [symmetric] norm_mult)
    qed
    have le_e: "∧x. [∀u∈{0..1}. 2 * cmod (f x (γ u) - l (γ u)) < e / B'; f x contour_integrable_on γ]
         ==> cmod (integral {0..1}
                    (λu. f x (γ u) * vector_derivative γ (at u) - l (γ u) * vector_derivative γ (at u))) < e"
      apply (rule le_less_trans [OF integral_norm_bound_integral ie])
        apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
       apply (blast intro: *)+
      done
    have "∀🪙F x in F. dist (contour_integral γ (f x)) (contour_integral γ l) < e"
      apply (rule eventually_mono [OF eventually_conj [OF ev_no' ev_fint]])
      apply (simp add: dist_norm contour_integrable_on path_image_def contour_integral_integral)
      apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric] le_e)
      done
  }
  then show "((λn. contour_integral γ (f n)) ---> contour_integral γ l) F"
    by (rule tendstoI)
qed

corollary🍋‹tag unimportant› contour_integral_uniform_limit_circlepath:
  assumes "∀🪙F n::'a in F. (f n) contour_integrable_on (circlepath z r)"
      and "uniform_limit (sphere z r) f l F"
      and "¬ trivial_limit F" "0 < r"
    shows "l contour_integrable_on (circlepath z r)"
          "((λn. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F"
  using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)

lemma has_contour_integral_linepath_same_Re_iff:
  assumes "Re z = c" "Re z' = c" "Im z = a" "Im z' = b" "a < b"
  shows   "(f has_contour_integral I) (linepath z z') ⟷
             ((λx. f (Complex c x)) has_integral (-i * I)) {a..b}"
proof -
  have "(f has_contour_integral I) (linepath z z') ⟷
          ((λx. f (linepath z z' x) * (z' - z)) has_integral I) {0..1}"
    by (subst has_contour_integral_linepath) simp_all
  also have "… ⟷ ((λx. f (c + (a + (b - a) * x) *🪙R i) * (i * (b - a))) has_integral I) {0..1}"
    using assms
    by (intro has_integral_cong arg_cong2[of _ _ _ _ "(*)"] arg_cong[of _ _ f])
       (auto simp: linepath_def complex_eq_iff algebra_simps)
  also have "{0..1} = (λx. x / (b - a)) ` {0..b-a}"
    using assms by simp
  also have "((λx. f (c + (a + (b-a) * x) *🪙R i) * (i * (b-a))) has_integral I) … ⟷
             ((λx. f (c + (a + x) *🪙R i) * (i * (b-a))) has_integral ((b-a) *🪙R I)) {0..b-a}"
    by (subst has_integral_stretch_real_iff) (use assms in simp_all)
  also have "… ⟷ ((λx. of_real (b-a) * i * (f (c + x *🪙R i))) has_integral (b-a) *🪙R I) {a..b}"
    by (subst has_integral_shift_real_ivl_iff[where c = "-a"])
       (simp_all add: scaleR_conv_of_real mult_ac)
  also have "… ⟷ ((λx. f (c + x *🪙R i)) has_integral (-i * I)) {a..b}"
    by (subst has_integral_mult_right_iff) (use assms in ‹auto simp: scaleR_conv_of_real›)
  finally show ?thesis
    by (simp add: scaleR_conv_of_real Complex_eq mult.commute)
qed

end