# HG changeset patch # User paulson # Date 1695818055 -3600 # Node ID 4de5b127c124e236fe3c25366ca48c276aee0118 # Parent 58415993905809f960f72b77d6301d5d78f4bdba Importing or moving a few more useful theorems diff -r 584159939058 -r 4de5b127c124 src/HOL/Analysis/Derivative.thy --- 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 (\w. f (c*w + a)) z = c * deriv f (c*z + a)" + apply (subst deriv_chain [where f="\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 (\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 \ :> df" and S: "open S" "\ \ S" and "df \ 0" shows "\ f constant_on S" diff -r 584159939058 -r 4de5b127c124 src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy --- 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]: - "\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) + "\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 @@ -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 \ S" - and fg: "\w. w \ S \ u * w \ T" - shows "(deriv ^^ n) (\w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)" + 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 (*) u ` S" + 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 (*) u ` S" + 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)) holomorphic_on S" + 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 u: "(*) u holomorphic_on S" "f holomorphic_on (*) u ` S" + 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)) holomorphic_on S" + 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))) z = deriv (\z. u^n * (deriv ^^ n) f (u*z)) z" + 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)) holomorphic_on S" + 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)) z" + 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)) analytic_on S" - by (meson S u analytic_on_open holo2 holomorphic_on_compose holomorphic_transform o_def) + then have "(\w. (deriv ^^ n) f (u * w+c)) analytic_on S" + proof - + have "(deriv ^^ n) f \ (\w. u * w+c) holomorphic_on S" + using holomorphic_on_compose[OF _ holo2] \(\w. u * w+c) holomorphic_on S\ + 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 "\ = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)" + also have "\ = 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 \ 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" diff -r 584159939058 -r 4de5b127c124 src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy --- 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 \ S \ continuous_on S (\w. 1 / (w - z))" by (rule continuous_intros | force)+ diff -r 584159939058 -r 4de5b127c124 src/HOL/Complex_Analysis/Laurent_Convergence.thy --- 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 \TODO: Better than @{thm deriv_compose_linear}?\ -lemma deriv_compose_linear': - assumes "f field_differentiable at (c*z + a)" - shows "deriv (\w. f (c*w + a)) z = c * deriv f (c*z + a)" - apply (subst deriv_chain[where f="\w. c*w + a",unfolded comp_def]) - using assms by (auto intro:derivative_intros) - -text \TODO: Better than @{thm 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 \ 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" - proof - - have "(deriv ^^ n) f \ (\w. u * w+c) holomorphic_on S" - using holomorphic_on_compose[OF _ holo2] \(\w. u * w+c) holomorphic_on S\ - 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 "\ = 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)