# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1744139154 -3600
# Node ID eea85bbd2feb080c784ef96ef3e616227f8c8df8
# Parent  67c024ec618e92179bc864f848653efa422915e6
Another of Manuel's theorems

diff -r 67c024ec618e -r eea85bbd2feb src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Tue Apr 08 19:06:09 2025 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Tue Apr 08 20:05:54 2025 +0100
@@ -1173,6 +1173,99 @@
     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 (\<lambda>n. f n holomorphic_on A) F"
+      and F: "F \<noteq> bot"
+      and A: "open A" "z \<in> A"
+    shows "((\<lambda>n. (deriv ^^ m) (f n) z) \<longlongrightarrow> (deriv ^^ m) g z) F"
+proof -
+  obtain r where r: "r > 0" "cball z r \<subseteq> A"
+    using A by (meson open_contains_cball)
+  have r': "ball z r \<subseteq> A"
+    using r by auto
+  define h where "h = (\<lambda>n z. f n z - g z)"
+  define c where "c = of_real (2*pi) * \<i> / fact m"
+  have [simp]: "c \<noteq> 0"
+    by (simp add: c_def)
+  have "g holomorphic_on ball z r \<and> 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 "\<forall>\<^sub>F n in F. continuous_on (cball z r) (f n) \<and> 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) (\<lambda>n x. h n x / (x - z) ^ (Suc m)) (\<lambda>_. 0) F"
+  proof -
+    have "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - z) ^ Suc m) (\<lambda>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 \<le> norm ((x - z) ^ Suc m)" if "x \<in> 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) (\<lambda>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 (\<lambda>n. ((\<lambda>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
+
+  have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. h n u / (u - z) ^ Suc m)) \<longlongrightarrow> 
+         contour_integral (circlepath z r) (\<lambda>u. 0 / (u - z) ^ Suc m)) F"
+  proof (rule contour_integral_uniform_limit_circlepath)
+    show "\<forall>\<^sub>F n in F. (\<lambda>u. h n u / (u - z) ^ Suc m) contour_integrable_on circlepath z r"
+      using has_integral by eventually_elim (blast intro: has_contour_integral_integrable)
+  qed (use r(1) \<open>F \<noteq> bot\<close> ulim' in simp_all)
+  hence "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. h n u / (u - z) ^ Suc m)) \<longlongrightarrow> 0) F"
+    by simp
+  also have "?this \<longleftrightarrow> ((\<lambda>n. c * (deriv ^^ m) (h n) z) \<longlongrightarrow> 0) F"
+  proof (rule tendsto_cong)
+    show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. h x u / (u - z) ^ Suc m) =
+                       c * (deriv ^^ m) (h x) z"
+      using has_integral by eventually_elim (simp add: contour_integral_unique)
+  qed
+  finally have "((\<lambda>n. (deriv ^^ m) g z + c * (deriv ^^ m) (h n) z / c) \<longlongrightarrow> 
+                  (deriv ^^ m) g z + 0 / c) F"
+    by (intro tendsto_intros) auto
+  also have "?this \<longleftrightarrow> ((\<lambda>n. (deriv ^^ m) (f n) z) \<longlongrightarrow> (deriv ^^ m) g z) F"
+  proof (intro filterlim_cong)
+    show "\<forall>\<^sub>F n in F. (deriv ^^ m) g z + c * (deriv ^^ m) (h n) z / c = (deriv ^^ m) (f n) z"
+      using f_holo
+    proof eventually_elim
+      case (elim n)
+      have "(deriv ^^ m) (h n) z = (deriv ^^ m) (f n) z - (deriv ^^ m) g z" unfolding h_def
+        by (rule higher_deriv_diff holomorphic_on_subset[OF elim r'] g_holo A)+ (use r(1) in auto)
+      thus ?case
+        by simp
+    qed
+  qed auto
+  finally show ?thesis .
+qed
+
 
 text\<open> Version showing that the limit is the limit of the derivatives.\<close>