Quelle Cauchy_Integral_Theorem.thy Sprache: Isabelle

section \<open>Complex Path Integrals and Cauchy's Integral Theorem\<close>

text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2015)\<close>

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 (- \\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel_measurable borel"
    by (intro borel_measurable_continuous_on_indicator continuous_intros) auto
  have "(\x. if x \ \\<^sub>\\<^sub>0 then ln (-Re x) + \ * pi else indicator (-\\<^sub>\\<^sub>0) x *\<^sub>R Ln x) \ borel \\<^sub>M borel"
    (is "?f \ _") by (rule measurable_If_set[OF _ cont]) auto
  hence "(\x. if x = 0 then Ln 0 else ?f x) \ borel \\<^sub>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\<open>The special case of midpoints used in the main quadrisection\<close>

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) *\<^sub>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) *\<^sub>R (b - a)"
  using assms by (auto simp: midpoint_def scaleR_conv_of_real)
qed (use assms in auto)

text\<open>A couple of special case lemmas that are useful below\<close>

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 * x\<^sup>2 + 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

subsection\<^marker>\<open>tag unimportant\<close> \<open>The key quadrisection step\<close>

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' \<le> K/2  \<and>  dist b' c' \<le> K/2  \<and>  dist c' a' \<le> K/2  \<and>
           e * (K/2)^2 \<le> 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 * K\<^sup>2 / 4 \ cmod (pathint a c' + pathint c' b' + pathint b' a)" |
           "e * K\<^sup>2 / 4 \ cmod (pathint a' c' + pathint c' b + pathint b a')" |
           "e * K\<^sup>2 / 4 \ cmod (pathint a' c + pathint c b' + pathint b' a')" |
           "e * K\<^sup>2 / 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

subsection\<^marker>\<open>tag unimportant\<close> \<open>Cauchy's theorem for triangles\<close>

lemma triangle_points_closer:
  fixes a::complex
  shows "\x \ convex hull {a,b,c}; y \ convex hull {a,b,c}\
         \<Longrightarrow> norm(x - y) \<le> norm(a - b) \<or>
             norm(x - y) \<le> norm(b - c) \<or>
             norm(x - y) \<le> 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 \<in> convex hull {a,b,c} \<and> convex hull {a,b,c} \<subseteq> S
              \<longrightarrow> norm(contour_integral(linepath a b) f + contour_integral(linepath b c) f +
                       contour_integral(linepath c a) f)
                  \<le> 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\
                     \<Longrightarrow> a \<le> 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) (\<lambda>y. f y - f x - f' * (y-x)) +
              contour_integral (linepath b c) (\<lambda>y. f y - f x - f' * (y-x)) +
              contour_integral (linepath c a) (\<lambda>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\<open>Hence the most basic theorem for a triangle.\<close>

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

proposition\<^marker>\<open>tag unimportant\<close> 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} \<subseteq> convex hull {a,b,c} \<and>
        dist x y \<le> K/2^n \<and> dist y z \<le> K/2^n \<and> dist z x \<le> K/2^n \<and>
        norm(?pathint x y + ?pathint y z + ?pathint z x) \<ge> 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)) \<ge> 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'.
               \<lbrakk>dist x' y' \<le> k; dist y' z' \<le> k; dist z' x' \<le> k;
                x \<in> convex hull {x',y',z'};
                convex hull {x',y',z'} \ convex hull {a,b,c}\
               \<Longrightarrow>
               cmod (?pathint x' y' + ?pathint y' z' + ?pathint z' x') * 10
                     \<le> e * (dist x' y' + dist y' z' + dist z' x')\<^sup>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))\<^sup>2
               \<le> (3 * K / 2 ^ n)\<^sup>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))\<^sup>2 \ e * (3 * K / 2 ^ n)\<^sup>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

subsection\<^marker>\<open>tag unimportant\<close> \<open>Version needing function holomorphic in interior only\<close>

lemma Cauchy_theorem_flat_lemma:
  assumes f: "continuous_on (convex hull {a,b,c}) f"
      and c: "c - a = k *\<^sub>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) *\<^sub>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 *\<^sub>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) *\<^sub>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 *\<^sub>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'. \x\convex hull {a, b, c}; x'\convex hull {a, b, c}; cmod (x' - x) < d1\
                           \<Longrightarrow> 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 *\<^sub>R (x - d)" for x
        have e: "0 < e" "e \ 1" "e \ d1 / (4 * C)" "e \ cmod y / 24 / C / B"
          using d1_pos \<open>C>0\<close> \<open>B>0\<close> ynz by (simp_all add: e_def)
        have e_le_d1: "e * (4 * C) \ d1"
          using e \<open>C>0\<close> 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 *\<^sub>R (b - d)) - (a - e *\<^sub>R (a - d)) - (b - a) = e *\<^sub>R (a - b)"
          by (simp add: algebra_simps)
        have "cmod y / (24 * C) \ cmod y / cmod (b - a) / 12"
          using False \<open>C>0\<close> 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: \<open>0<C\<close>)
        { fix u v
          assume uv: "u \ convex hull {a, b, c}" "v \ convex hull {a, b, c}" "u\v"
             and fpi_uv: "f contour_integrable_on linepath (shrink u) (shrink v)"
          have shr_uv: "shrink u \ interior(convex hull {a,b,c})"
                       "shrink v \ interior(convex hull {a,b,c})"
            using d e uv
            by (auto simp: hull_inc mem_interior_convex_shrink shrink_def)
          have cmod_fuv: "\x. 0\x \ x\1 \ cmod (f (linepath (shrink u) (shrink v) x)) \ B"
            using shr_uv by (blast intro: Bnf linepath_in_convex_hull interior_subset [THEN subsetD])
          { fix x::real   assume x: "0\x" "x\1"
            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) *\<^sub>R u - (1 - x) *\<^sub>R d) + cmod (x *\<^sub>R v - x *\<^sub>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) *\<^sub>R (u - d) + x *\<^sub>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 \<open>e>0\<close> 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))
                          \<le> 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 \<open>B>0\<close> diff_2C [of u v] uv by (auto simp: field_simps)
              also have "\ \ cmod y"
                using \<open>C>0\<close> \<open>B>0\<close> e by (simp add: field_simps)
              finally show "cmod (shrink v - shrink u - (v - u)) \ cmod y / 24 / C / B * 2 * C"
                using \<open>0 < B\<close> \<open>0 < C\<close> 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 \<open>C>0\<close> 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))
                       \<le> 2 * C * (cmod y / 24 / C)"
                using uv C  by (simp add: field_simps)
            qed (use \<open>0 < B\<close> 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))
                          \<le> 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)
                \<le> (B*(norm y /24/C/B)*2*C + (2*C)*(norm y/24/C)) * measure lborel (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 \<open>0 < B\<close> \<open>0 < C\<close>
            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))
                \<le> 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))
                \<le> 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 \<open>C > 0\<close> by auto
        ultimately obtain \<delta> where "\<delta> > 0" and
          "\x\convex hull {a, b, c}. \x'\convex hull {a, b, c}.
             dist x' x < \ \ dist (f x') (f x) < cmod y / (24 * C)"
          using \<open>C > 0\<close> ynz unfolding uniformly_continuous_on_def dist_norm by blast
        hence False using *[of \<delta>] 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

subsection\<^marker>\<open>tag unimportant\<close> \<open>Version allowing finite number of exceptional points\<close>

proposition\<^marker>\<open>tag unimportant\<close> 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 \<notin> 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

subsection\<^marker>\<open>tag unimportant\<close> \<open>Cauchy's theorem for an open starlike set\<close>

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 *\<^sub>R a + v *\<^sub>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
                   \<Longrightarrow> 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)) /\<^sub>R cmod (y - x)) \x\ 0"
    by (simp add: Lim_at dist_norm inverse_eq_divide)
  then have "(\y. (1 / cmod (y - x)) *\<^sub>R (?pathint a y - (?pathint a x + f x * (y - x)))) \x\ 0"
    using \<open>open S\<close> 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 \<open>Existence of a primitive\<close>
lemma holomorphic_starlike_primitive:
  fixes f :: "complex \ complex"
  assumes contf: "continuous_on S f"
      and S: "starlike S" and os: "open S"
      and k: "finite k"
      and fcd: "\x. x \ S - k \ f field_differentiable at x"
    shows "\g. \x \ S. (g has_field_derivative f x) (at x)"
proof -
  obtain a where a: "a\S" and a_cs: "\x. x\S \ closed_segment a x \ S"
    using S by (auto simp: starlike_def)
  { fix x b c
    assume "x \ S" "closed_segment b c \ S"
    then have abcs: "convex hull {a, b, c} \ S"
      by (simp add: a a_cs starlike_convex_subset)
    then have "continuous_on (convex hull {a, b, c}) f"
      by (simp add: continuous_on_subset [OF contf])
    then have "(f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)"
      using abcs interior_subset by (force intro: fcd Cauchy_theorem_triangle_cofinite [OF _ k])
  } note 0 = this
  show ?thesis
  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;
   \<And>x. x \<in> S - k \<Longrightarrow> f field_differentiable at x;
   valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
   \<Longrightarrow> (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\
   \<Longrightarrow> (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\<open>Cauchy's theorem for a convex set\<close>

text\<open>For a convex set we can avoid assuming openness and boundary analyticity\<close>

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\
                   \<Longrightarrow> 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. \y\S. y \ x \ cmod (y-x) < d \ cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
      using d1 by blast
  }
  then have "((\y. (?pathint x y - f x * (y - x)) /\<^sub>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)) *\<^sub>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 \<open>convex S\<close> 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: \<open>convex S\<close> 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 \<open>force+\<close>)

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 \<open>auto intro: holomorphic_on_imp_continuous_on\<close>)

corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_convex:
    "\continuous_on S f; convex S; finite K;
      \<And>x. x \<in> interior S - K \<Longrightarrow> f field_differentiable at x;
      valid_path g; path_image g \<subseteq> S; pathfinish g = pathstart g\<rbrakk>
     \<Longrightarrow> (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\<open>In particular for a disc\<close>
corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_disc:
    "\finite K; continuous_on (cball a e) f;
      \<And>x. x \<in> ball a e - K \<Longrightarrow> f field_differentiable at x;
     valid_path g; path_image g \<subseteq> cball a e;
     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
  by (auto intro: Cauchy_theorem_convex)

corollary\<^marker>\<open>tag unimportant\<close> Cauchy_theorem_disc_simple:
    "\f holomorphic_on (ball a e); valid_path g; path_image g \ ball a e;
     pathfinish g = pathstart g\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) g"
by (simp add: Cauchy_theorem_convex_simple)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Generalize integrability to local primitives\<close>

lemma contour_integral_local_primitive_lemma:
  fixes f :: "complex\complex"
  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
               \<Longrightarrow> \<exists>d h. 0 < d \<and>
                         (\<forall>y. norm(y - x) < d \<longrightarrow> (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) \
                          (\<lambda>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
               \<Longrightarrow> \<exists>d h. 0 < d \<and>
                         (\<forall>y. norm(y - x) < d \<longrightarrow> (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\<open>In particular if a function is holomorphic\<close>

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

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

text\<open>This formulation covers two cases: \<^term>\<open>g\<close> and \<^term>\<open>h\<close> share their
      start and end points; \<^term>\<open>g\<close> and \<^term>\<open>h\<close> both loop upon themselves.\<close>
lemma contour_integral_nearby:
  assumes os: "open S" and p: "path p" "path_image p \ S"
  shows "\d. 0 < d \
            (\<forall>g h. valid_path g \<and> valid_path h \<and>
                  (\<forall>t \<in> {0..1}. norm(g t - p t) < d \<and> norm(h t - p t) < d) \<and>
                  linked_paths atends g h
                  \<longrightarrow> path_image g \<subseteq> S \<and> path_image h \<subseteq> S \<and>
                      (\<forall>f. f holomorphic_on S \<longrightarrow> contour_integral h f = contour_integral g f))"
proof -
  have "\z. \e. z \ path_image p \ 0 < e \ ball z e \ S"
    using open_contains_ball os p(2) by blast
  then obtain ee where ee: "\z. z \ path_image p \ 0 < ee z \ ball z (ee z) \ S"
    by metis
  define cover where "cover = (\z. ball z (ee z/3)) ` (path_image p)"
  have "compact (path_image p)"
    by (metis p(1) compact_path_image)
  moreover have "path_image p \ (\c\path_image p. ball c (ee c / 3))"
    using ee by auto
  ultimately have "\D \ cover. finite D \ path_image p \ \D"
    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"
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.25 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.