--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Mon Sep 25 17:06:11 2023 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Wed Sep 27 13:34:15 2023 +0100
@@ -4,66 +4,6 @@
begin
-(* TODO: Move *)
-text \<open>TODO: Better than @{thm deriv_compose_linear}?\<close>
-lemma deriv_compose_linear':
- assumes "f field_differentiable at (c*z + a)"
- shows "deriv (\<lambda>w. f (c*w + a)) z = c * deriv f (c*z + a)"
- apply (subst deriv_chain[where f="\<lambda>w. c*w + a",unfolded comp_def])
- using assms by (auto intro:derivative_intros)
-
-text \<open>TODO: Better than @{thm higher_deriv_compose_linear}?\<close>
-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 \<in> S"
- and fg: "\<And>w. w \<in> S \<Longrightarrow> u*w + c \<in> T"
- shows "(deriv ^^ n) (\<lambda>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 (\<lambda>w. u * w+c) ` S"
- by (meson fg f holomorphic_on_subset image_subset_iff)
- have holo2: "(deriv ^^ n) f holomorphic_on (\<lambda>w. u * w+c) ` S"
- by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T)
- have holo3: "(\<lambda>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 "(\<lambda>w. u * w+c) holomorphic_on S" "f holomorphic_on (\<lambda>w. u * w+c) ` S"
- by (rule holo0 holomorphic_intros)+
- then have holo1: "(\<lambda>w. f (u * w+c)) holomorphic_on S"
- by (rule holomorphic_on_compose [where g=f, unfolded o_def])
- have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w+c))) z = deriv (\<lambda>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) (\<lambda>w. f (u * w+c)) holomorphic_on S"
- by (rule holomorphic_higher_deriv [OF holo1 S])
- qed (simp add: Suc.IH)
- also have "\<dots> = u^n * deriv (\<lambda>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 "(\<lambda>w. (deriv ^^ n) f (u * w+c)) analytic_on S"
- proof -
- have "(deriv ^^ n) f \<circ> (\<lambda>w. u * w+c) holomorphic_on S"
- using holomorphic_on_compose[OF _ holo2] \<open>(\<lambda>w. u * w+c) holomorphic_on S\<close>
- by simp
- then show ?thesis
- by (simp add: S analytic_on_open o_def)
- qed
- then show ?thesis
- by (intro deriv_cmult analytic_on_imp_differentiable_at [OF _ Suc.prems])
- qed
- also have "\<dots> = 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 fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n"
by (metis fps_to_fls_of_nat of_nat_numeral)