--- a/src/HOL/Analysis/Derivative.thy Mon Sep 25 17:06:11 2023 +0100
+++ b/src/HOL/Analysis/Derivative.thy Wed Sep 27 13:34:15 2023 +0100
@@ -2403,6 +2403,12 @@
unfolding DERIV_deriv_iff_field_differentiable[symmetric]
by (auto intro!: DERIV_imp_deriv derivative_intros)
+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)
+
lemma deriv_compose_linear:
assumes "f field_differentiable at (c * z)"
shows "deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
@@ -2413,7 +2419,6 @@
by simp
qed
-
lemma nonzero_deriv_nonconstant:
assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0"
shows "\<not> f constant_on S"
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Mon Sep 25 17:06:11 2023 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Wed Sep 27 13:34:15 2023 +0100
@@ -379,8 +379,14 @@
qed
lemma holomorphic_deriv [holomorphic_intros]:
- "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on S"
-by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+ "\<lbrakk>f holomorphic_on S; open S\<rbrakk> \<Longrightarrow> (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 \<subseteq> B" "open B"
+ shows "(\<lambda>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 \<Longrightarrow> (deriv f) analytic_on S"
using analytic_on_holomorphic holomorphic_deriv by auto
@@ -625,51 +631,64 @@
by (induction i arbitrary: z)
(auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
-lemma higher_deriv_compose_linear:
+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 \<in> T"
- shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
+ 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 (*) u ` S"
+ 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 (*) u ` S"
+ 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)) holomorphic_on S"
+ 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 u: "(*) u holomorphic_on S" "f holomorphic_on (*) u ` S"
+ 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)) holomorphic_on S"
+ 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))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
+ 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)) holomorphic_on S"
+ 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)) z"
+ 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)) analytic_on S"
- by (meson S u analytic_on_open holo2 holomorphic_on_compose holomorphic_transform o_def)
+ 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)"
+ also have "\<dots> = u * u ^ n * deriv ((deriv ^^ n) f) (u * z+c)"
proof -
- have "(deriv ^^ n) f field_differentiable at (u * z)"
+ 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)
+ 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 \<in> S"
+ and fg: "\<And>w. w \<in> S \<Longrightarrow> u * w \<in> T"
+ shows "(deriv ^^ n) (\<lambda>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) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Mon Sep 25 17:06:11 2023 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy Wed Sep 27 13:34:15 2023 +0100
@@ -1121,6 +1121,11 @@
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 \<notin> S \<Longrightarrow> continuous_on S (\<lambda>w. 1 / (w - z))"
by (rule continuous_intros | force)+
--- 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)