Theory HOL-Complex_Analysis.Cauchy_Integral_Theorem

section ‹Complex Path Integrals and Cauchy's Integral Theorem›

text‹By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)›

theory Cauchy_Integral_Theorem
imports
  "HOL-Analysis.Analysis"
  Contour_Integration
begin

lemma leibniz_rule_holomorphic:
  fixes f::"complex  'b::euclidean_space  complex"
  assumes "x t. x  U  t  cbox a b  ((λx. f x t) has_field_derivative fx x t) (at x within U)"
  assumes "x. x  U  (f x) integrable_on cbox a b"
  assumes "continuous_on (U × (cbox a b)) (λ(x, t). fx x t)"
  assumes "convex U"
  shows "(λx. integral (cbox a b) (f x)) holomorphic_on U"
  using leibniz_rule_field_differentiable[OF assms(1-3) _ assms(4)]
  by (auto simp: holomorphic_on_def)

lemma Ln_measurable [measurable]: "Ln  measurable borel borel"
proof -
  have *: "Ln (-of_real x) = of_real (ln x) + 𝗂 * pi" if "x > 0" for x
    using that by (subst Ln_minus) (auto simp: Ln_of_real)
  have **: "Ln (of_real x) = of_real (ln (-x)) + 𝗂 * pi" if "x < 0" for x
    using *[of "-x"] that by simp
  have cont: "(λx. indicat_real (- 0) x *R Ln x)  borel_measurable borel"
    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
  have "(λx. if x  0 then ln (-Re x) + 𝗂 * pi else indicator (-0) x *R Ln x)  borel M borel"
    (is "?f  _") by (rule measurable_If_set[OF _ cont]) auto
  hence "(λx. if x = 0 then Ln 0 else ?f x)  borel M borel" by measurable
  also have "(λx. if x = 0 then Ln 0 else ?f x) = Ln"
    by (auto simp: fun_eq_iff ** nonpos_Reals_def)
  finally show ?thesis .
qed

lemma powr_complex_measurable [measurable]:
  assumes [measurable]: "f  measurable M borel" "g  measurable M borel"
  shows   "(λx. f x powr g x :: complex)  measurable M borel"
  using assms by (simp add: powr_def) 

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

lemma has_contour_integral_midpoint:
  assumes "(f has_contour_integral i) (linepath a (midpoint a b))"
          "(f has_contour_integral j) (linepath (midpoint a b) b)"
    shows "(f has_contour_integral (i + j)) (linepath a b)"
proof (rule has_contour_integral_split)
  show "midpoint a b - a = (1/2) *R (b - a)"
  using assms by (auto simp: midpoint_def scaleR_conv_of_real)
qed (use assms in auto)

lemma contour_integral_midpoint:
  assumes "continuous_on (closed_segment a b) f"
  shows "contour_integral (linepath a b) f =
         contour_integral (linepath a (midpoint a b)) f + contour_integral (linepath (midpoint a b) b) f"
proof (rule contour_integral_split)
  show "midpoint a b - a = (1/2) *R (b - a)"
  using assms by (auto simp: midpoint_def scaleR_conv_of_real)
qed (use assms in auto)

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

lemma triangle_linear_has_chain_integral:
    "((λx. m*x + d) has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
proof (rule Cauchy_theorem_primitive)
  show "x. x  UNIV  ((λx. m / 2 * x2 + d * x) has_field_derivative m * x + d) (at x)"
    by (auto intro!: derivative_eq_intros)
qed auto

lemma has_chain_integral_chain_integral3:
  assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d)" 
           (is "(f has_contour_integral i) ?g")
  shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f = i"
       (is "?lhs = _")
proof -
  have "f contour_integrable_on ?g"
    using assms contour_integrable_on_def by blast
  then have "?lhs = contour_integral ?g f"
    by (simp add: valid_path_join has_contour_integral_integrable)
  then show ?thesis
    using assms contour_integral_unique by blast
qed

lemma has_chain_integral_chain_integral4:
  assumes "(f has_contour_integral i) (linepath a b +++ linepath b c +++ linepath c d +++ linepath d e)" 
           (is "(f has_contour_integral i) ?g")
  shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c d) f + contour_integral (linepath d e) f = i"
       (is "?lhs = _")
proof -
  have "f contour_integrable_on ?g"
    using assms contour_integrable_on_def by blast
  then have "?lhs = contour_integral ?g f"
    by (simp add: valid_path_join has_contour_integral_integrable)
  then show ?thesis
    using assms contour_integral_unique by blast
qed

subsectiontag unimportant› ‹The key quadrisection step›

lemma norm_sum_half:
  assumes "norm(a + b)  e"
    shows "norm a  e/2  norm b  e/2"
proof -
  have "e  norm (- a - b)"
    by (simp add: add.commute assms norm_minus_commute)
  thus ?thesis
    using norm_triangle_ineq4 order_trans by fastforce
qed

lemma norm_sum_lemma:
  assumes "e  norm (a + b + c + d)"
    shows "e / 4  norm a  e / 4  norm b  e / 4  norm c  e / 4  norm d"
proof -
  have "e  norm ((a + b) + (c + d))" using assms
    by (simp add: algebra_simps)
  then show ?thesis
    by (auto dest!: norm_sum_half)
qed

lemma Cauchy_theorem_quadrisection:
  assumes f: "continuous_on (convex hull {a,b,c}) f"
      and dist: "dist a b  K" "dist b c  K" "dist c a  K"
      and e: "e * K^2 
              norm (contour_integral(linepath a b) f + contour_integral(linepath b c) f + contour_integral(linepath c a) f)"
  shows "a' b' c'.
           a'  convex hull {a,b,c}  b'  convex hull {a,b,c}  c'  convex hull {a,b,c} 
           dist a' b'  K/2    dist b' c'  K/2    dist c' a'  K/2  
           e * (K/2)^2  norm(contour_integral(linepath a' b') f + contour_integral(linepath b' c') f + contour_integral(linepath c' a') f)"
         (is "x y z.  x y z")
proof -
  note divide_le_eq_numeral1 [simp del]
  define a' where "a' = midpoint b c"
  define b' where "b' = midpoint c a"
  define c' where "c' = midpoint a b"
  have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
    using f continuous_on_subset segments_subset_convex_hull by metis+
  have fcont': "continuous_on (closed_segment c' b') f"
               "continuous_on (closed_segment a' c') f"
               "continuous_on (closed_segment b' a') f"
    unfolding a'_def b'_def c'_def
    by (rule continuous_on_subset [OF f],
           metis midpoints_in_convex_hull convex_hull_subset hull_subset insert_subset segment_convex_hull)+
  define pathint where "pathint x y  contour_integral(linepath x y) f" for x y
  have *: "pathint a b + pathint b c + pathint c a =
          (pathint a c' + pathint c' b' + pathint b' a) +
          (pathint a' c' + pathint c' b + pathint b a') +
          (pathint a' c + pathint c b' + pathint b' a') +
          (pathint a' b' + pathint b' c' + pathint c' a')"
    unfolding pathint_def
    by (simp add: fcont' contour_integral_reverse_linepath) (simp add: a'_def b'_def c'_def contour_integral_midpoint fabc)
  have [simp]: "x y. cmod (x * 2 - y * 2) = cmod (x - y) * 2"
    by (metis left_diff_distrib mult.commute norm_mult_numeral1)
  have [simp]: "x y. cmod (x - y) = cmod (y - x)"
    by (simp add: norm_minus_commute)
  consider "e * K2 / 4  cmod (pathint a c' + pathint c' b' + pathint b' a)" |
           "e * K2 / 4  cmod (pathint a' c' + pathint c' b + pathint b a')" |
           "e * K2 / 4  cmod (pathint a' c + pathint c b' + pathint b' a')" |
           "e * K2 / 4  cmod (pathint a' b' + pathint b' c' + pathint c' a')"
    using assms by (metis "*" norm_sum_lemma pathint_def)
  then show ?thesis
  proof cases
    case 1 then have " a c' b'"
      using assms unfolding pathint_def [symmetric]
      apply (clarsimp simp: c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD])
      apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps)
      done
    then show ?thesis by blast
  next
    case 2 then  have " a' c' b"
      using assms unfolding pathint_def [symmetric]
      apply (clarsimp simp: a'_def c'_def midpoints_in_convex_hull hull_subset [THEN subsetD])
      apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps)
      done
    then show ?thesis by blast
  next
    case 3 then have " a' c b'"
      using assms unfolding pathint_def [symmetric]
      apply (clarsimp simp: a'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD])
      apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps)
      done
    then show ?thesis by blast
  next
    case 4 then have " a' b' c'"
      using assms unfolding pathint_def [symmetric]
      apply (clarsimp simp: a'_def c'_def b'_def midpoints_in_convex_hull hull_subset [THEN subsetD])
      apply (auto simp: midpoint_def dist_norm scaleR_conv_of_real field_split_simps)
      done
    then show ?thesis by blast
  qed
qed

subsectiontag unimportant› ‹Cauchy's theorem for triangles›

lemma triangle_points_closer:
  fixes a::complex
  shows "x  convex hull {a,b,c};  y  convex hull {a,b,c}
          norm(x - y)  norm(a - b) 
             norm(x - y)  norm(b - c) 
             norm(x - y)  norm(c - a)"
  using simplex_extremal_le [of "{a,b,c}"]
  by (auto simp: norm_minus_commute)


lemma holomorphic_point_small_triangle:
  assumes x: "x  S"
      and f: "continuous_on S f"
      and cd: "f field_differentiable (at x within S)"
      and e: "0 < e"
    shows "k>0. a b c. dist a b  k  dist b c  k  dist c a  k 
              x  convex hull {a,b,c}  convex hull {a,b,c}  S
               norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f +
                       contour_integral(linepath c a) f)
                   e*(dist a b + dist b c + dist c a)^2"
           (is "k>0. a b c. _  ?normle a b c")
proof -
  have le_of_3: "a x y z. 0  x*y; 0  x*z; 0  y*z; a  (e*(x + y + z))*x + (e*(x + y + z))*y + (e*(x + y + z))*z
                      a  e*(x + y + z)^2"
    by (simp add: algebra_simps power2_eq_square)
  have disj_le: "x  a  x  b  x  c; 0  a; 0  b; 0  c  x  a + b + c"
             for x::real and a b c
    by linarith
  have fabc: "f contour_integrable_on linepath a b" "f contour_integrable_on linepath b c" "f contour_integrable_on linepath c a"
              if "convex hull {a, b, c}  S" for a b c
    using segments_subset_convex_hull that
    by (metis continuous_on_subset f contour_integrable_continuous_linepath)+
  note path_bound = has_contour_integral_bound_linepath [simplified norm_minus_commute, OF has_contour_integral_integral]
  { fix f' a b c d
    assume d: "0 < d"
       and f': "y. cmod (y - x)  d; y  S  cmod (f y - f x - f' * (y - x))  e * cmod (y - x)"
       and le: "cmod (a - b)  d" "cmod (b - c)  d" "cmod (c - a)  d"
       and xc: "x  convex hull {a, b, c}"
       and S: "convex hull {a, b, c}  S"
    have pa: "contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f =
              contour_integral (linepath a b) (λy. f y - f x - f' * (y-x)) +
              contour_integral (linepath b c) (λy. f y - f x - f' * (y-x)) +
              contour_integral (linepath c a) (λy. f y - f x - f' * (y-x))"
      apply (simp add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc [OF S])
      apply (simp add: field_simps)
      done
    { fix y
      assume yc: "y  convex hull {a,b,c}"
      have "cmod (f y - f x - f' * (y - x))  e*norm(y - x)"
      proof (rule f')
        show "cmod (y - x)  d"
          by (metis triangle_points_closer [OF xc yc] le norm_minus_commute order_trans)
      qed (use S yc in blast)
      also have "  e * (cmod (a - b) + cmod (b - c) + cmod (c - a))"
        by (simp add: yc e xc disj_le [OF triangle_points_closer])
      finally have "cmod (f y - f x - f' * (y - x))  e * (cmod (a - b) + cmod (b - c) + cmod (c - a))" .
    } note cm_le = this
    have "?normle a b c"
      unfolding dist_norm pa
      using f' xc S e
      apply (intro le_of_3 norm_triangle_le add_mono path_bound)
      apply (simp_all add: contour_integral_diff contour_integral_lmul contour_integrable_lmul contour_integrable_diff fabc)
      apply (blast intro: cm_le elim: dest: segments_subset_convex_hull [THEN subsetD])+
      done
  } note * = this
  show ?thesis
    using cd e
    apply (simp add: field_differentiable_def has_field_derivative_def has_derivative_within_alt approachable_lt_le2 Ball_def)
    apply (clarify dest!: spec mp)
    using * unfolding dist_norm
    apply blast
    done
qed


text‹Hence the most basic theorem for a triangle.›

locale Chain =
  fixes x0 At Follows
  assumes At0: "At x0 0"
      and AtSuc: "x n. At x n  x'. At x' (Suc n)  Follows x' x"
begin
  primrec f where
    "f 0 = x0"
  | "f (Suc n) = (SOME x. At x (Suc n)  Follows x (f n))"

  lemma At: "At (f n) n"
  proof (induct n)
    case 0 show ?case
      by (simp add: At0)
  next
    case (Suc n) show ?case
      by (metis (no_types, lifting) AtSuc [OF Suc] f.simps(2) someI_ex)
  qed

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

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

lemma Chain3:
  assumes At0: "At x0 y0 z0 0"
      and AtSuc: "x y z n. At x y z n  x' y' z'. At x' y' z' (Suc n)  Follows x' y' z' x y z"
  obtains f g h where
    "f 0 = x0" "g 0 = y0" "h 0 = z0"
                      "n. At (f n) (g n) (h n) n"
                       "n. Follows (f(Suc n)) (g(Suc n)) (h(Suc n)) (f n) (g n) (h n)"
proof -
  interpret three: Chain "(x0,y0,z0)" "λ(x,y,z). At x y z" "λ(x',y',z'). λ(x,y,z). Follows x' y' z' x y z"
  proof qed (use At0 AtSuc in auto)
  show ?thesis
  proof
    show "n. Follows (fst (three.f (Suc n))) (fst (snd (three.f (Suc n))))
                      (snd (snd (three.f (Suc n)))) (fst (three.f n))
                     (fst (snd (three.f n))) (snd (snd (three.f n)))"
         "n. At (fst (three.f n)) (fst (snd (three.f n))) (snd (snd (three.f n))) n"
      using three.At three.Follows
      by (simp_all add: split_beta')
  qed auto
qed


propositiontag unimportant› Cauchy_theorem_triangle:
  assumes "f holomorphic_on (convex hull {a,b,c})"
    shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
proof -
  have contf: "continuous_on (convex hull {a,b,c}) f"
    by (metis assms holomorphic_on_imp_continuous_on)
  let ?pathint = "λx y. contour_integral(linepath x y) f"
  { fix y::complex
    assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
       and ynz: "y  0"
    define K where "K = 1 + max (dist a b) (max (dist b c) (dist c a))"
    define e where "e = norm y / K^2"
    have K1: "K  1"  by (simp add: K_def max.coboundedI1)
    then have K: "K > 0" by linarith
    have [iff]: "dist a b  K" "dist b c  K" "dist c a  K"
      by (simp_all add: K_def)
    have e: "e > 0"
      unfolding e_def using ynz K1 by simp
    define At where "At x y z n 
        convex hull {x,y,z}  convex hull {a,b,c} 
        dist x y  K/2^n  dist y z  K/2^n  dist z x  K/2^n 
        norm(?pathint x y + ?pathint y z + ?pathint z x)  e*(K/2^n)^2"
      for x y z n
    have At0: "At a b c 0"
      using fy
      by (simp add: At_def e_def has_chain_integral_chain_integral3)
    { fix x y z n
      assume At: "At x y z n"
      then have contf': "continuous_on (convex hull {x,y,z}) f"
        using contf At_def continuous_on_subset by metis
      have "x' y' z'. At x' y' z' (Suc n)  convex hull {x',y',z'}  convex hull {x,y,z}"
        using At Cauchy_theorem_quadrisection [OF contf', of "K/2^n" e]
        apply (simp add: At_def algebra_simps)
        apply (meson convex_hull_subset empty_subsetI insert_subset subsetCE)
        done
    } note AtSuc = this
    obtain fa fb fc
      where f0 [simp]: "fa 0 = a" "fb 0 = b" "fc 0 = c"
        and cosb: "n. convex hull {fa n, fb n, fc n}  convex hull {a,b,c}"
        and dist: "n. dist (fa n) (fb n)  K/2^n"
                  "n. dist (fb n) (fc n)  K/2^n"
                  "n. dist (fc n) (fa n)  K/2^n"
        and no: "n. norm(?pathint (fa n) (fb n) +
                           ?pathint (fb n) (fc n) +
                           ?pathint (fc n) (fa n))  e * (K/2^n)^2"
        and conv_le: "n. convex hull {fa(Suc n), fb(Suc n), fc(Suc n)}  convex hull {fa n, fb n, fc n}"
      by (rule Chain3 [of At, OF At0 AtSuc]) (auto simp: At_def)
    obtain x where x: "n. x  convex hull {fa n, fb n, fc n}"
    proof (rule bounded_closed_nest)
      show "n. closed (convex hull {fa n, fb n, fc n})"
        by (simp add: compact_imp_closed finite_imp_compact_convex_hull)
      show "m n. m  n  convex hull {fa n, fb n, fc n}  convex hull {fa m, fb m, fc m}"
        by (erule transitive_stepwise_le) (auto simp: conv_le)
    qed (fastforce intro: finite_imp_bounded_convex_hull)+
    then have xin: "x  convex hull {a,b,c}"
      using assms f0 by blast
    then have fx: "f field_differentiable at x within (convex hull {a,b,c})"
      using assms holomorphic_on_def by blast
    { fix k n
      assume k: "0 < k"
         and le:
            "x' y' z'.
               dist x' y'  k; dist y' z'  k; dist z' x'  k;
                x  convex hull {x',y',z'};
                convex hull {x',y',z'}  convex hull {a,b,c}
               
               cmod (?pathint x' y' + ?pathint y' z' + ?pathint z' x') * 10
                      e * (dist x' y' + dist y' z' + dist z' x')2"
         and Kk: "K / k < 2 ^ n"
      have "K / 2 ^ n < k" using Kk k
        by (auto simp: field_simps)
      then have DD: "dist (fa n) (fb n)  k" "dist (fb n) (fc n)  k" "dist (fc n) (fa n)  k"
        using dist [of n]  k
        by linarith+
      have dle: "(dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))2
                (3 * K / 2 ^ n)2"
        using dist [of n] e K
        by (simp add: abs_le_square_iff [symmetric])
      have less10: "x y::real. 0 < x  y  9*x  y < x*10"
        by linarith
      have "e * (dist (fa n) (fb n) + dist (fb n) (fc n) + dist (fc n) (fa n))2  e * (3 * K / 2 ^ n)2"
        using ynz dle e mult_le_cancel_left_pos by blast
      also have " <
          cmod (?pathint (fa n) (fb n) + ?pathint (fb n) (fc n) + ?pathint (fc n) (fa n)) * 10"
        using no [of n] e K
        by (simp add: e_def field_simps) (simp only: zero_less_norm_iff [symmetric])
      finally have False
        using le [OF DD x cosb] by auto
    } then
    have ?thesis
      using holomorphic_point_small_triangle [OF xin contf fx, of "e/10"] e
      apply clarsimp
      apply (rule_tac y1="K/k" in exE [OF real_arch_pow[of 2]], force+)
      done
  }
  moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
    by simp (meson contf continuous_on_subset contour_integrable_continuous_linepath segments_subset_convex_hull(1)
                   segments_subset_convex_hull(3) segments_subset_convex_hull(5))
  ultimately show ?thesis
    using has_contour_integral_integral by fastforce
qed

subsectiontag unimportant› ‹Version needing function holomorphic in interior only›

lemma Cauchy_theorem_flat_lemma:
  assumes f: "continuous_on (convex hull {a,b,c}) f"
      and c: "c - a = k *R (b - a)"
      and k: "0  k"
    shows "contour_integral (linepath a b) f + contour_integral (linepath b c) f +
          contour_integral (linepath c a) f = 0"
proof -
  have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
    using f continuous_on_subset segments_subset_convex_hull by metis+
  show ?thesis
  proof (cases "k  1")
    case True show ?thesis
      by (simp add: contour_integral_split [OF fabc(1) k True c] contour_integral_reverse_linepath fabc)
  next
    case False
    show ?thesis
    proof (subst contour_integral_split [symmetric])
      show "b - a = (1/k) *R (c - a)"
        using False c by force
      show "contour_integral (linepath a c) f + contour_integral (linepath c a) f = 0"
        by (simp add: contour_integral_reverse_linepath fabc(3))
      show "continuous_on (closed_segment a c) f"
        by (metis closed_segment_commute fabc(3))
    qed (use False in auto)
  qed
qed

lemma Cauchy_theorem_flat:
  assumes f: "continuous_on (convex hull {a,b,c}) f"
      and c: "c - a = k *R (b - a)"
    shows "contour_integral (linepath a b) f +
           contour_integral (linepath b c) f +
           contour_integral (linepath c a) f = 0"
proof (cases "0  k")
  case True with assms show ?thesis
    by (blast intro: Cauchy_theorem_flat_lemma)
next
  case False
  have "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
    using f continuous_on_subset segments_subset_convex_hull by metis+
  moreover have "contour_integral (linepath b a) f + contour_integral (linepath a c) f +
                 contour_integral (linepath c b) f = 0"
  proof (rule Cauchy_theorem_flat_lemma [of b a c f "1-k"])
    show "continuous_on (convex hull {b, a, c}) f"
      by (simp add: f insert_commute)
    show "c - b = (1 - k) *R (a - b)"
      using c by (auto simp: algebra_simps)
  qed (use False in auto)
  ultimately show ?thesis
    by (metis (no_types, lifting) contour_integral_reverse_linepath eq_neg_iff_add_eq_0 minus_add_cancel)
qed


proposition Cauchy_theorem_triangle_interior:
  assumes contf: "continuous_on (convex hull {a,b,c}) f"
      and holf:  "f holomorphic_on interior (convex hull {a,b,c})"
     shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
proof -
  define pathint where "pathint  λx y. contour_integral(linepath x y) f"
  have fabc: "continuous_on (closed_segment a b) f" "continuous_on (closed_segment b c) f" "continuous_on (closed_segment c a) f"
    using contf continuous_on_subset segments_subset_convex_hull by metis+
  have "bounded (f ` (convex hull {a,b,c}))"
    by (simp add: compact_continuous_image compact_convex_hull compact_imp_bounded contf)
  then obtain B where "0 < B" and Bnf: "x. x  convex hull {a,b,c}  norm (f x)  B"
     by (auto simp: dest!: bounded_pos [THEN iffD1])
  have "bounded (convex hull {a,b,c})"
    by (simp add: bounded_convex_hull)
  then obtain C where C: "0 < C" and Cno: "y. y  convex hull {a,b,c}  norm y < C"
    using bounded_pos_less by blast
  then have diff_2C: "norm(x - y)  2*C"
           if x: "x  convex hull {a, b, c}" and y: "y  convex hull {a, b, c}" for x y
  proof -
    have "cmod x  C"
      using x by (meson Cno not_le not_less_iff_gr_or_eq)
    hence "cmod (x - y)  C + C"
      using y by (meson Cno add_mono_thms_linordered_field(4) less_eq_real_def norm_triangle_ineq4 order_trans)
    thus "cmod (x - y)  2 * C"
      by (metis mult_2)
  qed
  have contf': "continuous_on (convex hull {b,a,c}) f"
    using contf by (simp add: insert_commute)
  { fix y::complex
    assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
       and ynz: "y  0"
    have pi_eq_y: "pathint a b + pathint b c + pathint c a= y"
      unfolding pathint_def by (rule has_chain_integral_chain_integral3 [OF fy])
    have ?thesis
    proof (cases "c=a  a=b  b=c")
      case True then show ?thesis
        using Cauchy_theorem_flat [OF contf, of 0]
        using has_chain_integral_chain_integral3 [OF fy] ynz
        by (force simp: fabc contour_integral_reverse_linepath)
    next
      case False
      then have car3: "card {a, b, c} = Suc (DIM(complex))"
        by auto
      { assume "interior(convex hull {a,b,c}) = {}"
        then have "collinear{a,b,c}"
          using interior_convex_hull_eq_empty [OF car3]
          by (simp add: collinear_3_eq_affine_dependent)
        with False obtain d where "c  a" "a  b" "b  c" "c - b = d *R (a - b)"
          by (auto simp: collinear_3 collinear_lemma)
        then have "False"
          using False Cauchy_theorem_flat [OF contf'] pi_eq_y ynz
          by (simp add: fabc add_eq_0_iff contour_integral_reverse_linepath pathint_def)
      }
      then obtain d where d: "d  interior (convex hull {a, b, c})"
        by blast
      { fix d1
        assume d1_pos: "0 < d1"
           and d1: "x x'. xconvex hull {a, b, c}; x'convex hull {a, b, c}; cmod (x' - x) < d1
                            cmod (f x' - f x) < cmod y / (24 * C)"
        define e where "e = min 1 (min (d1/(4*C)) ((norm y / 24 / C) / B))"
        define shrink where "shrink x = x - e *R (x - d)" for x
        have e: "0 < e" "e  1" "e  d1 / (4 * C)" "e  cmod y / 24 / C / B"
          using d1_pos C>0 B>0 ynz by (simp_all add: e_def)
        have e_le_d1: "e * (4 * C)  d1"
          using e C>0 by (simp add: field_simps)
        have "shrink a  interior(convex hull {a,b,c})"
             "shrink b  interior(convex hull {a,b,c})"
             "shrink c  interior(convex hull {a,b,c})"
          using d e by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
        then have fhp0: "(f has_contour_integral 0)
                (linepath (shrink a) (shrink b) +++ linepath (shrink b) (shrink c) +++ linepath (shrink c) (shrink a))"
          by (simp add: Cauchy_theorem_triangle holomorphic_on_subset [OF holf] hull_minimal)
        then have f_0_shrink: "pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a) = 0"
          by (simp add: has_chain_integral_chain_integral3 pathint_def)
        have fpi_abc: "f contour_integrable_on linepath (shrink a) (shrink b)"
                      "f contour_integrable_on linepath (shrink b) (shrink c)"
                      "f contour_integrable_on linepath (shrink c) (shrink a)"
          using fhp0  by (auto simp: valid_path_join dest: has_contour_integral_integrable)
        have cmod_shr: "x y. cmod (shrink y - shrink x - (y - x)) = e * cmod (x - y)"
          using e by (simp add: shrink_def real_vector.scale_right_diff_distrib [symmetric])
        have sh_eq: "a b d::complex. (b - e *R (b - d)) - (a - e *R (a - d)) - (b - a) = e *R (a - b)"
          by (simp add: algebra_simps)
        have "cmod y / (24 * C)  cmod y / cmod (b - a) / 12"
          using False C>0 diff_2C [of b a] ynz
          by (auto simp: field_split_simps hull_inc)
        have less_C: "x * cmod u < C" if "u  convex hull {a,b,c}" "0  x" "x  1" for x u
        proof (cases "x=0")
          case False
          with that show ?thesis
            using Cno [of u] mult_left_le_one_le [of "cmod u" x] le_less_trans norm_ge_zero by blast
        qed (simp add: 0<C)
        { fix u v
          assume uv: "u  convex hull {a, b, c}" "v  convex hull {a, b, c}" "uv"
             and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)"
          have shr_uv: "shrink u  interior(convex hull {a,b,c})"
                       "shrink v  interior(convex hull {a,b,c})"
            using d e uv
            by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
          have cmod_fuv: "x. 0x  x1  cmod (f (linepath (shrink u) (shrink v) x))  B"
            using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
          { fix x::real   assume x: "0x" "x1"
            have "¦1 - x¦ * cmod u < C" "¦x¦ * cmod v < C"
              using uv x by (auto intro!: less_C)
            moreover have  "¦x¦ * cmod d < C" "¦1 - x¦ * cmod d < C"
              using x d interior_subset by (auto intro!: less_C)
            ultimately
            have cmod_less_4C: "cmod ((1 - x) *R u - (1 - x) *R d) + cmod (x *R v - x *R d) < (C+C) + (C+C)"
              by (metis add_strict_mono le_less_trans norm_scaleR norm_triangle_ineq4)
            have ll: "linepath (shrink u) (shrink v) x - linepath u v x = -e * ((1 - x) *R (u - d) + x *R (v - d))"
              by (simp add: linepath_def shrink_def algebra_simps scaleR_conv_of_real)
            have cmod_less_dt: "cmod (linepath (shrink u) (shrink v) x - linepath u v x) < d1"
              unfolding ll norm_mult scaleR_diff_right
              using e>0 cmod_less_4C by (force intro: norm_triangle_lt less_le_trans [OF _ e_le_d1])
            have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) +
                          cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x))
                           B * (cmod y / 24 / C / B * 2 * C) + 2 * C * (cmod y / 24 / C)"
            proof (intro add_mono [OF mult_mono])
              show "cmod (f (linepath (shrink u) (shrink v) x))  B"
                using cmod_fuv x by blast
              have "B * (12 * (e * cmod (u - v)))  24 * e * C * B"
                using e B>0 diff_2C [of u v] uv by (auto simp: field_simps)
              also have "  cmod y"
                using C>0 B>0 e by (simp add: field_simps)
              finally show "cmod (shrink v - shrink u - (v - u))  cmod y / 24 / C / B * 2 * C"
                using 0 < B 0 < C by (simp add: cmod_shr mult_ac divide_simps)
              have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x)) < cmod y / (24 * C)"
                using x uv shr_uv cmod_less_dt
                by (auto simp: hull_inc intro: d1 interior_subset [THEN subsetD] linepath_in_convex_hull)
              also have "  cmod y / cmod (v - u) / 12"
                using False uv C>0 diff_2C [of v u] ynz
                by (auto simp: field_split_simps hull_inc)
              finally have "cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x))  cmod y / cmod (v - u) / 12"
                by simp
              then show "cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x))
                        2 * C * (cmod y / 24 / C)"
                using uv C  by (simp add: field_simps)
            qed (use 0 < B in auto)
            also have "  cmod y / 6"
              by simp
            finally have "cmod (f (linepath (shrink u) (shrink v) x)) * cmod (shrink v - shrink u - (v - u)) +
                          cmod (v - u) * cmod (f (linepath (shrink u) (shrink v) x) - f (linepath u v x))
                           cmod y / 6" .
          } note cmod_diff_le = this
          have f_uv: "continuous_on (closed_segment u v) f"
            by (blast intro: uv continuous_on_subset [OF contf closed_segment_subset_convex_hull])
          have **: "f' x' f x::complex. f'*x' - f*x = f' * (x' - x) + x * (f' - f)"
            by (simp add: algebra_simps)
          have "norm (pathint (shrink u) (shrink v) - pathint u v)
                 (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * content (cbox 0 (1::real))"
            apply (rule has_integral_bound
                    [of _ "λx. f(linepath (shrink u) (shrink v) x) * (shrink v - shrink u) - f(linepath u v x)*(v - u)"
                        _ 0 1])
            using ynz 0 < B 0 < C
            apply (simp_all add: pathint_def has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral
                fpi_uv f_uv contour_integrable_continuous_linepath del: le_divide_eq_numeral1)
            apply (auto simp: ** norm_triangle_le norm_mult cmod_diff_le simp del: le_divide_eq_numeral1)
            done
          also have "  norm y / 6"
            by simp
          finally have "norm (pathint (shrink u) (shrink v) - pathint u v)  norm y / 6" .
          } note * = this
          have "norm (pathint (shrink a) (shrink b) - pathint a b)  norm y / 6"
            using False fpi_abc by (rule_tac *) (auto simp: hull_inc)
          moreover
          have "norm (pathint (shrink b) (shrink c) - pathint b c)  norm y / 6"
            using False fpi_abc by (rule_tac *) (auto simp: hull_inc)
          moreover
          have "norm (pathint (shrink c) (shrink a) - pathint c a)  norm y / 6"
            using False fpi_abc by (rule_tac *) (auto simp: hull_inc)
          ultimately
          have "norm((pathint (shrink a) (shrink b) - pathint a b) +
                     (pathint (shrink b) (shrink c) - pathint b c) + (pathint (shrink c) (shrink a) - pathint c a))
                 norm y / 6 + norm y / 6 + norm y / 6"
            by (metis norm_triangle_le add_mono)
          also have " = norm y / 2"
            by simp
          finally have "norm((pathint (shrink a) (shrink b) + pathint (shrink b) (shrink c) + pathint (shrink c) (shrink a)) -
                          (pathint a b + pathint b c + pathint c a))
                 norm y / 2"
            by (simp add: algebra_simps)
          then
          have "norm(pathint a b + pathint b c + pathint c a)  norm y / 2"
            by (simp add: f_0_shrink) (metis (mono_tags) add.commute minus_add_distrib norm_minus_cancel uminus_add_conv_diff)
          then have "False"
            using pi_eq_y ynz by auto
        }
        note * = this
        have "uniformly_continuous_on (convex hull {a,b,c}) f"
          by (simp add: contf compact_convex_hull compact_uniformly_continuous)
        moreover have "norm y / (24 * C) > 0"
          using ynz C > 0 by auto
        ultimately obtain δ where "δ > 0" and
          "xconvex hull {a, b, c}. x'convex hull {a, b, c}.
             dist x' x < δ  dist (f x') (f x) < cmod y / (24 * C)"
          using C > 0 ynz unfolding uniformly_continuous_on_def dist_norm by blast
        hence False using *[of δ] by (auto simp: dist_norm)
        then show ?thesis ..
      qed
  }
  moreover have "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
    using fabc contour_integrable_continuous_linepath by auto
  ultimately show ?thesis
    using has_contour_integral_integral by fastforce
qed

subsectiontag unimportant› ‹Version allowing finite number of exceptional points›

propositiontag unimportant› Cauchy_theorem_triangle_cofinite:
  assumes "continuous_on (convex hull {a,b,c}) f"
      and "finite S"
      and "(x. x  interior(convex hull {a,b,c}) - S  f field_differentiable (at x))"
     shows "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
using assms
proof (induction "card S" arbitrary: a b c S rule: less_induct)
  case (less S a b c)
  show ?case
  proof (cases "S={}")
    case True with less show ?thesis
      by (fastforce simp: holomorphic_on_def field_differentiable_at_within Cauchy_theorem_triangle_interior)
  next
    case False
    then obtain d S' where d: "S = insert d S'" "d  S'"
      by (meson Set.set_insert all_not_in_conv)
    then show ?thesis
    proof (cases "d  convex hull {a,b,c}")
      case False
      show "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
      proof (rule less.hyps)
        show "x. x  interior (convex hull {a, b, c}) - S'  f field_differentiable at x"
        using False d interior_subset by (auto intro!: less.prems)
    qed (use d less.prems in auto)
    next
      case True
      have *: "convex hull {a, b, d}  convex hull {a, b, c}"
        by (meson True hull_subset insert_subset convex_hull_subset)
      have abd: "(f has_contour_integral 0) (linepath a b +++ linepath b d +++ linepath d a)"
      proof (rule less.hyps)
        show "x. x  interior (convex hull {a, b, d}) - S'  f field_differentiable at x"
          using d not_in_interior_convex_hull_3
          by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono)
      qed (use d continuous_on_subset [OF  _ *] less.prems in auto)
      have *: "convex hull {b, c, d}  convex hull {a, b, c}"
        by (meson True hull_subset insert_subset convex_hull_subset)
      have bcd: "(f has_contour_integral 0) (linepath b c +++ linepath c d +++ linepath d b)"
      proof (rule less.hyps)
        show "x. x  interior (convex hull {b, c, d}) - S'  f field_differentiable at x"
          using d not_in_interior_convex_hull_3
          by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono)
      qed (use d continuous_on_subset [OF  _ *] less.prems in auto)
      have *: "convex hull {c, a, d}  convex hull {a, b, c}"
        by (meson True hull_subset insert_subset convex_hull_subset)
      have cad: "(f has_contour_integral 0) (linepath c a +++ linepath a d +++ linepath d c)"
      proof (rule less.hyps)
        show "x. x  interior (convex hull {c, a, d}) - S'  f field_differentiable at x"
          using d not_in_interior_convex_hull_3
          by (clarsimp intro!: less.prems) (metis * insert_absorb insert_subset interior_mono)
      qed (use d continuous_on_subset [OF  _ *] less.prems in auto)
      have "f contour_integrable_on linepath a b"
        using less.prems abd contour_integrable_joinD1 contour_integrable_on_def by blast
      moreover have "f contour_integrable_on linepath b c"
        using less.prems bcd contour_integrable_joinD1 contour_integrable_on_def by blast
      moreover have "f contour_integrable_on linepath c a"
        using less.prems cad contour_integrable_joinD1 contour_integrable_on_def by blast
      ultimately have fpi: "f contour_integrable_on (linepath a b +++ linepath b c +++ linepath c a)"
        by auto
      { fix y::complex
        assume fy: "(f has_contour_integral y) (linepath a b +++ linepath b c +++ linepath c a)"
           and ynz: "y  0"
        have cont_ad: "continuous_on (closed_segment a d) f"
          by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(3))
        have cont_bd: "continuous_on (closed_segment b d) f"
          by (meson True closed_segment_subset_convex_hull continuous_on_subset hull_subset insert_subset less.prems(1))
        have cont_cd: "continuous_on (closed_segment c d) f"
          by (meson "*" continuous_on_subset less.prems(1) segments_subset_convex_hull(2))
        have "contour_integral  (linepath a b) f = - (contour_integral (linepath b d) f + (contour_integral (linepath d a) f))"
             "contour_integral  (linepath b c) f = - (contour_integral (linepath c d) f + (contour_integral (linepath d b) f))"
             "contour_integral  (linepath c a) f = - (contour_integral (linepath a d) f + contour_integral (linepath d c) f)"
            using has_chain_integral_chain_integral3 [OF abd]
                  has_chain_integral_chain_integral3 [OF bcd]
                  has_chain_integral_chain_integral3 [OF cad]
            by (simp_all add: algebra_simps add_eq_0_iff)
        then have ?thesis
          using cont_ad cont_bd cont_cd fy has_chain_integral_chain_integral3 contour_integral_reverse_linepath by fastforce
      }
      then show ?thesis
        using fpi contour_integrable_on_def by blast
    qed
  qed
qed

subsectiontag unimportant› ‹Cauchy's theorem for an open starlike set›

lemma starlike_convex_subset:
  assumes S: "a  S" "closed_segment b c  S" and subs: "x. x  S  closed_segment a x  S"
  shows "convex hull {a,b,c}  S"
proof -
  have "convex hull {b, c}  S"
    using assms(2) segment_convex_hull by auto
  then have "u v d. 0  u; 0  v; u + v = 1; d  convex hull {b, c}  u *R a + v *R d  S"
    by (meson subs convexD convex_closed_segment ends_in_segment subsetCE)
  then show ?thesis
    by (auto simp add: convex_hull_insert [of "{b,c}" a])
qed

lemma triangle_contour_integrals_starlike_primitive:
  assumes contf: "continuous_on S f"
      and S: "a  S" "open S"
      and x: "x  S"
      and subs: "y. y  S  closed_segment a y  S"
      and zer: "b c. closed_segment b c  S
                    contour_integral (linepath a b) f + contour_integral (linepath b c) f +
                       contour_integral (linepath c a) f = 0"
    shows "((λx. contour_integral(linepath a x) f) has_field_derivative f x) (at x)"
proof -
  let ?pathint = "λx y. contour_integral(linepath x y) f"
  { fix e y
    assume e: "0 < e" and bxe: "ball x e  S" and close: "cmod (y - x) < e"
    have y: "y  S"
      using bxe close  by (force simp: dist_norm norm_minus_commute)
    have cont_ayf: "continuous_on (closed_segment a y) f"
      using contf continuous_on_subset subs y by blast
    have xys: "closed_segment x y  S"
      by (metis bxe centre_in_ball close closed_segment_subset convex_ball dist_norm dual_order.trans e mem_ball norm_minus_commute)
    have "?pathint a y - ?pathint a x = ?pathint x y"
      using zer [OF xys]  contour_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  } note [simp] = this
  { fix e::real
    assume e: "0 < e"
    have cont_atx: "continuous (at x) f"
      using x S contf continuous_on_eq_continuous_at by blast
    then obtain d1 where d1: "d1>0" and d1_less: "y. cmod (y - x) < d1  cmod (f y - f x) < e/2"
      unfolding continuous_at Lim_at dist_norm  using e
      by (drule_tac x="e/2" in spec) force
    obtain d2 where d2: "d2>0" "ball x d2  S" using  open S x
      by (auto simp: open_contains_ball)
    have dpos: "min d1 d2 > 0" using d1 d2 by simp
    { fix y
      assume yx: "y  x" and close: "cmod (y - x) < min d1 d2"
      have y: "y  S"
        using d2 close  by (force simp: dist_norm norm_minus_commute)
      have "closed_segment x y  S"
        using close d2  by (auto simp: dist_norm norm_minus_commute dest!: segment_bound(1))
      then have fxy: "f contour_integrable_on linepath x y"
        by (metis contour_integrable_continuous_linepath continuous_on_subset [OF contf])
      then obtain i where i: "(f has_contour_integral i) (linepath x y)"
        by (auto simp: contour_integrable_on_def)
      then have "((λw. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)"
        by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath])
      then have "cmod (i - f x * (y - x))  e / 2 * cmod (y - x)"
      proof (rule has_contour_integral_bound_linepath)
        show "u. u  closed_segment x y  cmod (f u - f x)  e / 2"
          by (meson close d1_less le_less_trans less_imp_le min.strict_boundedE segment_bound1)
      qed (use e in simp)
      also have " < e * cmod (y - x)"
        by (simp add: e yx)
      finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
        using i yx  by (simp add: contour_integral_unique divide_less_eq)
    }
    then have "d>0. y. y  x  cmod (y-x) < d  cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
      using dpos by blast
  }
  then have "(λy. (?pathint x y - f x * (y - x)) /R cmod (y - x)) x 0"
    by (simp add: Lim_at dist_norm inverse_eq_divide)
  then have "(λy. (1 / cmod (y - x)) *R (?pathint a y - (?pathint a x + f x * (y - x)))) x 0"
    using open S x 
    by (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at intro:  Lim_transform [OF _ tendsto_eventually])
  then show ?thesis
    by (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
qed

text ‹Existence of a primitive›
lemma holomorphic_starlike_primitive:
  fixes f :: "complex  complex"
  assumes contf: "continuous_on S f"
      and S: "starlike S" and os: "open S"
      and k: "finite k"
      and fcd: "x. x  S - k  f field_differentiable at x"
    shows "g. x  S. (g has_field_derivative f x) (at x)"
proof -
  obtain a where a: "aS" and a_cs: "x. xS  closed_segment a x  S"
    using S by (auto simp: starlike_def)
  { fix x b c
    assume "x  S" "closed_segment b c  S"
    then have abcs: "convex hull {a, b, c}  S"
      by (simp add: a a_cs starlike_convex_subset)
    then have "continuous_on (convex hull {a, b, c}) f"
      by (simp add: continuous_on_subset [OF contf])
    then have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
      using abcs interior_subset by (force intro: fcd Cauchy_theorem_triangle_cofinite [OF _ k])
  } note 0 = this
  show ?thesis
  proof (intro exI ballI)
    show "x. x  S  ((λx. contour_integral (linepath a x) f) has_field_derivative f x) (at x)"
      using "0" a a_cs contf has_chain_integral_chain_integral3 os triangle_contour_integrals_starlike_primitive by force
  qed
qed

lemma Cauchy_theorem_starlike:
 "open S; starlike S; finite k; continuous_on S f;
   x. x  S - k  f field_differentiable at x;
   valid_path g; path_image g  S; pathfinish g = pathstart g
    (f has_contour_integral 0)  g"
  by (metis holomorphic_starlike_primitive Cauchy_theorem_primitive at_within_open)

lemma Cauchy_theorem_starlike_simple:
  "open S; starlike S; f holomorphic_on S; valid_path g; path_image g  S; pathfinish g = pathstart g
    (f has_contour_integral 0) g"
  using Cauchy_theorem_starlike [OF _ _ finite.emptyI]
  by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at)

subsection‹Cauchy's theorem for a convex set›

text‹For a convex set we can avoid assuming openness and boundary analyticity›

lemma triangle_contour_integrals_convex_primitive:
  assumes contf: "continuous_on S f"
      and S: "a  S" "convex S"
      and x: "x  S"
      and zer: "b c. b  S; c  S
                    contour_integral (linepath a b) f + contour_integral (linepath b c) f +
                       contour_integral (linepath c a) f = 0"
    shows "((λx. contour_integral(linepath a x) f) has_field_derivative f x) (at x within S)"
proof -
  let ?pathint = "λx y. contour_integral(linepath x y) f"
  { fix y
    assume y: "y  S"
    have cont_ayf: "continuous_on (closed_segment a y) f"
      using S y  by (meson contf continuous_on_subset convex_contains_segment)
    have xys: "closed_segment x y  S"  (*?*)
      using convex_contains_segment S x y by auto
    have "?pathint a y - ?pathint a x = ?pathint x y"
      using zer [OF x y]  contour_integral_reverse_linepath [OF cont_ayf]  add_eq_0_iff by force
  } note [simp] = this
  { fix e::real
    assume e: "0 < e"
    have cont_atx: "continuous (at x within S) f"
      using x S contf  by (simp add: continuous_on_eq_continuous_within)
    then obtain d1 where d1: "d1>0" and d1_less: "y. y  S; cmod (y - x) < d1  cmod (f y - f x) < e/2"
      unfolding continuous_within Lim_within dist_norm using e
      by (drule_tac x="e/2" in spec) force
    { fix y
      assume yx: "y  x" and close: "cmod (y - x) < d1" and y: "y  S"
      have fxy: "f contour_integrable_on linepath x y"
        using convex_contains_segment S x y
        by (blast intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
      then obtain i where i: "(f has_contour_integral i) (linepath x y)"
        by (auto simp: contour_integrable_on_def)
      then have "((λw. f w - f x) has_contour_integral (i - f x * (y - x))) (linepath x y)"
        by (rule has_contour_integral_diff [OF _ has_contour_integral_const_linepath])
      then have "cmod (i - f x * (y - x))  e / 2 * cmod (y - x)"
      proof (rule has_contour_integral_bound_linepath)
        show "u. u  closed_segment x y  cmod (f u - f x)  e / 2"
          by (meson assms(3) close convex_contains_segment d1_less le_less_trans less_imp_le segment_bound1 subset_iff x y)
      qed (use e in simp)
      also have " < e * cmod (y - x)"
        by (simp add: e yx)
      finally have "cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
        using i yx  by (simp add: contour_integral_unique divide_less_eq)
    }
    then have "d>0. yS. y  x  cmod (y-x) < d  cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
      using d1 by blast
  }
  then have "((λy. (?pathint x y - f x * (y - x)) /R cmod (y - x))  0) (at x within S)"
    by (simp add: Lim_within dist_norm inverse_eq_divide)
  then have "((λy. (1 / cmod (y - x)) *R (?pathint a y - (?pathint a x + f x * (y - x))))  0)
             (at x within S)"
    using linordered_field_no_ub
    by (force simp: inverse_eq_divide [symmetric] eventually_at intro: Lim_transform [OF _ tendsto_eventually])
  then show ?thesis
    by (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
qed

lemma contour_integral_convex_primitive:
  assumes "convex S" "continuous_on S f"
          "a b c. a  S; b  S; c  S  (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
  obtains g where "x. x  S  (g has_field_derivative f x) (at x within S)"
proof (cases "S={}")
  case False
  with assms that show ?thesis
    by (blast intro: triangle_contour_integrals_convex_primitive has_chain_integral_chain_integral3)
qed auto

lemma holomorphic_convex_primitive:
  fixes f :: "complex  complex"
  assumes "convex S" "finite K" and contf: "continuous_on S f"
    and fd: "x. x  interior S - K  f field_differentiable at x"
  obtains g where "x. x  S  (g has_field_derivative f x) (at x within S)"
proof (rule contour_integral_convex_primitive [OF convex S contf Cauchy_theorem_triangle_cofinite])
  have *: "convex hull {a, b, c}  S" if "a  S" "b  S" "c  S" for a b c
    by (simp add: convex S hull_minimal that)
  show "continuous_on (convex hull {a, b, c}) f" if "a  S" "b  S" "c  S" for a b c
    by (meson "*" contf continuous_on_subset that)
  show "f field_differentiable at x" if "a  S" "b  S" "c  S" "x  interior (convex hull {a, b, c}) - K" for a b c x
    by (metis "*" DiffD1 DiffD2 DiffI fd interior_mono subsetCE that)
qed (use assms in force+)

lemma holomorphic_convex_primitive':
  fixes f :: "complex  complex"
  assumes "convex S" and "open S" and "f holomorphic_on S"
  obtains g where "x. x  S  (g has_field_derivative f x) (at x within S)"
proof (rule holomorphic_convex_primitive)
  fix x assume "x  interior S - {}"
  with assms show "f field_differentiable at x"
    by (auto intro!: holomorphic_on_imp_differentiable_at simp: interior_open)
qed (use assms in auto intro: holomorphic_on_imp_continuous_on)

corollarytag unimportant› Cauchy_theorem_convex:
    "continuous_on S f; convex S; finite K;
      x. x  interior S - K  f field_differentiable at x;
      valid_path g; path_image g  S; pathfinish g = pathstart g
      (f has_contour_integral 0) g"
  by (metis holomorphic_convex_primitive Cauchy_theorem_primitive)

corollary Cauchy_theorem_convex_simple:
  assumes holf: "f holomorphic_on S" 
      and "convex S" "valid_path g" "path_image g  S" "pathfinish g = pathstart g"
  shows "(f has_contour_integral 0) g"
proof -
  have "f holomorphic_on interior S"
    by (meson holf holomorphic_on_subset interior_subset)
  with Cauchy_theorem_convex [where K = "{}"] show ?thesis
    using assms
    by (metis Diff_empty finite.emptyI holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at open_interior)
qed

text‹In particular for a disc›
corollarytag unimportant› Cauchy_theorem_disc:
    "finite K; continuous_on (cball a e) f;
      x. x  ball a e - K  f field_differentiable at x;
     valid_path g; path_image g  cball a e;
     pathfinish g = pathstart g  (f has_contour_integral 0) g"
  by (auto intro: Cauchy_theorem_convex)

corollarytag unimportant› Cauchy_theorem_disc_simple:
    "f holomorphic_on (ball a e); valid_path g; path_image g  ball a e;
     pathfinish g = pathstart g  (f has_contour_integral 0) g"
by (simp add: Cauchy_theorem_convex_simple)

subsectiontag unimportant› ‹Generalize integrability to local primitives›

lemma contour_integral_local_primitive_lemma:
  fixes f :: "complexcomplex"
  assumes gpd: "g piecewise_differentiable_on {a..b}"
      and dh: "x. x  S  (f has_field_derivative f' x) (at x within S)"
      and gs: "x. x  {a..b}  g x  S"
    shows "(λx. f' (g x) * vector_derivative g (at x within {a..b})) integrable_on {a..b}"
proof (cases "cbox a b = {}")
  case False
  then show ?thesis
    unfolding integrable_on_def by (auto intro: assms contour_integral_primitive_lemma)
qed auto

lemma contour_integral_local_primitive_any:
  fixes f :: "complex  complex"
  assumes gpd: "g piecewise_differentiable_on {a..b}"
      and dh: "x. x  S
                d h. 0 < d 
                         (y. norm(y - x) < d  (h has_field_derivative f y) (at y within S))"
      and gs: "x. x  {a..b}  g x  S"
  shows "(λx. f(g x) * vector_derivative g (at x)) integrable_on {a..b}"
proof -
  { fix x
    assume x: "a  x" "x  b"
    obtain d h where d: "0 < d"
               and h: "(y. norm(y - g x) < d  (h has_field_derivative f y) (at y within S))"
      using x gs dh by (metis atLeastAtMost_iff)
    have "continuous_on {a..b} g" using gpd piecewise_differentiable_on_def by blast
    then obtain e where e: "e>0" and lessd: "x'. x'  {a..b}  ¦x' - x¦ < e  cmod (g x' - g x) < d"
      using x d by (fastforce simp: dist_norm continuous_on_iff)
    have "e>0. u v. u  x  x  v  {u..v}  ball x e  (u  v  a  u  v  b) 
                          (λx. f (g x) * vector_derivative g (at x)) integrable_on {u..v}"
    proof -
      have "(λx. f (g x) * vector_derivative g (at x within {u..v})) integrable_on {u..v}"
        if "u  x" "x  v" and ball: "{u..v}  ball x e" and auvb: "u  v  a  u  v  b"
        for u v
      proof (rule contour_integral_local_primitive_lemma)
        show "g piecewise_differentiable_on {u..v}"
          by (metis atLeastatMost_subset_iff gpd piecewise_differentiable_on_subset auvb)
        show "x. x  g ` {u..v}  (h has_field_derivative f x) (at x within g ` {u..v})"
          using that by (force simp: ball_def dist_norm intro: lessd gs DERIV_subset [OF h])
      qed auto
      then show ?thesis
        using e integrable_on_localized_vector_derivative by blast
    qed
  } then
  show ?thesis
    by (force simp: intro!: integrable_on_little_subintervals [of a b, simplified])
qed

lemma contour_integral_local_primitive:
  fixes f :: "complex  complex"
  assumes g: "valid_path g" "path_image g  S"
      and dh: "x. x  S
                d h. 0 < d 
                         (y. norm(y - x) < d  (h has_field_derivative f y) (at y within S))"
    shows "f contour_integrable_on g"
proof -
  have "(λx. f (g x) * vector_derivative g (at x)) integrable_on {0..1}"
    using contour_integral_local_primitive_any [OF _ dh] g
    unfolding path_image_def valid_path_def
    by (metis (no_types, lifting) image_subset_iff piecewise_C1_imp_differentiable)
  then show ?thesis
    using contour_integrable_on by presburger
qed


text‹In particular if a function is holomorphic›

lemma contour_integrable_holomorphic:
  assumes contf: "continuous_on S f"
      and os: "open S"
      and k: "finite k"
      and g: "valid_path g" "path_image g  S"
      and fcd: "x. x  S - k  f field_differentiable at x"
    shows "f contour_integrable_on g"
proof -
  { fix z
    assume z: "z  S"
    obtain d where "d>0" and d: "ball z d  S" using  open S z
      by (auto simp: open_contains_ball)
    then have contfb: "continuous_on (ball z d) f"
      using contf continuous_on_subset by blast
    obtain h where "yball z d. (h has_field_derivative f y) (at y within ball z d)"
      by (metis holomorphic_convex_primitive [OF convex_ball k contfb fcd] d interior_subset Diff_iff subsetD)
    then have "yball z d. (h has_field_derivative f y) (at y within S)"
      by (metis open_ball at_within_open d os subsetCE)
    then have "h. (y. cmod (y - z) < d  (h has_field_derivative f y) (at y within S))"
      by (force simp: dist_norm norm_minus_commute)
    then have "d h. 0 < d  (y. cmod (y - z) < d  (h has_field_derivative f y) (at y within S))"
      using 0 < d by blast
  }
  then show ?thesis
    by (rule contour_integral_local_primitive [OF g])
qed

lemma contour_integrable_holomorphic_simple:
  assumes fh: "f holomorphic_on S"
      and os: "open S"
      and g: "valid_path g" "path_image g  S"
    shows "f contour_integrable_on g"
proof -
  have "x. x  S  f field_differentiable at x"
    using fh holomorphic_on_imp_differentiable_at os by blast
  moreover have "continuous_on S f"
    by (simp add: fh holomorphic_on_imp_continuous_on)
  ultimately show ?thesis
    by (metis Diff_empty contour_integrable_holomorphic finite.emptyI g os)
qed

lemma analytic_imp_contour_integrable:
  assumes "f analytic_on path_image p" "valid_path p"
  shows   "f contour_integrable_on p"
  by (meson analytic_on_holomorphic assms contour_integrable_holomorphic_simple)

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

lemma contour_integrable_inversediff:
  assumes g: "valid_path g"
      and notin: "z  path_image g"
    shows "(λw. 1 / (w-z)) contour_integrable_on g"
proof (rule contour_integrable_holomorphic_simple)
  show "(λw. 1 / (w-z)) holomorphic_on UNIV - {z}"
    by (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
qed (use assms in auto)

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

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

text‹This formulation covers two cases: termg and termh share their
      start and end points; termg and termh both loop upon themselves.›
lemma contour_integral_nearby:
  assumes os: "open S" and p: "path p" "path_image p  S"
  shows "d. 0 < d 
            (g h. valid_path g  valid_path h 
                  (t  {0..1}. norm(g t - p t) < d  norm(h t - p t) < d) 
                  linked_paths atends g h
                   path_image g  S  path_image h  S 
                      (f. f holomorphic_on S  contour_integral h f = contour_integral g f))"
proof -
  have "z. e. z  path_image p  0 < e  ball z e  S"
    using open_contains_ball os p(2) by blast
  then obtain ee where ee: "z. z  path_image p  0 < ee z  ball z (ee z)  S"
    by metis
  define cover where "cover = (λz. ball z (ee z/3)) ` (path_image p)"
  have "compact (path_image p)"
    by (metis p(1) compact_path_image)
  moreover have "path_image p  (cpath_image p. ball c (ee c / 3))"
    using ee by auto
  ultimately have "D  cover. finite D  path_image p  D"
    by (simp add: compact_eq_Heine_Borel cover_def)
  then obtain D where D: "D  cover" "finite D" "path_image p  D"
    by blast
  then obtain k where k: "k  {0..1}" "finite k" and D_eq: "D = ((λz. ball z (ee z / 3))  p) ` k"
    unfolding cover_def path_image_def image_comp 
    by (meson finite_subset_image)
  then have kne: "k  {}"
    using D by auto
  have pi: "i. i  k  p i  path_image p"
    using k  by (auto simp: path_image_def)
  then have eepi: "i. i  k  0 < ee((p i))"
    by (metis ee)
  define e where "e = Min((ee  p) ` k)"
  have fin_eep: "finite ((ee  p) ` k)"
    using k  by blast
  have "0 < e"
    using ee k  by (simp add: kne e_def Min_gr_iff [OF fin_eep] eepi)
  have "uniformly_continuous_on {0..1} p"
    using p  by (simp add: path_def compact_uniformly_continuous)
  then obtain d::real where d: "d>0"
          and de: "x x'. ¦x' - x¦ < d  x{0..1}  x'{0..1}  cmod (p x' - p x) < e/3"
    unfolding uniformly_continuous_on_def dist_norm real_norm_def
    by (metis divide_pos_pos 0 < e zero_less_numeral)
  then obtain N::nat where N: "N>0" "inverse N < d"
    using real_arch_inverse [of d]   by auto
  show ?thesis
  proof (intro exI conjI allI; clarify?)
    show "e/3 > 0"
      using 0 < e by simp
    fix g h
    assume g: "valid_path g" and ghp: "t{0..1}. cmod (g t - p t) < e / 3   cmod (h t - p t) < e / 3"
       and h: "valid_path h"
       and joins: "linked_paths atends g h"
    { fix t::real
      assume t: "0  t" "t  1"
      then obtain u where u: "u  k" and ptu: "p t  ball(p u) (ee(p u) / 3)"
        using path_image p  D D_eq by (force simp: path_image_def)
      then have ele: "e  ee (p u)" using fin_eep
        by (simp add: e_def)
      have "cmod (g t - p t) < e / 3" "cmod (h t - p t) < e / 3"
        using ghp t by auto
      with ele have "cmod (g t - p t) < ee (p u) / 3"
                    "cmod (h t - p t) < ee (p u) / 3"
        by linarith+
      then have "g t  ball(p u) (ee(p u))"  "h t  ball(p u) (ee(p u))"
        using norm_diff_triangle_ineq [of "g t" "p t" "p t" "p u"]
              norm_diff_triangle_ineq [of "h t" "p t" "p t" "p u"] ptu eepi u
        by (force simp: dist_norm ball_def norm_minus_commute)+
      then have "g t  S" "h t  S" using ee u k
        by (auto simp: path_image_def ball_def)
    }
    then have ghs: "path_image g  S" "path_image h  S"
      by (auto simp: path_image_def)
    moreover
    { fix f
      assume fhols: "f holomorphic_on S"
      then have fpa: "f contour_integrable_on g"  "f contour_integrable_on h"
        using g ghs h holomorphic_on_imp_continuous_on os contour_integrable_holomorphic_simple
        by blast+
      have contf: "continuous_on S f"
        by (simp add: fhols holomorphic_on_imp_continuous_on)
      { fix z
        assume z: "z  path_image p"
        have "f holomorphic_on ball z (ee z)"
          using fhols ee z holomorphic_on_subset by blast
        then have "ff. (w  ball z (ee z). (ff has_field_derivative f w) (at w))"
          using holomorphic_convex_primitive [of "ball z (ee z)" "{}" f, simplified]
          by (metis open_ball at_within_open holomorphic_on_def holomorphic_on_imp_continuous_on mem_ball)
      }
      then obtain ff where ff:
            "z w. z  path_image p; w  ball z (ee z)  (ff z has_field_derivative f w) (at w)"
        by metis
      { fix n
        assume n: "n  N"
        then have "contour_integral(subpath 0 (n/N) h) f - contour_integral(subpath 0 (n/N) g) f =
                   contour_integral(linepath (g(n/N)) (h(n/N))) f - contour_integral(linepath (g 0) (h 0)) f"
        proof (induct n)
          case 0 show ?case by simp
        next
          case (Suc n)
          obtain t where t: "t  k" and "p (n/N)  ball(p t) (ee(p t) / 3)"
            using path_image p  D [THEN subsetD, where c="p (n/N)"] D_eq N Suc.prems
            by (force simp: path_image_def)
          then have ptu: "cmod (p t - p (n/N)) < ee (p t) / 3"
            by (simp add: dist_norm)
          have e3le: "e/3  ee (p t) / 3"  using fin_eep t
            by (simp add: e_def)
          { fix x
            assume x: "n/N  x" "x  (1 + n)/N"
            then have nN01: "0  n/N" "(1 + n)/N  1"
              using Suc.prems by auto
            then have x01: "0  x" "x  1"
              using x by linarith+
            have "cmod (p t - p x)  < ee (p t) / 3 + e/3"
            proof (rule norm_diff_triangle_less [OF ptu de])
              show "¦real n / real N - x¦ < d"
                using x N by (auto simp: field_simps)
            qed (use x01 Suc.prems in auto)
            then have ptx: "cmod (p t - p x) < 2*ee (p t)/3"
              using e3le eepi [OF t] by simp
            have "cmod (p t - g x) < 2*ee (p t)/3 + e/3"
              using ghp x01 
              by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx])
            also have "  ee (p t)"
              using e3le eepi [OF t] by simp
            finally have gg: "cmod (p t - g x) < ee (p t)" .
            have "cmod (p t - h x) < 2*ee (p t)/3 + e/3 "
              using ghp x01 
              by (force simp add: norm_minus_commute intro!: norm_diff_triangle_less [OF ptx])
            also have "  ee (p t)"
              using e3le eepi [OF t] by simp
            finally have "cmod (p t - g x) < ee (p t)" "cmod (p t - h x) < ee (p t)"
              using gg by auto
          } note ptgh_ee = this
          have "closed_segment (g (n/N)) (h (n/N)) = path_image (linepath (h (n/N)) (g (n/N)))"
            by (simp add: closed_segment_commute)
          also have pi_hgn: "  ball (p t) (ee (p t))"
            using ptgh_ee [of "n/N"] Suc.prems
            by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
          finally have gh_ns: "closed_segment (g (n/N)) (h (n/N))  S"
            using ee pi t by blast
          have pi_ghn': "path_image (linepath (g ((1 + n) / N)) (h ((1 + n) / N)))  ball (p t) (ee (p t))"
            using ptgh_ee [of "(1+n)/N"] Suc.prems
            by (auto simp: field_simps dist_norm dest: segment_furthest_le [where y="p t"])
          then have gh_n's: "closed_segment (g ((1 + n) / N)) (h ((1 + n) / N))  S"
            using N>0 Suc.prems ee pi t
            by (auto simp: Path_Connected.path_image_join field_simps)
          have pi_subset_ball:
                "path_image (subpath (n/N) ((1+n) / N) g +++ linepath (g ((1+n) / N)) (h ((1+n) / N)) +++
                             subpath ((1+n) / N) (n/N) h +++ linepath (h (n/N)) (g (n/N)))
                  ball (p t) (ee (p t))"
          proof (intro subset_path_image_join pi_hgn pi_ghn')
            show "path_image (subpath (n/N) ((1+n) / N) g)  ball (p t) (ee (p t))"
                 "path_image (subpath ((1+n) / N) (n/N) h)  ball (p t) (ee (p t))"
              using N>0 Suc.prems
              by (auto simp: path_image_subpath dist_norm field_simps ptgh_ee)
          qed
          have pi0: "(f has_contour_integral 0)
                       (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
                        subpath ((Suc n) / N) (n/N) h +++ linepath(h (n/N)) (g (n/N)))"
          proof (rule Cauchy_theorem_primitive)
            show "x. x  ball (p t) (ee (p t)) 
                       (ff (p t) has_field_derivative f x) (at x within ball (p t) (ee (p t)))"
              by (metis ff open_ball at_within_open pi t)
            qed (use Suc.prems pi_subset_ball in simp_all add: valid_path_subpath g h)
          have fpa1: "f contour_integrable_on subpath (n/N) (real (Suc n) / real N) g"
            using Suc.prems by (simp add: contour_integrable_subpath g fpa)
          have fpa2: "f contour_integrable_on linepath (g (real (Suc n) / real N)) (h (real (Suc n) / real N))"
            using gh_n's
            by (auto intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
          have fpa3: "f contour_integrable_on linepath (h (n/N)) (g (n/N))"
            using gh_ns
            by (auto simp: closed_segment_commute intro!: contour_integrable_continuous_linepath continuous_on_subset [OF contf])
          have eq0: "contour_integral (subpath (n/N) ((Suc n) / real N) g) f +
                     contour_integral (linepath (g ((Suc n) / N)) (h ((Suc n) / N))) f +
                     contour_integral (subpath ((Suc n) / N) (n/N) h) f +
                     contour_integral (linepath (h (n/N)) (g (n/N))) f = 0"
            using contour_integral_unique [OF pi0] Suc.prems
            by (simp add: g h fpa valid_path_subpath contour_integrable_subpath
                          fpa1 fpa2 fpa3 algebra_simps del: of_nat_Suc)
          have *: "hn he hn' gn gd gn' hgn ghn gh0 ghn'.
                    hn - gn = ghn - gh0;
                     gd + ghn' + he + hgn = (0::complex);
                     hn - he = hn'; gn + gd = gn'; hgn = -ghn  hn' - gn' = ghn' - gh0"
            by (auto simp: algebra_simps)
          have "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
                contour_integral (subpath 0 (n/N) h) f + contour_integral (subpath (n/N) ((Suc n) / N) h) f"
            unfolding reversepath_subpath [symmetric, of "((Suc n) / N)"]
            using Suc.prems by (simp add: h fpa contour_integral_reversepath valid_path_subpath contour_integrable_subpath)
          also have " = contour_integral (subpath 0 ((Suc n) / N) h) f"
            using Suc.prems by (simp add: contour_integral_subpath_combine h fpa)
          finally have pi0_eq:
               "contour_integral (subpath 0 (n/N) h) f - contour_integral (subpath ((Suc n) / N) (n/N) h) f =
                contour_integral (subpath 0 ((Suc n) / N) h) f" .
          show ?case
          proof (rule * [OF Suc.hyps eq0 pi0_eq])
            show "contour_integral (subpath 0 (n/N) g) f +
                  contour_integral (subpath (n/N) ((Suc n) / N) g) f =
                  contour_integral (subpath 0 ((Suc n) / N) g) f"
              using Suc.prems contour_integral_subpath_combine fpa(1) g by auto
            show "contour_integral (linepath (h (n/N)) (g (n/N))) f = - contour_integral (linepath (g (n/N)) (h (n/N))) f"
              by (metis contour_integral_unique fpa3 has_contour_integral_integral has_contour_integral_reverse_linepath)
          qed (use Suc.prems in auto)
      qed
      } note ind = this
      have "contour_integral h f = contour_integral g f"
        using ind [OF order_refl] N joins
        by (simp add: linked_paths_def pathstart_def pathfinish_def split: if_split_asm)
    }
    ultimately
    show "path_image g  S  path_image h  S  (f. f holomorphic_on S  contour_integral h f = contour_integral g f)"
      by metis
  qed
qed


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

lemma contour_integral_bound_exists:
assumes S: "open S"
    and g: "valid_path g"
    and pag: "path_image g  S"
  shows "L. 0 < L 
             (f B. f holomorphic_on S  (z  S. norm(f z)  B)
                norm(contour_integral g f)  L*B)"
proof -
  have "path g" using g
    by (simp add: valid_path_imp_path)
  then obtain d::real and p
    where d: "0 < d"
      and p: "polynomial_function p" "path_image p  S"
      and pi: "f. f holomorphic_on S  contour_integral g f = contour_integral p f"
    using contour_integral_nearby_ends [OF S path g pag]
    by (metis cancel_comm_monoid_add_class.diff_cancel g norm_zero path_approx_polynomial_function valid_path_polynomial_function)
  then obtain p' where p': "polynomial_function p'"
    "x. (p has_vector_derivative (p' x)) (at x)"
    by (blast intro: has_vector_derivative_polynomial_function that)
  then have "bounded(p' ` {0..1})"
    using continuous_on_polymonial_function
    by (force simp: intro!: compact_imp_bounded compact_continuous_image)
  then obtain L where L: "L>0" and nop': "x. 0  x; x  1  norm (p' x)  L"
    by (force simp: bounded_pos)
  { fix f B
    assume f: "f holomorphic_on S" and B: "z. zS  cmod (f z)  B"
    then have "f contour_integrable_on p  valid_path p"
      using p S
      by (blast intro: valid_path_polynomial_function contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on)
    moreover have "cmod (vector_derivative p (at x)) * cmod (f (p x))  L * B" if "0  x" "x  1" for x
    proof (rule mult_mono)
      show "cmod (vector_derivative p (at x))  L"
        by (metis nop' p'(2) that vector_derivative_at)
      show "cmod (f (p x))  B"
        by (metis B atLeastAtMost_iff imageI p(2) path_defs(4) subset_eq that)
    qed (use L>0 in auto)
    ultimately 
    have "cmod (integral {0..1} (λx. f (p x) * vector_derivative p (at x)))  L * B"
      by (intro order_trans [OF integral_norm_bound_integral])
         (auto simp: mult.commute norm_mult contour_integrable_on)
    then have "cmod (contour_integral g f)  L * B"
      using contour_integral_integral f pi by presburger
  } then
  show ?thesis using L > 0
    by (intro exI[of _ L]) auto
qed


subsection‹Homotopy forms of Cauchy's theorem›

lemma Cauchy_theorem_homotopic:
    assumes hom: "if atends then homotopic_paths S g h else homotopic_loops S g h"
        and "open S" and f: "f holomorphic_on S"
        and vpg: "valid_path g" and vph: "valid_path h"
    shows "contour_integral g f = contour_integral h f"
proof -
  have pathsf: "linked_paths atends g h"
    using hom  by (auto simp: linked_paths_def homotopic_paths_imp_pathstart homotopic_paths_imp_pathfinish homotopic_loops_imp_loop)
  obtain k :: "real × real  complex"
    where contk: "continuous_on ({0..1} × {0..1}) k"
      and ks: "k ` ({0..1} × {0..1})  S"
      and k [simp]: "x. k (0, x) = g x" "x. k (1, x) = h x"
      and ksf: "t{0..1}. linked_paths atends g (λx. k (t, x))"
      using hom pathsf by (auto simp: linked_paths_def homotopic_paths_def homotopic_loops_def homotopic_with_def split: if_split_asm)
  have ucontk: "uniformly_continuous_on ({0..1} × {0..1}) k"
    by (blast intro: compact_Times compact_uniformly_continuous [OF contk])
  { fix t::real assume t: "t  {0..1}"
    have "Pair t ` {0..1}  {0..1} × {0..1}"
      using t by force
    then have pak: "path (k  (λu. (t, u)))"
      unfolding path_def
      by (intro continuous_intros continuous_on_subset [OF contk])+
    have pik: "path_image (k  Pair t)  S"
      using ks t by (auto simp: path_image_def)
    obtain e where "e>0" and e:
         "g h. valid_path g; valid_path h;
                  u{0..1}. cmod (g u - (k  Pair t) u) < e  cmod (h u - (k  Pair t) u) < e;
                  linked_paths atends g h
                  contour_integral h f = contour_integral g f"
      using contour_integral_nearby [OF open S pak pik, of atends] f by metis
    obtain d where "d>0" and d:
        "x x'. x  {0..1} × {0..1}; x'  {0..1} × {0..1}; norm (x'-x) < d  norm (k x' - k x) < e/4"
      by (rule uniformly_continuous_onE [OF ucontk, of "e/4"]) (auto simp: dist_norm e>0)
    { fix t1 t2
      assume t1: "0  t1" "t1  1" and t2: "0  t2" "t2  1" and ltd: "¦t1 - t¦ < d" "¦t2 - t¦ < d"
      have no2: "norm(g1 - kt) < e" if "norm(g1 - k1) < e/4" "norm(k1 - kt) < e/4" for g1 k1 kt :: complex
      proof (rule norm_triangle_half_l)
        show "cmod (g1 - k1) < e/2" "cmod (kt - k1) < e/2"
          using e > 0 that by (auto simp: norm_minus_commute intro: order_less_trans)
      qed
      have "d>0. g1 g2. valid_path g1  valid_path g2 
                          (u{0..1}. cmod (g1 u - k (t1, u)) < d  cmod (g2 u - k (t2, u)) < d) 
                          linked_paths atends g1 g2 
                          contour_integral g2 f = contour_integral g1 f"
        using t t1 t2 ltd e > 0
        by (rule_tac x="e/4" in exI) (auto intro!: e simp: d no2 simp del: less_divide_eq_numeral1)
    }
    then have "e. 0 < e 
              (t1 t2. t1  {0..1}  t2  {0..1}  ¦t1 - t¦ < e  ¦t2 - t¦ < e
                 (d. 0 < d 
                     (g1 g2. valid_path g1  valid_path g2 
                       (u  {0..1}.
                          norm(g1 u - k((t1,u))) < d  norm(g2 u - k((t2,u))) < d) 
                          linked_paths atends g1 g2
                           contour_integral g2 f = contour_integral g1 f)))"
      by (rule_tac x=d in exI) (simp add: d > 0)
  }
  then obtain ee where ee:
       "t. t  {0..1}  ee t > 0 
          (t1 t2. t1  {0..1}  t2  {0..1}  ¦t1 - t¦ < ee t  ¦t2 - t¦ < ee t
             (d. 0 < d 
                 (g1 g2. valid_path g1  valid_path g2 
                   (u  {0..1}.
                      norm(g1 u - k((t1,u))) < d  norm(g2 u - k((t2,u))) < d) 
                      linked_paths atends g1 g2
                       contour_integral g2 f = contour_integral g1 f)))"
    by metis
  note ee_rule = ee [THEN conjunct2, rule_format, of 0 0 0]
  define C where "C = (λt. ball t (ee t / 3)) ` {0..1}"
  obtain C' where C': "C'  C" "finite C'" and C'01: "{0..1}  C'"
  proof (rule compactE [OF compact_interval])
    show "{0..1}  C"
      using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
  qed (use C_def in auto)
  define kk where "kk = {t  {0..1}. ball t (ee t / 3)  C'}"
  have kk01: "kk  {0..1}" by (auto simp: kk_def)
  define e where "e = Min (ee ` kk)"
  have C'_eq: "C' = (λt. ball t (ee t / 3)) ` kk"
    using C' by (auto simp: kk_def C_def)
  have ee_pos[simp]: "t. t  {0..1}  ee t > 0"
    by (simp add: kk_def ee)
  moreover have "finite kk"
    using finite C' kk01 by (force simp: C'_eq inj_on_def ball_eq_ball_iff dest: ee_pos finite_imageD)
  moreover have "kk  {}" using {0..1}  C' C'_eq by force
  ultimately have "e > 0"
    using finite_less_Inf_iff [of "ee ` kk" 0] kk01 by (force simp: e_def)
  then obtain N::nat where "N > 0" and N: "1/N < e/3"
    by (meson divide_pos_pos nat_approx_posE zero_less_Suc zero_less_numeral)
  have e_le_ee: "i. i  kk  e  ee i"
    using finite kk by (simp add: e_def Min_le_iff [of "ee ` kk"])
  have plus: "t  kk. x  ball t (ee t / 3)" if "x  {0..1}" for x
    using C' subsetD [OF C'01 that]  unfolding C'_eq by blast
  have [OF order_refl]:
      "d. 0 < d  (j. valid_path j  (u  {0..1}. norm(j u - k (n/N, u)) < d)  linked_paths atends g j
                         contour_integral j f = contour_integral g f)"
       if "n  N" for n
  using that
  proof (induct n)
    case 0 show ?case 
      using ee_rule 
      by clarsimp (metis diff_self norm_eq_zero vpg)
  next
    case (Suc n)
    then have N01: "n/N  {0..1}" "(Suc n)/N  {0..1}"  by auto
    then obtain t where t: "t  kk" "n/N  ball t (ee t / 3)"
      using plus [of "n/N"] by blast
    then have nN_less: "¦n/N - t¦ < ee t"
      by (simp add: dist_norm del: less_divide_eq_numeral1)
    have n'N_less: "¦real (Suc n) / real N - t¦ < ee t"
      using t N N > 0 e_le_ee [of t]
      by (simp add: dist_norm add_divide_distrib abs_diff_less_iff del: less_divide_eq_numeral1) (simp add: field_simps)
    have t01: "t  {0..1}" using kk  {0..1} t  kk by blast
    obtain d1 where "d1 > 0" and d1:
        "g1 g2. valid_path g1; valid_path g2;
                   u{0..1}. cmod (g1 u - k (n/N, u)) < d1  cmod (g2 u - k ((Suc n) / N, u)) < d1;
                   linked_paths atends g1 g2
                    contour_integral g2 f = contour_integral g1 f"
      using ee [THEN conjunct2, rule_format, OF t01 N01 nN_less n'N_less] by fastforce
    have "n  N" using Suc.prems by auto
    with Suc.hyps
    obtain d2 where "d2 > 0"
      and d2: "j. valid_path j; u{0..1}. cmod (j u - k (n/N, u)) < d2; linked_paths atends g j
                      contour_integral j f = contour_integral g f"
      by auto
    have "Pair (n/ N) ` {0..1}  {0..1} × {0..1}"
      using N01 by auto
    then have "continuous_on {0..1} (k  (λu. (n/N, u)))"
      by (intro continuous_intros continuous_on_subset [OF contk])
    then have pkn: "path (λu. k (n/N, u))"
      by (simp add: path_def)
    have min12: "min d1 d2 > 0" by (simp add: 0 < d1 0 < d2)
    obtain p where "polynomial_function p"
        and psf: "pathstart p = pathstart (λu. k (n/N, u))"
                 "pathfinish p = pathfinish (λu. k (n/N, u))"
        and pk_le:  "t. t{0..1}  cmod (p t - k (n/N, t)) < min d1 d2"
      using path_approx_polynomial_function [OF pkn min12] by blast
    then have vpp: "valid_path p" using valid_path_polynomial_function by blast
    have lpa: "linked_paths atends g p"
      by (metis (mono_tags, lifting) N01(1) ksf linked_paths_def pathfinish_def pathstart_def psf)
    show ?case
    proof (intro exI; safe)
      fix j
      assume "valid_path j" "linked_paths atends g j"
        and "u{0..1}. cmod (j u - k (real (Suc n) / real N, u)) < min d1 d2"
      then have "contour_integral j f = contour_integral p f"
        using pk_le N01(1) ksf by (force intro!: vpp d1 simp add: linked_paths_def psf)
      also have "... = contour_integral g f"
        using pk_le by (force intro!: vpp d2 lpa)
      finally show "contour_integral j f = contour_integral g f" .
    qed (simp add: 0 < d1 0 < d2)
  qed
  then obtain d where "0 < d"
                       "j. valid_path j  (u  {0..1}. norm(j u - k (1,u)) < d)  linked_paths atends g j
                             contour_integral j f = contour_integral g f"
    using N>0 by auto
  then have "linked_paths atends g h  contour_integral h f = contour_integral g f"
    using N>0 vph by fastforce
  then show ?thesis
    by (simp add: pathsf)
qed

proposition Cauchy_theorem_homotopic_paths:
    assumes hom: "homotopic_paths S g h"
        and "open S" and f: "f holomorphic_on S"
        and vpg: "valid_path g" and vph: "valid_path h"
    shows "contour_integral g f = contour_integral h f"
  using Cauchy_theorem_homotopic [of True S g h] assms by simp

proposition Cauchy_theorem_homotopic_loops:
    assumes hom: "homotopic_loops S g h"
        and "open S" and f: "f holomorphic_on S"
        and vpg: "valid_path g" and vph: "valid_path h"
    shows "contour_integral g f = contour_integral h f"
  using Cauchy_theorem_homotopic [of False S g h] assms by simp

lemma has_contour_integral_newpath:
    "(f has_contour_integral y) h; f contour_integrable_on g; contour_integral g f = contour_integral h f
      (f has_contour_integral y) g"
  using has_contour_integral_integral contour_integral_unique by auto

lemma Cauchy_theorem_null_homotopic:
     "f holomorphic_on S; open S; valid_path g; homotopic_loops S g (linepath a a) 
       (f has_contour_integral 0) g"
  by (metis Cauchy_theorem_homotopic_loops contour_integrable_holomorphic_simple valid_path_linepath
            contour_integral_trivial has_contour_integral_integral homotopic_loops_imp_subset)

end