src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
 author paulson Fri Jan 22 16:00:03 2016 +0000 (2016-01-22) changeset 62217 527488dc8b90 parent 62131 1baed43f453e child 62397 5ae24f33d343 permissions -rw-r--r--
Reorganised a huge proof
 lp15@56215 ` 1` ```(* Author: John Harrison, Marco Maggesi, Graziano Gentili, Gianni Ciolli, Valentina Bruno ``` lp15@56215 ` 2` ``` Ported from "hol_light/Multivariate/canal.ml" by L C Paulson (2014) ``` lp15@56215 ` 3` ```*) ``` lp15@56215 ` 4` wenzelm@60420 ` 5` ```section \Complex Analysis Basics\ ``` lp15@56215 ` 6` lp15@56215 ` 7` ```theory Complex_Analysis_Basics ``` paulson@62131 ` 8` ```imports Cartesian_Euclidean_Space "~~/src/HOL/Library/Nonpos_Ints" ``` lp15@56215 ` 9` ```begin ``` lp15@56215 ` 10` lp15@59730 ` 11` paulson@62131 ` 12` ```subsection\General lemmas\ ``` lp15@59730 ` 13` paulson@62131 ` 14` ```lemma nonneg_Reals_cmod_eq_Re: "z \ \\<^sub>\\<^sub>0 \ norm z = Re z" ``` paulson@62131 ` 15` ``` by (simp add: complex_nonneg_Reals_iff cmod_eq_Re) ``` hoelzl@56370 ` 16` hoelzl@56370 ` 17` ```lemma has_derivative_mult_right: ``` hoelzl@56370 ` 18` ``` fixes c:: "'a :: real_normed_algebra" ``` hoelzl@56370 ` 19` ``` shows "((op * c) has_derivative (op * c)) F" ``` hoelzl@56370 ` 20` ```by (rule has_derivative_mult_right [OF has_derivative_id]) ``` hoelzl@56370 ` 21` lp15@61609 ` 22` ```lemma has_derivative_of_real[derivative_intros, simp]: ``` hoelzl@56370 ` 23` ``` "(f has_derivative f') F \ ((\x. of_real (f x)) has_derivative (\x. of_real (f' x))) F" ``` hoelzl@56370 ` 24` ``` using bounded_linear.has_derivative[OF bounded_linear_of_real] . ``` hoelzl@56370 ` 25` hoelzl@56370 ` 26` ```lemma has_vector_derivative_real_complex: ``` lp15@61806 ` 27` ``` "DERIV f (of_real a) :> f' \ ((\x. f (of_real x)) has_vector_derivative f') (at a within s)" ``` lp15@61806 ` 28` ``` using has_derivative_compose[of of_real of_real a _ f "op * f'"] ``` hoelzl@56370 ` 29` ``` by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def) ``` lp15@56215 ` 30` lp15@56238 ` 31` ```lemma fact_cancel: ``` lp15@56238 ` 32` ``` fixes c :: "'a::real_field" ``` lp15@59730 ` 33` ``` shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" ``` hoelzl@56369 ` 34` ``` by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps) ``` hoelzl@56889 ` 35` lp15@56215 ` 36` ```lemma bilinear_times: ``` hoelzl@56369 ` 37` ``` fixes c::"'a::real_algebra" shows "bilinear (\x y::'a. x*y)" ``` hoelzl@56369 ` 38` ``` by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) ``` lp15@56215 ` 39` lp15@56215 ` 40` ```lemma linear_cnj: "linear cnj" ``` hoelzl@56369 ` 41` ``` using bounded_linear.linear[OF bounded_linear_cnj] . ``` lp15@56215 ` 42` lp15@56215 ` 43` ```lemma tendsto_Re_upper: ``` lp15@61609 ` 44` ``` assumes "~ (trivial_limit F)" ``` wenzelm@61973 ` 45` ``` "(f \ l) F" ``` lp15@56215 ` 46` ``` "eventually (\x. Re(f x) \ b) F" ``` lp15@56215 ` 47` ``` shows "Re(l) \ b" ``` lp15@56215 ` 48` ``` by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Re) ``` lp15@56215 ` 49` lp15@56215 ` 50` ```lemma tendsto_Re_lower: ``` lp15@61609 ` 51` ``` assumes "~ (trivial_limit F)" ``` wenzelm@61973 ` 52` ``` "(f \ l) F" ``` lp15@56215 ` 53` ``` "eventually (\x. b \ Re(f x)) F" ``` lp15@56215 ` 54` ``` shows "b \ Re(l)" ``` lp15@56215 ` 55` ``` by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Re) ``` lp15@56215 ` 56` lp15@56215 ` 57` ```lemma tendsto_Im_upper: ``` lp15@61609 ` 58` ``` assumes "~ (trivial_limit F)" ``` wenzelm@61973 ` 59` ``` "(f \ l) F" ``` lp15@56215 ` 60` ``` "eventually (\x. Im(f x) \ b) F" ``` lp15@56215 ` 61` ``` shows "Im(l) \ b" ``` lp15@56215 ` 62` ``` by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Im) ``` lp15@56215 ` 63` lp15@56215 ` 64` ```lemma tendsto_Im_lower: ``` lp15@61609 ` 65` ``` assumes "~ (trivial_limit F)" ``` wenzelm@61973 ` 66` ``` "(f \ l) F" ``` lp15@56215 ` 67` ``` "eventually (\x. b \ Im(f x)) F" ``` lp15@56215 ` 68` ``` shows "b \ Im(l)" ``` lp15@56215 ` 69` ``` by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Im) ``` lp15@56215 ` 70` hoelzl@56370 ` 71` ```lemma lambda_zero: "(\h::'a::mult_zero. 0) = op * 0" ``` hoelzl@56370 ` 72` ``` by auto ``` hoelzl@56370 ` 73` hoelzl@56370 ` 74` ```lemma lambda_one: "(\x::'a::monoid_mult. x) = op * 1" ``` hoelzl@56370 ` 75` ``` by auto ``` hoelzl@56370 ` 76` lp15@56215 ` 77` ```lemma continuous_mult_left: ``` lp15@61609 ` 78` ``` fixes c::"'a::real_normed_algebra" ``` lp15@56215 ` 79` ``` shows "continuous F f \ continuous F (\x. c * f x)" ``` lp15@56215 ` 80` ```by (rule continuous_mult [OF continuous_const]) ``` lp15@56215 ` 81` lp15@56215 ` 82` ```lemma continuous_mult_right: ``` lp15@61609 ` 83` ``` fixes c::"'a::real_normed_algebra" ``` lp15@56215 ` 84` ``` shows "continuous F f \ continuous F (\x. f x * c)" ``` lp15@56215 ` 85` ```by (rule continuous_mult [OF _ continuous_const]) ``` lp15@56215 ` 86` lp15@56215 ` 87` ```lemma continuous_on_mult_left: ``` lp15@61609 ` 88` ``` fixes c::"'a::real_normed_algebra" ``` lp15@56215 ` 89` ``` shows "continuous_on s f \ continuous_on s (\x. c * f x)" ``` lp15@56215 ` 90` ```by (rule continuous_on_mult [OF continuous_on_const]) ``` lp15@56215 ` 91` lp15@56215 ` 92` ```lemma continuous_on_mult_right: ``` lp15@61609 ` 93` ``` fixes c::"'a::real_normed_algebra" ``` lp15@56215 ` 94` ``` shows "continuous_on s f \ continuous_on s (\x. f x * c)" ``` lp15@56215 ` 95` ```by (rule continuous_on_mult [OF _ continuous_on_const]) ``` lp15@56215 ` 96` hoelzl@56371 ` 97` ```lemma uniformly_continuous_on_cmul_right [continuous_intros]: ``` lp15@56215 ` 98` ``` fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" ``` hoelzl@56332 ` 99` ``` shows "uniformly_continuous_on s f \ uniformly_continuous_on s (\x. f x * c)" ``` lp15@61609 ` 100` ``` using bounded_linear.uniformly_continuous_on[OF bounded_linear_mult_left] . ``` lp15@56215 ` 101` hoelzl@56371 ` 102` ```lemma uniformly_continuous_on_cmul_left[continuous_intros]: ``` lp15@56215 ` 103` ``` fixes f :: "'a::real_normed_vector \ 'b::real_normed_algebra" ``` lp15@56215 ` 104` ``` assumes "uniformly_continuous_on s f" ``` lp15@56215 ` 105` ``` shows "uniformly_continuous_on s (\x. c * f x)" ``` lp15@56215 ` 106` ```by (metis assms bounded_linear.uniformly_continuous_on bounded_linear_mult_right) ``` lp15@56215 ` 107` lp15@56215 ` 108` ```lemma continuous_within_norm_id [continuous_intros]: "continuous (at x within S) norm" ``` lp15@56215 ` 109` ``` by (rule continuous_norm [OF continuous_ident]) ``` lp15@56215 ` 110` lp15@56215 ` 111` ```lemma continuous_on_norm_id [continuous_intros]: "continuous_on S norm" ``` hoelzl@56369 ` 112` ``` by (intro continuous_on_id continuous_on_norm) ``` lp15@56215 ` 113` wenzelm@60420 ` 114` ```subsection\DERIV stuff\ ``` lp15@56215 ` 115` lp15@56215 ` 116` ```lemma DERIV_zero_connected_constant: ``` lp15@56215 ` 117` ``` fixes f :: "'a::{real_normed_field,euclidean_space} \ 'a" ``` lp15@56215 ` 118` ``` assumes "connected s" ``` lp15@56215 ` 119` ``` and "open s" ``` lp15@56215 ` 120` ``` and "finite k" ``` lp15@56215 ` 121` ``` and "continuous_on s f" ``` lp15@56215 ` 122` ``` and "\x\(s - k). DERIV f x :> 0" ``` lp15@56215 ` 123` ``` obtains c where "\x. x \ s \ f(x) = c" ``` lp15@56215 ` 124` ```using has_derivative_zero_connected_constant [OF assms(1-4)] assms ``` hoelzl@56369 ` 125` ```by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def) ``` lp15@56215 ` 126` lp15@56215 ` 127` ```lemma DERIV_zero_constant: ``` hoelzl@56370 ` 128` ``` fixes f :: "'a::{real_normed_field, real_inner} \ 'a" ``` lp15@56215 ` 129` ``` shows "\convex s; ``` lp15@61609 ` 130` ``` \x. x\s \ (f has_field_derivative 0) (at x within s)\ ``` lp15@56215 ` 131` ``` \ \c. \x \ s. f(x) = c" ``` hoelzl@56370 ` 132` ``` by (auto simp: has_field_derivative_def lambda_zero intro: has_derivative_zero_constant) ``` lp15@56215 ` 133` lp15@56215 ` 134` ```lemma DERIV_zero_unique: ``` hoelzl@56370 ` 135` ``` fixes f :: "'a::{real_normed_field, real_inner} \ 'a" ``` lp15@56215 ` 136` ``` assumes "convex s" ``` lp15@56215 ` 137` ``` and d0: "\x. x\s \ (f has_field_derivative 0) (at x within s)" ``` lp15@56215 ` 138` ``` and "a \ s" ``` lp15@56215 ` 139` ``` and "x \ s" ``` lp15@56215 ` 140` ``` shows "f x = f a" ``` hoelzl@56370 ` 141` ``` by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)]) ``` hoelzl@56332 ` 142` ``` (metis d0 has_field_derivative_imp_has_derivative lambda_zero) ``` lp15@56215 ` 143` lp15@56215 ` 144` ```lemma DERIV_zero_connected_unique: ``` hoelzl@56370 ` 145` ``` fixes f :: "'a::{real_normed_field, real_inner} \ 'a" ``` lp15@56215 ` 146` ``` assumes "connected s" ``` lp15@56215 ` 147` ``` and "open s" ``` lp15@56215 ` 148` ``` and d0: "\x. x\s \ DERIV f x :> 0" ``` lp15@56215 ` 149` ``` and "a \ s" ``` lp15@56215 ` 150` ``` and "x \ s" ``` lp15@61609 ` 151` ``` shows "f x = f a" ``` hoelzl@56370 ` 152` ``` by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)]) ``` hoelzl@56370 ` 153` ``` (metis has_field_derivative_def lambda_zero d0) ``` lp15@56215 ` 154` lp15@56215 ` 155` ```lemma DERIV_transform_within: ``` lp15@56215 ` 156` ``` assumes "(f has_field_derivative f') (at a within s)" ``` lp15@56215 ` 157` ``` and "0 < d" "a \ s" ``` lp15@56215 ` 158` ``` and "\x. x\s \ dist x a < d \ f x = g x" ``` lp15@56215 ` 159` ``` shows "(g has_field_derivative f') (at a within s)" ``` lp15@56215 ` 160` ``` using assms unfolding has_field_derivative_def ``` hoelzl@56332 ` 161` ``` by (blast intro: has_derivative_transform_within) ``` lp15@56215 ` 162` lp15@56215 ` 163` ```lemma DERIV_transform_within_open: ``` lp15@56215 ` 164` ``` assumes "DERIV f a :> f'" ``` lp15@56215 ` 165` ``` and "open s" "a \ s" ``` lp15@56215 ` 166` ``` and "\x. x\s \ f x = g x" ``` lp15@56215 ` 167` ``` shows "DERIV g a :> f'" ``` lp15@56215 ` 168` ``` using assms unfolding has_field_derivative_def ``` lp15@56215 ` 169` ```by (metis has_derivative_transform_within_open) ``` lp15@56215 ` 170` lp15@56215 ` 171` ```lemma DERIV_transform_at: ``` lp15@56215 ` 172` ``` assumes "DERIV f a :> f'" ``` lp15@56215 ` 173` ``` and "0 < d" ``` lp15@56215 ` 174` ``` and "\x. dist x a < d \ f x = g x" ``` lp15@56215 ` 175` ``` shows "DERIV g a :> f'" ``` lp15@56215 ` 176` ``` by (blast intro: assms DERIV_transform_within) ``` lp15@56215 ` 177` lp15@59615 ` 178` ```(*generalising DERIV_isconst_all, which requires type real (using the ordering)*) ``` lp15@59615 ` 179` ```lemma DERIV_zero_UNIV_unique: ``` lp15@59615 ` 180` ``` fixes f :: "'a::{real_normed_field, real_inner} \ 'a" ``` lp15@61609 ` 181` ``` shows "(\x. DERIV f x :> 0) \ f x = f a" ``` lp15@59615 ` 182` ```by (metis DERIV_zero_unique UNIV_I assms convex_UNIV) ``` lp15@59615 ` 183` wenzelm@60420 ` 184` ```subsection \Some limit theorems about real part of real series etc.\ ``` hoelzl@56370 ` 185` hoelzl@56370 ` 186` ```(*MOVE? But not to Finite_Cartesian_Product*) ``` hoelzl@56370 ` 187` ```lemma sums_vec_nth : ``` hoelzl@56370 ` 188` ``` assumes "f sums a" ``` hoelzl@56370 ` 189` ``` shows "(\x. f x \$ i) sums a \$ i" ``` hoelzl@56370 ` 190` ```using assms unfolding sums_def ``` hoelzl@56370 ` 191` ```by (auto dest: tendsto_vec_nth [where i=i]) ``` hoelzl@56370 ` 192` hoelzl@56370 ` 193` ```lemma summable_vec_nth : ``` hoelzl@56370 ` 194` ``` assumes "summable f" ``` hoelzl@56370 ` 195` ``` shows "summable (\x. f x \$ i)" ``` hoelzl@56370 ` 196` ```using assms unfolding summable_def ``` hoelzl@56370 ` 197` ```by (blast intro: sums_vec_nth) ``` hoelzl@56370 ` 198` wenzelm@60420 ` 199` ```subsection \Complex number lemmas\ ``` hoelzl@56370 ` 200` hoelzl@56370 ` 201` ```lemma ``` hoelzl@56370 ` 202` ``` shows open_halfspace_Re_lt: "open {z. Re(z) < b}" ``` hoelzl@56370 ` 203` ``` and open_halfspace_Re_gt: "open {z. Re(z) > b}" ``` hoelzl@56370 ` 204` ``` and closed_halfspace_Re_ge: "closed {z. Re(z) \ b}" ``` hoelzl@56370 ` 205` ``` and closed_halfspace_Re_le: "closed {z. Re(z) \ b}" ``` hoelzl@56370 ` 206` ``` and closed_halfspace_Re_eq: "closed {z. Re(z) = b}" ``` hoelzl@56370 ` 207` ``` and open_halfspace_Im_lt: "open {z. Im(z) < b}" ``` hoelzl@56370 ` 208` ``` and open_halfspace_Im_gt: "open {z. Im(z) > b}" ``` hoelzl@56370 ` 209` ``` and closed_halfspace_Im_ge: "closed {z. Im(z) \ b}" ``` hoelzl@56370 ` 210` ``` and closed_halfspace_Im_le: "closed {z. Im(z) \ b}" ``` hoelzl@56370 ` 211` ``` and closed_halfspace_Im_eq: "closed {z. Im(z) = b}" ``` hoelzl@56370 ` 212` ``` by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re ``` lp15@60150 ` 213` ``` isCont_Im continuous_ident continuous_const)+ ``` hoelzl@56370 ` 214` wenzelm@61070 ` 215` ```lemma closed_complex_Reals: "closed (\ :: complex set)" ``` hoelzl@56370 ` 216` ```proof - ``` wenzelm@61070 ` 217` ``` have "(\ :: complex set) = {z. Im z = 0}" ``` hoelzl@56370 ` 218` ``` by (auto simp: complex_is_Real_iff) ``` hoelzl@56370 ` 219` ``` then show ?thesis ``` hoelzl@56370 ` 220` ``` by (metis closed_halfspace_Im_eq) ``` hoelzl@56370 ` 221` ```qed ``` hoelzl@56370 ` 222` lp15@60017 ` 223` ```lemma closed_Real_halfspace_Re_le: "closed (\ \ {w. Re w \ x})" ``` lp15@60017 ` 224` ``` by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le) ``` lp15@60017 ` 225` paulson@62131 ` 226` ```corollary closed_nonpos_Reals_complex [simp]: "closed (\\<^sub>\\<^sub>0 :: complex set)" ``` paulson@62131 ` 227` ```proof - ``` paulson@62131 ` 228` ``` have "\\<^sub>\\<^sub>0 = \ \ {z. Re(z) \ 0}" ``` paulson@62131 ` 229` ``` using complex_nonpos_Reals_iff complex_is_Real_iff by auto ``` paulson@62131 ` 230` ``` then show ?thesis ``` paulson@62131 ` 231` ``` by (metis closed_Real_halfspace_Re_le) ``` paulson@62131 ` 232` ```qed ``` paulson@62131 ` 233` lp15@60017 ` 234` ```lemma closed_Real_halfspace_Re_ge: "closed (\ \ {w. x \ Re(w)})" ``` lp15@60017 ` 235` ``` using closed_halfspace_Re_ge ``` lp15@60017 ` 236` ``` by (simp add: closed_Int closed_complex_Reals) ``` lp15@60017 ` 237` paulson@62131 ` 238` ```corollary closed_nonneg_Reals_complex [simp]: "closed (\\<^sub>\\<^sub>0 :: complex set)" ``` paulson@62131 ` 239` ```proof - ``` paulson@62131 ` 240` ``` have "\\<^sub>\\<^sub>0 = \ \ {z. Re(z) \ 0}" ``` paulson@62131 ` 241` ``` using complex_nonneg_Reals_iff complex_is_Real_iff by auto ``` paulson@62131 ` 242` ``` then show ?thesis ``` paulson@62131 ` 243` ``` by (metis closed_Real_halfspace_Re_ge) ``` paulson@62131 ` 244` ```qed ``` paulson@62131 ` 245` lp15@60017 ` 246` ```lemma closed_real_abs_le: "closed {w \ \. \Re w\ \ r}" ``` lp15@60017 ` 247` ```proof - ``` lp15@60017 ` 248` ``` have "{w \ \. \Re w\ \ r} = (\ \ {w. Re w \ r}) \ (\ \ {w. Re w \ -r})" ``` lp15@60017 ` 249` ``` by auto ``` lp15@60017 ` 250` ``` then show "closed {w \ \. \Re w\ \ r}" ``` lp15@60017 ` 251` ``` by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le) ``` lp15@60017 ` 252` ```qed ``` lp15@60017 ` 253` hoelzl@56370 ` 254` ```lemma real_lim: ``` hoelzl@56370 ` 255` ``` fixes l::complex ``` wenzelm@61973 ` 256` ``` assumes "(f \ l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" ``` hoelzl@56370 ` 257` ``` shows "l \ \" ``` hoelzl@56370 ` 258` ```proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)]) ``` hoelzl@56370 ` 259` ``` show "eventually (\x. f x \ \) F" ``` hoelzl@56370 ` 260` ``` using assms(3, 4) by (auto intro: eventually_mono) ``` hoelzl@56370 ` 261` ```qed ``` hoelzl@56370 ` 262` hoelzl@56370 ` 263` ```lemma real_lim_sequentially: ``` hoelzl@56370 ` 264` ``` fixes l::complex ``` wenzelm@61973 ` 265` ``` shows "(f \ l) sequentially \ (\N. \n\N. f n \ \) \ l \ \" ``` hoelzl@56370 ` 266` ```by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially) ``` hoelzl@56370 ` 267` lp15@61609 ` 268` ```lemma real_series: ``` hoelzl@56370 ` 269` ``` fixes l::complex ``` hoelzl@56370 ` 270` ``` shows "f sums l \ (\n. f n \ \) \ l \ \" ``` hoelzl@56370 ` 271` ```unfolding sums_def ``` hoelzl@56370 ` 272` ```by (metis real_lim_sequentially setsum_in_Reals) ``` hoelzl@56370 ` 273` hoelzl@56370 ` 274` ```lemma Lim_null_comparison_Re: ``` wenzelm@61973 ` 275` ``` assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g \ 0) F" shows "(f \ 0) F" ``` hoelzl@56889 ` 276` ``` by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp ``` lp15@56215 ` 277` wenzelm@60420 ` 278` ```subsection\Holomorphic functions\ ``` lp15@56215 ` 279` wenzelm@61975 ` 280` ```text\Could be generalized to real normed fields, but in practice that would only include the reals\ ``` lp15@56215 ` 281` ```definition complex_differentiable :: "[complex \ complex, complex filter] \ bool" ``` lp15@61609 ` 282` ``` (infixr "(complex'_differentiable)" 50) ``` lp15@56215 ` 283` ``` where "f complex_differentiable F \ \f'. (f has_field_derivative f') F" ``` lp15@56215 ` 284` hoelzl@56370 ` 285` ```lemma complex_differentiable_imp_continuous_at: ``` hoelzl@56370 ` 286` ``` "f complex_differentiable (at x within s) \ continuous (at x within s) f" ``` lp15@56215 ` 287` ``` by (metis DERIV_continuous complex_differentiable_def) ``` lp15@56215 ` 288` lp15@56215 ` 289` ```lemma complex_differentiable_within_subset: ``` lp15@56215 ` 290` ``` "\f complex_differentiable (at x within s); t \ s\ ``` lp15@56215 ` 291` ``` \ f complex_differentiable (at x within t)" ``` hoelzl@56370 ` 292` ``` by (metis DERIV_subset complex_differentiable_def) ``` lp15@56215 ` 293` lp15@56215 ` 294` ```lemma complex_differentiable_at_within: ``` lp15@56215 ` 295` ``` "\f complex_differentiable (at x)\ ``` lp15@56215 ` 296` ``` \ f complex_differentiable (at x within s)" ``` lp15@56215 ` 297` ``` unfolding complex_differentiable_def ``` lp15@56215 ` 298` ``` by (metis DERIV_subset top_greatest) ``` lp15@56215 ` 299` lp15@61520 ` 300` ```lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F" ``` lp15@56215 ` 301` ```proof - ``` hoelzl@56370 ` 302` ``` show ?thesis ``` hoelzl@56370 ` 303` ``` unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs ``` lp15@56215 ` 304` ``` by (force intro: has_derivative_mult_right) ``` lp15@56215 ` 305` ```qed ``` lp15@56215 ` 306` lp15@61520 ` 307` ```lemma complex_differentiable_const [derivative_intros]: "(\z. c) complex_differentiable F" ``` lp15@56215 ` 308` ``` unfolding complex_differentiable_def has_field_derivative_def ``` hoelzl@56369 ` 309` ``` by (rule exI [where x=0]) ``` lp15@61609 ` 310` ``` (metis has_derivative_const lambda_zero) ``` lp15@56215 ` 311` lp15@61520 ` 312` ```lemma complex_differentiable_ident [derivative_intros]: "(\z. z) complex_differentiable F" ``` lp15@56215 ` 313` ``` unfolding complex_differentiable_def has_field_derivative_def ``` hoelzl@56369 ` 314` ``` by (rule exI [where x=1]) ``` hoelzl@56369 ` 315` ``` (simp add: lambda_one [symmetric]) ``` lp15@56215 ` 316` lp15@61520 ` 317` ```lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F" ``` hoelzl@56370 ` 318` ``` unfolding id_def by (rule complex_differentiable_ident) ``` hoelzl@56370 ` 319` lp15@61520 ` 320` ```lemma complex_differentiable_minus [derivative_intros]: ``` hoelzl@56370 ` 321` ``` "f complex_differentiable F \ (\z. - (f z)) complex_differentiable F" ``` lp15@56215 ` 322` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 323` ``` by (metis field_differentiable_minus) ``` lp15@56215 ` 324` lp15@61520 ` 325` ```lemma complex_differentiable_add [derivative_intros]: ``` lp15@56215 ` 326` ``` assumes "f complex_differentiable F" "g complex_differentiable F" ``` lp15@56215 ` 327` ``` shows "(\z. f z + g z) complex_differentiable F" ``` lp15@56215 ` 328` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 329` ``` by (metis field_differentiable_add) ``` lp15@56215 ` 330` lp15@61520 ` 331` ```lemma complex_differentiable_setsum [derivative_intros]: ``` hoelzl@56370 ` 332` ``` "(\i. i \ I \ (f i) complex_differentiable F) \ (\z. \i\I. f i z) complex_differentiable F" ``` hoelzl@56370 ` 333` ``` by (induct I rule: infinite_finite_induct) ``` hoelzl@56370 ` 334` ``` (auto intro: complex_differentiable_add complex_differentiable_const) ``` hoelzl@56370 ` 335` lp15@61520 ` 336` ```lemma complex_differentiable_diff [derivative_intros]: ``` lp15@56215 ` 337` ``` assumes "f complex_differentiable F" "g complex_differentiable F" ``` lp15@56215 ` 338` ``` shows "(\z. f z - g z) complex_differentiable F" ``` lp15@56215 ` 339` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 340` ``` by (metis field_differentiable_diff) ``` lp15@56215 ` 341` lp15@61520 ` 342` ```lemma complex_differentiable_inverse [derivative_intros]: ``` lp15@56215 ` 343` ``` assumes "f complex_differentiable (at a within s)" "f a \ 0" ``` lp15@56215 ` 344` ``` shows "(\z. inverse (f z)) complex_differentiable (at a within s)" ``` lp15@56215 ` 345` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 346` ``` by (metis DERIV_inverse_fun) ``` lp15@56215 ` 347` lp15@61520 ` 348` ```lemma complex_differentiable_mult [derivative_intros]: ``` lp15@61609 ` 349` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 350` ``` "g complex_differentiable (at a within s)" ``` lp15@56215 ` 351` ``` shows "(\z. f z * g z) complex_differentiable (at a within s)" ``` lp15@56215 ` 352` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 353` ``` by (metis DERIV_mult [of f _ a s g]) ``` lp15@61609 ` 354` lp15@61520 ` 355` ```lemma complex_differentiable_divide [derivative_intros]: ``` lp15@61609 ` 356` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 357` ``` "g complex_differentiable (at a within s)" ``` lp15@56215 ` 358` ``` "g a \ 0" ``` lp15@56215 ` 359` ``` shows "(\z. f z / g z) complex_differentiable (at a within s)" ``` lp15@56215 ` 360` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 361` ``` by (metis DERIV_divide [of f _ a s g]) ``` lp15@56215 ` 362` lp15@61520 ` 363` ```lemma complex_differentiable_power [derivative_intros]: ``` lp15@61609 ` 364` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 365` ``` shows "(\z. f z ^ n) complex_differentiable (at a within s)" ``` lp15@56215 ` 366` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 367` ``` by (metis DERIV_power) ``` lp15@56215 ` 368` lp15@56215 ` 369` ```lemma complex_differentiable_transform_within: ``` lp15@56215 ` 370` ``` "0 < d \ ``` lp15@56215 ` 371` ``` x \ s \ ``` lp15@56215 ` 372` ``` (\x'. x' \ s \ dist x' x < d \ f x' = g x') \ ``` lp15@56215 ` 373` ``` f complex_differentiable (at x within s) ``` lp15@56215 ` 374` ``` \ g complex_differentiable (at x within s)" ``` lp15@56215 ` 375` ``` unfolding complex_differentiable_def has_field_derivative_def ``` lp15@56215 ` 376` ``` by (blast intro: has_derivative_transform_within) ``` lp15@56215 ` 377` lp15@56215 ` 378` ```lemma complex_differentiable_compose_within: ``` lp15@61609 ` 379` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 380` ``` "g complex_differentiable (at (f a) within f`s)" ``` lp15@56215 ` 381` ``` shows "(g o f) complex_differentiable (at a within s)" ``` lp15@56215 ` 382` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 383` ``` by (metis DERIV_image_chain) ``` lp15@56215 ` 384` hoelzl@56370 ` 385` ```lemma complex_differentiable_compose: ``` hoelzl@56370 ` 386` ``` "f complex_differentiable at z \ g complex_differentiable at (f z) ``` hoelzl@56370 ` 387` ``` \ (g o f) complex_differentiable at z" ``` hoelzl@56370 ` 388` ```by (metis complex_differentiable_at_within complex_differentiable_compose_within) ``` hoelzl@56370 ` 389` lp15@56215 ` 390` ```lemma complex_differentiable_within_open: ``` lp15@61609 ` 391` ``` "\a \ s; open s\ \ f complex_differentiable at a within s \ ``` lp15@56215 ` 392` ``` f complex_differentiable at a" ``` lp15@56215 ` 393` ``` unfolding complex_differentiable_def ``` lp15@56215 ` 394` ``` by (metis at_within_open) ``` lp15@56215 ` 395` wenzelm@60420 ` 396` ```subsection\Caratheodory characterization.\ ``` lp15@56215 ` 397` lp15@56215 ` 398` ```lemma complex_differentiable_caratheodory_at: ``` lp15@56215 ` 399` ``` "f complex_differentiable (at z) \ ``` lp15@56215 ` 400` ``` (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z) g)" ``` lp15@56215 ` 401` ``` using CARAT_DERIV [of f] ``` lp15@56215 ` 402` ``` by (simp add: complex_differentiable_def has_field_derivative_def) ``` lp15@56215 ` 403` lp15@56215 ` 404` ```lemma complex_differentiable_caratheodory_within: ``` lp15@56215 ` 405` ``` "f complex_differentiable (at z within s) \ ``` lp15@56215 ` 406` ``` (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z within s) g)" ``` lp15@56215 ` 407` ``` using DERIV_caratheodory_within [of f] ``` lp15@56215 ` 408` ``` by (simp add: complex_differentiable_def has_field_derivative_def) ``` lp15@56215 ` 409` wenzelm@60420 ` 410` ```subsection\Holomorphic\ ``` hoelzl@56370 ` 411` hoelzl@56370 ` 412` ```definition holomorphic_on :: "[complex \ complex, complex set] \ bool" ``` hoelzl@56370 ` 413` ``` (infixl "(holomorphic'_on)" 50) ``` hoelzl@56370 ` 414` ``` where "f holomorphic_on s \ \x\s. f complex_differentiable (at x within s)" ``` lp15@61609 ` 415` lp15@61520 ` 416` ```named_theorems holomorphic_intros "structural introduction rules for holomorphic_on" ``` lp15@61520 ` 417` paulson@62131 ` 418` ```lemma holomorphic_onI [intro?]: "(\x. x \ s \ f complex_differentiable (at x within s)) \ f holomorphic_on s" ``` paulson@62131 ` 419` ``` by (simp add: holomorphic_on_def) ``` paulson@62131 ` 420` paulson@62131 ` 421` ```lemma holomorphic_onD [dest?]: "\f holomorphic_on s; x \ s\ \ f complex_differentiable (at x within s)" ``` paulson@62131 ` 422` ``` by (simp add: holomorphic_on_def) ``` paulson@62131 ` 423` paulson@62131 ` 424` ```lemma holomorphic_on_imp_differentiable_at: ``` paulson@62131 ` 425` ``` "\f holomorphic_on s; open s; x \ s\ \ f complex_differentiable (at x)" ``` paulson@62131 ` 426` ```using at_within_open holomorphic_on_def by fastforce ``` paulson@62131 ` 427` lp15@61520 ` 428` ```lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}" ``` hoelzl@56370 ` 429` ``` by (simp add: holomorphic_on_def) ``` hoelzl@56370 ` 430` hoelzl@56370 ` 431` ```lemma holomorphic_on_open: ``` hoelzl@56370 ` 432` ``` "open s \ f holomorphic_on s \ (\x \ s. \f'. DERIV f x :> f')" ``` hoelzl@56370 ` 433` ``` by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s]) ``` hoelzl@56370 ` 434` lp15@61609 ` 435` ```lemma holomorphic_on_imp_continuous_on: ``` hoelzl@56370 ` 436` ``` "f holomorphic_on s \ continuous_on s f" ``` lp15@61609 ` 437` ``` by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def) ``` hoelzl@56370 ` 438` hoelzl@56370 ` 439` ```lemma holomorphic_on_subset: ``` hoelzl@56370 ` 440` ``` "f holomorphic_on s \ t \ s \ f holomorphic_on t" ``` hoelzl@56370 ` 441` ``` unfolding holomorphic_on_def ``` hoelzl@56370 ` 442` ``` by (metis complex_differentiable_within_subset subsetD) ``` hoelzl@56370 ` 443` hoelzl@56370 ` 444` ```lemma holomorphic_transform: "\f holomorphic_on s; \x. x \ s \ f x = g x\ \ g holomorphic_on s" ``` hoelzl@56370 ` 445` ``` by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def) ``` hoelzl@56370 ` 446` hoelzl@56370 ` 447` ```lemma holomorphic_cong: "s = t ==> (\x. x \ s \ f x = g x) \ f holomorphic_on s \ g holomorphic_on t" ``` hoelzl@56370 ` 448` ``` by (metis holomorphic_transform) ``` hoelzl@56370 ` 449` lp15@62217 ` 450` ```lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s" ``` hoelzl@56370 ` 451` ``` unfolding holomorphic_on_def by (metis complex_differentiable_linear) ``` hoelzl@56370 ` 452` lp15@62217 ` 453` ```lemma holomorphic_on_const [simp, holomorphic_intros]: "(\z. c) holomorphic_on s" ``` hoelzl@56370 ` 454` ``` unfolding holomorphic_on_def by (metis complex_differentiable_const) ``` hoelzl@56370 ` 455` lp15@62217 ` 456` ```lemma holomorphic_on_ident [simp, holomorphic_intros]: "(\x. x) holomorphic_on s" ``` hoelzl@56370 ` 457` ``` unfolding holomorphic_on_def by (metis complex_differentiable_ident) ``` hoelzl@56370 ` 458` lp15@62217 ` 459` ```lemma holomorphic_on_id [simp, holomorphic_intros]: "id holomorphic_on s" ``` hoelzl@56370 ` 460` ``` unfolding id_def by (rule holomorphic_on_ident) ``` hoelzl@56370 ` 461` hoelzl@56370 ` 462` ```lemma holomorphic_on_compose: ``` hoelzl@56370 ` 463` ``` "f holomorphic_on s \ g holomorphic_on (f ` s) \ (g o f) holomorphic_on s" ``` hoelzl@56370 ` 464` ``` using complex_differentiable_compose_within[of f _ s g] ``` hoelzl@56370 ` 465` ``` by (auto simp: holomorphic_on_def) ``` hoelzl@56370 ` 466` hoelzl@56370 ` 467` ```lemma holomorphic_on_compose_gen: ``` hoelzl@56370 ` 468` ``` "f holomorphic_on s \ g holomorphic_on t \ f ` s \ t \ (g o f) holomorphic_on s" ``` hoelzl@56370 ` 469` ``` by (metis holomorphic_on_compose holomorphic_on_subset) ``` hoelzl@56370 ` 470` lp15@61520 ` 471` ```lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \ (\z. -(f z)) holomorphic_on s" ``` hoelzl@56370 ` 472` ``` by (metis complex_differentiable_minus holomorphic_on_def) ``` hoelzl@56370 ` 473` lp15@61520 ` 474` ```lemma holomorphic_on_add [holomorphic_intros]: ``` hoelzl@56370 ` 475` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z + g z) holomorphic_on s" ``` hoelzl@56370 ` 476` ``` unfolding holomorphic_on_def by (metis complex_differentiable_add) ``` hoelzl@56370 ` 477` lp15@61520 ` 478` ```lemma holomorphic_on_diff [holomorphic_intros]: ``` hoelzl@56370 ` 479` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z - g z) holomorphic_on s" ``` hoelzl@56370 ` 480` ``` unfolding holomorphic_on_def by (metis complex_differentiable_diff) ``` hoelzl@56370 ` 481` lp15@61520 ` 482` ```lemma holomorphic_on_mult [holomorphic_intros]: ``` hoelzl@56370 ` 483` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z * g z) holomorphic_on s" ``` hoelzl@56370 ` 484` ``` unfolding holomorphic_on_def by (metis complex_differentiable_mult) ``` hoelzl@56370 ` 485` lp15@61520 ` 486` ```lemma holomorphic_on_inverse [holomorphic_intros]: ``` hoelzl@56370 ` 487` ``` "\f holomorphic_on s; \z. z \ s \ f z \ 0\ \ (\z. inverse (f z)) holomorphic_on s" ``` hoelzl@56370 ` 488` ``` unfolding holomorphic_on_def by (metis complex_differentiable_inverse) ``` hoelzl@56370 ` 489` lp15@61520 ` 490` ```lemma holomorphic_on_divide [holomorphic_intros]: ``` hoelzl@56370 ` 491` ``` "\f holomorphic_on s; g holomorphic_on s; \z. z \ s \ g z \ 0\ \ (\z. f z / g z) holomorphic_on s" ``` hoelzl@56370 ` 492` ``` unfolding holomorphic_on_def by (metis complex_differentiable_divide) ``` hoelzl@56370 ` 493` lp15@61520 ` 494` ```lemma holomorphic_on_power [holomorphic_intros]: ``` hoelzl@56370 ` 495` ``` "f holomorphic_on s \ (\z. (f z)^n) holomorphic_on s" ``` hoelzl@56370 ` 496` ``` unfolding holomorphic_on_def by (metis complex_differentiable_power) ``` hoelzl@56370 ` 497` lp15@61520 ` 498` ```lemma holomorphic_on_setsum [holomorphic_intros]: ``` hoelzl@56370 ` 499` ``` "(\i. i \ I \ (f i) holomorphic_on s) \ (\x. setsum (\i. f i x) I) holomorphic_on s" ``` hoelzl@56370 ` 500` ``` unfolding holomorphic_on_def by (metis complex_differentiable_setsum) ``` hoelzl@56370 ` 501` hoelzl@56370 ` 502` ```lemma DERIV_deriv_iff_complex_differentiable: ``` hoelzl@56370 ` 503` ``` "DERIV f x :> deriv f x \ f complex_differentiable at x" ``` hoelzl@56370 ` 504` ``` unfolding complex_differentiable_def by (metis DERIV_imp_deriv) ``` hoelzl@56370 ` 505` hoelzl@56370 ` 506` ```lemma complex_derivative_chain: ``` hoelzl@56370 ` 507` ``` "f complex_differentiable at x \ g complex_differentiable at (f x) ``` hoelzl@56370 ` 508` ``` \ deriv (g o f) x = deriv g (f x) * deriv f x" ``` hoelzl@56370 ` 509` ``` by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv) ``` hoelzl@56370 ` 510` lp15@61848 ` 511` ```lemma deriv_linear: "deriv (\w. c * w) = (\z. c)" ``` hoelzl@56370 ` 512` ``` by (metis DERIV_imp_deriv DERIV_cmult_Id) ``` hoelzl@56370 ` 513` lp15@61848 ` 514` ```lemma deriv_ident: "deriv (\w. w) = (\z. 1)" ``` hoelzl@56370 ` 515` ``` by (metis DERIV_imp_deriv DERIV_ident) ``` hoelzl@56370 ` 516` lp15@61848 ` 517` ```lemma deriv_const: "deriv (\w. c) = (\z. 0)" ``` hoelzl@56370 ` 518` ``` by (metis DERIV_imp_deriv DERIV_const) ``` hoelzl@56370 ` 519` hoelzl@56370 ` 520` ```lemma complex_derivative_add: ``` lp15@61609 ` 521` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 522` ``` \ deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 523` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 524` ``` by (auto intro!: DERIV_imp_deriv derivative_intros) ``` hoelzl@56370 ` 525` hoelzl@56370 ` 526` ```lemma complex_derivative_diff: ``` lp15@61609 ` 527` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 528` ``` \ deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 529` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 530` ``` by (auto intro!: DERIV_imp_deriv derivative_intros) ``` hoelzl@56370 ` 531` hoelzl@56370 ` 532` ```lemma complex_derivative_mult: ``` lp15@61609 ` 533` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 534` ``` \ deriv (\w. f w * g w) z = f z * deriv g z + deriv f z * g z" ``` hoelzl@56370 ` 535` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 536` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 537` hoelzl@56370 ` 538` ```lemma complex_derivative_cmult: ``` hoelzl@56370 ` 539` ``` "f complex_differentiable at z \ deriv (\w. c * f w) z = c * deriv f z" ``` hoelzl@56370 ` 540` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 541` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 542` hoelzl@56370 ` 543` ```lemma complex_derivative_cmult_right: ``` hoelzl@56370 ` 544` ``` "f complex_differentiable at z \ deriv (\w. f w * c) z = deriv f z * c" ``` hoelzl@56370 ` 545` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 546` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 547` lp15@62217 ` 548` ```lemma complex_derivative_cdivide_right: ``` lp15@62217 ` 549` ``` "f complex_differentiable at z \ deriv (\w. f w / c) z = deriv f z / c" ``` lp15@62217 ` 550` ``` unfolding Fields.field_class.field_divide_inverse ``` lp15@62217 ` 551` ``` by (blast intro: complex_derivative_cmult_right) ``` lp15@62217 ` 552` hoelzl@56370 ` 553` ```lemma complex_derivative_transform_within_open: ``` lp15@61609 ` 554` ``` "\f holomorphic_on s; g holomorphic_on s; open s; z \ s; \w. w \ s \ f w = g w\ ``` hoelzl@56370 ` 555` ``` \ deriv f z = deriv g z" ``` hoelzl@56370 ` 556` ``` unfolding holomorphic_on_def ``` hoelzl@56370 ` 557` ``` by (rule DERIV_imp_deriv) ``` hoelzl@56370 ` 558` ``` (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open) ``` hoelzl@56370 ` 559` hoelzl@56370 ` 560` ```lemma complex_derivative_compose_linear: ``` hoelzl@56370 ` 561` ``` "f complex_differentiable at (c * z) \ deriv (\w. f (c * w)) z = c * deriv f (c * z)" ``` hoelzl@56370 ` 562` ```apply (rule DERIV_imp_deriv) ``` hoelzl@56370 ` 563` ```apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric]) ``` haftmann@59554 ` 564` ```apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id]) ``` haftmann@59554 ` 565` ```apply (simp add: algebra_simps) ``` hoelzl@56370 ` 566` ```done ``` hoelzl@56370 ` 567` wenzelm@60420 ` 568` ```subsection\Analyticity on a set\ ``` lp15@56215 ` 569` lp15@61609 ` 570` ```definition analytic_on (infixl "(analytic'_on)" 50) ``` lp15@56215 ` 571` ``` where ``` lp15@56215 ` 572` ``` "f analytic_on s \ \x \ s. \e. 0 < e \ f holomorphic_on (ball x e)" ``` lp15@56215 ` 573` hoelzl@56370 ` 574` ```lemma analytic_imp_holomorphic: "f analytic_on s \ f holomorphic_on s" ``` hoelzl@56370 ` 575` ``` by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def) ``` hoelzl@56370 ` 576` ``` (metis centre_in_ball complex_differentiable_at_within) ``` lp15@56215 ` 577` hoelzl@56370 ` 578` ```lemma analytic_on_open: "open s \ f analytic_on s \ f holomorphic_on s" ``` lp15@56215 ` 579` ```apply (auto simp: analytic_imp_holomorphic) ``` lp15@56215 ` 580` ```apply (auto simp: analytic_on_def holomorphic_on_def) ``` lp15@56215 ` 581` ```by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball) ``` lp15@56215 ` 582` lp15@56215 ` 583` ```lemma analytic_on_imp_differentiable_at: ``` lp15@56215 ` 584` ``` "f analytic_on s \ x \ s \ f complex_differentiable (at x)" ``` hoelzl@56370 ` 585` ``` apply (auto simp: analytic_on_def holomorphic_on_def) ``` lp15@56215 ` 586` ```by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open) ``` lp15@56215 ` 587` hoelzl@56370 ` 588` ```lemma analytic_on_subset: "f analytic_on s \ t \ s \ f analytic_on t" ``` lp15@56215 ` 589` ``` by (auto simp: analytic_on_def) ``` lp15@56215 ` 590` hoelzl@56370 ` 591` ```lemma analytic_on_Un: "f analytic_on (s \ t) \ f analytic_on s \ f analytic_on t" ``` lp15@56215 ` 592` ``` by (auto simp: analytic_on_def) ``` lp15@56215 ` 593` wenzelm@60585 ` 594` ```lemma analytic_on_Union: "f analytic_on (\s) \ (\t \ s. f analytic_on t)" ``` hoelzl@56370 ` 595` ``` by (auto simp: analytic_on_def) ``` hoelzl@56370 ` 596` hoelzl@56370 ` 597` ```lemma analytic_on_UN: "f analytic_on (\i\I. s i) \ (\i\I. f analytic_on (s i))" ``` lp15@56215 ` 598` ``` by (auto simp: analytic_on_def) ``` lp15@61609 ` 599` lp15@56215 ` 600` ```lemma analytic_on_holomorphic: ``` lp15@56215 ` 601` ``` "f analytic_on s \ (\t. open t \ s \ t \ f holomorphic_on t)" ``` lp15@56215 ` 602` ``` (is "?lhs = ?rhs") ``` lp15@56215 ` 603` ```proof - ``` lp15@56215 ` 604` ``` have "?lhs \ (\t. open t \ s \ t \ f analytic_on t)" ``` lp15@56215 ` 605` ``` proof safe ``` lp15@56215 ` 606` ``` assume "f analytic_on s" ``` lp15@56215 ` 607` ``` then show "\t. open t \ s \ t \ f analytic_on t" ``` lp15@56215 ` 608` ``` apply (simp add: analytic_on_def) ``` lp15@56215 ` 609` ``` apply (rule exI [where x="\{u. open u \ f analytic_on u}"], auto) ``` lp15@56215 ` 610` ``` apply (metis Topology_Euclidean_Space.open_ball analytic_on_open centre_in_ball) ``` lp15@56215 ` 611` ``` by (metis analytic_on_def) ``` lp15@56215 ` 612` ``` next ``` lp15@56215 ` 613` ``` fix t ``` lp15@61609 ` 614` ``` assume "open t" "s \ t" "f analytic_on t" ``` lp15@56215 ` 615` ``` then show "f analytic_on s" ``` lp15@56215 ` 616` ``` by (metis analytic_on_subset) ``` lp15@56215 ` 617` ``` qed ``` lp15@56215 ` 618` ``` also have "... \ ?rhs" ``` lp15@56215 ` 619` ``` by (auto simp: analytic_on_open) ``` lp15@56215 ` 620` ``` finally show ?thesis . ``` lp15@56215 ` 621` ```qed ``` lp15@56215 ` 622` lp15@56215 ` 623` ```lemma analytic_on_linear: "(op * c) analytic_on s" ``` hoelzl@56370 ` 624` ``` by (auto simp add: analytic_on_holomorphic holomorphic_on_linear) ``` lp15@56215 ` 625` lp15@56215 ` 626` ```lemma analytic_on_const: "(\z. c) analytic_on s" ``` hoelzl@56370 ` 627` ``` by (metis analytic_on_def holomorphic_on_const zero_less_one) ``` hoelzl@56370 ` 628` hoelzl@56370 ` 629` ```lemma analytic_on_ident: "(\x. x) analytic_on s" ``` hoelzl@56370 ` 630` ``` by (simp add: analytic_on_def holomorphic_on_ident gt_ex) ``` lp15@56215 ` 631` lp15@56215 ` 632` ```lemma analytic_on_id: "id analytic_on s" ``` hoelzl@56370 ` 633` ``` unfolding id_def by (rule analytic_on_ident) ``` lp15@56215 ` 634` lp15@56215 ` 635` ```lemma analytic_on_compose: ``` lp15@56215 ` 636` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 637` ``` and g: "g analytic_on (f ` s)" ``` lp15@56215 ` 638` ``` shows "(g o f) analytic_on s" ``` lp15@56215 ` 639` ```unfolding analytic_on_def ``` lp15@56215 ` 640` ```proof (intro ballI) ``` lp15@56215 ` 641` ``` fix x ``` lp15@56215 ` 642` ``` assume x: "x \ s" ``` lp15@56215 ` 643` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f ``` lp15@56215 ` 644` ``` by (metis analytic_on_def) ``` lp15@56215 ` 645` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g ``` lp15@61609 ` 646` ``` by (metis analytic_on_def g image_eqI x) ``` lp15@56215 ` 647` ``` have "isCont f x" ``` lp15@56215 ` 648` ``` by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x) ``` lp15@56215 ` 649` ``` with e' obtain d where d: "0 < d" and fd: "f ` ball x d \ ball (f x) e'" ``` lp15@56215 ` 650` ``` by (auto simp: continuous_at_ball) ``` lp15@61609 ` 651` ``` have "g \ f holomorphic_on ball x (min d e)" ``` lp15@56215 ` 652` ``` apply (rule holomorphic_on_compose) ``` lp15@56215 ` 653` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 654` ``` by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball) ``` lp15@56215 ` 655` ``` then show "\e>0. g \ f holomorphic_on ball x e" ``` lp15@61609 ` 656` ``` by (metis d e min_less_iff_conj) ``` lp15@56215 ` 657` ```qed ``` lp15@56215 ` 658` lp15@56215 ` 659` ```lemma analytic_on_compose_gen: ``` lp15@56215 ` 660` ``` "f analytic_on s \ g analytic_on t \ (\z. z \ s \ f z \ t) ``` lp15@56215 ` 661` ``` \ g o f analytic_on s" ``` lp15@56215 ` 662` ```by (metis analytic_on_compose analytic_on_subset image_subset_iff) ``` lp15@56215 ` 663` lp15@56215 ` 664` ```lemma analytic_on_neg: ``` lp15@56215 ` 665` ``` "f analytic_on s \ (\z. -(f z)) analytic_on s" ``` lp15@56215 ` 666` ```by (metis analytic_on_holomorphic holomorphic_on_minus) ``` lp15@56215 ` 667` lp15@56215 ` 668` ```lemma analytic_on_add: ``` lp15@56215 ` 669` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 670` ``` and g: "g analytic_on s" ``` lp15@56215 ` 671` ``` shows "(\z. f z + g z) analytic_on s" ``` lp15@56215 ` 672` ```unfolding analytic_on_def ``` lp15@56215 ` 673` ```proof (intro ballI) ``` lp15@56215 ` 674` ``` fix z ``` lp15@56215 ` 675` ``` assume z: "z \ s" ``` lp15@56215 ` 676` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 677` ``` by (metis analytic_on_def) ``` lp15@56215 ` 678` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 679` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 680` ``` have "(\z. f z + g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 681` ``` apply (rule holomorphic_on_add) ``` lp15@56215 ` 682` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 683` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 684` ``` then show "\e>0. (\z. f z + g z) holomorphic_on ball z e" ``` lp15@56215 ` 685` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 686` ```qed ``` lp15@56215 ` 687` lp15@56215 ` 688` ```lemma analytic_on_diff: ``` lp15@56215 ` 689` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 690` ``` and g: "g analytic_on s" ``` lp15@56215 ` 691` ``` shows "(\z. f z - g z) analytic_on s" ``` lp15@56215 ` 692` ```unfolding analytic_on_def ``` lp15@56215 ` 693` ```proof (intro ballI) ``` lp15@56215 ` 694` ``` fix z ``` lp15@56215 ` 695` ``` assume z: "z \ s" ``` lp15@56215 ` 696` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 697` ``` by (metis analytic_on_def) ``` lp15@56215 ` 698` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 699` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 700` ``` have "(\z. f z - g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 701` ``` apply (rule holomorphic_on_diff) ``` lp15@56215 ` 702` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 703` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 704` ``` then show "\e>0. (\z. f z - g z) holomorphic_on ball z e" ``` lp15@56215 ` 705` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 706` ```qed ``` lp15@56215 ` 707` lp15@56215 ` 708` ```lemma analytic_on_mult: ``` lp15@56215 ` 709` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 710` ``` and g: "g analytic_on s" ``` lp15@56215 ` 711` ``` shows "(\z. f z * g z) analytic_on s" ``` lp15@56215 ` 712` ```unfolding analytic_on_def ``` lp15@56215 ` 713` ```proof (intro ballI) ``` lp15@56215 ` 714` ``` fix z ``` lp15@56215 ` 715` ``` assume z: "z \ s" ``` lp15@56215 ` 716` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 717` ``` by (metis analytic_on_def) ``` lp15@56215 ` 718` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 719` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 720` ``` have "(\z. f z * g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 721` ``` apply (rule holomorphic_on_mult) ``` lp15@56215 ` 722` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 723` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 724` ``` then show "\e>0. (\z. f z * g z) holomorphic_on ball z e" ``` lp15@56215 ` 725` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 726` ```qed ``` lp15@56215 ` 727` lp15@56215 ` 728` ```lemma analytic_on_inverse: ``` lp15@56215 ` 729` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 730` ``` and nz: "(\z. z \ s \ f z \ 0)" ``` lp15@56215 ` 731` ``` shows "(\z. inverse (f z)) analytic_on s" ``` lp15@56215 ` 732` ```unfolding analytic_on_def ``` lp15@56215 ` 733` ```proof (intro ballI) ``` lp15@56215 ` 734` ``` fix z ``` lp15@56215 ` 735` ``` assume z: "z \ s" ``` lp15@56215 ` 736` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 737` ``` by (metis analytic_on_def) ``` lp15@56215 ` 738` ``` have "continuous_on (ball z e) f" ``` lp15@56215 ` 739` ``` by (metis fh holomorphic_on_imp_continuous_on) ``` lp15@61609 ` 740` ``` then obtain e' where e': "0 < e'" and nz': "\y. dist z y < e' \ f y \ 0" ``` lp15@61609 ` 741` ``` by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz) ``` lp15@61609 ` 742` ``` have "(\z. inverse (f z)) holomorphic_on ball z (min e e')" ``` lp15@56215 ` 743` ``` apply (rule holomorphic_on_inverse) ``` lp15@56215 ` 744` ``` apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball) ``` lp15@61609 ` 745` ``` by (metis nz' mem_ball min_less_iff_conj) ``` lp15@56215 ` 746` ``` then show "\e>0. (\z. inverse (f z)) holomorphic_on ball z e" ``` lp15@56215 ` 747` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 748` ```qed ``` lp15@56215 ` 749` lp15@56215 ` 750` lp15@56215 ` 751` ```lemma analytic_on_divide: ``` lp15@56215 ` 752` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 753` ``` and g: "g analytic_on s" ``` lp15@56215 ` 754` ``` and nz: "(\z. z \ s \ g z \ 0)" ``` lp15@56215 ` 755` ``` shows "(\z. f z / g z) analytic_on s" ``` lp15@56215 ` 756` ```unfolding divide_inverse ``` lp15@56215 ` 757` ```by (metis analytic_on_inverse analytic_on_mult f g nz) ``` lp15@56215 ` 758` lp15@56215 ` 759` ```lemma analytic_on_power: ``` lp15@56215 ` 760` ``` "f analytic_on s \ (\z. (f z) ^ n) analytic_on s" ``` lp15@56215 ` 761` ```by (induct n) (auto simp: analytic_on_const analytic_on_mult) ``` lp15@56215 ` 762` lp15@56215 ` 763` ```lemma analytic_on_setsum: ``` hoelzl@56369 ` 764` ``` "(\i. i \ I \ (f i) analytic_on s) \ (\x. setsum (\i. f i x) I) analytic_on s" ``` hoelzl@56369 ` 765` ``` by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add) ``` lp15@56215 ` 766` wenzelm@60420 ` 767` ```subsection\analyticity at a point.\ ``` lp15@56215 ` 768` lp15@56215 ` 769` ```lemma analytic_at_ball: ``` lp15@56215 ` 770` ``` "f analytic_on {z} \ (\e. 0 f holomorphic_on ball z e)" ``` lp15@56215 ` 771` ```by (metis analytic_on_def singleton_iff) ``` lp15@56215 ` 772` lp15@56215 ` 773` ```lemma analytic_at: ``` lp15@56215 ` 774` ``` "f analytic_on {z} \ (\s. open s \ z \ s \ f holomorphic_on s)" ``` lp15@56215 ` 775` ```by (metis analytic_on_holomorphic empty_subsetI insert_subset) ``` lp15@56215 ` 776` lp15@56215 ` 777` ```lemma analytic_on_analytic_at: ``` lp15@56215 ` 778` ``` "f analytic_on s \ (\z \ s. f analytic_on {z})" ``` lp15@56215 ` 779` ```by (metis analytic_at_ball analytic_on_def) ``` lp15@56215 ` 780` lp15@56215 ` 781` ```lemma analytic_at_two: ``` lp15@56215 ` 782` ``` "f analytic_on {z} \ g analytic_on {z} \ ``` lp15@56215 ` 783` ``` (\s. open s \ z \ s \ f holomorphic_on s \ g holomorphic_on s)" ``` lp15@56215 ` 784` ``` (is "?lhs = ?rhs") ``` lp15@61609 ` 785` ```proof ``` lp15@56215 ` 786` ``` assume ?lhs ``` lp15@61609 ` 787` ``` then obtain s t ``` lp15@56215 ` 788` ``` where st: "open s" "z \ s" "f holomorphic_on s" ``` lp15@56215 ` 789` ``` "open t" "z \ t" "g holomorphic_on t" ``` lp15@56215 ` 790` ``` by (auto simp: analytic_at) ``` lp15@56215 ` 791` ``` show ?rhs ``` lp15@56215 ` 792` ``` apply (rule_tac x="s \ t" in exI) ``` lp15@56215 ` 793` ``` using st ``` lp15@56215 ` 794` ``` apply (auto simp: Diff_subset holomorphic_on_subset) ``` lp15@56215 ` 795` ``` done ``` lp15@56215 ` 796` ```next ``` lp15@61609 ` 797` ``` assume ?rhs ``` lp15@56215 ` 798` ``` then show ?lhs ``` lp15@56215 ` 799` ``` by (force simp add: analytic_at) ``` lp15@56215 ` 800` ```qed ``` lp15@56215 ` 801` wenzelm@60420 ` 802` ```subsection\Combining theorems for derivative with ``analytic at'' hypotheses\ ``` lp15@56215 ` 803` lp15@61609 ` 804` ```lemma ``` lp15@56215 ` 805` ``` assumes "f analytic_on {z}" "g analytic_on {z}" ``` hoelzl@56370 ` 806` ``` shows complex_derivative_add_at: "deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 807` ``` and complex_derivative_diff_at: "deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 808` ``` and complex_derivative_mult_at: "deriv (\w. f w * g w) z = ``` hoelzl@56370 ` 809` ``` f z * deriv g z + deriv f z * g z" ``` lp15@56215 ` 810` ```proof - ``` lp15@56215 ` 811` ``` obtain s where s: "open s" "z \ s" "f holomorphic_on s" "g holomorphic_on s" ``` lp15@56215 ` 812` ``` using assms by (metis analytic_at_two) ``` hoelzl@56370 ` 813` ``` show "deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 814` ``` apply (rule DERIV_imp_deriv [OF DERIV_add]) ``` lp15@56215 ` 815` ``` using s ``` hoelzl@56370 ` 816` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 817` ``` done ``` hoelzl@56370 ` 818` ``` show "deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 819` ``` apply (rule DERIV_imp_deriv [OF DERIV_diff]) ``` lp15@56215 ` 820` ``` using s ``` hoelzl@56370 ` 821` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 822` ``` done ``` hoelzl@56370 ` 823` ``` show "deriv (\w. f w * g w) z = f z * deriv g z + deriv f z * g z" ``` hoelzl@56370 ` 824` ``` apply (rule DERIV_imp_deriv [OF DERIV_mult']) ``` lp15@56215 ` 825` ``` using s ``` hoelzl@56370 ` 826` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 827` ``` done ``` lp15@56215 ` 828` ```qed ``` lp15@56215 ` 829` lp15@56215 ` 830` ```lemma complex_derivative_cmult_at: ``` hoelzl@56370 ` 831` ``` "f analytic_on {z} \ deriv (\w. c * f w) z = c * deriv f z" ``` lp15@61848 ` 832` ```by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const) ``` lp15@56215 ` 833` lp15@56215 ` 834` ```lemma complex_derivative_cmult_right_at: ``` hoelzl@56370 ` 835` ``` "f analytic_on {z} \ deriv (\w. f w * c) z = deriv f z * c" ``` lp15@61848 ` 836` ```by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const) ``` lp15@56215 ` 837` wenzelm@60420 ` 838` ```subsection\Complex differentiation of sequences and series\ ``` lp15@56215 ` 839` eberlm@61531 ` 840` ```(* TODO: Could probably be simplified using Uniform_Limit *) ``` lp15@56215 ` 841` ```lemma has_complex_derivative_sequence: ``` lp15@56215 ` 842` ``` fixes s :: "complex set" ``` lp15@56215 ` 843` ``` assumes cvs: "convex s" ``` lp15@56215 ` 844` ``` and df: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" ``` lp15@56215 ` 845` ``` and conv: "\e. 0 < e \ \N. \n x. n \ N \ x \ s \ norm (f' n x - g' x) \ e" ``` wenzelm@61973 ` 846` ``` and "\x l. x \ s \ ((\n. f n x) \ l) sequentially" ``` wenzelm@61973 ` 847` ``` shows "\g. \x \ s. ((\n. f n x) \ g x) sequentially \ ``` lp15@56215 ` 848` ``` (g has_field_derivative (g' x)) (at x within s)" ``` lp15@56215 ` 849` ```proof - ``` wenzelm@61973 ` 850` ``` from assms obtain x l where x: "x \ s" and tf: "((\n. f n x) \ l) sequentially" ``` lp15@56215 ` 851` ``` by blast ``` lp15@56215 ` 852` ``` { fix e::real assume e: "e > 0" ``` lp15@56215 ` 853` ``` then obtain N where N: "\n\N. \x. x \ s \ cmod (f' n x - g' x) \ e" ``` lp15@61609 ` 854` ``` by (metis conv) ``` lp15@56215 ` 855` ``` have "\N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" ``` lp15@56215 ` 856` ``` proof (rule exI [of _ N], clarify) ``` lp15@56215 ` 857` ``` fix n y h ``` lp15@56215 ` 858` ``` assume "N \ n" "y \ s" ``` lp15@56215 ` 859` ``` then have "cmod (f' n y - g' y) \ e" ``` lp15@56215 ` 860` ``` by (metis N) ``` lp15@56215 ` 861` ``` then have "cmod h * cmod (f' n y - g' y) \ cmod h * e" ``` lp15@56215 ` 862` ``` by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) ``` lp15@56215 ` 863` ``` then show "cmod (f' n y * h - g' y * h) \ e * cmod h" ``` lp15@56215 ` 864` ``` by (simp add: norm_mult [symmetric] field_simps) ``` lp15@56215 ` 865` ``` qed ``` lp15@56215 ` 866` ``` } note ** = this ``` lp15@56215 ` 867` ``` show ?thesis ``` lp15@56215 ` 868` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 869` ``` proof (rule has_derivative_sequence [OF cvs _ _ x]) ``` lp15@56215 ` 870` ``` show "\n. \x\s. (f n has_derivative (op * (f' n x))) (at x within s)" ``` lp15@56215 ` 871` ``` by (metis has_field_derivative_def df) ``` wenzelm@61969 ` 872` ``` next show "(\n. f n x) \ l" ``` lp15@56215 ` 873` ``` by (rule tf) ``` lp15@56215 ` 874` ``` next show "\e>0. \N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" ``` lp15@56215 ` 875` ``` by (blast intro: **) ``` lp15@56215 ` 876` ``` qed ``` lp15@56215 ` 877` ```qed ``` lp15@56215 ` 878` lp15@56215 ` 879` lp15@56215 ` 880` ```lemma has_complex_derivative_series: ``` lp15@56215 ` 881` ``` fixes s :: "complex set" ``` lp15@56215 ` 882` ``` assumes cvs: "convex s" ``` lp15@56215 ` 883` ``` and df: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" ``` lp15@61609 ` 884` ``` and conv: "\e. 0 < e \ \N. \n x. n \ N \ x \ s ``` lp15@56215 ` 885` ``` \ cmod ((\i e" ``` lp15@56215 ` 886` ``` and "\x l. x \ s \ ((\n. f n x) sums l)" ``` lp15@56215 ` 887` ``` shows "\g. \x \ s. ((\n. f n x) sums g x) \ ((g has_field_derivative g' x) (at x within s))" ``` lp15@56215 ` 888` ```proof - ``` lp15@56215 ` 889` ``` from assms obtain x l where x: "x \ s" and sf: "((\n. f n x) sums l)" ``` lp15@56215 ` 890` ``` by blast ``` lp15@56215 ` 891` ``` { fix e::real assume e: "e > 0" ``` lp15@61609 ` 892` ``` then obtain N where N: "\n x. n \ N \ x \ s ``` lp15@56215 ` 893` ``` \ cmod ((\i e" ``` lp15@61609 ` 894` ``` by (metis conv) ``` lp15@56215 ` 895` ``` have "\N. \n\N. \x\s. \h. cmod ((\i e * cmod h" ``` lp15@56215 ` 896` ``` proof (rule exI [of _ N], clarify) ``` lp15@56215 ` 897` ``` fix n y h ``` lp15@56215 ` 898` ``` assume "N \ n" "y \ s" ``` lp15@56215 ` 899` ``` then have "cmod ((\i e" ``` lp15@56215 ` 900` ``` by (metis N) ``` lp15@56215 ` 901` ``` then have "cmod h * cmod ((\i cmod h * e" ``` lp15@56215 ` 902` ``` by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) ``` lp15@56215 ` 903` ``` then show "cmod ((\i e * cmod h" ``` lp15@56215 ` 904` ``` by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib) ``` lp15@56215 ` 905` ``` qed ``` lp15@56215 ` 906` ``` } note ** = this ``` lp15@56215 ` 907` ``` show ?thesis ``` lp15@56215 ` 908` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 909` ``` proof (rule has_derivative_series [OF cvs _ _ x]) ``` lp15@56215 ` 910` ``` fix n x ``` lp15@56215 ` 911` ``` assume "x \ s" ``` lp15@56215 ` 912` ``` then show "((f n) has_derivative (\z. z * f' n x)) (at x within s)" ``` lp15@56215 ` 913` ``` by (metis df has_field_derivative_def mult_commute_abs) ``` lp15@56215 ` 914` ``` next show " ((\n. f n x) sums l)" ``` lp15@56215 ` 915` ``` by (rule sf) ``` lp15@56215 ` 916` ``` next show "\e>0. \N. \n\N. \x\s. \h. cmod ((\i e * cmod h" ``` lp15@56215 ` 917` ``` by (blast intro: **) ``` lp15@56215 ` 918` ``` qed ``` lp15@56215 ` 919` ```qed ``` lp15@56215 ` 920` eberlm@61531 ` 921` eberlm@61531 ` 922` ```lemma complex_differentiable_series: ``` eberlm@61531 ` 923` ``` fixes f :: "nat \ complex \ complex" ``` eberlm@61531 ` 924` ``` assumes "convex s" "open s" ``` eberlm@61531 ` 925` ``` assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" ``` eberlm@61531 ` 926` ``` assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" and x: "x \ s" ``` eberlm@61531 ` 928` ``` shows "summable (\n. f n x)" and "(\x. \n. f n x) complex_differentiable (at x)" ``` eberlm@61531 ` 929` ```proof - ``` eberlm@61531 ` 930` ``` from assms(4) obtain g' where A: "uniform_limit s (\n x. \iopen s\ have s: "at x within s = at x" by (rule at_within_open) ``` eberlm@61531 ` 933` ``` have "\g. \x\s. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within s)" ``` eberlm@61531 ` 934` ``` by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within) ``` eberlm@61531 ` 935` ``` then obtain g where g: "\x. x \ s \ (\n. f n x) sums g x" ``` eberlm@61531 ` 936` ``` "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast ``` eberlm@61531 ` 937` ``` from g[OF x] show "summable (\n. f n x)" by (auto simp: summable_def) ``` eberlm@61531 ` 938` ``` from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)" ``` eberlm@61531 ` 939` ``` by (simp add: has_field_derivative_def s) ``` eberlm@61531 ` 940` ``` have "((\x. \n. f n x) has_derivative op * (g' x)) (at x)" ``` paulson@62087 ` 941` ``` by (rule has_derivative_transform_within_open[OF g' \open s\ x]) ``` eberlm@61531 ` 942` ``` (insert g, auto simp: sums_iff) ``` eberlm@61531 ` 943` ``` thus "(\x. \n. f n x) complex_differentiable (at x)" unfolding differentiable_def ``` eberlm@61531 ` 944` ``` by (auto simp: summable_def complex_differentiable_def has_field_derivative_def) ``` eberlm@61531 ` 945` ```qed ``` eberlm@61531 ` 946` eberlm@61531 ` 947` ```lemma complex_differentiable_series': ``` eberlm@61531 ` 948` ``` fixes f :: "nat \ complex \ complex" ``` eberlm@61531 ` 949` ``` assumes "convex s" "open s" ``` eberlm@61531 ` 950` ``` assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" ``` eberlm@61531 ` 951` ``` assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" ``` eberlm@61531 ` 953` ``` shows "(\x. \n. f n x) complex_differentiable (at x0)" ``` wenzelm@61808 ` 954` ``` using complex_differentiable_series[OF assms, of x0] \x0 \ s\ by blast+ ``` eberlm@61531 ` 955` wenzelm@60420 ` 956` ```subsection\Bound theorem\ ``` lp15@56215 ` 957` lp15@56215 ` 958` ```lemma complex_differentiable_bound: ``` lp15@56215 ` 959` ``` fixes s :: "complex set" ``` lp15@56215 ` 960` ``` assumes cvs: "convex s" ``` lp15@56215 ` 961` ``` and df: "\z. z \ s \ (f has_field_derivative f' z) (at z within s)" ``` lp15@56215 ` 962` ``` and dn: "\z. z \ s \ norm (f' z) \ B" ``` lp15@56215 ` 963` ``` and "x \ s" "y \ s" ``` lp15@56215 ` 964` ``` shows "norm(f x - f y) \ B * norm(x - y)" ``` lp15@56215 ` 965` ``` apply (rule differentiable_bound [OF cvs]) ``` huffman@56223 ` 966` ``` apply (rule ballI, erule df [unfolded has_field_derivative_def]) ``` huffman@56223 ` 967` ``` apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn) ``` huffman@56223 ` 968` ``` apply fact ``` huffman@56223 ` 969` ``` apply fact ``` lp15@56215 ` 970` ``` done ``` lp15@56215 ` 971` wenzelm@60420 ` 972` ```subsection\Inverse function theorem for complex derivatives.\ ``` lp15@56215 ` 973` lp15@56215 ` 974` ```lemma has_complex_derivative_inverse_basic: ``` lp15@56215 ` 975` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 976` ``` shows "DERIV f (g y) :> f' \ ``` lp15@56215 ` 977` ``` f' \ 0 \ ``` lp15@56215 ` 978` ``` continuous (at y) g \ ``` lp15@56215 ` 979` ``` open t \ ``` lp15@56215 ` 980` ``` y \ t \ ``` lp15@56215 ` 981` ``` (\z. z \ t \ f (g z) = z) ``` lp15@56215 ` 982` ``` \ DERIV g y :> inverse (f')" ``` lp15@56215 ` 983` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 984` ``` apply (rule has_derivative_inverse_basic) ``` lp15@56215 ` 985` ``` apply (auto simp: bounded_linear_mult_right) ``` lp15@56215 ` 986` ``` done ``` lp15@56215 ` 987` lp15@56215 ` 988` ```(*Used only once, in Multivariate/cauchy.ml. *) ``` lp15@56215 ` 989` ```lemma has_complex_derivative_inverse_strong: ``` lp15@56215 ` 990` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 991` ``` shows "DERIV f x :> f' \ ``` lp15@56215 ` 992` ``` f' \ 0 \ ``` lp15@56215 ` 993` ``` open s \ ``` lp15@56215 ` 994` ``` x \ s \ ``` lp15@56215 ` 995` ``` continuous_on s f \ ``` lp15@56215 ` 996` ``` (\z. z \ s \ g (f z) = z) ``` lp15@56215 ` 997` ``` \ DERIV g (f x) :> inverse (f')" ``` lp15@56215 ` 998` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 999` ``` apply (rule has_derivative_inverse_strong [of s x f g ]) ``` lp15@61609 ` 1000` ``` using assms ``` lp15@56215 ` 1001` ``` by auto ``` lp15@56215 ` 1002` lp15@56215 ` 1003` ```lemma has_complex_derivative_inverse_strong_x: ``` lp15@56215 ` 1004` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 1005` ``` shows "DERIV f (g y) :> f' \ ``` lp15@56215 ` 1006` ``` f' \ 0 \ ``` lp15@56215 ` 1007` ``` open s \ ``` lp15@56215 ` 1008` ``` continuous_on s f \ ``` lp15@56215 ` 1009` ``` g y \ s \ f(g y) = y \ ``` lp15@56215 ` 1010` ``` (\z. z \ s \ g (f z) = z) ``` lp15@56215 ` 1011` ``` \ DERIV g y :> inverse (f')" ``` lp15@56215 ` 1012` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 1013` ``` apply (rule has_derivative_inverse_strong_x [of s g y f]) ``` lp15@61609 ` 1014` ``` using assms ``` lp15@56215 ` 1015` ``` by auto ``` lp15@56215 ` 1016` wenzelm@60420 ` 1017` ```subsection \Taylor on Complex Numbers\ ``` lp15@56215 ` 1018` lp15@56215 ` 1019` ```lemma setsum_Suc_reindex: ``` lp15@56215 ` 1020` ``` fixes f :: "nat \ 'a::ab_group_add" ``` lp15@56215 ` 1021` ``` shows "setsum f {0..n} = f 0 - f (Suc n) + setsum (\i. f (Suc i)) {0..n}" ``` lp15@56215 ` 1022` ```by (induct n) auto ``` lp15@56215 ` 1023` lp15@56215 ` 1024` ```lemma complex_taylor: ``` lp15@61609 ` 1025` ``` assumes s: "convex s" ``` lp15@56215 ` 1026` ``` and f: "\i x. x \ s \ i \ n \ (f i has_field_derivative f (Suc i) x) (at x within s)" ``` lp15@56215 ` 1027` ``` and B: "\x. x \ s \ cmod (f (Suc n) x) \ B" ``` lp15@56215 ` 1028` ``` and w: "w \ s" ``` lp15@56215 ` 1029` ``` and z: "z \ s" ``` lp15@59730 ` 1030` ``` shows "cmod(f 0 z - (\i\n. f i w * (z-w) ^ i / (fact i))) ``` lp15@56215 ` 1031` ``` \ B * cmod(z - w)^(Suc n) / fact n" ``` lp15@56215 ` 1032` ```proof - ``` lp15@56215 ` 1033` ``` have wzs: "closed_segment w z \ s" using assms ``` lp15@56215 ` 1034` ``` by (metis convex_contains_segment) ``` lp15@56215 ` 1035` ``` { fix u ``` lp15@56215 ` 1036` ``` assume "u \ closed_segment w z" ``` lp15@56215 ` 1037` ``` then have "u \ s" ``` lp15@56215 ` 1038` ``` by (metis wzs subsetD) ``` lp15@59730 ` 1039` ``` have "(\i\n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) + ``` lp15@61609 ` 1040` ``` f (Suc i) u * (z-u)^i / (fact i)) = ``` lp15@59730 ` 1041` ``` f (Suc n) u * (z-u) ^ n / (fact n)" ``` lp15@56215 ` 1042` ``` proof (induction n) ``` lp15@56215 ` 1043` ``` case 0 show ?case by simp ``` lp15@56215 ` 1044` ``` next ``` lp15@56215 ` 1045` ``` case (Suc n) ``` lp15@59730 ` 1046` ``` have "(\i\Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) + ``` lp15@61609 ` 1047` ``` f (Suc i) u * (z-u) ^ i / (fact i)) = ``` lp15@59730 ` 1048` ``` f (Suc n) u * (z-u) ^ n / (fact n) + ``` lp15@59730 ` 1049` ``` f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) - ``` lp15@59730 ` 1050` ``` f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))" ``` hoelzl@56479 ` 1051` ``` using Suc by simp ``` lp15@59730 ` 1052` ``` also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))" ``` lp15@56215 ` 1053` ``` proof - ``` lp15@59730 ` 1054` ``` have "(fact(Suc n)) * ``` lp15@59730 ` 1055` ``` (f(Suc n) u *(z-u) ^ n / (fact n) + ``` lp15@59730 ` 1056` ``` f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / (fact(Suc n)) - ``` lp15@59730 ` 1057` ``` f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / (fact(Suc n))) = ``` lp15@59730 ` 1058` ``` ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) + ``` lp15@59730 ` 1059` ``` ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) - ``` lp15@59730 ` 1060` ``` ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))" ``` lp15@59730 ` 1061` ``` by (simp add: algebra_simps del: fact.simps) ``` lp15@59730 ` 1062` ``` also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) + ``` lp15@59730 ` 1063` ``` (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) - ``` lp15@59730 ` 1064` ``` (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))" ``` lp15@59730 ` 1065` ``` by (simp del: fact.simps) ``` lp15@59730 ` 1066` ``` also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) + ``` lp15@59730 ` 1067` ``` (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) - ``` lp15@59730 ` 1068` ``` (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))" ``` lp15@59730 ` 1069` ``` by (simp only: fact.simps of_nat_mult ac_simps) simp ``` lp15@56215 ` 1070` ``` also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)" ``` lp15@56215 ` 1071` ``` by (simp add: algebra_simps) ``` lp15@56215 ` 1072` ``` finally show ?thesis ``` lp15@59730 ` 1073` ``` by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps) ``` lp15@56215 ` 1074` ``` qed ``` lp15@56215 ` 1075` ``` finally show ?case . ``` lp15@56215 ` 1076` ``` qed ``` lp15@61609 ` 1077` ``` then have "((\v. (\i\n. f i v * (z - v)^i / (fact i))) ``` lp15@59730 ` 1078` ``` has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n)) ``` lp15@56215 ` 1079` ``` (at u within s)" ``` hoelzl@56381 ` 1080` ``` apply (intro derivative_eq_intros) ``` wenzelm@60420 ` 1081` ``` apply (blast intro: assms \u \ s\) ``` lp15@56215 ` 1082` ``` apply (rule refl)+ ``` lp15@56215 ` 1083` ``` apply (auto simp: field_simps) ``` lp15@56215 ` 1084` ``` done ``` lp15@56215 ` 1085` ``` } note sum_deriv = this ``` lp15@56215 ` 1086` ``` { fix u ``` lp15@56215 ` 1087` ``` assume u: "u \ closed_segment w z" ``` lp15@56215 ` 1088` ``` then have us: "u \ s" ``` lp15@56215 ` 1089` ``` by (metis wzs subsetD) ``` lp15@56215 ` 1090` ``` have "cmod (f (Suc n) u) * cmod (z - u) ^ n \ cmod (f (Suc n) u) * cmod (u - z) ^ n" ``` lp15@56215 ` 1091` ``` by (metis norm_minus_commute order_refl) ``` lp15@56215 ` 1092` ``` also have "... \ cmod (f (Suc n) u) * cmod (z - w) ^ n" ``` lp15@56215 ` 1093` ``` by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u]) ``` lp15@56215 ` 1094` ``` also have "... \ B * cmod (z - w) ^ n" ``` lp15@56215 ` 1095` ``` by (metis norm_ge_zero zero_le_power mult_right_mono B [OF us]) ``` lp15@56215 ` 1096` ``` finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \ B * cmod (z - w) ^ n" . ``` lp15@56215 ` 1097` ``` } note cmod_bound = this ``` lp15@59730 ` 1098` ``` have "(\i\n. f i z * (z - z) ^ i / (fact i)) = (\i\n. (f i z / (fact i)) * 0 ^ i)" ``` lp15@56215 ` 1099` ``` by simp ``` lp15@59730 ` 1100` ``` also have "\ = f 0 z / (fact 0)" ``` lp15@56215 ` 1101` ``` by (subst setsum_zero_power) simp ``` lp15@61609 ` 1102` ``` finally have "cmod (f 0 z - (\i\n. f i w * (z - w) ^ i / (fact i))) ``` lp15@59730 ` 1103` ``` \ cmod ((\i\n. f i w * (z - w) ^ i / (fact i)) - ``` lp15@59730 ` 1104` ``` (\i\n. f i z * (z - z) ^ i / (fact i)))" ``` lp15@56215 ` 1105` ``` by (simp add: norm_minus_commute) ``` lp15@59730 ` 1106` ``` also have "... \ B * cmod (z - w) ^ n / (fact n) * cmod (w - z)" ``` lp15@61609 ` 1107` ``` apply (rule complex_differentiable_bound ``` lp15@59730 ` 1108` ``` [where f' = "\w. f (Suc n) w * (z - w)^n / (fact n)" ``` paulson@61518 ` 1109` ``` and s = "closed_segment w z", OF convex_closed_segment]) ``` lp15@61609 ` 1110` ``` apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs] ``` lp15@56215 ` 1111` ``` norm_divide norm_mult norm_power divide_le_cancel cmod_bound) ``` lp15@56215 ` 1112` ``` done ``` lp15@59730 ` 1113` ``` also have "... \ B * cmod (z - w) ^ Suc n / (fact n)" ``` lp15@61609 ` 1114` ``` by (simp add: algebra_simps norm_minus_commute) ``` lp15@56215 ` 1115` ``` finally show ?thesis . ``` lp15@56215 ` 1116` ```qed ``` lp15@56215 ` 1117` wenzelm@60420 ` 1118` ```text\Something more like the traditional MVT for real components.\ ``` hoelzl@56370 ` 1119` lp15@56238 ` 1120` ```lemma complex_mvt_line: ``` hoelzl@56369 ` 1121` ``` assumes "\u. u \ closed_segment w z \ (f has_field_derivative f'(u)) (at u)" ``` paulson@61518 ` 1122` ``` shows "\u. u \ closed_segment w z \ Re(f z) - Re(f w) = Re(f'(u) * (z - w))" ``` lp15@56238 ` 1123` ```proof - ``` lp15@56238 ` 1124` ``` have twz: "\t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)" ``` lp15@56238 ` 1125` ``` by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) ``` hoelzl@56381 ` 1126` ``` note assms[unfolded has_field_derivative_def, derivative_intros] ``` lp15@56238 ` 1127` ``` show ?thesis ``` lp15@56238 ` 1128` ``` apply (cut_tac mvt_simple ``` lp15@56238 ` 1129` ``` [of 0 1 "Re o f o (\t. (1 - t) *\<^sub>R w + t *\<^sub>R z)" ``` lp15@56238 ` 1130` ``` "\u. Re o (\h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\t. t *\<^sub>R (z - w))"]) ``` lp15@56238 ` 1131` ``` apply auto ``` lp15@56238 ` 1132` ``` apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI) ``` paulson@61518 ` 1133` ``` apply (auto simp: closed_segment_def twz) [] ``` paulson@61518 ` 1134` ``` apply (intro derivative_eq_intros has_derivative_at_within, simp_all) ``` hoelzl@56369 ` 1135` ``` apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib) ``` paulson@61518 ` 1136` ``` apply (force simp: twz closed_segment_def) ``` lp15@56238 ` 1137` ``` done ``` lp15@56238 ` 1138` ```qed ``` lp15@56238 ` 1139` lp15@56238 ` 1140` ```lemma complex_taylor_mvt: ``` lp15@56238 ` 1141` ``` assumes "\i x. \x \ closed_segment w z; i \ n\ \ ((f i) has_field_derivative f (Suc i) x) (at x)" ``` lp15@56238 ` 1142` ``` shows "\u. u \ closed_segment w z \ ``` lp15@56238 ` 1143` ``` Re (f 0 z) = ``` lp15@59730 ` 1144` ``` Re ((\i = 0..n. f i w * (z - w) ^ i / (fact i)) + ``` lp15@59730 ` 1145` ``` (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))" ``` lp15@56238 ` 1146` ```proof - ``` lp15@56238 ` 1147` ``` { fix u ``` lp15@56238 ` 1148` ``` assume u: "u \ closed_segment w z" ``` lp15@56238 ` 1149` ``` have "(\i = 0..n. ``` lp15@56238 ` 1150` ``` (f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / ``` lp15@59730 ` 1151` ``` (fact i)) = ``` lp15@56238 ` 1152` ``` f (Suc 0) u - ``` lp15@56238 ` 1153` ``` (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1154` ``` (fact (Suc n)) + ``` lp15@56238 ` 1155` ``` (\i = 0..n. ``` lp15@56238 ` 1156` ``` (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) / ``` lp15@59730 ` 1157` ``` (fact (Suc i)))" ``` lp15@56238 ` 1158` ``` by (subst setsum_Suc_reindex) simp ``` lp15@56238 ` 1159` ``` also have "... = f (Suc 0) u - ``` lp15@56238 ` 1160` ``` (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1161` ``` (fact (Suc n)) + ``` lp15@56238 ` 1162` ``` (\i = 0..n. ``` lp15@61609 ` 1163` ``` f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) - ``` lp15@59730 ` 1164` ``` f (Suc i) u * (z-u) ^ i / (fact i))" ``` haftmann@57514 ` 1165` ``` by (simp only: diff_divide_distrib fact_cancel ac_simps) ``` lp15@56238 ` 1166` ``` also have "... = f (Suc 0) u - ``` lp15@56238 ` 1167` ``` (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1168` ``` (fact (Suc n)) + ``` lp15@59730 ` 1169` ``` f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u" ``` lp15@56238 ` 1170` ``` by (subst setsum_Suc_diff) auto ``` lp15@59730 ` 1171` ``` also have "... = f (Suc n) u * (z-u) ^ n / (fact n)" ``` lp15@56238 ` 1172` ``` by (simp only: algebra_simps diff_divide_distrib fact_cancel) ``` lp15@61609 ` 1173` ``` finally have "(\i = 0..n. (f (Suc i) u * (z - u) ^ i ``` lp15@59730 ` 1174` ``` - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) = ``` lp15@59730 ` 1175` ``` f (Suc n) u * (z - u) ^ n / (fact n)" . ``` lp15@59730 ` 1176` ``` then have "((\u. \i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative ``` lp15@59730 ` 1177` ``` f (Suc n) u * (z - u) ^ n / (fact n)) (at u)" ``` hoelzl@56381 ` 1178` ``` apply (intro derivative_eq_intros)+ ``` lp15@56238 ` 1179` ``` apply (force intro: u assms) ``` lp15@56238 ` 1180` ``` apply (rule refl)+ ``` haftmann@57514 ` 1181` ``` apply (auto simp: ac_simps) ``` lp15@56238 ` 1182` ``` done ``` lp15@56238 ` 1183` ``` } ``` lp15@56238 ` 1184` ``` then show ?thesis ``` lp15@59730 ` 1185` ``` apply (cut_tac complex_mvt_line [of w z "\u. \i = 0..n. f i u * (z-u) ^ i / (fact i)" ``` lp15@59730 ` 1186` ``` "\u. (f (Suc n) u * (z-u)^n / (fact n))"]) ``` lp15@56238 ` 1187` ``` apply (auto simp add: intro: open_closed_segment) ``` lp15@56238 ` 1188` ``` done ``` lp15@56238 ` 1189` ```qed ``` lp15@56238 ` 1190` lp15@60017 ` 1191` wenzelm@60420 ` 1192` ```subsection \Polynomal function extremal theorem, from HOL Light\ ``` lp15@60017 ` 1193` lp15@60017 ` 1194` ```lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*) ``` lp15@60017 ` 1195` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@60017 ` 1196` ``` assumes "0 < e" ``` lp15@60017 ` 1197` ``` shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)" ``` lp15@60017 ` 1198` ```proof (induct n) ``` lp15@60017 ` 1199` ``` case 0 with assms ``` lp15@60017 ` 1200` ``` show ?case ``` lp15@60017 ` 1201` ``` apply (rule_tac x="norm (c 0) / e" in exI) ``` lp15@60017 ` 1202` ``` apply (auto simp: field_simps) ``` lp15@60017 ` 1203` ``` done ``` lp15@60017 ` 1204` ```next ``` lp15@60017 ` 1205` ``` case (Suc n) ``` lp15@60017 ` 1206` ``` obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" ``` lp15@60017 ` 1207` ``` using Suc assms by blast ``` lp15@60017 ` 1208` ``` show ?case ``` lp15@60017 ` 1209` ``` proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc) ``` lp15@60017 ` 1210` ``` fix z::'a ``` lp15@60017 ` 1211` ``` assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z" ``` lp15@60017 ` 1212` ``` then have z2: "e + norm (c (Suc n)) \ e * norm z" ``` lp15@60017 ` 1213` ``` using assms by (simp add: field_simps) ``` lp15@60017 ` 1214` ``` have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" ``` lp15@60017 ` 1215` ``` using M [OF z1] by simp ``` lp15@60017 ` 1216` ``` then have "norm (\i\n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" ``` lp15@60017 ` 1217` ``` by simp ``` lp15@60017 ` 1218` ``` then have "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" ``` lp15@60017 ` 1219` ``` by (blast intro: norm_triangle_le elim: ) ``` lp15@60017 ` 1220` ``` also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n" ``` lp15@60017 ` 1221` ``` by (simp add: norm_power norm_mult algebra_simps) ``` lp15@60017 ` 1222` ``` also have "... \ (e * norm z) * norm z ^ Suc n" ``` lp15@60017 ` 1223` ``` by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) ``` lp15@60017 ` 1224` ``` finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" ``` lp15@60162 ` 1225` ``` by simp ``` lp15@60017 ` 1226` ``` qed ``` lp15@60017 ` 1227` ```qed ``` lp15@60017 ` 1228` lp15@60017 ` 1229` ```lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*) ``` lp15@60017 ` 1230` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@60017 ` 1231` ``` assumes k: "c k \ 0" "1\k" and kn: "k\n" ``` lp15@60017 ` 1232` ``` shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity" ``` lp15@60017 ` 1233` ```using kn ``` lp15@60017 ` 1234` ```proof (induction n) ``` lp15@60017 ` 1235` ``` case 0 ``` lp15@60017 ` 1236` ``` then show ?case ``` lp15@60017 ` 1237` ``` using k by simp ``` lp15@60017 ` 1238` ```next ``` lp15@60017 ` 1239` ``` case (Suc m) ``` lp15@60017 ` 1240` ``` let ?even = ?case ``` lp15@60017 ` 1241` ``` show ?even ``` lp15@60017 ` 1242` ``` proof (cases "c (Suc m) = 0") ``` lp15@60017 ` 1243` ``` case True ``` lp15@60017 ` 1244` ``` then show ?even using Suc k ``` lp15@60017 ` 1245` ``` by auto (metis antisym_conv less_eq_Suc_le not_le) ``` lp15@60017 ` 1246` ``` next ``` lp15@60017 ` 1247` ``` case False ``` lp15@60017 ` 1248` ``` then obtain M where M: ``` lp15@60017 ` 1249` ``` "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m" ``` lp15@60017 ` 1250` ``` using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc ``` lp15@60017 ` 1251` ``` by auto ``` lp15@60017 ` 1252` ``` have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)" ``` lp15@60017 ` 1253` ``` proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc) ``` lp15@60017 ` 1254` ``` fix z::'a ``` lp15@60017 ` 1255` ``` assume z1: "M \ norm z" "1 \ norm z" ``` lp15@60017 ` 1256` ``` and "\B\ * 2 / norm (c (Suc m)) \ norm z" ``` lp15@60017 ` 1257` ``` then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2" ``` lp15@60017 ` 1258` ``` using False by (simp add: field_simps) ``` lp15@60017 ` 1259` ``` have nz: "norm z \ norm z ^ Suc m" ``` wenzelm@60420 ` 1260` ``` by (metis \1 \ norm z\ One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc) ``` lp15@60017 ` 1261` ``` have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)" ``` lp15@60017 ` 1262` ``` by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2) ``` lp15@60017 ` 1263` ``` have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i) ``` lp15@60017 ` 1264` ``` \ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m" ``` lp15@60017 ` 1265` ``` using M [of z] Suc z1 by auto ``` lp15@60017 ` 1266` ``` also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)" ``` lp15@60017 ` 1267` ``` using nz by (simp add: mult_mono del: power_Suc) ``` lp15@60017 ` 1268` ``` finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)" ``` lp15@60017 ` 1269` ``` using Suc.IH ``` lp15@60017 ` 1270` ``` apply (auto simp: eventually_at_infinity) ``` lp15@60017 ` 1271` ``` apply (rule *) ``` lp15@60017 ` 1272` ``` apply (simp add: field_simps norm_mult norm_power) ``` lp15@60017 ` 1273` ``` done ``` lp15@60017 ` 1274` ``` qed ``` lp15@60017 ` 1275` ``` then show ?even ``` lp15@60017 ` 1276` ``` by (simp add: eventually_at_infinity) ``` lp15@60017 ` 1277` ``` qed ``` lp15@60017 ` 1278` ```qed ``` lp15@60017 ` 1279` lp15@56215 ` 1280` ```end ```