# HG changeset patch
# User Manuel Eberl <manuel@pruvisto.org>
# Date 1745319212 -7200
# Node ID 34190188b40fb8839546e209d5575d4c7adf9cb6
# Parent  42964a5121a9d5cf937f7d5d008395e85d640fda
some facts about derivatives of products

diff -r 42964a5121a9 -r 34190188b40f src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Fri Apr 18 16:51:31 2025 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Tue Apr 22 12:53:32 2025 +0200
@@ -1266,6 +1266,58 @@
   finally show ?thesis .
 qed
 
+lemma 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 (f n) z) \<longlongrightarrow> deriv g z) F"
+  using higher_deriv_complex_uniform_limit[OF assms, of 1] by simp
+
+lemma logderiv_prodinf_complex_uniform_limit:
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  assumes lim: "uniform_limit A (\<lambda>n x. \<Prod>k<n. f k x) P sequentially"
+  assumes holo: "\<And>k. f k holomorphic_on A"
+  assumes nz: "P z \<noteq> 0"
+  assumes A: "open A" "z \<in> A"
+  shows   "(\<lambda>k. deriv (f k) z / f k z) sums (deriv P z / P z)"
+proof -
+  define f' where "f' = (\<lambda>k. deriv (f k))"
+  note [derivative_intros] = has_field_derivative_prod'
+  have [derivative_intros]: 
+    "(f k has_field_derivative f' k z) (at z within B)" if "z \<in> A" for B z k
+    using that holomorphic_derivI[OF holo[of k],  of z B] A unfolding f'_def by auto
+  have lim': "(\<lambda>n. \<Prod>k<n. f k z) \<longlonglongrightarrow> P z"
+    using lim by (rule tendsto_uniform_limitI) fact+
+
+  have nz': "f k z \<noteq> 0" for k
+  proof
+    assume "f k z = 0"
+    have "eventually (\<lambda>n. (\<Prod>k<n. f k z) = 0) sequentially"
+      using eventually_gt_at_top[of k] by eventually_elim (use \<open>f k z = 0\<close> in auto)
+    hence "(\<lambda>n. (\<Prod>k<n. f k z)) \<longlonglongrightarrow> 0"
+      by (rule tendsto_eventually)
+    with lim' have "P z = 0"
+      using tendsto_unique sequentially_bot by blast
+    with nz show False
+      by simp
+  qed
+
+  from lim have "(\<lambda>n. deriv (\<lambda>x. \<Prod>k<n. f k x) z) \<longlonglongrightarrow> deriv P z"
+    by (rule deriv_complex_uniform_limit)
+       (use A in \<open>auto intro!: always_eventually holomorphic_intros holo\<close>)
+  also have "(\<lambda>n. deriv (\<lambda>x. \<Prod>k<n. f k x) z) = (\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z))"
+    using \<open>z \<in> A\<close> by (auto intro!: ext DERIV_imp_deriv derivative_eq_intros simp: nz')
+  finally have "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z)) \<longlonglongrightarrow> deriv P z" .
+  hence "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z) / (\<Prod>k<n. f k z)) \<longlonglongrightarrow> deriv P z / P z"
+    by (intro tendsto_intros) (use nz lim' in auto)
+  also have "(\<lambda>n. (\<Prod>k<n. f k z) * (\<Sum>k<n. f' k z / f k z) / (\<Prod>k<n. f k z)) =
+             (\<lambda>n. (\<Sum>k<n. f' k z / f k z))"
+    by (simp add: nz')
+  finally show "(\<lambda>k. f' k z / f k z) sums (deriv P z / P z)"
+    unfolding sums_def .
+qed
+
 
 text\<open> Version showing that the limit is the limit of the derivatives.\<close>
 
diff -r 42964a5121a9 -r 34190188b40f src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Apr 18 16:51:31 2025 +0200
+++ b/src/HOL/Deriv.thy	Tue Apr 22 12:53:32 2025 +0200
@@ -1156,6 +1156,35 @@
   ((\<lambda>x. f (g x)) has_field_derivative Da * Db) (at x within s)"
   by (rule DERIV_chain')
 
+text \<open>Derivative of a finite product\<close>
+
+lemma has_field_derivative_prod:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (f x has_field_derivative f' x) (at z)"
+  shows   "((\<lambda>u. \<Prod>x\<in>A. f x u) has_field_derivative (\<Sum>x\<in>A. f' x * (\<Prod>y\<in>A-{x}. f y z))) (at z)"
+  using assms
+proof (induction A rule: infinite_finite_induct)
+  case (insert x A)
+  have eq: "insert x A - {y} = insert x (A - {y})" if "y \<in> A" for y
+    using insert.hyps that by auto
+  show ?case
+    using insert.hyps
+    by (auto intro!: derivative_eq_intros insert.prems insert.IH sum.cong
+             simp: sum_distrib_left sum_distrib_right eq)
+qed auto
+
+lemma has_field_derivative_prod':
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x z \<noteq> 0"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (f x has_field_derivative f' x) (at z)"
+  defines "P \<equiv> (\<lambda>A u. \<Prod>x\<in>A. f x u)"
+  shows   "(P A has_field_derivative (P A z * (\<Sum>x\<in>A. f' x / f x z))) (at z)"
+proof (cases "finite A")
+  case True
+  note [derivative_intros] = has_field_derivative_prod
+  show ?thesis using assms True
+    by (auto intro!: derivative_eq_intros
+             simp: prod_diff1 sum_distrib_left sum_distrib_right mult_ac)
+qed (auto simp: P_def)
+
 text \<open>Standard version\<close>
 
 lemma DERIV_chain: