Quelle Cauchy_Integral_Formula.thy Sprache: Isabelle

section \<open>Cauchy's Integral Formula\<close>
theory Cauchy_Integral_Formula
  imports Winding_Numbers
begin

subsection\<open>Proof\<close>

lemma Cauchy_integral_formula_weak:
    assumes S: "convex S" and "finite k" and conf: "continuous_on S f"
        and fcd: "(\x. x \ interior S - k \ f field_differentiable at x)"
        and z: "z \ interior S - k" and vpg: "valid_path \"
        and pasz: "path_image \ \ S - {z}" and loop: "pathfinish \ = pathstart \"
      shows "((\w. f w / (w-z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \"
proof -
  let ?fz = "\w. (f w - f z)/(w-z)"
  obtain f' where f': "(f has_field_derivative f') (at z)"
    using fcd [OF z] by (auto simp: field_differentiable_def)
  have pas: "path_image \ \ S" and znotin: "z \ path_image \" using pasz by blast+
  have c: "continuous (at x within S) (\w. if w = z then f' else (f w - f z) / (w-z))" if "x \ S" for x
  proof (cases "x = z")
    case True then show ?thesis
      using LIM_equal [of "z" ?fz "\w. if w = z then f' else ?fz w"] has_field_derivativeD [OF f']
      by (force simp add: continuous_within Lim_at_imp_Lim_at_within)
  next
    case False
    then have dxz: "dist x z > 0" by auto
    have cf: "continuous (at x within S) f"
      using conf continuous_on_eq_continuous_within that by blast
    have "continuous (at x within S) (\w. (f w - f z) / (w-z))"
      by (rule cf continuous_intros | simp add: False)+
    then show ?thesis
      using continuous_transform_within [OF _ dxz that] by (force simp: dist_commute)
  qed
  have fink': "finite (insert z k)" using \finite k\ by blast
  have *: "((\w. if w = z then f' else ?fz w) has_contour_integral 0) \"
  proof (rule Cauchy_theorem_convex [OF _ S fink' _ vpg pas loop])
    show "(\w. if w = z then f' else ?fz w) field_differentiable at w"
      if "w \ interior S - insert z k" for w
    proof (rule field_differentiable_transform_within)
      show "(\w. ?fz w) field_differentiable at w"
        using that by (intro derivative_intros fcd; simp)
    qed (use that in \<open>auto simp add: dist_pos_lt dist_commute\<close>)
  qed (use c in \<open>force simp: continuous_on_eq_continuous_within\<close>)
  note ** = has_contour_integral_add [OF has_contour_integral_lmul [OF has_contour_integral_winding_number [OF vpg znotin], of "f z"] *]
  show ?thesis
    apply (rule has_contour_integral_eq)
    using znotin ** apply (auto simp: ac_simps divide_simps)
    done
qed

theorem Cauchy_integral_formula_convex_simple:
  assumes "convex S" and holf: "f holomorphic_on S" and "z \ interior S" "valid_path \" "path_image \ \ S - {z}"
      "pathfinish \ = pathstart \"
    shows "((\w. f w / (w-z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \"
proof -
  have "\x. x \ interior S \ f field_differentiable at x"
    using holf at_within_interior holomorphic_onD interior_subset by fastforce
  then show ?thesis
    using assms
    by (intro Cauchy_integral_formula_weak [where k = "{}"]) (auto simp: holomorphic_on_imp_continuous_on)
qed

text\<open> Hence the Cauchy formula for points inside a circle.\<close>

theorem Cauchy_integral_circlepath:
  assumes contf: "continuous_on (cball z r) f" and holf: "f holomorphic_on (ball z r)" and wz: "norm(w-z) < r"
  shows "((\u. f u/(u-w)) has_contour_integral (2 * of_real pi * \ * f w))
         (circlepath z r)"
proof -
  have "r > 0"
    using assms le_less_trans norm_ge_zero by blast
  have "((\u. f u / (u-w)) has_contour_integral (2 * pi) * \ * winding_number (circlepath z r) w * f w)
        (circlepath z r)"
  proof (rule Cauchy_integral_formula_weak [where S = "cball z r" and k = "{}"])
    show "\x. x \ interior (cball z r) - {} \
         f field_differentiable at x"
      using holf holomorphic_on_imp_differentiable_at by auto
    have "w \ sphere z r"
      by simp (metis dist_commute dist_norm not_le order_refl wz)
    then show "path_image (circlepath z r) \ cball z r - {w}"
      using \<open>r > 0\<close> by (auto simp add: cball_def sphere_def)
  qed (use wz in \<open>simp_all add: dist_norm norm_minus_commute contf\<close>)
  then show ?thesis
    by (simp add: winding_number_circlepath assms)
qed

corollary\<^marker>\<open>tag unimportant\<close> Cauchy_integral_circlepath_simple:
  assumes "f holomorphic_on cball z r" "norm(w-z) < r"
  shows "((\u. f u/(u-w)) has_contour_integral (2 * of_real pi * \ * f w))
         (circlepath z r)"
using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath)

subsection\<^marker>\<open>tag unimportant\<close> \<open>General stepping result for derivative formulas\<close>

lemma Cauchy_next_derivative:
  fixes f' :: "complex \ complex"
  defines "h \ \k w u. f' u / (u-w)^k"
  assumes "continuous_on (path_image \) f'"
      and leB: "\t. t \ {0..1} \ norm (vector_derivative \ (at t)) \ B"
      and int: "\w. w \ S - path_image \ \ (h k w has_contour_integral f w) \"
      and k: "k \ 0"
      and "open S"
      and \<gamma>: "valid_path \<gamma>"
      and w: "w \ S - path_image \"
    shows "h (Suc k) w contour_integrable_on \"
      and "(f has_field_derivative (k * contour_integral \ (h (Suc k) w))) (at w)" (is "?thes2")
proof -
  have "open (S - path_image \)" using \open S\ closed_valid_path_image \ by blast
  then obtain d where "d>0" and d: "ball w d \ S - path_image \" using w
    using open_contains_ball by blast
  have [simp]: "\n. cmod (1 + of_nat n) = 1 + of_nat n"
    by (metis norm_of_nat of_nat_Suc)
  have cint: "(\z. (h k x z - h k w z) / (x * k - w * k)) contour_integrable_on \"
    if "x \ w" "cmod (x-w) < d" for x::complex
  proof -
    have "x \ S - path_image \"
      by (metis d dist_commute dist_norm mem_ball subsetD that(2))
    then show ?thesis
      using contour_integrable_diff contour_integrable_div contour_integrable_on_def int w
      by meson
  qed
  then have 1: "\\<^sub>F x in at w. (\z. (h k x z - h k w z) / (x-w) / of_nat k)
                         contour_integrable_on \<gamma>"
    unfolding eventually_at
    by (force intro: exI [where x=d] simp add: \<open>d > 0\<close> dist_norm field_simps)
  have bim_g: "bounded (image f' (path_image \))"
    by (simp add: compact_imp_bounded compact_continuous_image compact_valid_path_image assms)
  then obtain C where "C > 0" and C: "\x. \0 \ x; x \ 1\ \ cmod (f' (\ x)) \ C"
    by (force simp: bounded_pos path_image_def)
  have twom: "\\<^sub>F n in at w.
               \<forall>x\<in>path_image \<gamma>.
                cmod ((inverse (x-n) ^ k - inverse (x-w) ^ k) / (n-w) / k - inverse (x-w) ^ Suc k) < e"
         if "0 < e" for e
  proof -
    have *: "cmod ((inverse (x-u) ^ k - inverse (x-w) ^ k) / ((u-w) * k) - inverse (x-w) ^ Suc k) < e"
            if x: "x \ path_image \" and "u \ w" and uwd: "cmod (u-w) < d/2"
                and uw_less: "cmod (u-w) < e * (d/2) ^ (k+2) / (1 + real k)"
            for u x
    proof -
      define ff where [abs_def]:
        "ff n w =
          (if n = 0 then inverse(x-w)^k
           else if n = 1 then k / (x-w)^(Suc k)
           else (k * of_real(Suc k)) / (x-w)^(k + 2))" for n :: nat and w
      have km1: "\z::complex. z \ 0 \ z ^ (k - Suc 0) = z ^ k / z"
        by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
      have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d/2))"
              if "z \ ball w (d/2)" "i \ 1" for i z
      proof -
        have "z \ path_image \"
          using \<open>x \<in> path_image \<gamma>\<close> d that ball_divide_subset_numeral by blast
        then have xz[simp]: "x \ z" using \x \ path_image \\ by blast
        then have neq: "x * x + z * z \ x * (z * 2)"
          by (blast intro: dest!: sum_sqs_eq)
        with xz have "\v. v \ 0 \ (x * x + z * z) * v \ (x * (z * 2) * v)" by auto
        then have neqq: "\v. v \ 0 \ x * (x * v) + z * (z * v) \ x * (z * (2 * v))"
          by (simp add: algebra_simps)
        show ?thesis using \<open>i \<le> 1\<close>
          apply (simp add: ff_def dist_norm Nat.le_Suc_eq, safe)
          apply (rule derivative_eq_intros | simp add: km1 | simp add: field_simps neq neqq)+
          done
      qed
      { fix a::real and b::real assume ab: "a > 0" "b > 0"
        then have "k * (1 + real k) * (1 / a) \ k * (1 + real k) * (4 / b) \ b \ 4 * a"
          by (subst mult_le_cancel_left_pos)
            (use \<open>k \<noteq> 0\<close> in \<open>auto simp: divide_simps\<close>)
        with ab have "real k * (1 + real k) / a \ (real k * 4 + real k * real k * 4) / b \ b \ 4 * a"
          by (simp add: field_simps)
      } note canc = this
      have ff2: "cmod (ff (Suc 1) v) \ real (k * (k + 1)) / (d/2) ^ (k + 2)"
                if "v \ ball w (d/2)" for v
      proof -
        have lessd: "\z. cmod (\ z - v) < d/2 \ cmod (w - \ z) < d"
          by (metis that norm_minus_commute norm_triangle_half_r dist_norm mem_ball)
        have "d/2 \ cmod (x-v)" using d x that
          using lessd d x unfolding path_image_def
          by (smt (verit, best) dist_norm imageE insert_Diff mem_ball subset_Diff_insert)
        then have "d \ cmod (x-v) * 2"
          by (simp add: field_split_simps)
        then have dpow_le: "d ^ (k+2) \ (cmod (x-v) * 2) ^ (k+2)"
          using \<open>0 < d\<close> order_less_imp_le power_mono by blast
        have "x \ v" using that
          using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
        then show ?thesis
        using \<open>d > 0\<close> apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
        using dpow_le apply (simp add: field_split_simps)
        done
      qed
      have ub: "u \ ball w (d/2)"
        using uwd by (simp add: dist_commute dist_norm)
      have "cmod (inverse (x-u) ^ k - (inverse (x-w) ^ k + of_nat k * (u-w) / ((x-w) * (x-w) ^ k)))
                  \<le> (real k * 4 + real k * real k * 4) * (cmod (u-w) * cmod (u-w)) / (d * (d * (d/2) ^ k))"
        using complex_Taylor [OF _ ff1 ff2 _ ub, of w, simplified]
        by (simp add: ff_def \<open>0 < d\<close>)
      then have "cmod (inverse (x-u) ^ k - (inverse (x-w) ^ k + of_nat k * (u-w) / ((x-w) * (x-w) ^ k)))
                  \<le> (cmod (u-w) * real k) * (1 + real k) * cmod (u-w) / (d/2) ^ (k+2)"
        by (simp add: field_simps)
      then have "cmod (inverse (x-u) ^ k - (inverse (x-w) ^ k + of_nat k * (u-w) / ((x-w) * (x-w) ^ k)))
                 / (cmod (u-w) * real k)
                  \<le> (1 + real k) * cmod (u-w) / (d/2) ^ (k+2)"
        using \<open>k \<noteq> 0\<close> \<open>u \<noteq> w\<close> by (simp add: mult_ac zero_less_mult_iff pos_divide_le_eq)
      also have "\ < e"
        using uw_less \<open>0 < d\<close> by (simp add: mult_ac divide_simps)
      finally have e: "cmod (inverse (x-u)^k - (inverse (x-w)^k + of_nat k * (u-w) / ((x-w) * (x-w)^k)))
                        / cmod ((u-w) * real k)   <   e"
        by (simp add: norm_mult)
      have "x \ u"
        using uwd \<open>0 < d\<close> x d by (force simp: dist_norm ball_def norm_minus_commute)
      show ?thesis
        using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close> \<open>u \<noteq> w\<close> le_less_trans [OF _ e]
        by (simp add: field_simps flip: norm_divide)
    qed
    show ?thesis
      unfolding eventually_at
      apply (rule_tac x = "min (d/2) ((e*(d/2)^(k + 2))/(Suc k))" in exI)
      apply (force simp: \<open>d > 0\<close> dist_norm that simp del: power_Suc intro: *)
      done
  qed
  have 2: "uniform_limit (path_image \) (\x z. (h k x z - h k w z) / (x-w) / k) (h (Suc k) w) (at w)"
    unfolding uniform_limit_iff dist_norm
  proof clarify
    fix e::real
    assume "0 < e"
    have *: "cmod ((h k x (\ u) - h k w (\ u)) / ((x-w) * k) - h (Suc k) w (\ u)) < e"
          if ec: "cmod ((inverse (\ u - x) ^ k - inverse (\ u - w) ^ k) / ((x-w) * k) -
                  inverse (\<gamma> u - w) * inverse (\<gamma> u - w) ^ k) < e / C"
                 and x: "0 \ u" "u \ 1"
               for x u
    proof (cases "(f' (\ u)) = 0")
      case True then show ?thesis by (simp add: \<open>0 < e\<close> h_def)
    next
      case False
      have "cmod ((h k x (\ u) - h k w (\ u)) / ((x-w) * k) - h (Suc k) w (\ u)) =
            cmod (f' (\ u) * ((inverse (\ u - x) ^ k - inverse (\ u - w) ^ k) / ((x-w) * k) -
                             inverse (\<gamma> u - w) * inverse (\<gamma> u - w) ^ k))"
        by (simp add: h_def field_simps)
      also have "\ = cmod (f' (\ u)) *
                       cmod ((inverse (\<gamma> u - x) ^ k - inverse (\<gamma> u - w) ^ k) / ((x-w) * k) -
                             inverse (\<gamma> u - w) * inverse (\<gamma> u - w) ^ k)"
        by (simp add: norm_mult)
      also have "\ < cmod (f' (\ u)) * (e/C)"
        using False mult_strict_left_mono [OF ec] by force
      also have "\ \ e" using C
        by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
      finally show ?thesis .
    qed
    show "\\<^sub>F u in at w.
              \<forall>x\<in>path_image \<gamma>.
               cmod ((h k u x - h k w x) / (u-w) / of_nat k - h (Suc k) w x) < e"
      using twom [OF divide_pos_pos [OF \<open>0 < e\<close> \<open>C > 0\<close>]] *
      unfolding path_image_def h_def
      by (force elim: eventually_mono)
  qed
  show "h (Suc k) w contour_integrable_on \"
    using contour_integral_uniform_limit [OF 1 2 leB \<gamma>] by (simp add: h_def)
  have *: "(\u. contour_integral \ (\x. (h k u x - h k w x) / (u-w) / k))
           \<midarrow>w\<rightarrow> contour_integral \<gamma> (h (Suc k) w)"
    by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
  have **: "contour_integral \ (\x. (h k u x - h k w x) / ((u-w) * k)) =
              (f u - f w) / (u-w) / k"
    if "dist u w < d" for u
  proof -
    have "u \ S - path_image \"
      by (metis subsetD d dist_commute mem_ball that)
    then have "(h k u has_contour_integral f u) \" "(h k w has_contour_integral f w) \"
      using w by (simp_all add: field_simps int)
    then show ?thesis
      using contour_integral_unique has_contour_integral_diff
        has_contour_integral_div by force
  qed
  show ?thes2
    unfolding has_field_derivative_iff
    by (simp add: \<open>k \<noteq> 0\<close> ** Lim_transform_within [OF tendsto_mult_left [OF *] \<open>0 < d\<close>])
qed

lemma Cauchy_next_derivative_circlepath:
  assumes contf: "continuous_on (path_image (circlepath z r)) f"
      and int: "\w. w \ ball z r \ ((\u. f u / (u-w)^k) has_contour_integral g w) (circlepath z r)"
      and k: "k \ 0"
      and w: "w \ ball z r"
    shows "(\u. f u / (u-w)^(Suc k)) contour_integrable_on (circlepath z r)"
           (is "?thes1")
      and "(g has_field_derivative (k * contour_integral (circlepath z r) (\u. f u/(u-w)^(Suc k)))) (at w)"
           (is "?thes2")
proof -
  have "r > 0" using w
    using ball_eq_empty by fastforce
  have wim: "w \ ball z r - path_image (circlepath z r)"
    using w by (auto simp: dist_norm)
  show ?thes1 ?thes2
    by (rule Cauchy_next_derivative [OF contf _ int k open_ball valid_path_circlepath wim, where B = "2 * pi * \r\"];
        auto simp: vector_derivative_circlepath norm_mult)+
qed

text\<open> In particular, the first derivative formula.\<close>

lemma Cauchy_derivative_integral_circlepath:
  assumes contf: "continuous_on (cball z r) f"
      and holf: "f holomorphic_on ball z r"
      and w: "w \ ball z r"
    shows "(\u. f u/(u-w)^2) contour_integrable_on (circlepath z r)"
           (is "?thes1")
      and "(f has_field_derivative (1 / (2 * of_real pi * \) * contour_integral(circlepath z r) (\u. f u / (u-w)^2))) (at w)"
           (is "?thes2")
proof -
  have [simp]: "r \ 0" using w
    using ball_eq_empty by fastforce
  have f: "continuous_on (path_image (circlepath z r)) f"
    by (rule continuous_on_subset [OF contf]) (force simp: cball_def sphere_def)
  have int: "\w. dist z w < r \
                 ((\<lambda>u. f u / (u-w)) has_contour_integral (\<lambda>x. 2 * of_real pi * \<i> * f x) w) (circlepath z r)"
    by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
  show ?thes1
    unfolding power2_eq_square
    using int Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1]
    by fastforce
  have "((\x. 2 * of_real pi * \ * f x) has_field_derivative contour_integral (circlepath z r) (\u. f u / (u-w)^2)) (at w)"
    unfolding power2_eq_square
    using int Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\x. 2 * of_real pi * \ * f x"]
    by fastforce
  then have fder: "(f has_field_derivative contour_integral (circlepath z r) (\u. f u / (u-w)^2) / (2 * of_real pi * \)) (at w)"
    by (rule DERIV_cdivide [where f = "\x. 2 * of_real pi * \ * f x" and c = "2 * of_real pi * \", simplified])
  show ?thes2
    by simp (rule fder)
qed

subsection\<open>Existence of all higher derivatives\<close>

proposition derivative_is_holomorphic:
  assumes "open S"
      and fder: "\z. z \ S \ (f has_field_derivative f' z) (at z)"
    shows "f' holomorphic_on S"
proof -
  have *: "\h. (f' has_field_derivative h) (at z)" if "z \ S" for z
  proof -
    obtain r where "r > 0" and r: "cball z r \ S"
      using open_contains_cball \<open>z \<in> S\<close> \<open>open S\<close> by blast
    then have holf_cball: "f holomorphic_on cball z r"
      unfolding holomorphic_on_def
      using field_differentiable_at_within field_differentiable_def fder by fastforce
    then have "continuous_on (path_image (circlepath z r)) f"
      using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
    then have contfpi: "continuous_on (path_image (circlepath z r)) (\x. 1/(2 * of_real pi*\) * f x)"
      by (auto intro: continuous_intros)+
    have contf_cball: "continuous_on (cball z r) f" using holf_cball
      by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
    have holf_ball: "f holomorphic_on ball z r" using holf_cball
      using ball_subset_cball holomorphic_on_subset by blast
    { fix w  assume w: "w \ ball z r"
      have intf: "(\u. f u / (u-w)\<^sup>2) contour_integrable_on circlepath z r"
        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
      have fder': "(f has_field_derivative 1 / (2 * of_real pi * \) * contour_integral (circlepath z r) (\u. f u / (u-w)\<^sup>2))
                  (at w)"
        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
      have f'_eq: "f' w = contour_integral (circlepath z r) (\<lambda>u. f u / (u-w)\<^sup>2) / (2 * of_real pi * \<i>)"
        using fder' ball_subset_cball r w by (force intro: DERIV_unique [OF fder])
      have "((\u. f u / (u-w)\<^sup>2 / (2 * of_real pi * \)) has_contour_integral
                contour_integral (circlepath z r) (\<lambda>u. f u / (u-w)\<^sup>2) / (2 * of_real pi * \<i>))
                (circlepath z r)"
        by (rule has_contour_integral_div [OF has_contour_integral_integral [OF intf]])
      then have "((\u. f u / (2 * of_real pi * \ * (u-w)\<^sup>2)) has_contour_integral
                contour_integral (circlepath z r) (\<lambda>u. f u / (u-w)\<^sup>2) / (2 * of_real pi * \<i>))
                (circlepath z r)"
        by (simp add: algebra_simps)
      then have "((\u. f u / (2 * of_real pi * \ * (u-w)\<^sup>2)) has_contour_integral f' w) (circlepath z r)"
        by (simp add: f'_eq)
    } note * = this
    show ?thesis
      using Cauchy_next_derivative_circlepath [OF contfpi, of 2 f'] \0 < r\ *
      using centre_in_ball mem_ball by force
  qed
  show ?thesis
    by (simp add: holomorphic_on_open [OF \<open>open S\<close>] *)
qed

lemma holomorphic_deriv [holomorphic_intros]:
  "\f holomorphic_on S; open S\ \ (deriv f) holomorphic_on S"
  by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)

lemma holomorphic_deriv_compose:
  assumes g: "g holomorphic_on B" and f: "f holomorphic_on A" and "f ` A \ B" "open B"
  shows   "(\x. deriv g (f x)) holomorphic_on A"
  using holomorphic_on_compose_gen [OF f holomorphic_deriv[OF g]] assms
  by (auto simp: o_def)

lemma analytic_deriv [analytic_intros]: "f analytic_on S \ (deriv f) analytic_on S"
  using analytic_on_holomorphic holomorphic_deriv by auto

lemma holomorphic_higher_deriv [holomorphic_intros]: "\f holomorphic_on S; open S\ \ (deriv ^^ n) f holomorphic_on S"
  by (induction n) (auto simp: holomorphic_deriv)

lemma analytic_higher_deriv [analytic_intros]: "f analytic_on S \ (deriv ^^ n) f analytic_on S"
  unfolding analytic_on_def using holomorphic_higher_deriv by blast

lemma has_field_derivative_higher_deriv:
     "\f holomorphic_on S; open S; x \ S\
      \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
  using holomorphic_derivI holomorphic_higher_deriv by fastforce

lemma higher_deriv_cmult:
  assumes "f holomorphic_on A" "x \ A" "open A"
  shows   "(deriv ^^ j) (\x. c * f x) x = c * (deriv ^^ j) f x"
  using assms
proof (induction j arbitrary: f x)
  case (Suc j f x)
  have "deriv ((deriv ^^ j) (\x. c * f x)) x = deriv (\x. c * (deriv ^^ j) f x) x"
    using eventually_nhds_in_open[of A x] assms(2,3) Suc.prems
    by (intro deriv_cong_ev refl) (auto elim!: eventually_mono simp: Suc.IH)
  also have "\ = c * deriv ((deriv ^^ j) f) x" using Suc.prems assms(2,3)
    by (intro deriv_cmult holomorphic_on_imp_differentiable_at holomorphic_higher_deriv) auto
  finally show ?case by simp
qed simp_all

lemma higher_deriv_cmult':
  assumes "f analytic_on {x}"
  shows   "(deriv ^^ j) (\x. c * f x) x = c * (deriv ^^ j) f x"
  using assms higher_deriv_cmult[of f _ x j c] assms
  using analytic_at_two by blast

lemma deriv_cmult':
  assumes "f analytic_on {x}"
  shows   "deriv (\x. c * f x) x = c * deriv f x"
  using higher_deriv_cmult'[OF assms, of 1 c] by simp

lemma analytic_derivI:
  assumes "f analytic_on {z}"
  shows   "(f has_field_derivative (deriv f z)) (at z within A)"
  using assms holomorphic_derivI[of f _ z] analytic_at by blast

lemma deriv_compose_analytic:
  fixes f g :: "complex \ complex"
  assumes "f analytic_on {g z}" "g analytic_on {z}"
  shows "deriv (\x. f (g x)) z = deriv f (g z) * deriv g z"
proof -
  have "((f \ g) has_field_derivative (deriv f (g z) * deriv g z)) (at z)"
    by (intro DERIV_chain analytic_derivI assms)
  thus ?thesis
    by (auto intro!: DERIV_imp_deriv simp add: o_def)
qed

lemma valid_path_compose_holomorphic:
  assumes "valid_path g" "f holomorphic_on S" and "open S" "path_image g \ S"
  shows "valid_path (f \ g)"
  by (meson assms holomorphic_deriv holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at
      holomorphic_on_subset subsetD valid_path_compose)

lemma valid_path_compose_analytic:
  assumes "valid_path g" and holo:"f analytic_on S" and "path_image g \ S"
  shows "valid_path (f \ g)"
proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
  fix x assume "x \ path_image g"
  then show "f field_differentiable at x"
    using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
next
  show "continuous_on (path_image g) (deriv f)"
    by (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic analytic_intros
              analytic_on_subset[OF holo] assms)
qed

lemma analytic_on_deriv [analytic_intros]:
  assumes "f analytic_on g ` A"
  assumes "g analytic_on A"
  shows   "(\x. deriv f (g x)) analytic_on A"
proof -
  have "(deriv f \ g) analytic_on A"
    by (rule analytic_on_compose_gen[OF assms(2) analytic_deriv[OF assms(1)]]) auto
  thus ?thesis
    by (simp add: o_def)
qed

lemma contour_integral_comp_analyticW:
  assumes "f analytic_on s" "valid_path \" "path_image \ \ s"
  shows "contour_integral (f \ \) g = contour_integral \ (\w. deriv f w * g (f w))"
proof -
  obtain spikes where "finite spikes" and \<gamma>_diff: "\<gamma> C1_differentiable_on {0..1} - spikes"
    using \<open>valid_path \<gamma>\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
  show "contour_integral (f \ \) g
      = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"
    unfolding contour_integral_integral
  proof (rule integral_spike[rule_format,OF negligible_finite[OF \<open>finite spikes\<close>]])
    fix t::real assume t:"t \ {0..1} - spikes"
    then have "\ differentiable at t"
      using \<gamma>_diff unfolding C1_differentiable_on_eq by auto
    moreover have "f field_differentiable at (\ t)"
    proof -
      have "\ t \ s" using t assms unfolding path_image_def by auto
      thus ?thesis
        using \<open>f analytic_on s\<close>  analytic_on_imp_differentiable_at by blast
    qed
    ultimately show "deriv f (\ t) * g (f (\ t)) * vector_derivative \ (at t) =
         g ((f \<circ> \<gamma>) t) * vector_derivative (f \<circ> \<gamma>) (at t)"
      by (subst vector_derivative_chain_at_general) (simp_all add:field_simps)
  qed
qed

subsection\<open>Morera's theorem\<close>

lemma Morera_local_triangle_ball:
  assumes "\z. z \ S
          \<Longrightarrow> \<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
                    (\<forall>b c. closed_segment b c \<subseteq> ball a e
                           \<longrightarrow> contour_integral (linepath a b) f +
                               contour_integral (linepath b c) f +
                               contour_integral (linepath c a) f = 0)"
  shows "f analytic_on S"
proof -
  { fix z  assume "z \ S"
    with assms obtain e a where
            "0 < e" and z: "z \ ball a e" and contf: "continuous_on (ball a e) f"
        and 0: "\b c. closed_segment b c \ ball a e
                      \<Longrightarrow> contour_integral (linepath a b) f +
                          contour_integral (linepath b c) f +
                          contour_integral (linepath c a) f = 0"
      by blast
    have az: "dist a z < e" using mem_ball z by blast
    have "\e>0. f holomorphic_on ball z e"
    proof (intro exI conjI)
      show "f holomorphic_on ball z (e - dist a z)"
      proof (rule holomorphic_on_subset)
        show "ball z (e - dist a z) \ ball a e"
          by (simp add: dist_commute ball_subset_ball_iff)
        have sub_ball: "\y. dist a y < e \ closed_segment a y \ ball a e"
          by (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
        show "f holomorphic_on ball a e"
          using triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a]
            derivative_is_holomorphic[OF open_ball]
          by (force simp add: 0 \<open>0 < e\<close> sub_ball)
      qed
    qed (simp add: az)
  }
  then show ?thesis
    by (simp add: analytic_on_def)
qed

lemma Morera_local_triangle:
  assumes "\z. z \ S
          \<Longrightarrow> \<exists>t. open t \<and> z \<in> t \<and> continuous_on t f \<and>
                  (\<forall>a b c. convex hull {a,b,c} \<subseteq> t
                              \<longrightarrow> contour_integral (linepath a b) f +
                                  contour_integral (linepath b c) f +
                                  contour_integral (linepath c a) f = 0)"
  shows "f analytic_on S"
proof -
  { fix z  assume "z \ S"
    with assms obtain t where
            "open t" and z: "z \ t" and contf: "continuous_on t f"
        and 0: "\a b c. convex hull {a,b,c} \ t
                      \<Longrightarrow> contour_integral (linepath a b) f +
                          contour_integral (linepath b c) f +
                          contour_integral (linepath c a) f = 0"
      by force
    then obtain e where "e>0" and e: "ball z e \ t"
      using open_contains_ball by blast
    have [simp]: "continuous_on (ball z e) f" using contf
      using continuous_on_subset e by blast
    have eq0: "\b c. closed_segment b c \ ball z e \
                         contour_integral (linepath z b) f +
                         contour_integral (linepath b c) f +
                         contour_integral (linepath c z) f = 0"
      by (meson 0 z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
    have "\e a. 0 < e \ z \ ball a e \ continuous_on (ball a e) f \
                (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
                       contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
      using \<open>e > 0\<close> eq0 by force
  }
  then show ?thesis
    by (simp add: Morera_local_triangle_ball)
qed

proposition Morera_triangle:
    "\continuous_on S f; open S;
      \<And>a b c. convex hull {a,b,c} \<subseteq> S
              \<longrightarrow> contour_integral (linepath a b) f +
                  contour_integral (linepath b c) f +
                  contour_integral (linepath c a) f = 0\<rbrakk>
     \<Longrightarrow> f analytic_on S"
  using Morera_local_triangle by blast

subsection\<open>Combining theorems for higher derivatives including Leibniz rule\<close>

lemma higher_deriv_linear [simp]:
    "(deriv ^^ n) (\w. c*w) = (\z. if n = 0 then c*z else if n = 1 then c else 0)"
  by (induction n) auto

lemma higher_deriv_const [simp]: "(deriv ^^ n) (\w. c) = (\w. if n=0 then c else 0)"
  by (induction n) auto

lemma higher_deriv_ident [simp]:
     "(deriv ^^ n) (\w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
proof (induction n)
  case (Suc n)
  then show ?case by (metis higher_deriv_linear lambda_one)
qed auto

lemma higher_deriv_id [simp]:
     "(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)"
  by (simp add: id_def)

lemma has_complex_derivative_funpow_1:
     "\(f has_field_derivative 1) (at z); f z = z\ \ (f^^n has_field_derivative 1) (at z)"
proof (induction n)
  case 0
  then show ?case
    by (simp add: id_def)
next
  case (Suc n)
  then show ?case
    by (metis DERIV_chain funpow_Suc_right mult.right_neutral)
qed

lemma higher_deriv_uminus:
  assumes "f holomorphic_on S" "open S" and z: "z \ S"
    shows "(deriv ^^ n) (\w. -(f w)) z = - ((deriv ^^ n) f z)"
using z
proof (induction n arbitrary: z)
  case 0 then show ?case by simp
next
  case (Suc n z)
  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
    using Suc.prems assms has_field_derivative_higher_deriv by auto
  have "\x. x \ S \ - (deriv ^^ n) f x = (deriv ^^ n) (\w. - f w) x"
    by (auto simp add: Suc)
  then have "((deriv ^^ n) (\w. - f w) has_field_derivative - deriv ((deriv ^^ n) f) z) (at z)"
    using  has_field_derivative_transform_within_open [of "\w. -((deriv ^^ n) f w)"]
    using "*" DERIV_minus Suc.prems \<open>open S\<close> by blast
  then show ?case
    by (simp add: DERIV_imp_deriv)
qed

lemma higher_deriv_add:
  fixes z::complex
  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \ S"
    shows "(deriv ^^ n) (\w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
using z
proof (induction n arbitrary: z)
  case 0 then show ?case by simp
next
  case (Suc n z)
  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
          "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
    using Suc.prems assms has_field_derivative_higher_deriv by auto
  have "\x. x \ S \ (deriv ^^ n) f x + (deriv ^^ n) g x = (deriv ^^ n) (\w. f w + g w) x"
    by (auto simp add: Suc)
  then have "((deriv ^^ n) (\w. f w + g w) has_field_derivative
        deriv ((deriv ^^ n) f) z + deriv ((deriv ^^ n) g) z) (at z)"
    using  has_field_derivative_transform_within_open [of "\w. (deriv ^^ n) f w + (deriv ^^ n) g w"]
    using "*" Deriv.field_differentiable_add Suc.prems \<open>open S\<close> by blast
  then show ?case
    by (simp add: DERIV_imp_deriv)
qed

lemma higher_deriv_diff:
  fixes z::complex
  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" "z \ S"
    shows "(deriv ^^ n) (\w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
  unfolding diff_conv_add_uminus higher_deriv_add
  using assms higher_deriv_add higher_deriv_uminus holomorphic_on_minus by presburger

lemma Suc_choose: "Suc n choose k = (n choose k) + (if k = 0 then 0 else (n choose (k-1)))"
  by (cases k) simp_all

lemma higher_deriv_mult:
  fixes z::complex
  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \ S"
    shows "(deriv ^^ n) (\w. f w * g w) z =
           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n-i)) g z)"
using z
proof (induction n arbitrary: z)
  case 0 then show ?case by simp
next
  case (Suc n z)
  have *: "\n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
          "\n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
    using Suc.prems assms has_field_derivative_higher_deriv by auto
  have sumeq: "(\i = 0..n.
               of_nat (n choose i) * (deriv ((deriv ^^ i) f) z * (deriv ^^ (n-i)) g z + deriv ((deriv ^^ (n-i)) g) z * (deriv ^^ i) f z)) =
            g z * deriv ((deriv ^^ n) f) z + (\<Sum>i = 0..n. (deriv ^^ i) f z * (of_nat (Suc n choose i) * (deriv ^^ (Suc n - i)) g z))"
    apply (simp add: Suc_choose algebra_simps sum.distrib)
    apply (subst (4) sum_Suc_reindex)
    apply (auto simp: algebra_simps Suc_diff_le intro: sum.cong)
    done
  have "((deriv ^^ n) (\w. f w * g w) has_field_derivative
         (\<Sum>i = 0..Suc n. (Suc n choose i) * (deriv ^^ i) f z * (deriv ^^ (Suc n - i)) g z))
        (at z)"
    apply (rule has_field_derivative_transform_within_open
        [of "\w. (\i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n-i)) g w)" _ _ S])
       apply (simp add: algebra_simps)
       apply (rule derivative_eq_intros | simp)+
           apply (auto intro: DERIV_mult * \<open>open S\<close> Suc.prems Suc.IH [symmetric])
    by (metis (no_types, lifting) mult.commute sum.cong sumeq)
  then show ?case
    unfolding funpow.simps o_apply
    by (simp add: DERIV_imp_deriv)
qed

lemma higher_deriv_transform_within_open:
  fixes z::complex
  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" and z: "z \ S"
      and fg: "\w. w \ S \ f w = g w"
    shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
using z
by (induction i arbitrary: z)
   (auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)

lemma higher_deriv_compose_linear':
  fixes z::complex
  assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \ S"
      and fg: "\w. w \ S \ u*w + c \ T"
    shows "(deriv ^^ n) (\w. f (u*w + c)) z = u^n * (deriv ^^ n) f (u*z + c)"
using z
proof (induction n arbitrary: z)
  case 0 then show ?case by simp
next
  case (Suc n z)
  have holo0: "f holomorphic_on (\w. u * w+c) ` S"
    by (meson fg f holomorphic_on_subset image_subset_iff)
  have holo2: "(deriv ^^ n) f holomorphic_on (\w. u * w+c) ` S"
    by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
  have holo3: "(\z. u ^ n * (deriv ^^ n) f (u * z+c)) holomorphic_on S"
    by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros)
  have "(\w. u * w+c) holomorphic_on S" "f holomorphic_on (\w. u * w+c) ` S"
    by (rule holo0 holomorphic_intros)+
  then have holo1: "(\w. f (u * w+c)) holomorphic_on S"
    by (rule holomorphic_on_compose [where g=f, unfolded o_def])
  have "deriv ((deriv ^^ n) (\w. f (u * w+c))) z = deriv (\z. u^n * (deriv ^^ n) f (u*z+c)) z"
  proof (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems])
    show "(deriv ^^ n) (\w. f (u * w+c)) holomorphic_on S"
      by (rule holomorphic_higher_deriv [OF holo1 S])
  qed (simp add: Suc.IH)
  also have "\ = u^n * deriv (\z. (deriv ^^ n) f (u * z+c)) z"
  proof -
    have "(deriv ^^ n) f analytic_on T"
      by (simp add: analytic_on_open f holomorphic_higher_deriv T)
    then have "(\w. (deriv ^^ n) f (u * w+c)) analytic_on S"
        using holomorphic_on_compose[OF _ holo2] \<open>(\<lambda>w. u * w+c) holomorphic_on S\<close>
        by (simp add: S analytic_on_open o_def)
    then show ?thesis
      by (intro deriv_cmult analytic_on_imp_differentiable_at [OF _ Suc.prems])
  qed
  also have "\ = u * u ^ n * deriv ((deriv ^^ n) f) (u * z+c)"
  proof -
    have "(deriv ^^ n) f field_differentiable at (u * z+c)"
      using Suc.prems T f fg holomorphic_higher_deriv holomorphic_on_imp_differentiable_at by blast
    then show ?thesis
      by (simp add: deriv_compose_linear')
  qed
  finally show ?case
    by simp
qed

lemma higher_deriv_compose_linear:
  fixes z::complex
  assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \ S"
      and fg: "\w. w \ S \ u * w \ T"
    shows "(deriv ^^ n) (\w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
  using higher_deriv_compose_linear' [where c=0] assms by simp

lemma higher_deriv_add_at:
  assumes "f analytic_on {z}" "g analytic_on {z}"
    shows "(deriv ^^ n) (\w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
  using analytic_at_two assms higher_deriv_add by blast

lemma higher_deriv_diff_at:
  assumes "f analytic_on {z}" "g analytic_on {z}"
    shows "(deriv ^^ n) (\w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
  using analytic_at_two assms higher_deriv_diff by blast

lemma higher_deriv_uminus_at:
   "f analytic_on {z} \ (deriv ^^ n) (\w. -(f w)) z = - ((deriv ^^ n) f z)"
  using higher_deriv_uminus by (auto simp: analytic_at)

lemma higher_deriv_mult_at:
  assumes "f analytic_on {z}" "g analytic_on {z}"
    shows "(deriv ^^ n) (\w. f w * g w) z =
           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n-i)) g z)"
  using analytic_at_two assms higher_deriv_mult by blast

text\<open> Nonexistence of isolated singularities and a stronger integral formula.\<close>

proposition no_isolated_singularity:
  fixes z::complex
  assumes f: "continuous_on S f" and holf: "f holomorphic_on (S-K)" and S: "open S" and K: "finite K"
    shows "f holomorphic_on S"
proof -
  { fix z
    assume "z \ S" and cdf: "\x. x \ S - K \ f field_differentiable at x"
    have "f field_differentiable at z"
    proof (cases "z \ K")
      case False then show ?thesis by (blast intro: cdf \<open>z \<in> S\<close>)
    next
      case True
      with finite_set_avoid [OF K, of z]
      obtain d where "d>0" and d: "\x. \x\K; x \ z\ \ d \ dist z x"
        by blast
      obtain e where "e>0" and e: "ball z e \ S"
        using  S \<open>z \<in> S\<close> by (force simp: open_contains_ball)
      have fde: "continuous_on (ball z (min d e)) f"
        by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
      have cont: "{a,b,c} \ ball z (min d e) \ continuous_on (convex hull {a, b, c}) f" for a b c
        by (simp add: hull_minimal continuous_on_subset [OF fde])
      have fd: "\{a,b,c} \ ball z (min d e); x \ interior (convex hull {a, b, c}) - K\
            \<Longrightarrow> f field_differentiable at x" for a b c x
        by (metis cdf Diff_iff Int_iff ball_min_Int subsetD convex_ball e interior_mono interior_subset subset_hull)
      obtain g where "\w. w \ ball z (min d e) \ (g has_field_derivative f w) (at w within ball z (min d e))"
        apply (rule contour_integral_convex_primitive
                     [OF convex_ball fde Cauchy_theorem_triangle_cofinite [OF _ K]])
        using cont fd by auto
      then have "f holomorphic_on ball z (min d e)"
        by (metis open_ball at_within_open derivative_is_holomorphic)
      then show ?thesis
        unfolding holomorphic_on_def
        by (metis open_ball \<open>0 < d\<close> \<open>0 < e\<close> at_within_open centre_in_ball min_less_iff_conj)
    qed
  }
  with holf S K show ?thesis
    by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
qed

lemma no_isolated_singularity':
  fixes z::complex
  assumes f: "\z. z \ K \ (f \ f z) (at z within S)"
      and holf: "f holomorphic_on (S-K)" and S: "open S" and K: "finite K"
    shows "f holomorphic_on S"
proof (rule no_isolated_singularity[OF _ assms(2-)])
  have "continuous_on (S-K) f"
    using holf holomorphic_on_imp_continuous_on by auto
  then show "continuous_on S f"
    by (metis Diff_iff K S at_within_open continuous_on_eq_continuous_at
        continuous_within f finite_imp_closed open_Diff)
qed

proposition Cauchy_integral_formula_convex:
  assumes S: "convex S" and K: "finite K" and contf: "continuous_on S f"
    and fcd: "(\x. x \ interior S - K \ f field_differentiable at x)"
    and z: "z \ interior S" and vpg: "valid_path \"
    and pasz: "path_image \ \ S - {z}" and loop: "pathfinish \ = pathstart \"
  shows "((\w. f w / (w-z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \"
proof -
  have *: "\x. x \ interior S \ f field_differentiable at x"
    unfolding holomorphic_on_open [symmetric] field_differentiable_def
    using no_isolated_singularity [where S = "interior S"]
    by (meson K contf continuous_on_subset fcd field_differentiable_def open_interior
        has_field_derivative_at_within holomorphic_derivI holomorphic_onI interior_subset)
  show ?thesis
    by (rule Cauchy_integral_formula_weak [OF S finite.emptyI contf]) (use * assms in auto)
qed

text\<open> Formula for higher derivatives.\<close>

lemma Cauchy_has_contour_integral_higher_derivative_circlepath:
  assumes contf: "continuous_on (cball z r) f"
      and holf: "f holomorphic_on ball z r"
      and w: "w \ ball z r"
    shows "((\u. f u / (u-w) ^ (Suc k)) has_contour_integral ((2 * pi * \) / (fact k) * (deriv ^^ k) f w))
           (circlepath z r)"
using w
proof (induction k arbitrary: w)
  case 0 then show ?case
    using assms by (auto simp: Cauchy_integral_circlepath dist_commute dist_norm)
next
  case (Suc k)
  have [simp]: "r > 0" using w
    using ball_eq_empty by fastforce
  have f: "continuous_on (path_image (circlepath z r)) f"
    by (rule continuous_on_subset [OF contf]) (force simp: cball_def sphere_def less_imp_le)
  obtain X where X: "((\u. f u / (u-w) ^ Suc (Suc k)) has_contour_integral X) (circlepath z r)"
    using Cauchy_next_derivative_circlepath(1) [OF f Suc.IH _ Suc.prems]
    by (auto simp: contour_integrable_on_def)
  then have con: "contour_integral (circlepath z r) ((\u. f u / (u-w) ^ Suc (Suc k))) = X"
    by (rule contour_integral_unique)
  have "\n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
    using Suc.prems assms has_field_derivative_higher_deriv by auto
  then have dnf_diff: "\n. (deriv ^^ n) f field_differentiable (at w)"
    by (force simp: field_differentiable_def)
  have "deriv (\w. complex_of_real (2 * pi) * \ / (fact k) * (deriv ^^ k) f w) w =
          of_nat (Suc k) * contour_integral (circlepath z r) (\<lambda>u. f u / (u-w) ^ Suc (Suc k))"
    by (force intro!: DERIV_imp_deriv Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
  also have "\ = of_nat (Suc k) * X"
    by (simp only: con)
  finally have "deriv (\w. ((2 * pi) * \ / (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
  then have "((2 * pi) * \ / (fact k)) * deriv (\w. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
    by (metis deriv_cmult dnf_diff)
  then have "deriv (\w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \ / (fact k))"
    by (simp add: field_simps)
  then show ?case
  using of_nat_eq_0_iff X by fastforce
qed

lemma Cauchy_higher_derivative_integral_circlepath:
  assumes contf: "continuous_on (cball z r) f"
      and holf: "f holomorphic_on ball z r"
      and w: "w \ ball z r"
    shows "(\u. f u / (u-w)^(Suc k)) contour_integrable_on (circlepath z r)"
           (is "?thes1")
      and "(deriv ^^ k) f w = (fact k) / (2 * pi * \) * contour_integral(circlepath z r) (\u. f u/(u-w)^(Suc k))"
           (is "?thes2")
proof -
  have *: "((\u. f u / (u-w) ^ Suc k) has_contour_integral (2 * pi) * \ / (fact k) * (deriv ^^ k) f w)
           (circlepath z r)"
    using Cauchy_has_contour_integral_higher_derivative_circlepath [OF assms]
    by simp
  show ?thes1 using *
    using contour_integrable_on_def by blast
  show ?thes2
    unfolding contour_integral_unique [OF *] by (simp add: field_split_simps)
qed

corollary Cauchy_contour_integral_circlepath:
  assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r"
  shows "contour_integral(circlepath z r) (\u. f u/(u-w)^(Suc k)) = (2 * pi * \) * (deriv ^^ k) f w / (fact k)"
  by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])

lemma Cauchy_contour_integral_circlepath_2:
  assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r"
    shows "contour_integral(circlepath z r) (\u. f u/(u-w)^2) = (2 * pi * \) * deriv f w"
  using Cauchy_contour_integral_circlepath [OF assms, of 1]
  by (simp add: power2_eq_square)

subsection\<open>A holomorphic function is analytic, i.e. has local power series\<close>

theorem holomorphic_power_series:
  assumes holf: "f holomorphic_on ball z r"
      and w: "w \ ball z r"
    shows "((\n. (deriv ^^ n) f z / (fact n) * (w-z)^n) sums f w)"
proof -
  \<comment> \<open>Replacing \<^term>\<open>r\<close> and the original (weak) premises with stronger ones\<close>
  obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \ ball z r"
  proof
    have "cball z ((r + dist w z) / 2) \ ball z r"
      using w by (simp add: dist_commute field_sum_of_halves subset_eq)
    then show "f holomorphic_on cball z ((r + dist w z) / 2)"
      by (rule holomorphic_on_subset [OF holf])
    have "r > 0"
      by (metis w dist_norm mem_ball norm_ge_zero not_less_iff_gr_or_eq order_less_le_trans)
    then show "0 < (r + dist w z) / 2"
      by simp (use zero_le_dist [of w z] in linarith)
  qed (use w in \<open>auto simp: dist_commute\<close>)
  then have holf: "f holomorphic_on ball z r"
    using ball_subset_cball holomorphic_on_subset by blast
  have contf: "continuous_on (cball z r) f"
    by (simp add: holfc holomorphic_on_imp_continuous_on)
  have cint: "\k. (\u. f u / (u-z) ^ Suc k) contour_integrable_on circlepath z r"
    by (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf]) (simp add: \<open>0 < r\<close>)
  obtain B where "0 < B" and B: "\u. u \ cball z r \ norm(f u) \ B"
    by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
  obtain k where k: "0 < k" "k \ r" and wz_eq: "norm(w-z) = r - k"
             and kle: "\u. norm(u-z) = r \ k \ norm(u-w)"
  proof
    show "\u. cmod (u-z) = r \ r - dist z w \ cmod (u-w)"
      by (metis add_diff_eq diff_add_cancel dist_norm norm_diff_ineq)
  qed (use w in \<open>auto simp: dist_norm norm_minus_commute\<close>)
  have ul: "uniform_limit (sphere z r) (\n x. (\kx. f x / (x-w)) sequentially"
    unfolding uniform_limit_iff dist_norm
  proof clarify
    fix e::real
    assume "0 < e"
    have rr: "0 \ (r-k) / r" "(r-k) / r < 1" using k by auto
    obtain n where n: "((r-k) / r) ^ n < e / B * k"
      using real_arch_pow_inv [of "e/B*k" "(r-k)/r"] \<open>0 < e\<close> \<open>0 < B\<close> k by force
    have "norm ((\k
         if "n \ N" and r: "r = dist z u" for N u
    proof -
      have N: "((r-k) / r) ^ N < e / B * k"
        using le_less_trans [OF power_decreasing n]
        using \<open>n \<le> N\<close> k by auto
      have u [simp]: "(u \ z) \ (u \ w)"
        using \<open>0 < r\<close> r w by auto
      have wzu_not1: "(w-z) / (u-z) \ 1"
        by (metis (no_types) dist_norm divide_eq_1_iff less_irrefl mem_ball norm_minus_commute r w)
      have "norm ((\k
            = norm ((\<Sum>k<N. (((w-z) / (u-z)) ^ k)) * f u * (u-w) / (u-z) - f u)"
        unfolding sum_distrib_right sum_divide_distrib power_divide by (simp add: algebra_simps)
      also have "\ = norm ((((w-z) / (u-z)) ^ N - 1) * (u-w) / (((w-z) / (u-z) - 1) * (u-z)) - 1) * norm (f u)"
        using \<open>0 < B\<close>
        apply (simp add: geometric_sum [OF wzu_not1] flip: norm_mult)
        apply (simp add: field_simps)
        done
      also have "\ = norm ((u-z) ^ N * (w-u) - ((w-z) ^ N - (u-z) ^ N) * (u-w)) / (r ^ N * norm (u-w)) * norm (f u)"
        using \<open>0 < r\<close> r by (simp add: divide_simps norm_mult norm_divide norm_power dist_norm norm_minus_commute)
      also have "\ = norm ((w-z) ^ N * (w-u)) / (r ^ N * norm (u-w)) * norm (f u)"
        by (simp add: algebra_simps)
      also have "\ = norm (w-z) ^ N * norm (f u) / r ^ N"
        by (simp add: norm_mult norm_power norm_minus_commute)
      also have "\ \ (((r-k)/r)^N) * B"
        using \<open>0 < r\<close> w k
        by (simp add: B divide_simps mult_mono r wz_eq)
      also have "\ < e * k"
        using \<open>0 < B\<close> N by (simp add: divide_simps)
      also have "\ \ e * norm (u-w)"
        using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm)
      finally show ?thesis
        by (simp add: field_split_simps norm_divide del: power_Suc)
    qed
    with \<open>0 < r\<close> show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>sphere z r.
                norm ((\<Sum>k<n. (w-z) ^ k * (f x / (x-z) ^ Suc k)) - f x / (x-w)) < e"
      by (auto simp: mult_ac less_imp_le eventually_sequentially Ball_def)
  qed
  have \<section>: "\<And>x k. k\<in> {..<x} \<Longrightarrow>
           (\<lambda>u. (w-z) ^ k * (f u / (u-z) ^ Suc k)) contour_integrable_on circlepath z r"
    using contour_integrable_lmul [OF cint, of "(w-z) ^ a" for a] by (simp add: field_simps)
  have eq: "\n.
             (\<Sum>k<n. contour_integral (circlepath z r) (\<lambda>u. f u / (u-z) ^ Suc k) * (w-z) ^ k) =
             contour_integral (circlepath z r) (\<lambda>u. \<Sum>k<n. (w-z) ^ k * (f u / (u-z) ^ Suc k))"
    apply (subst contour_integral_sum)
    apply (simp_all only: \<section> finite_lessThan contour_integral_lmul cint algebra_simps)
    done
  have "\u k. k \ {.. (\x. f x / (x-z) ^ Suc k) contour_integrable_on circlepath z r"
    using \<open>0 < r\<close> by (force intro!: Cauchy_higher_derivative_integral_circlepath [OF contf holf])
  then have "\u. (\y. \k
    by (intro contour_integrable_sum contour_integrable_lmul, simp)
  then have "(\k. contour_integral (circlepath z r) (\u. f u/(u-z)^(Suc k)) * (w-z)^k)
        sums contour_integral (circlepath z r) (\<lambda>u. f u/(u-w))"
    unfolding sums_def eq
    using \<open>0 < r\<close> contour_integral_uniform_limit_circlepath [OF eventuallyI ul]
    by fastforce
  then have "(\k. contour_integral (circlepath z r) (\u. f u/(u-z)^(Suc k)) * (w-z)^k)
             sums (2 * of_real pi * \<i> * f w)"
    using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
  then have "(\k. contour_integral (circlepath z r) (\u. f u / (u-z) ^ Suc k) * (w-z)^k / (\ * (of_real pi * 2)))
            sums ((2 * of_real pi * \<i> * f w) / (\<i> * (complex_of_real pi * 2)))"
    by (rule sums_divide)
  then have "(\n. (w-z) ^ n * contour_integral (circlepath z r) (\u. f u / (u-z) ^ Suc n) / (\ * (of_real pi * 2)))
            sums f w"
    by (simp add: field_simps)
  then show ?thesis
    by (simp add: field_simps \<open>0 < r\<close> Cauchy_higher_derivative_integral_circlepath [OF contf holf])
qed

subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra\<close>

text\<open> These weak Liouville versions don't even need the derivative formula.\<close>

lemma Liouville_weak_0:
  assumes holf: "f holomorphic_on UNIV" and inf: "(f \ 0) at_infinity"
    shows "f z = 0"
proof (rule ccontr)
  assume fz: "f z \ 0"
  with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
  obtain B where B: "\x. B \ cmod x \ norm (f x) * 2 < cmod (f z)"
    by (auto simp: dist_norm)
  define R where "R = 1 + \B\ + norm z"
  have "R > 0"
    unfolding R_def by (smt (verit) norm_ge_zero)
  have *: "((\u. f u / (u-z)) has_contour_integral 2 * complex_of_real pi * \ * f z) (circlepath z R)"
    using continuous_on_subset holf  holomorphic_on_subset \<open>0 < R\<close>
    by (force intro: holomorphic_on_imp_continuous_on Cauchy_integral_circlepath)
  have "cmod (x-z) = R \ cmod (f x) * 2 < cmod (f z)" for x
    unfolding R_def by (rule B) (use norm_triangle_ineq4 [of x z] in auto)
  with \<open>R > 0\<close> fz show False
    using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"]
    by (auto simp: less_imp_le norm_mult norm_divide field_split_simps)
qed

proposition Liouville_weak:
  assumes "f holomorphic_on UNIV" and "(f \ l) at_infinity"
    shows "f z = l"
  using Liouville_weak_0 [of "\z. f z - l"]
  by (simp add: assms holomorphic_on_diff LIM_zero)

proposition Liouville_weak_inverse:
  assumes "f holomorphic_on UNIV" and unbounded: "\B. eventually (\x. norm (f x) \ B) at_infinity"
    obtains z where "f z = 0"
proof -
  { assume f: "\z. f z \ 0"
    have 1: "(\x. 1 / f x) holomorphic_on UNIV"
      by (simp add: holomorphic_on_divide assms f)
    have 2: "((\x. 1 / f x) \ 0) at_infinity"
    proof (rule tendstoI [OF eventually_mono])
      fix e::real
      assume "e > 0"
      show "eventually (\x. 2/e \ cmod (f x)) at_infinity"
        by (rule_tac B="2/e" in unbounded)
    qed (simp add: dist_norm norm_divide field_split_simps)
    have False
      using Liouville_weak_0 [OF 1 2] f by simp
  }
  then show ?thesis
    using that by blast
qed

text\<open> In particular we get the Fundamental Theorem of Algebra.\<close>

theorem fundamental_theorem_of_algebra:
    fixes a :: "nat \ complex"
  assumes "a 0 = 0 \ (\i \ {1..n}. a i \ 0)"
  obtains z where "(\i\n. a i * z^i) = 0"
using assms
proof (elim disjE bexE)
  assume "a 0 = 0" then show ?thesis
    by (auto simp: that [of 0])
next
  fix i
  assume i: "i \ {1..n}" and nz: "a i \ 0"
  have 1: "(\z. \i\n. a i * z^i) holomorphic_on UNIV"
    by (rule holomorphic_intros)+
  show thesis
  proof (rule Liouville_weak_inverse [OF 1])
    show "\\<^sub>F x in at_infinity. B \ cmod (\i\n. a i * x ^ i)" for B
      using i nz by (intro polyfun_extremal exI[of _ i]) auto
  qed (use that in auto)
qed

subsection\<open>Weierstrass convergence theorem\<close>

lemma holomorphic_uniform_limit:
  assumes cont: "eventually (\n. continuous_on (cball z r) (f n) \ (f n) holomorphic_on ball z r) F"
      and ulim: "uniform_limit (cball z r) f g F"
      and F:  "\ trivial_limit F"
  obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r"
proof (cases r "0::real" rule: linorder_cases)
  case less then show ?thesis by (force simp: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
next
  case equal then show ?thesis
    by (force simp: holomorphic_on_def intro: that)
next
  case greater
  have contg: "continuous_on (cball z r) g"
    using cont uniform_limit_theorem [OF eventually_mono ulim F]  by blast
  have "path_image (circlepath z r) \ cball z r"
    using \<open>0 < r\<close> by auto
  then have 1: "continuous_on (path_image (circlepath z r)) (\x. 1 / (2 * complex_of_real pi * \) * g x)"
    by (intro continuous_intros continuous_on_subset [OF contg])
  have 2: "((\u. 1 / (2 * of_real pi * \) * g u / (u-w) ^ 1) has_contour_integral g w) (circlepath z r)"
       if w: "w \ ball z r" for w
  proof -
    define d where "d = (r - norm(w-z))"
    have "0 < d"  "d \ r" using w by (auto simp: norm_minus_commute d_def dist_norm)
    have dle: "\u. cmod (z-u) = r \ d \ cmod (u-w)"
      unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
    have ev_int: "\\<^sub>F n in F. (\u. f n u / (u-w)) contour_integrable_on circlepath z r"
      using w
      by (auto intro: eventually_mono [OF cont] Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
    have "\e. \0 < r; 0 < d; 0 < e\
         \<Longrightarrow> \<forall>\<^sub>F n in F.
                \<forall>x\<in>sphere z r.
                   x \<noteq> w \<longrightarrow>
                   cmod (f n x - g x) < e * cmod (x-w)"
      apply (rule_tac e1="e * d" in eventually_mono [OF uniform_limitD [OF ulim]])
       apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
      done
    then have ul_less: "uniform_limit (sphere z r) (\n x. f n x / (x-w)) (\x. g x / (x-w)) F"
      using greater \<open>0 < d\<close>
      by (auto simp add: uniform_limit_iff dist_norm norm_divide diff_divide_distrib [symmetric] divide_simps)
    have g_cint: "(\u. g u/(u-w)) contour_integrable_on circlepath z r"
      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
    have cif_tends_cig: "((\n. contour_integral(circlepath z r) (\u. f n u / (u-w))) \ contour_integral(circlepath z r) (\u. g u/(u-w))) F"
      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
    have f_tends_cig: "((\n. 2 * of_real pi * \ * f n w) \ contour_integral (circlepath z r) (\u. g u / (u-w))) F"
    proof (rule Lim_transform_eventually)
      show "\\<^sub>F x in F. contour_integral (circlepath z r) (\u. f x u / (u-w))
                     = 2 * of_real pi * \<i> * f x w"
        using w\<open>0 < d\<close> d_def
        by (auto intro: eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
    qed (auto simp: cif_tends_cig)
    have "\e. 0 < e \ \\<^sub>F n in F. dist (f n w) (g w) < e"
      by (rule eventually_mono [OF uniform_limitD [OF ulim]]) (use w in auto)
    then have "((\n. 2 * of_real pi * \ * f n w) \ 2 * of_real pi * \ * g w) F"
      by (rule tendsto_mult_left [OF tendstoI])
    then have "((\u. g u / (u-w)) has_contour_integral 2 * of_real pi * \ * g w) (circlepath z r)"
      using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
      by fastforce
    then have "((\u. g u / (2 * of_real pi * \ * (u-w))) has_contour_integral g w) (circlepath z r)"
      using has_contour_integral_div [where c = "2 * of_real pi * \"]
      by (force simp: field_simps)
    then show ?thesis
      by (simp add: dist_norm)
  qed
  show ?thesis
    using Cauchy_next_derivative_circlepath(2) [OF 1 2, simplified]
    by (fastforce simp add: holomorphic_on_open contg intro: that)
qed

lemma higher_deriv_complex_uniform_limit:
  assumes ulim: "uniform_limit A f g F"
      and f_holo: "eventually (\n. f n holomorphic_on A) F"
      and F: "F \ bot"
      and A: "open A" "z \ A"
    shows "((\n. (deriv ^^ m) (f n) z) \ (deriv ^^ m) g z) F"
proof -
  obtain r where r: "r > 0" "cball z r \ A"
    using A by (meson open_contains_cball)
  have r': "ball z r \ A"
    using r by auto
  define h where "h = (\n z. f n z - g z)"
  define c where "c = of_real (2*pi) * \ / fact m"
  have [simp]: "c \ 0"
    by (simp add: c_def)
  have "g holomorphic_on ball z r \ continuous_on (cball z r) g"
  proof (rule holomorphic_uniform_limit)
    show "uniform_limit (cball z r) f g F"
      by (rule uniform_limit_on_subset[OF ulim r(2)])
    show "\\<^sub>F n in F. continuous_on (cball z r) (f n) \ f n holomorphic_on ball z r" using f_holo
      by eventually_elim
         (use holomorphic_on_subset[OF _ r(2)] holomorphic_on_subset[OF _ r']
          in  \<open>auto intro!: holomorphic_on_imp_continuous_on\<close>)
  qed (use F in auto)
  hence g_holo: "g holomorphic_on ball z r" and g_cont: "continuous_on (cball z r) g"
    by blast+

  have ulim': "uniform_limit (sphere z r) (\n x. h n x / (x - z) ^ (Suc m)) (\_. 0) F"
  proof -
    have "uniform_limit (sphere z r) (\n x. f n x / (x - z) ^ Suc m) (\x. g x / (x - z) ^ Suc m) F"
    proof (intro uniform_lim_divide uniform_limit_intros uniform_limit_on_subset[OF ulim])
      have "compact (g ` sphere z r)"
        by (intro compact_continuous_image continuous_on_subset[OF g_cont]) auto
      thus "bounded (g ` sphere z r)"
        by (rule compact_imp_bounded)
      show "r ^ Suc m \ norm ((x - z) ^ Suc m)" if "x \ sphere z r" for x unfolding norm_power
        by (intro power_mono) (use that r(1) in \<open>auto simp: dist_norm norm_minus_commute\<close>)
    qed (use r in auto)
    hence "uniform_limit (sphere z r) (\n x. f n x / (x - z) ^ Suc m - g x / (x - z) ^ Suc m)
             (\<lambda>x. g x / (x - z) ^ Suc m - g x / (x - z) ^ Suc m) F"
      by (intro uniform_limit_intros)
    thus ?thesis
      by (simp add: h_def diff_divide_distrib)
  qed

  have has_integral: "eventually (\n. ((\u. h n u / (u - z) ^ Suc m) has_contour_integral
                         c * (deriv ^^ m) (h n) z) (circlepath z r)) F"
    using f_holo
  proof eventually_elim
    case (elim n)
    show ?case
      unfolding c_def
    proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath)
      show "continuous_on (cball z r) (h n)" unfolding h_def
        by (intro continuous_intros g_cont holomorphic_on_imp_continuous_on
                  holomorphic_on_subset[OF elim] r)
      show "h n holomorphic_on ball z r"
        unfolding h_def by (intro holomorphic_intros g_holo holomorphic_on_subset[OF elim] r')
    qed (use r(1) in auto)
  qed

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

--> maximum size reached

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

quality99%

¤ Dauer der Verarbeitung: 0.27 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.