src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
 author paulson Mon Dec 07 16:44:26 2015 +0000 (2015-12-07) changeset 61806 d2e62ae01cd8 parent 61610 4f54d2759a0b child 61808 fc1556774cfe permissions -rw-r--r--
Cauchy's integral formula for circles. Starting to fix eventually_mono.
 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 ``` wenzelm@61560 ` 8` ```imports Cartesian_Euclidean_Space ``` lp15@56215 ` 9` ```begin ``` lp15@56215 ` 10` lp15@59730 ` 11` lp15@59730 ` 12` ```lemma cmod_fact [simp]: "cmod (fact n) = fact n" ``` lp15@59730 ` 13` ``` by (metis norm_of_nat of_nat_fact) ``` lp15@59730 ` 14` wenzelm@60420 ` 15` ```subsection\General lemmas\ ``` 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)" ``` lp15@61609 ` 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)" ``` lp15@61609 ` 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)" ``` lp15@61609 ` 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)" ``` lp15@61609 ` 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` lp15@60017 ` 226` ```lemma closed_Real_halfspace_Re_ge: "closed (\ \ {w. x \ Re(w)})" ``` lp15@60017 ` 227` ``` using closed_halfspace_Re_ge ``` lp15@60017 ` 228` ``` by (simp add: closed_Int closed_complex_Reals) ``` lp15@60017 ` 229` lp15@60017 ` 230` ```lemma closed_real_abs_le: "closed {w \ \. \Re w\ \ r}" ``` lp15@60017 ` 231` ```proof - ``` lp15@60017 ` 232` ``` have "{w \ \. \Re w\ \ r} = (\ \ {w. Re w \ r}) \ (\ \ {w. Re w \ -r})" ``` lp15@60017 ` 233` ``` by auto ``` lp15@60017 ` 234` ``` then show "closed {w \ \. \Re w\ \ r}" ``` lp15@60017 ` 235` ``` by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le) ``` lp15@60017 ` 236` ```qed ``` lp15@60017 ` 237` hoelzl@56370 ` 238` ```lemma real_lim: ``` hoelzl@56370 ` 239` ``` fixes l::complex ``` hoelzl@56370 ` 240` ``` assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" ``` hoelzl@56370 ` 241` ``` shows "l \ \" ``` hoelzl@56370 ` 242` ```proof (rule Lim_in_closed_set[OF closed_complex_Reals _ assms(2,1)]) ``` hoelzl@56370 ` 243` ``` show "eventually (\x. f x \ \) F" ``` hoelzl@56370 ` 244` ``` using assms(3, 4) by (auto intro: eventually_mono) ``` hoelzl@56370 ` 245` ```qed ``` hoelzl@56370 ` 246` hoelzl@56370 ` 247` ```lemma real_lim_sequentially: ``` hoelzl@56370 ` 248` ``` fixes l::complex ``` hoelzl@56370 ` 249` ``` shows "(f ---> l) sequentially \ (\N. \n\N. f n \ \) \ l \ \" ``` hoelzl@56370 ` 250` ```by (rule real_lim [where F=sequentially]) (auto simp: eventually_sequentially) ``` hoelzl@56370 ` 251` lp15@61609 ` 252` ```lemma real_series: ``` hoelzl@56370 ` 253` ``` fixes l::complex ``` hoelzl@56370 ` 254` ``` shows "f sums l \ (\n. f n \ \) \ l \ \" ``` hoelzl@56370 ` 255` ```unfolding sums_def ``` hoelzl@56370 ` 256` ```by (metis real_lim_sequentially setsum_in_Reals) ``` hoelzl@56370 ` 257` hoelzl@56370 ` 258` ```lemma Lim_null_comparison_Re: ``` hoelzl@56889 ` 259` ``` assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F" ``` hoelzl@56889 ` 260` ``` by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp ``` lp15@56215 ` 261` wenzelm@60420 ` 262` ```subsection\Holomorphic functions\ ``` lp15@56215 ` 263` lp15@56215 ` 264` ```definition complex_differentiable :: "[complex \ complex, complex filter] \ bool" ``` lp15@61609 ` 265` ``` (infixr "(complex'_differentiable)" 50) ``` lp15@56215 ` 266` ``` where "f complex_differentiable F \ \f'. (f has_field_derivative f') F" ``` lp15@56215 ` 267` hoelzl@56370 ` 268` ```lemma complex_differentiable_imp_continuous_at: ``` hoelzl@56370 ` 269` ``` "f complex_differentiable (at x within s) \ continuous (at x within s) f" ``` lp15@56215 ` 270` ``` by (metis DERIV_continuous complex_differentiable_def) ``` lp15@56215 ` 271` lp15@56215 ` 272` ```lemma complex_differentiable_within_subset: ``` lp15@56215 ` 273` ``` "\f complex_differentiable (at x within s); t \ s\ ``` lp15@56215 ` 274` ``` \ f complex_differentiable (at x within t)" ``` hoelzl@56370 ` 275` ``` by (metis DERIV_subset complex_differentiable_def) ``` lp15@56215 ` 276` lp15@56215 ` 277` ```lemma complex_differentiable_at_within: ``` lp15@56215 ` 278` ``` "\f complex_differentiable (at x)\ ``` lp15@56215 ` 279` ``` \ f complex_differentiable (at x within s)" ``` lp15@56215 ` 280` ``` unfolding complex_differentiable_def ``` lp15@56215 ` 281` ``` by (metis DERIV_subset top_greatest) ``` lp15@56215 ` 282` lp15@61520 ` 283` ```lemma complex_differentiable_linear [derivative_intros]: "(op * c) complex_differentiable F" ``` lp15@56215 ` 284` ```proof - ``` hoelzl@56370 ` 285` ``` show ?thesis ``` hoelzl@56370 ` 286` ``` unfolding complex_differentiable_def has_field_derivative_def mult_commute_abs ``` lp15@56215 ` 287` ``` by (force intro: has_derivative_mult_right) ``` lp15@56215 ` 288` ```qed ``` lp15@56215 ` 289` lp15@61520 ` 290` ```lemma complex_differentiable_const [derivative_intros]: "(\z. c) complex_differentiable F" ``` lp15@56215 ` 291` ``` unfolding complex_differentiable_def has_field_derivative_def ``` hoelzl@56369 ` 292` ``` by (rule exI [where x=0]) ``` lp15@61609 ` 293` ``` (metis has_derivative_const lambda_zero) ``` lp15@56215 ` 294` lp15@61520 ` 295` ```lemma complex_differentiable_ident [derivative_intros]: "(\z. z) complex_differentiable F" ``` lp15@56215 ` 296` ``` unfolding complex_differentiable_def has_field_derivative_def ``` hoelzl@56369 ` 297` ``` by (rule exI [where x=1]) ``` hoelzl@56369 ` 298` ``` (simp add: lambda_one [symmetric]) ``` lp15@56215 ` 299` lp15@61520 ` 300` ```lemma complex_differentiable_id [derivative_intros]: "id complex_differentiable F" ``` hoelzl@56370 ` 301` ``` unfolding id_def by (rule complex_differentiable_ident) ``` hoelzl@56370 ` 302` lp15@61520 ` 303` ```lemma complex_differentiable_minus [derivative_intros]: ``` hoelzl@56370 ` 304` ``` "f complex_differentiable F \ (\z. - (f z)) complex_differentiable F" ``` lp15@56215 ` 305` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 306` ``` by (metis field_differentiable_minus) ``` lp15@56215 ` 307` lp15@61520 ` 308` ```lemma complex_differentiable_add [derivative_intros]: ``` lp15@56215 ` 309` ``` assumes "f complex_differentiable F" "g complex_differentiable F" ``` lp15@56215 ` 310` ``` shows "(\z. f z + g z) complex_differentiable F" ``` lp15@56215 ` 311` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 312` ``` by (metis field_differentiable_add) ``` lp15@56215 ` 313` lp15@61520 ` 314` ```lemma complex_differentiable_setsum [derivative_intros]: ``` hoelzl@56370 ` 315` ``` "(\i. i \ I \ (f i) complex_differentiable F) \ (\z. \i\I. f i z) complex_differentiable F" ``` hoelzl@56370 ` 316` ``` by (induct I rule: infinite_finite_induct) ``` hoelzl@56370 ` 317` ``` (auto intro: complex_differentiable_add complex_differentiable_const) ``` hoelzl@56370 ` 318` lp15@61520 ` 319` ```lemma complex_differentiable_diff [derivative_intros]: ``` lp15@56215 ` 320` ``` assumes "f complex_differentiable F" "g complex_differentiable F" ``` lp15@56215 ` 321` ``` shows "(\z. f z - g z) complex_differentiable F" ``` lp15@56215 ` 322` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 323` ``` by (metis field_differentiable_diff) ``` lp15@56215 ` 324` lp15@61520 ` 325` ```lemma complex_differentiable_inverse [derivative_intros]: ``` lp15@56215 ` 326` ``` assumes "f complex_differentiable (at a within s)" "f a \ 0" ``` lp15@56215 ` 327` ``` shows "(\z. inverse (f z)) complex_differentiable (at a within s)" ``` lp15@56215 ` 328` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 329` ``` by (metis DERIV_inverse_fun) ``` lp15@56215 ` 330` lp15@61520 ` 331` ```lemma complex_differentiable_mult [derivative_intros]: ``` lp15@61609 ` 332` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 333` ``` "g complex_differentiable (at a within s)" ``` lp15@56215 ` 334` ``` shows "(\z. f z * g z) complex_differentiable (at a within s)" ``` lp15@56215 ` 335` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 336` ``` by (metis DERIV_mult [of f _ a s g]) ``` lp15@61609 ` 337` lp15@61520 ` 338` ```lemma complex_differentiable_divide [derivative_intros]: ``` lp15@61609 ` 339` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 340` ``` "g complex_differentiable (at a within s)" ``` lp15@56215 ` 341` ``` "g a \ 0" ``` lp15@56215 ` 342` ``` shows "(\z. f z / g z) complex_differentiable (at a within s)" ``` lp15@56215 ` 343` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 344` ``` by (metis DERIV_divide [of f _ a s g]) ``` lp15@56215 ` 345` lp15@61520 ` 346` ```lemma complex_differentiable_power [derivative_intros]: ``` lp15@61609 ` 347` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 348` ``` shows "(\z. f z ^ n) complex_differentiable (at a within s)" ``` lp15@56215 ` 349` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 350` ``` by (metis DERIV_power) ``` lp15@56215 ` 351` lp15@56215 ` 352` ```lemma complex_differentiable_transform_within: ``` lp15@56215 ` 353` ``` "0 < d \ ``` lp15@56215 ` 354` ``` x \ s \ ``` lp15@56215 ` 355` ``` (\x'. x' \ s \ dist x' x < d \ f x' = g x') \ ``` lp15@56215 ` 356` ``` f complex_differentiable (at x within s) ``` lp15@56215 ` 357` ``` \ g complex_differentiable (at x within s)" ``` lp15@56215 ` 358` ``` unfolding complex_differentiable_def has_field_derivative_def ``` lp15@56215 ` 359` ``` by (blast intro: has_derivative_transform_within) ``` lp15@56215 ` 360` lp15@56215 ` 361` ```lemma complex_differentiable_compose_within: ``` lp15@61609 ` 362` ``` assumes "f complex_differentiable (at a within s)" ``` lp15@56215 ` 363` ``` "g complex_differentiable (at (f a) within f`s)" ``` lp15@56215 ` 364` ``` shows "(g o f) complex_differentiable (at a within s)" ``` lp15@56215 ` 365` ``` using assms unfolding complex_differentiable_def ``` lp15@56215 ` 366` ``` by (metis DERIV_image_chain) ``` lp15@56215 ` 367` hoelzl@56370 ` 368` ```lemma complex_differentiable_compose: ``` hoelzl@56370 ` 369` ``` "f complex_differentiable at z \ g complex_differentiable at (f z) ``` hoelzl@56370 ` 370` ``` \ (g o f) complex_differentiable at z" ``` hoelzl@56370 ` 371` ```by (metis complex_differentiable_at_within complex_differentiable_compose_within) ``` hoelzl@56370 ` 372` lp15@56215 ` 373` ```lemma complex_differentiable_within_open: ``` lp15@61609 ` 374` ``` "\a \ s; open s\ \ f complex_differentiable at a within s \ ``` lp15@56215 ` 375` ``` f complex_differentiable at a" ``` lp15@56215 ` 376` ``` unfolding complex_differentiable_def ``` lp15@56215 ` 377` ``` by (metis at_within_open) ``` lp15@56215 ` 378` wenzelm@60420 ` 379` ```subsection\Caratheodory characterization.\ ``` lp15@56215 ` 380` lp15@56215 ` 381` ```lemma complex_differentiable_caratheodory_at: ``` lp15@56215 ` 382` ``` "f complex_differentiable (at z) \ ``` lp15@56215 ` 383` ``` (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z) g)" ``` lp15@56215 ` 384` ``` using CARAT_DERIV [of f] ``` lp15@56215 ` 385` ``` by (simp add: complex_differentiable_def has_field_derivative_def) ``` lp15@56215 ` 386` lp15@56215 ` 387` ```lemma complex_differentiable_caratheodory_within: ``` lp15@56215 ` 388` ``` "f complex_differentiable (at z within s) \ ``` lp15@56215 ` 389` ``` (\g. (\w. f(w) - f(z) = g(w) * (w - z)) \ continuous (at z within s) g)" ``` lp15@56215 ` 390` ``` using DERIV_caratheodory_within [of f] ``` lp15@56215 ` 391` ``` by (simp add: complex_differentiable_def has_field_derivative_def) ``` lp15@56215 ` 392` wenzelm@60420 ` 393` ```subsection\Holomorphic\ ``` hoelzl@56370 ` 394` hoelzl@56370 ` 395` ```definition holomorphic_on :: "[complex \ complex, complex set] \ bool" ``` hoelzl@56370 ` 396` ``` (infixl "(holomorphic'_on)" 50) ``` hoelzl@56370 ` 397` ``` where "f holomorphic_on s \ \x\s. f complex_differentiable (at x within s)" ``` lp15@61609 ` 398` lp15@61520 ` 399` ```named_theorems holomorphic_intros "structural introduction rules for holomorphic_on" ``` lp15@61520 ` 400` lp15@61520 ` 401` ```lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}" ``` hoelzl@56370 ` 402` ``` by (simp add: holomorphic_on_def) ``` hoelzl@56370 ` 403` hoelzl@56370 ` 404` ```lemma holomorphic_on_open: ``` hoelzl@56370 ` 405` ``` "open s \ f holomorphic_on s \ (\x \ s. \f'. DERIV f x :> f')" ``` hoelzl@56370 ` 406` ``` by (auto simp: holomorphic_on_def complex_differentiable_def has_field_derivative_def at_within_open [of _ s]) ``` hoelzl@56370 ` 407` lp15@61609 ` 408` ```lemma holomorphic_on_imp_continuous_on: ``` hoelzl@56370 ` 409` ``` "f holomorphic_on s \ continuous_on s f" ``` lp15@61609 ` 410` ``` by (metis complex_differentiable_imp_continuous_at continuous_on_eq_continuous_within holomorphic_on_def) ``` hoelzl@56370 ` 411` hoelzl@56370 ` 412` ```lemma holomorphic_on_subset: ``` hoelzl@56370 ` 413` ``` "f holomorphic_on s \ t \ s \ f holomorphic_on t" ``` hoelzl@56370 ` 414` ``` unfolding holomorphic_on_def ``` hoelzl@56370 ` 415` ``` by (metis complex_differentiable_within_subset subsetD) ``` hoelzl@56370 ` 416` hoelzl@56370 ` 417` ```lemma holomorphic_transform: "\f holomorphic_on s; \x. x \ s \ f x = g x\ \ g holomorphic_on s" ``` hoelzl@56370 ` 418` ``` by (metis complex_differentiable_transform_within linordered_field_no_ub holomorphic_on_def) ``` hoelzl@56370 ` 419` hoelzl@56370 ` 420` ```lemma holomorphic_cong: "s = t ==> (\x. x \ s \ f x = g x) \ f holomorphic_on s \ g holomorphic_on t" ``` hoelzl@56370 ` 421` ``` by (metis holomorphic_transform) ``` hoelzl@56370 ` 422` lp15@61520 ` 423` ```lemma holomorphic_on_linear [holomorphic_intros]: "(op * c) holomorphic_on s" ``` hoelzl@56370 ` 424` ``` unfolding holomorphic_on_def by (metis complex_differentiable_linear) ``` hoelzl@56370 ` 425` lp15@61520 ` 426` ```lemma holomorphic_on_const [holomorphic_intros]: "(\z. c) holomorphic_on s" ``` hoelzl@56370 ` 427` ``` unfolding holomorphic_on_def by (metis complex_differentiable_const) ``` hoelzl@56370 ` 428` lp15@61520 ` 429` ```lemma holomorphic_on_ident [holomorphic_intros]: "(\x. x) holomorphic_on s" ``` hoelzl@56370 ` 430` ``` unfolding holomorphic_on_def by (metis complex_differentiable_ident) ``` hoelzl@56370 ` 431` lp15@61520 ` 432` ```lemma holomorphic_on_id [holomorphic_intros]: "id holomorphic_on s" ``` hoelzl@56370 ` 433` ``` unfolding id_def by (rule holomorphic_on_ident) ``` hoelzl@56370 ` 434` hoelzl@56370 ` 435` ```lemma holomorphic_on_compose: ``` hoelzl@56370 ` 436` ``` "f holomorphic_on s \ g holomorphic_on (f ` s) \ (g o f) holomorphic_on s" ``` hoelzl@56370 ` 437` ``` using complex_differentiable_compose_within[of f _ s g] ``` hoelzl@56370 ` 438` ``` by (auto simp: holomorphic_on_def) ``` hoelzl@56370 ` 439` hoelzl@56370 ` 440` ```lemma holomorphic_on_compose_gen: ``` hoelzl@56370 ` 441` ``` "f holomorphic_on s \ g holomorphic_on t \ f ` s \ t \ (g o f) holomorphic_on s" ``` hoelzl@56370 ` 442` ``` by (metis holomorphic_on_compose holomorphic_on_subset) ``` hoelzl@56370 ` 443` lp15@61520 ` 444` ```lemma holomorphic_on_minus [holomorphic_intros]: "f holomorphic_on s \ (\z. -(f z)) holomorphic_on s" ``` hoelzl@56370 ` 445` ``` by (metis complex_differentiable_minus holomorphic_on_def) ``` hoelzl@56370 ` 446` lp15@61520 ` 447` ```lemma holomorphic_on_add [holomorphic_intros]: ``` hoelzl@56370 ` 448` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z + g z) holomorphic_on s" ``` hoelzl@56370 ` 449` ``` unfolding holomorphic_on_def by (metis complex_differentiable_add) ``` hoelzl@56370 ` 450` lp15@61520 ` 451` ```lemma holomorphic_on_diff [holomorphic_intros]: ``` hoelzl@56370 ` 452` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z - g z) holomorphic_on s" ``` hoelzl@56370 ` 453` ``` unfolding holomorphic_on_def by (metis complex_differentiable_diff) ``` hoelzl@56370 ` 454` lp15@61520 ` 455` ```lemma holomorphic_on_mult [holomorphic_intros]: ``` hoelzl@56370 ` 456` ``` "\f holomorphic_on s; g holomorphic_on s\ \ (\z. f z * g z) holomorphic_on s" ``` hoelzl@56370 ` 457` ``` unfolding holomorphic_on_def by (metis complex_differentiable_mult) ``` hoelzl@56370 ` 458` lp15@61520 ` 459` ```lemma holomorphic_on_inverse [holomorphic_intros]: ``` hoelzl@56370 ` 460` ``` "\f holomorphic_on s; \z. z \ s \ f z \ 0\ \ (\z. inverse (f z)) holomorphic_on s" ``` hoelzl@56370 ` 461` ``` unfolding holomorphic_on_def by (metis complex_differentiable_inverse) ``` hoelzl@56370 ` 462` lp15@61520 ` 463` ```lemma holomorphic_on_divide [holomorphic_intros]: ``` hoelzl@56370 ` 464` ``` "\f holomorphic_on s; g holomorphic_on s; \z. z \ s \ g z \ 0\ \ (\z. f z / g z) holomorphic_on s" ``` hoelzl@56370 ` 465` ``` unfolding holomorphic_on_def by (metis complex_differentiable_divide) ``` hoelzl@56370 ` 466` lp15@61520 ` 467` ```lemma holomorphic_on_power [holomorphic_intros]: ``` hoelzl@56370 ` 468` ``` "f holomorphic_on s \ (\z. (f z)^n) holomorphic_on s" ``` hoelzl@56370 ` 469` ``` unfolding holomorphic_on_def by (metis complex_differentiable_power) ``` hoelzl@56370 ` 470` lp15@61520 ` 471` ```lemma holomorphic_on_setsum [holomorphic_intros]: ``` hoelzl@56370 ` 472` ``` "(\i. i \ I \ (f i) holomorphic_on s) \ (\x. setsum (\i. f i x) I) holomorphic_on s" ``` hoelzl@56370 ` 473` ``` unfolding holomorphic_on_def by (metis complex_differentiable_setsum) ``` hoelzl@56370 ` 474` hoelzl@56370 ` 475` ```lemma DERIV_deriv_iff_complex_differentiable: ``` hoelzl@56370 ` 476` ``` "DERIV f x :> deriv f x \ f complex_differentiable at x" ``` hoelzl@56370 ` 477` ``` unfolding complex_differentiable_def by (metis DERIV_imp_deriv) ``` hoelzl@56370 ` 478` hoelzl@56370 ` 479` ```lemma complex_derivative_chain: ``` hoelzl@56370 ` 480` ``` "f complex_differentiable at x \ g complex_differentiable at (f x) ``` hoelzl@56370 ` 481` ``` \ deriv (g o f) x = deriv g (f x) * deriv f x" ``` hoelzl@56370 ` 482` ``` by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv) ``` hoelzl@56370 ` 483` hoelzl@56370 ` 484` ```lemma complex_derivative_linear: "deriv (\w. c * w) = (\z. c)" ``` hoelzl@56370 ` 485` ``` by (metis DERIV_imp_deriv DERIV_cmult_Id) ``` hoelzl@56370 ` 486` hoelzl@56370 ` 487` ```lemma complex_derivative_ident: "deriv (\w. w) = (\z. 1)" ``` hoelzl@56370 ` 488` ``` by (metis DERIV_imp_deriv DERIV_ident) ``` hoelzl@56370 ` 489` hoelzl@56370 ` 490` ```lemma complex_derivative_const: "deriv (\w. c) = (\z. 0)" ``` hoelzl@56370 ` 491` ``` by (metis DERIV_imp_deriv DERIV_const) ``` hoelzl@56370 ` 492` hoelzl@56370 ` 493` ```lemma complex_derivative_add: ``` lp15@61609 ` 494` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 495` ``` \ deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 496` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 497` ``` by (auto intro!: DERIV_imp_deriv derivative_intros) ``` hoelzl@56370 ` 498` hoelzl@56370 ` 499` ```lemma complex_derivative_diff: ``` lp15@61609 ` 500` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 501` ``` \ deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 502` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 503` ``` by (auto intro!: DERIV_imp_deriv derivative_intros) ``` hoelzl@56370 ` 504` hoelzl@56370 ` 505` ```lemma complex_derivative_mult: ``` lp15@61609 ` 506` ``` "\f complex_differentiable at z; g complex_differentiable at z\ ``` hoelzl@56370 ` 507` ``` \ deriv (\w. f w * g w) z = f z * deriv g z + deriv f z * g z" ``` hoelzl@56370 ` 508` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 509` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 510` hoelzl@56370 ` 511` ```lemma complex_derivative_cmult: ``` hoelzl@56370 ` 512` ``` "f complex_differentiable at z \ deriv (\w. c * f w) z = c * deriv f z" ``` hoelzl@56370 ` 513` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 514` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 515` hoelzl@56370 ` 516` ```lemma complex_derivative_cmult_right: ``` hoelzl@56370 ` 517` ``` "f complex_differentiable at z \ deriv (\w. f w * c) z = deriv f z * c" ``` hoelzl@56370 ` 518` ``` unfolding DERIV_deriv_iff_complex_differentiable[symmetric] ``` hoelzl@56381 ` 519` ``` by (auto intro!: DERIV_imp_deriv derivative_eq_intros) ``` hoelzl@56370 ` 520` hoelzl@56370 ` 521` ```lemma complex_derivative_transform_within_open: ``` lp15@61609 ` 522` ``` "\f holomorphic_on s; g holomorphic_on s; open s; z \ s; \w. w \ s \ f w = g w\ ``` hoelzl@56370 ` 523` ``` \ deriv f z = deriv g z" ``` hoelzl@56370 ` 524` ``` unfolding holomorphic_on_def ``` hoelzl@56370 ` 525` ``` by (rule DERIV_imp_deriv) ``` hoelzl@56370 ` 526` ``` (metis DERIV_deriv_iff_complex_differentiable DERIV_transform_within_open at_within_open) ``` hoelzl@56370 ` 527` hoelzl@56370 ` 528` ```lemma complex_derivative_compose_linear: ``` hoelzl@56370 ` 529` ``` "f complex_differentiable at (c * z) \ deriv (\w. f (c * w)) z = c * deriv f (c * z)" ``` hoelzl@56370 ` 530` ```apply (rule DERIV_imp_deriv) ``` hoelzl@56370 ` 531` ```apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric]) ``` haftmann@59554 ` 532` ```apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id]) ``` haftmann@59554 ` 533` ```apply (simp add: algebra_simps) ``` hoelzl@56370 ` 534` ```done ``` hoelzl@56370 ` 535` wenzelm@60420 ` 536` ```subsection\Analyticity on a set\ ``` lp15@56215 ` 537` lp15@61609 ` 538` ```definition analytic_on (infixl "(analytic'_on)" 50) ``` lp15@56215 ` 539` ``` where ``` lp15@56215 ` 540` ``` "f analytic_on s \ \x \ s. \e. 0 < e \ f holomorphic_on (ball x e)" ``` lp15@56215 ` 541` hoelzl@56370 ` 542` ```lemma analytic_imp_holomorphic: "f analytic_on s \ f holomorphic_on s" ``` hoelzl@56370 ` 543` ``` by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def) ``` hoelzl@56370 ` 544` ``` (metis centre_in_ball complex_differentiable_at_within) ``` lp15@56215 ` 545` hoelzl@56370 ` 546` ```lemma analytic_on_open: "open s \ f analytic_on s \ f holomorphic_on s" ``` lp15@56215 ` 547` ```apply (auto simp: analytic_imp_holomorphic) ``` lp15@56215 ` 548` ```apply (auto simp: analytic_on_def holomorphic_on_def) ``` lp15@56215 ` 549` ```by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball) ``` lp15@56215 ` 550` lp15@56215 ` 551` ```lemma analytic_on_imp_differentiable_at: ``` lp15@56215 ` 552` ``` "f analytic_on s \ x \ s \ f complex_differentiable (at x)" ``` hoelzl@56370 ` 553` ``` apply (auto simp: analytic_on_def holomorphic_on_def) ``` lp15@56215 ` 554` ```by (metis Topology_Euclidean_Space.open_ball centre_in_ball complex_differentiable_within_open) ``` lp15@56215 ` 555` hoelzl@56370 ` 556` ```lemma analytic_on_subset: "f analytic_on s \ t \ s \ f analytic_on t" ``` lp15@56215 ` 557` ``` by (auto simp: analytic_on_def) ``` lp15@56215 ` 558` hoelzl@56370 ` 559` ```lemma analytic_on_Un: "f analytic_on (s \ t) \ f analytic_on s \ f analytic_on t" ``` lp15@56215 ` 560` ``` by (auto simp: analytic_on_def) ``` lp15@56215 ` 561` wenzelm@60585 ` 562` ```lemma analytic_on_Union: "f analytic_on (\s) \ (\t \ s. f analytic_on t)" ``` hoelzl@56370 ` 563` ``` by (auto simp: analytic_on_def) ``` hoelzl@56370 ` 564` hoelzl@56370 ` 565` ```lemma analytic_on_UN: "f analytic_on (\i\I. s i) \ (\i\I. f analytic_on (s i))" ``` lp15@56215 ` 566` ``` by (auto simp: analytic_on_def) ``` lp15@61609 ` 567` lp15@56215 ` 568` ```lemma analytic_on_holomorphic: ``` lp15@56215 ` 569` ``` "f analytic_on s \ (\t. open t \ s \ t \ f holomorphic_on t)" ``` lp15@56215 ` 570` ``` (is "?lhs = ?rhs") ``` lp15@56215 ` 571` ```proof - ``` lp15@56215 ` 572` ``` have "?lhs \ (\t. open t \ s \ t \ f analytic_on t)" ``` lp15@56215 ` 573` ``` proof safe ``` lp15@56215 ` 574` ``` assume "f analytic_on s" ``` lp15@56215 ` 575` ``` then show "\t. open t \ s \ t \ f analytic_on t" ``` lp15@56215 ` 576` ``` apply (simp add: analytic_on_def) ``` lp15@56215 ` 577` ``` apply (rule exI [where x="\{u. open u \ f analytic_on u}"], auto) ``` lp15@56215 ` 578` ``` apply (metis Topology_Euclidean_Space.open_ball analytic_on_open centre_in_ball) ``` lp15@56215 ` 579` ``` by (metis analytic_on_def) ``` lp15@56215 ` 580` ``` next ``` lp15@56215 ` 581` ``` fix t ``` lp15@61609 ` 582` ``` assume "open t" "s \ t" "f analytic_on t" ``` lp15@56215 ` 583` ``` then show "f analytic_on s" ``` lp15@56215 ` 584` ``` by (metis analytic_on_subset) ``` lp15@56215 ` 585` ``` qed ``` lp15@56215 ` 586` ``` also have "... \ ?rhs" ``` lp15@56215 ` 587` ``` by (auto simp: analytic_on_open) ``` lp15@56215 ` 588` ``` finally show ?thesis . ``` lp15@56215 ` 589` ```qed ``` lp15@56215 ` 590` lp15@56215 ` 591` ```lemma analytic_on_linear: "(op * c) analytic_on s" ``` hoelzl@56370 ` 592` ``` by (auto simp add: analytic_on_holomorphic holomorphic_on_linear) ``` lp15@56215 ` 593` lp15@56215 ` 594` ```lemma analytic_on_const: "(\z. c) analytic_on s" ``` hoelzl@56370 ` 595` ``` by (metis analytic_on_def holomorphic_on_const zero_less_one) ``` hoelzl@56370 ` 596` hoelzl@56370 ` 597` ```lemma analytic_on_ident: "(\x. x) analytic_on s" ``` hoelzl@56370 ` 598` ``` by (simp add: analytic_on_def holomorphic_on_ident gt_ex) ``` lp15@56215 ` 599` lp15@56215 ` 600` ```lemma analytic_on_id: "id analytic_on s" ``` hoelzl@56370 ` 601` ``` unfolding id_def by (rule analytic_on_ident) ``` lp15@56215 ` 602` lp15@56215 ` 603` ```lemma analytic_on_compose: ``` lp15@56215 ` 604` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 605` ``` and g: "g analytic_on (f ` s)" ``` lp15@56215 ` 606` ``` shows "(g o f) analytic_on s" ``` lp15@56215 ` 607` ```unfolding analytic_on_def ``` lp15@56215 ` 608` ```proof (intro ballI) ``` lp15@56215 ` 609` ``` fix x ``` lp15@56215 ` 610` ``` assume x: "x \ s" ``` lp15@56215 ` 611` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f ``` lp15@56215 ` 612` ``` by (metis analytic_on_def) ``` lp15@56215 ` 613` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g ``` lp15@61609 ` 614` ``` by (metis analytic_on_def g image_eqI x) ``` lp15@56215 ` 615` ``` have "isCont f x" ``` lp15@56215 ` 616` ``` by (metis analytic_on_imp_differentiable_at complex_differentiable_imp_continuous_at f x) ``` lp15@56215 ` 617` ``` with e' obtain d where d: "0 < d" and fd: "f ` ball x d \ ball (f x) e'" ``` lp15@56215 ` 618` ``` by (auto simp: continuous_at_ball) ``` lp15@61609 ` 619` ``` have "g \ f holomorphic_on ball x (min d e)" ``` lp15@56215 ` 620` ``` apply (rule holomorphic_on_compose) ``` lp15@56215 ` 621` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 622` ``` by (metis fd gh holomorphic_on_subset image_mono min.cobounded1 subset_ball) ``` lp15@56215 ` 623` ``` then show "\e>0. g \ f holomorphic_on ball x e" ``` lp15@61609 ` 624` ``` by (metis d e min_less_iff_conj) ``` lp15@56215 ` 625` ```qed ``` lp15@56215 ` 626` lp15@56215 ` 627` ```lemma analytic_on_compose_gen: ``` lp15@56215 ` 628` ``` "f analytic_on s \ g analytic_on t \ (\z. z \ s \ f z \ t) ``` lp15@56215 ` 629` ``` \ g o f analytic_on s" ``` lp15@56215 ` 630` ```by (metis analytic_on_compose analytic_on_subset image_subset_iff) ``` lp15@56215 ` 631` lp15@56215 ` 632` ```lemma analytic_on_neg: ``` lp15@56215 ` 633` ``` "f analytic_on s \ (\z. -(f z)) analytic_on s" ``` lp15@56215 ` 634` ```by (metis analytic_on_holomorphic holomorphic_on_minus) ``` lp15@56215 ` 635` lp15@56215 ` 636` ```lemma analytic_on_add: ``` lp15@56215 ` 637` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 638` ``` and g: "g analytic_on s" ``` lp15@56215 ` 639` ``` shows "(\z. f z + g z) analytic_on s" ``` lp15@56215 ` 640` ```unfolding analytic_on_def ``` lp15@56215 ` 641` ```proof (intro ballI) ``` lp15@56215 ` 642` ``` fix z ``` lp15@56215 ` 643` ``` assume z: "z \ s" ``` lp15@56215 ` 644` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 645` ``` by (metis analytic_on_def) ``` lp15@56215 ` 646` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 647` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 648` ``` have "(\z. f z + g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 649` ``` apply (rule holomorphic_on_add) ``` lp15@56215 ` 650` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 651` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 652` ``` then show "\e>0. (\z. f z + g z) holomorphic_on ball z e" ``` lp15@56215 ` 653` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 654` ```qed ``` lp15@56215 ` 655` lp15@56215 ` 656` ```lemma analytic_on_diff: ``` lp15@56215 ` 657` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 658` ``` and g: "g analytic_on s" ``` lp15@56215 ` 659` ``` shows "(\z. f z - g z) analytic_on s" ``` lp15@56215 ` 660` ```unfolding analytic_on_def ``` lp15@56215 ` 661` ```proof (intro ballI) ``` lp15@56215 ` 662` ``` fix z ``` lp15@56215 ` 663` ``` assume z: "z \ s" ``` lp15@56215 ` 664` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 665` ``` by (metis analytic_on_def) ``` lp15@56215 ` 666` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 667` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 668` ``` have "(\z. f z - g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 669` ``` apply (rule holomorphic_on_diff) ``` lp15@56215 ` 670` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 671` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 672` ``` then show "\e>0. (\z. f z - g z) holomorphic_on ball z e" ``` lp15@56215 ` 673` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 674` ```qed ``` lp15@56215 ` 675` lp15@56215 ` 676` ```lemma analytic_on_mult: ``` lp15@56215 ` 677` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 678` ``` and g: "g analytic_on s" ``` lp15@56215 ` 679` ``` shows "(\z. f z * g z) analytic_on s" ``` lp15@56215 ` 680` ```unfolding analytic_on_def ``` lp15@56215 ` 681` ```proof (intro ballI) ``` lp15@56215 ` 682` ``` fix z ``` lp15@56215 ` 683` ``` assume z: "z \ s" ``` lp15@56215 ` 684` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 685` ``` by (metis analytic_on_def) ``` lp15@56215 ` 686` ``` obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g ``` lp15@61609 ` 687` ``` by (metis analytic_on_def g z) ``` lp15@61609 ` 688` ``` have "(\z. f z * g z) holomorphic_on ball z (min e e')" ``` lp15@61609 ` 689` ``` apply (rule holomorphic_on_mult) ``` lp15@56215 ` 690` ``` apply (metis fh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 691` ``` by (metis gh holomorphic_on_subset min.bounded_iff order_refl subset_ball) ``` lp15@56215 ` 692` ``` then show "\e>0. (\z. f z * g z) holomorphic_on ball z e" ``` lp15@56215 ` 693` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 694` ```qed ``` lp15@56215 ` 695` lp15@56215 ` 696` ```lemma analytic_on_inverse: ``` lp15@56215 ` 697` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 698` ``` and nz: "(\z. z \ s \ f z \ 0)" ``` lp15@56215 ` 699` ``` shows "(\z. inverse (f z)) analytic_on s" ``` lp15@56215 ` 700` ```unfolding analytic_on_def ``` lp15@56215 ` 701` ```proof (intro ballI) ``` lp15@56215 ` 702` ``` fix z ``` lp15@56215 ` 703` ``` assume z: "z \ s" ``` lp15@56215 ` 704` ``` then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f ``` lp15@56215 ` 705` ``` by (metis analytic_on_def) ``` lp15@56215 ` 706` ``` have "continuous_on (ball z e) f" ``` lp15@56215 ` 707` ``` by (metis fh holomorphic_on_imp_continuous_on) ``` lp15@61609 ` 708` ``` then obtain e' where e': "0 < e'" and nz': "\y. dist z y < e' \ f y \ 0" ``` lp15@61609 ` 709` ``` by (metis Topology_Euclidean_Space.open_ball centre_in_ball continuous_on_open_avoid e z nz) ``` lp15@61609 ` 710` ``` have "(\z. inverse (f z)) holomorphic_on ball z (min e e')" ``` lp15@56215 ` 711` ``` apply (rule holomorphic_on_inverse) ``` lp15@56215 ` 712` ``` apply (metis fh holomorphic_on_subset min.cobounded2 min.commute subset_ball) ``` lp15@61609 ` 713` ``` by (metis nz' mem_ball min_less_iff_conj) ``` lp15@56215 ` 714` ``` then show "\e>0. (\z. inverse (f z)) holomorphic_on ball z e" ``` lp15@56215 ` 715` ``` by (metis e e' min_less_iff_conj) ``` lp15@56215 ` 716` ```qed ``` lp15@56215 ` 717` lp15@56215 ` 718` lp15@56215 ` 719` ```lemma analytic_on_divide: ``` lp15@56215 ` 720` ``` assumes f: "f analytic_on s" ``` lp15@56215 ` 721` ``` and g: "g analytic_on s" ``` lp15@56215 ` 722` ``` and nz: "(\z. z \ s \ g z \ 0)" ``` lp15@56215 ` 723` ``` shows "(\z. f z / g z) analytic_on s" ``` lp15@56215 ` 724` ```unfolding divide_inverse ``` lp15@56215 ` 725` ```by (metis analytic_on_inverse analytic_on_mult f g nz) ``` lp15@56215 ` 726` lp15@56215 ` 727` ```lemma analytic_on_power: ``` lp15@56215 ` 728` ``` "f analytic_on s \ (\z. (f z) ^ n) analytic_on s" ``` lp15@56215 ` 729` ```by (induct n) (auto simp: analytic_on_const analytic_on_mult) ``` lp15@56215 ` 730` lp15@56215 ` 731` ```lemma analytic_on_setsum: ``` hoelzl@56369 ` 732` ``` "(\i. i \ I \ (f i) analytic_on s) \ (\x. setsum (\i. f i x) I) analytic_on s" ``` hoelzl@56369 ` 733` ``` by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add) ``` lp15@56215 ` 734` wenzelm@60420 ` 735` ```subsection\analyticity at a point.\ ``` lp15@56215 ` 736` lp15@56215 ` 737` ```lemma analytic_at_ball: ``` lp15@56215 ` 738` ``` "f analytic_on {z} \ (\e. 0 f holomorphic_on ball z e)" ``` lp15@56215 ` 739` ```by (metis analytic_on_def singleton_iff) ``` lp15@56215 ` 740` lp15@56215 ` 741` ```lemma analytic_at: ``` lp15@56215 ` 742` ``` "f analytic_on {z} \ (\s. open s \ z \ s \ f holomorphic_on s)" ``` lp15@56215 ` 743` ```by (metis analytic_on_holomorphic empty_subsetI insert_subset) ``` lp15@56215 ` 744` lp15@56215 ` 745` ```lemma analytic_on_analytic_at: ``` lp15@56215 ` 746` ``` "f analytic_on s \ (\z \ s. f analytic_on {z})" ``` lp15@56215 ` 747` ```by (metis analytic_at_ball analytic_on_def) ``` lp15@56215 ` 748` lp15@56215 ` 749` ```lemma analytic_at_two: ``` lp15@56215 ` 750` ``` "f analytic_on {z} \ g analytic_on {z} \ ``` lp15@56215 ` 751` ``` (\s. open s \ z \ s \ f holomorphic_on s \ g holomorphic_on s)" ``` lp15@56215 ` 752` ``` (is "?lhs = ?rhs") ``` lp15@61609 ` 753` ```proof ``` lp15@56215 ` 754` ``` assume ?lhs ``` lp15@61609 ` 755` ``` then obtain s t ``` lp15@56215 ` 756` ``` where st: "open s" "z \ s" "f holomorphic_on s" ``` lp15@56215 ` 757` ``` "open t" "z \ t" "g holomorphic_on t" ``` lp15@56215 ` 758` ``` by (auto simp: analytic_at) ``` lp15@56215 ` 759` ``` show ?rhs ``` lp15@56215 ` 760` ``` apply (rule_tac x="s \ t" in exI) ``` lp15@56215 ` 761` ``` using st ``` lp15@56215 ` 762` ``` apply (auto simp: Diff_subset holomorphic_on_subset) ``` lp15@56215 ` 763` ``` done ``` lp15@56215 ` 764` ```next ``` lp15@61609 ` 765` ``` assume ?rhs ``` lp15@56215 ` 766` ``` then show ?lhs ``` lp15@56215 ` 767` ``` by (force simp add: analytic_at) ``` lp15@56215 ` 768` ```qed ``` lp15@56215 ` 769` wenzelm@60420 ` 770` ```subsection\Combining theorems for derivative with ``analytic at'' hypotheses\ ``` lp15@56215 ` 771` lp15@61609 ` 772` ```lemma ``` lp15@56215 ` 773` ``` assumes "f analytic_on {z}" "g analytic_on {z}" ``` hoelzl@56370 ` 774` ``` shows complex_derivative_add_at: "deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 775` ``` and complex_derivative_diff_at: "deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 776` ``` and complex_derivative_mult_at: "deriv (\w. f w * g w) z = ``` hoelzl@56370 ` 777` ``` f z * deriv g z + deriv f z * g z" ``` lp15@56215 ` 778` ```proof - ``` lp15@56215 ` 779` ``` obtain s where s: "open s" "z \ s" "f holomorphic_on s" "g holomorphic_on s" ``` lp15@56215 ` 780` ``` using assms by (metis analytic_at_two) ``` hoelzl@56370 ` 781` ``` show "deriv (\w. f w + g w) z = deriv f z + deriv g z" ``` hoelzl@56370 ` 782` ``` apply (rule DERIV_imp_deriv [OF DERIV_add]) ``` lp15@56215 ` 783` ``` using s ``` hoelzl@56370 ` 784` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 785` ``` done ``` hoelzl@56370 ` 786` ``` show "deriv (\w. f w - g w) z = deriv f z - deriv g z" ``` hoelzl@56370 ` 787` ``` apply (rule DERIV_imp_deriv [OF DERIV_diff]) ``` lp15@56215 ` 788` ``` using s ``` hoelzl@56370 ` 789` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 790` ``` done ``` hoelzl@56370 ` 791` ``` show "deriv (\w. f w * g w) z = f z * deriv g z + deriv f z * g z" ``` hoelzl@56370 ` 792` ``` apply (rule DERIV_imp_deriv [OF DERIV_mult']) ``` lp15@56215 ` 793` ``` using s ``` hoelzl@56370 ` 794` ``` apply (auto simp: holomorphic_on_open complex_differentiable_def DERIV_deriv_iff_complex_differentiable) ``` lp15@56215 ` 795` ``` done ``` lp15@56215 ` 796` ```qed ``` lp15@56215 ` 797` lp15@56215 ` 798` ```lemma complex_derivative_cmult_at: ``` hoelzl@56370 ` 799` ``` "f analytic_on {z} \ deriv (\w. c * f w) z = c * deriv f z" ``` lp15@56215 ` 800` ```by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const) ``` lp15@56215 ` 801` lp15@56215 ` 802` ```lemma complex_derivative_cmult_right_at: ``` hoelzl@56370 ` 803` ``` "f analytic_on {z} \ deriv (\w. f w * c) z = deriv f z * c" ``` lp15@56215 ` 804` ```by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const) ``` lp15@56215 ` 805` wenzelm@60420 ` 806` ```subsection\Complex differentiation of sequences and series\ ``` lp15@56215 ` 807` eberlm@61531 ` 808` ```(* TODO: Could probably be simplified using Uniform_Limit *) ``` lp15@56215 ` 809` ```lemma has_complex_derivative_sequence: ``` lp15@56215 ` 810` ``` fixes s :: "complex set" ``` lp15@56215 ` 811` ``` assumes cvs: "convex s" ``` lp15@56215 ` 812` ``` and df: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" ``` lp15@56215 ` 813` ``` and conv: "\e. 0 < e \ \N. \n x. n \ N \ x \ s \ norm (f' n x - g' x) \ e" ``` lp15@56215 ` 814` ``` and "\x l. x \ s \ ((\n. f n x) ---> l) sequentially" ``` lp15@61609 ` 815` ``` shows "\g. \x \ s. ((\n. f n x) ---> g x) sequentially \ ``` lp15@56215 ` 816` ``` (g has_field_derivative (g' x)) (at x within s)" ``` lp15@56215 ` 817` ```proof - ``` lp15@56215 ` 818` ``` from assms obtain x l where x: "x \ s" and tf: "((\n. f n x) ---> l) sequentially" ``` lp15@56215 ` 819` ``` by blast ``` lp15@56215 ` 820` ``` { fix e::real assume e: "e > 0" ``` lp15@56215 ` 821` ``` then obtain N where N: "\n\N. \x. x \ s \ cmod (f' n x - g' x) \ e" ``` lp15@61609 ` 822` ``` by (metis conv) ``` lp15@56215 ` 823` ``` have "\N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" ``` lp15@56215 ` 824` ``` proof (rule exI [of _ N], clarify) ``` lp15@56215 ` 825` ``` fix n y h ``` lp15@56215 ` 826` ``` assume "N \ n" "y \ s" ``` lp15@56215 ` 827` ``` then have "cmod (f' n y - g' y) \ e" ``` lp15@56215 ` 828` ``` by (metis N) ``` lp15@56215 ` 829` ``` then have "cmod h * cmod (f' n y - g' y) \ cmod h * e" ``` lp15@56215 ` 830` ``` by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) ``` lp15@56215 ` 831` ``` then show "cmod (f' n y * h - g' y * h) \ e * cmod h" ``` lp15@56215 ` 832` ``` by (simp add: norm_mult [symmetric] field_simps) ``` lp15@56215 ` 833` ``` qed ``` lp15@56215 ` 834` ``` } note ** = this ``` lp15@56215 ` 835` ``` show ?thesis ``` lp15@56215 ` 836` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 837` ``` proof (rule has_derivative_sequence [OF cvs _ _ x]) ``` lp15@56215 ` 838` ``` show "\n. \x\s. (f n has_derivative (op * (f' n x))) (at x within s)" ``` lp15@56215 ` 839` ``` by (metis has_field_derivative_def df) ``` lp15@56215 ` 840` ``` next show "(\n. f n x) ----> l" ``` lp15@56215 ` 841` ``` by (rule tf) ``` lp15@56215 ` 842` ``` next show "\e>0. \N. \n\N. \x\s. \h. cmod (f' n x * h - g' x * h) \ e * cmod h" ``` lp15@56215 ` 843` ``` by (blast intro: **) ``` lp15@56215 ` 844` ``` qed ``` lp15@56215 ` 845` ```qed ``` lp15@56215 ` 846` lp15@56215 ` 847` lp15@56215 ` 848` ```lemma has_complex_derivative_series: ``` lp15@56215 ` 849` ``` fixes s :: "complex set" ``` lp15@56215 ` 850` ``` assumes cvs: "convex s" ``` lp15@56215 ` 851` ``` and df: "\n x. x \ s \ (f n has_field_derivative f' n x) (at x within s)" ``` lp15@61609 ` 852` ``` and conv: "\e. 0 < e \ \N. \n x. n \ N \ x \ s ``` lp15@56215 ` 853` ``` \ cmod ((\i e" ``` lp15@56215 ` 854` ``` and "\x l. x \ s \ ((\n. f n x) sums l)" ``` lp15@56215 ` 855` ``` shows "\g. \x \ s. ((\n. f n x) sums g x) \ ((g has_field_derivative g' x) (at x within s))" ``` lp15@56215 ` 856` ```proof - ``` lp15@56215 ` 857` ``` from assms obtain x l where x: "x \ s" and sf: "((\n. f n x) sums l)" ``` lp15@56215 ` 858` ``` by blast ``` lp15@56215 ` 859` ``` { fix e::real assume e: "e > 0" ``` lp15@61609 ` 860` ``` then obtain N where N: "\n x. n \ N \ x \ s ``` lp15@56215 ` 861` ``` \ cmod ((\i e" ``` lp15@61609 ` 862` ``` by (metis conv) ``` lp15@56215 ` 863` ``` have "\N. \n\N. \x\s. \h. cmod ((\i e * cmod h" ``` lp15@56215 ` 864` ``` proof (rule exI [of _ N], clarify) ``` lp15@56215 ` 865` ``` fix n y h ``` lp15@56215 ` 866` ``` assume "N \ n" "y \ s" ``` lp15@56215 ` 867` ``` then have "cmod ((\i e" ``` lp15@56215 ` 868` ``` by (metis N) ``` lp15@56215 ` 869` ``` then have "cmod h * cmod ((\i cmod h * e" ``` lp15@56215 ` 870` ``` by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) ``` lp15@56215 ` 871` ``` then show "cmod ((\i e * cmod h" ``` lp15@56215 ` 872` ``` by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib) ``` lp15@56215 ` 873` ``` qed ``` lp15@56215 ` 874` ``` } note ** = this ``` lp15@56215 ` 875` ``` show ?thesis ``` lp15@56215 ` 876` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 877` ``` proof (rule has_derivative_series [OF cvs _ _ x]) ``` lp15@56215 ` 878` ``` fix n x ``` lp15@56215 ` 879` ``` assume "x \ s" ``` lp15@56215 ` 880` ``` then show "((f n) has_derivative (\z. z * f' n x)) (at x within s)" ``` lp15@56215 ` 881` ``` by (metis df has_field_derivative_def mult_commute_abs) ``` lp15@56215 ` 882` ``` next show " ((\n. f n x) sums l)" ``` lp15@56215 ` 883` ``` by (rule sf) ``` lp15@56215 ` 884` ``` next show "\e>0. \N. \n\N. \x\s. \h. cmod ((\i e * cmod h" ``` lp15@56215 ` 885` ``` by (blast intro: **) ``` lp15@56215 ` 886` ``` qed ``` lp15@56215 ` 887` ```qed ``` lp15@56215 ` 888` eberlm@61531 ` 889` eberlm@61531 ` 890` ```lemma complex_differentiable_series: ``` eberlm@61531 ` 891` ``` fixes f :: "nat \ complex \ complex" ``` eberlm@61531 ` 892` ``` assumes "convex s" "open s" ``` eberlm@61531 ` 893` ``` assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" ``` eberlm@61531 ` 894` ``` assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" and x: "x \ s" ``` eberlm@61531 ` 896` ``` shows "summable (\n. f n x)" and "(\x. \n. f n x) complex_differentiable (at x)" ``` eberlm@61531 ` 897` ```proof - ``` eberlm@61531 ` 898` ``` from assms(4) obtain g' where A: "uniform_limit s (\n x. \ig. \x\s. (\n. f n x) sums g x \ (g has_field_derivative g' x) (at x within s)" ``` eberlm@61531 ` 902` ``` by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within) ``` eberlm@61531 ` 903` ``` then obtain g where g: "\x. x \ s \ (\n. f n x) sums g x" ``` eberlm@61531 ` 904` ``` "\x. x \ s \ (g has_field_derivative g' x) (at x within s)" by blast ``` eberlm@61531 ` 905` ``` from g[OF x] show "summable (\n. f n x)" by (auto simp: summable_def) ``` eberlm@61531 ` 906` ``` from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)" ``` eberlm@61531 ` 907` ``` by (simp add: has_field_derivative_def s) ``` eberlm@61531 ` 908` ``` have "((\x. \n. f n x) has_derivative op * (g' x)) (at x)" ``` eberlm@61531 ` 909` ``` by (rule has_derivative_transform_within_open[OF `open s` x _ g']) ``` eberlm@61531 ` 910` ``` (insert g, auto simp: sums_iff) ``` eberlm@61531 ` 911` ``` thus "(\x. \n. f n x) complex_differentiable (at x)" unfolding differentiable_def ``` eberlm@61531 ` 912` ``` by (auto simp: summable_def complex_differentiable_def has_field_derivative_def) ``` eberlm@61531 ` 913` ```qed ``` eberlm@61531 ` 914` eberlm@61531 ` 915` ```lemma complex_differentiable_series': ``` eberlm@61531 ` 916` ``` fixes f :: "nat \ complex \ complex" ``` eberlm@61531 ` 917` ``` assumes "convex s" "open s" ``` eberlm@61531 ` 918` ``` assumes "\n x. x \ s \ (f n has_field_derivative f' n x) (at x)" ``` eberlm@61531 ` 919` ``` assumes "uniformly_convergent_on s (\n x. \i s" "summable (\n. f n x0)" ``` eberlm@61531 ` 921` ``` shows "(\x. \n. f n x) complex_differentiable (at x0)" ``` eberlm@61531 ` 922` ``` using complex_differentiable_series[OF assms, of x0] `x0 \ s` by blast+ ``` eberlm@61531 ` 923` wenzelm@60420 ` 924` ```subsection\Bound theorem\ ``` lp15@56215 ` 925` lp15@56215 ` 926` ```lemma complex_differentiable_bound: ``` lp15@56215 ` 927` ``` fixes s :: "complex set" ``` lp15@56215 ` 928` ``` assumes cvs: "convex s" ``` lp15@56215 ` 929` ``` and df: "\z. z \ s \ (f has_field_derivative f' z) (at z within s)" ``` lp15@56215 ` 930` ``` and dn: "\z. z \ s \ norm (f' z) \ B" ``` lp15@56215 ` 931` ``` and "x \ s" "y \ s" ``` lp15@56215 ` 932` ``` shows "norm(f x - f y) \ B * norm(x - y)" ``` lp15@56215 ` 933` ``` apply (rule differentiable_bound [OF cvs]) ``` huffman@56223 ` 934` ``` apply (rule ballI, erule df [unfolded has_field_derivative_def]) ``` huffman@56223 ` 935` ``` apply (rule ballI, rule onorm_le, simp add: norm_mult mult_right_mono dn) ``` huffman@56223 ` 936` ``` apply fact ``` huffman@56223 ` 937` ``` apply fact ``` lp15@56215 ` 938` ``` done ``` lp15@56215 ` 939` wenzelm@60420 ` 940` ```subsection\Inverse function theorem for complex derivatives.\ ``` lp15@56215 ` 941` lp15@56215 ` 942` ```lemma has_complex_derivative_inverse_basic: ``` lp15@56215 ` 943` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 944` ``` shows "DERIV f (g y) :> f' \ ``` lp15@56215 ` 945` ``` f' \ 0 \ ``` lp15@56215 ` 946` ``` continuous (at y) g \ ``` lp15@56215 ` 947` ``` open t \ ``` lp15@56215 ` 948` ``` y \ t \ ``` lp15@56215 ` 949` ``` (\z. z \ t \ f (g z) = z) ``` lp15@56215 ` 950` ``` \ DERIV g y :> inverse (f')" ``` lp15@56215 ` 951` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 952` ``` apply (rule has_derivative_inverse_basic) ``` lp15@56215 ` 953` ``` apply (auto simp: bounded_linear_mult_right) ``` lp15@56215 ` 954` ``` done ``` lp15@56215 ` 955` lp15@56215 ` 956` ```(*Used only once, in Multivariate/cauchy.ml. *) ``` lp15@56215 ` 957` ```lemma has_complex_derivative_inverse_strong: ``` lp15@56215 ` 958` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 959` ``` shows "DERIV f x :> f' \ ``` lp15@56215 ` 960` ``` f' \ 0 \ ``` lp15@56215 ` 961` ``` open s \ ``` lp15@56215 ` 962` ``` x \ s \ ``` lp15@56215 ` 963` ``` continuous_on s f \ ``` lp15@56215 ` 964` ``` (\z. z \ s \ g (f z) = z) ``` lp15@56215 ` 965` ``` \ DERIV g (f x) :> inverse (f')" ``` lp15@56215 ` 966` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 967` ``` apply (rule has_derivative_inverse_strong [of s x f g ]) ``` lp15@61609 ` 968` ``` using assms ``` lp15@56215 ` 969` ``` by auto ``` lp15@56215 ` 970` lp15@56215 ` 971` ```lemma has_complex_derivative_inverse_strong_x: ``` lp15@56215 ` 972` ``` fixes f :: "complex \ complex" ``` lp15@56215 ` 973` ``` shows "DERIV f (g y) :> f' \ ``` lp15@56215 ` 974` ``` f' \ 0 \ ``` lp15@56215 ` 975` ``` open s \ ``` lp15@56215 ` 976` ``` continuous_on s f \ ``` lp15@56215 ` 977` ``` g y \ s \ f(g y) = y \ ``` lp15@56215 ` 978` ``` (\z. z \ s \ g (f z) = z) ``` lp15@56215 ` 979` ``` \ DERIV g y :> inverse (f')" ``` lp15@56215 ` 980` ``` unfolding has_field_derivative_def ``` lp15@56215 ` 981` ``` apply (rule has_derivative_inverse_strong_x [of s g y f]) ``` lp15@61609 ` 982` ``` using assms ``` lp15@56215 ` 983` ``` by auto ``` lp15@56215 ` 984` wenzelm@60420 ` 985` ```subsection \Taylor on Complex Numbers\ ``` lp15@56215 ` 986` lp15@56215 ` 987` ```lemma setsum_Suc_reindex: ``` lp15@56215 ` 988` ``` fixes f :: "nat \ 'a::ab_group_add" ``` lp15@56215 ` 989` ``` shows "setsum f {0..n} = f 0 - f (Suc n) + setsum (\i. f (Suc i)) {0..n}" ``` lp15@56215 ` 990` ```by (induct n) auto ``` lp15@56215 ` 991` lp15@56215 ` 992` ```lemma complex_taylor: ``` lp15@61609 ` 993` ``` assumes s: "convex s" ``` lp15@56215 ` 994` ``` and f: "\i x. x \ s \ i \ n \ (f i has_field_derivative f (Suc i) x) (at x within s)" ``` lp15@56215 ` 995` ``` and B: "\x. x \ s \ cmod (f (Suc n) x) \ B" ``` lp15@56215 ` 996` ``` and w: "w \ s" ``` lp15@56215 ` 997` ``` and z: "z \ s" ``` lp15@59730 ` 998` ``` shows "cmod(f 0 z - (\i\n. f i w * (z-w) ^ i / (fact i))) ``` lp15@56215 ` 999` ``` \ B * cmod(z - w)^(Suc n) / fact n" ``` lp15@56215 ` 1000` ```proof - ``` lp15@56215 ` 1001` ``` have wzs: "closed_segment w z \ s" using assms ``` lp15@56215 ` 1002` ``` by (metis convex_contains_segment) ``` lp15@56215 ` 1003` ``` { fix u ``` lp15@56215 ` 1004` ``` assume "u \ closed_segment w z" ``` lp15@56215 ` 1005` ``` then have "u \ s" ``` lp15@56215 ` 1006` ``` by (metis wzs subsetD) ``` lp15@59730 ` 1007` ``` have "(\i\n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) + ``` lp15@61609 ` 1008` ``` f (Suc i) u * (z-u)^i / (fact i)) = ``` lp15@59730 ` 1009` ``` f (Suc n) u * (z-u) ^ n / (fact n)" ``` lp15@56215 ` 1010` ``` proof (induction n) ``` lp15@56215 ` 1011` ``` case 0 show ?case by simp ``` lp15@56215 ` 1012` ``` next ``` lp15@56215 ` 1013` ``` case (Suc n) ``` lp15@59730 ` 1014` ``` have "(\i\Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) + ``` lp15@61609 ` 1015` ``` f (Suc i) u * (z-u) ^ i / (fact i)) = ``` lp15@59730 ` 1016` ``` f (Suc n) u * (z-u) ^ n / (fact n) + ``` lp15@59730 ` 1017` ``` f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) - ``` lp15@59730 ` 1018` ``` f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))" ``` hoelzl@56479 ` 1019` ``` using Suc by simp ``` lp15@59730 ` 1020` ``` also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))" ``` lp15@56215 ` 1021` ``` proof - ``` lp15@59730 ` 1022` ``` have "(fact(Suc n)) * ``` lp15@59730 ` 1023` ``` (f(Suc n) u *(z-u) ^ n / (fact n) + ``` lp15@59730 ` 1024` ``` f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / (fact(Suc n)) - ``` lp15@59730 ` 1025` ``` f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / (fact(Suc n))) = ``` lp15@59730 ` 1026` ``` ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) + ``` lp15@59730 ` 1027` ``` ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) - ``` lp15@59730 ` 1028` ``` ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))" ``` lp15@59730 ` 1029` ``` by (simp add: algebra_simps del: fact.simps) ``` lp15@59730 ` 1030` ``` also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) + ``` lp15@59730 ` 1031` ``` (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) - ``` lp15@59730 ` 1032` ``` (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))" ``` lp15@59730 ` 1033` ``` by (simp del: fact.simps) ``` lp15@59730 ` 1034` ``` also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) + ``` lp15@59730 ` 1035` ``` (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) - ``` lp15@59730 ` 1036` ``` (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))" ``` lp15@59730 ` 1037` ``` by (simp only: fact.simps of_nat_mult ac_simps) simp ``` lp15@56215 ` 1038` ``` also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)" ``` lp15@56215 ` 1039` ``` by (simp add: algebra_simps) ``` lp15@56215 ` 1040` ``` finally show ?thesis ``` lp15@59730 ` 1041` ``` by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps) ``` lp15@56215 ` 1042` ``` qed ``` lp15@56215 ` 1043` ``` finally show ?case . ``` lp15@56215 ` 1044` ``` qed ``` lp15@61609 ` 1045` ``` then have "((\v. (\i\n. f i v * (z - v)^i / (fact i))) ``` lp15@59730 ` 1046` ``` has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n)) ``` lp15@56215 ` 1047` ``` (at u within s)" ``` hoelzl@56381 ` 1048` ``` apply (intro derivative_eq_intros) ``` wenzelm@60420 ` 1049` ``` apply (blast intro: assms \u \ s\) ``` lp15@56215 ` 1050` ``` apply (rule refl)+ ``` lp15@56215 ` 1051` ``` apply (auto simp: field_simps) ``` lp15@56215 ` 1052` ``` done ``` lp15@56215 ` 1053` ``` } note sum_deriv = this ``` lp15@56215 ` 1054` ``` { fix u ``` lp15@56215 ` 1055` ``` assume u: "u \ closed_segment w z" ``` lp15@56215 ` 1056` ``` then have us: "u \ s" ``` lp15@56215 ` 1057` ``` by (metis wzs subsetD) ``` lp15@56215 ` 1058` ``` have "cmod (f (Suc n) u) * cmod (z - u) ^ n \ cmod (f (Suc n) u) * cmod (u - z) ^ n" ``` lp15@56215 ` 1059` ``` by (metis norm_minus_commute order_refl) ``` lp15@56215 ` 1060` ``` also have "... \ cmod (f (Suc n) u) * cmod (z - w) ^ n" ``` lp15@56215 ` 1061` ``` by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u]) ``` lp15@56215 ` 1062` ``` also have "... \ B * cmod (z - w) ^ n" ``` lp15@56215 ` 1063` ``` by (metis norm_ge_zero zero_le_power mult_right_mono B [OF us]) ``` lp15@56215 ` 1064` ``` finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \ B * cmod (z - w) ^ n" . ``` lp15@56215 ` 1065` ``` } note cmod_bound = this ``` lp15@59730 ` 1066` ``` have "(\i\n. f i z * (z - z) ^ i / (fact i)) = (\i\n. (f i z / (fact i)) * 0 ^ i)" ``` lp15@56215 ` 1067` ``` by simp ``` lp15@59730 ` 1068` ``` also have "\ = f 0 z / (fact 0)" ``` lp15@56215 ` 1069` ``` by (subst setsum_zero_power) simp ``` lp15@61609 ` 1070` ``` finally have "cmod (f 0 z - (\i\n. f i w * (z - w) ^ i / (fact i))) ``` lp15@59730 ` 1071` ``` \ cmod ((\i\n. f i w * (z - w) ^ i / (fact i)) - ``` lp15@59730 ` 1072` ``` (\i\n. f i z * (z - z) ^ i / (fact i)))" ``` lp15@56215 ` 1073` ``` by (simp add: norm_minus_commute) ``` lp15@59730 ` 1074` ``` also have "... \ B * cmod (z - w) ^ n / (fact n) * cmod (w - z)" ``` lp15@61609 ` 1075` ``` apply (rule complex_differentiable_bound ``` lp15@59730 ` 1076` ``` [where f' = "\w. f (Suc n) w * (z - w)^n / (fact n)" ``` paulson@61518 ` 1077` ``` and s = "closed_segment w z", OF convex_closed_segment]) ``` lp15@61609 ` 1078` ``` apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs] ``` lp15@56215 ` 1079` ``` norm_divide norm_mult norm_power divide_le_cancel cmod_bound) ``` lp15@56215 ` 1080` ``` done ``` lp15@59730 ` 1081` ``` also have "... \ B * cmod (z - w) ^ Suc n / (fact n)" ``` lp15@61609 ` 1082` ``` by (simp add: algebra_simps norm_minus_commute) ``` lp15@56215 ` 1083` ``` finally show ?thesis . ``` lp15@56215 ` 1084` ```qed ``` lp15@56215 ` 1085` wenzelm@60420 ` 1086` ```text\Something more like the traditional MVT for real components.\ ``` hoelzl@56370 ` 1087` lp15@56238 ` 1088` ```lemma complex_mvt_line: ``` hoelzl@56369 ` 1089` ``` assumes "\u. u \ closed_segment w z \ (f has_field_derivative f'(u)) (at u)" ``` paulson@61518 ` 1090` ``` shows "\u. u \ closed_segment w z \ Re(f z) - Re(f w) = Re(f'(u) * (z - w))" ``` lp15@56238 ` 1091` ```proof - ``` lp15@56238 ` 1092` ``` have twz: "\t. (1 - t) *\<^sub>R w + t *\<^sub>R z = w + t *\<^sub>R (z - w)" ``` lp15@56238 ` 1093` ``` by (simp add: real_vector.scale_left_diff_distrib real_vector.scale_right_diff_distrib) ``` hoelzl@56381 ` 1094` ``` note assms[unfolded has_field_derivative_def, derivative_intros] ``` lp15@56238 ` 1095` ``` show ?thesis ``` lp15@56238 ` 1096` ``` apply (cut_tac mvt_simple ``` lp15@56238 ` 1097` ``` [of 0 1 "Re o f o (\t. (1 - t) *\<^sub>R w + t *\<^sub>R z)" ``` lp15@56238 ` 1098` ``` "\u. Re o (\h. f'((1 - u) *\<^sub>R w + u *\<^sub>R z) * h) o (\t. t *\<^sub>R (z - w))"]) ``` lp15@56238 ` 1099` ``` apply auto ``` lp15@56238 ` 1100` ``` apply (rule_tac x="(1 - x) *\<^sub>R w + x *\<^sub>R z" in exI) ``` paulson@61518 ` 1101` ``` apply (auto simp: closed_segment_def twz) [] ``` paulson@61518 ` 1102` ``` apply (intro derivative_eq_intros has_derivative_at_within, simp_all) ``` hoelzl@56369 ` 1103` ``` apply (simp add: fun_eq_iff real_vector.scale_right_diff_distrib) ``` paulson@61518 ` 1104` ``` apply (force simp: twz closed_segment_def) ``` lp15@56238 ` 1105` ``` done ``` lp15@56238 ` 1106` ```qed ``` lp15@56238 ` 1107` lp15@56238 ` 1108` ```lemma complex_taylor_mvt: ``` lp15@56238 ` 1109` ``` assumes "\i x. \x \ closed_segment w z; i \ n\ \ ((f i) has_field_derivative f (Suc i) x) (at x)" ``` lp15@56238 ` 1110` ``` shows "\u. u \ closed_segment w z \ ``` lp15@56238 ` 1111` ``` Re (f 0 z) = ``` lp15@59730 ` 1112` ``` Re ((\i = 0..n. f i w * (z - w) ^ i / (fact i)) + ``` lp15@59730 ` 1113` ``` (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))" ``` lp15@56238 ` 1114` ```proof - ``` lp15@56238 ` 1115` ``` { fix u ``` lp15@56238 ` 1116` ``` assume u: "u \ closed_segment w z" ``` lp15@56238 ` 1117` ``` have "(\i = 0..n. ``` lp15@56238 ` 1118` ``` (f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / ``` lp15@59730 ` 1119` ``` (fact i)) = ``` lp15@56238 ` 1120` ``` f (Suc 0) u - ``` lp15@56238 ` 1121` ``` (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1122` ``` (fact (Suc n)) + ``` lp15@56238 ` 1123` ``` (\i = 0..n. ``` lp15@56238 ` 1124` ``` (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) / ``` lp15@59730 ` 1125` ``` (fact (Suc i)))" ``` lp15@56238 ` 1126` ``` by (subst setsum_Suc_reindex) simp ``` lp15@56238 ` 1127` ``` also have "... = f (Suc 0) u - ``` lp15@56238 ` 1128` ``` (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1129` ``` (fact (Suc n)) + ``` lp15@56238 ` 1130` ``` (\i = 0..n. ``` lp15@61609 ` 1131` ``` f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i)) - ``` lp15@59730 ` 1132` ``` f (Suc i) u * (z-u) ^ i / (fact i))" ``` haftmann@57514 ` 1133` ``` by (simp only: diff_divide_distrib fact_cancel ac_simps) ``` lp15@56238 ` 1134` ``` also have "... = f (Suc 0) u - ``` lp15@56238 ` 1135` ``` (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) / ``` lp15@59730 ` 1136` ``` (fact (Suc n)) + ``` lp15@59730 ` 1137` ``` f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u" ``` lp15@56238 ` 1138` ``` by (subst setsum_Suc_diff) auto ``` lp15@59730 ` 1139` ``` also have "... = f (Suc n) u * (z-u) ^ n / (fact n)" ``` lp15@56238 ` 1140` ``` by (simp only: algebra_simps diff_divide_distrib fact_cancel) ``` lp15@61609 ` 1141` ``` finally have "(\i = 0..n. (f (Suc i) u * (z - u) ^ i ``` lp15@59730 ` 1142` ``` - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) = ``` lp15@59730 ` 1143` ``` f (Suc n) u * (z - u) ^ n / (fact n)" . ``` lp15@59730 ` 1144` ``` then have "((\u. \i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative ``` lp15@59730 ` 1145` ``` f (Suc n) u * (z - u) ^ n / (fact n)) (at u)" ``` hoelzl@56381 ` 1146` ``` apply (intro derivative_eq_intros)+ ``` lp15@56238 ` 1147` ``` apply (force intro: u assms) ``` lp15@56238 ` 1148` ``` apply (rule refl)+ ``` haftmann@57514 ` 1149` ``` apply (auto simp: ac_simps) ``` lp15@56238 ` 1150` ``` done ``` lp15@56238 ` 1151` ``` } ``` lp15@56238 ` 1152` ``` then show ?thesis ``` lp15@59730 ` 1153` ``` apply (cut_tac complex_mvt_line [of w z "\u. \i = 0..n. f i u * (z-u) ^ i / (fact i)" ``` lp15@59730 ` 1154` ``` "\u. (f (Suc n) u * (z-u)^n / (fact n))"]) ``` lp15@56238 ` 1155` ``` apply (auto simp add: intro: open_closed_segment) ``` lp15@56238 ` 1156` ``` done ``` lp15@56238 ` 1157` ```qed ``` lp15@56238 ` 1158` lp15@60017 ` 1159` wenzelm@60420 ` 1160` ```subsection \Polynomal function extremal theorem, from HOL Light\ ``` lp15@60017 ` 1161` lp15@60017 ` 1162` ```lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*) ``` lp15@60017 ` 1163` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@60017 ` 1164` ``` assumes "0 < e" ``` lp15@60017 ` 1165` ``` shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)" ``` lp15@60017 ` 1166` ```proof (induct n) ``` lp15@60017 ` 1167` ``` case 0 with assms ``` lp15@60017 ` 1168` ``` show ?case ``` lp15@60017 ` 1169` ``` apply (rule_tac x="norm (c 0) / e" in exI) ``` lp15@60017 ` 1170` ``` apply (auto simp: field_simps) ``` lp15@60017 ` 1171` ``` done ``` lp15@60017 ` 1172` ```next ``` lp15@60017 ` 1173` ``` case (Suc n) ``` lp15@60017 ` 1174` ``` obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" ``` lp15@60017 ` 1175` ``` using Suc assms by blast ``` lp15@60017 ` 1176` ``` show ?case ``` lp15@60017 ` 1177` ``` proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc) ``` lp15@60017 ` 1178` ``` fix z::'a ``` lp15@60017 ` 1179` ``` assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z" ``` lp15@60017 ` 1180` ``` then have z2: "e + norm (c (Suc n)) \ e * norm z" ``` lp15@60017 ` 1181` ``` using assms by (simp add: field_simps) ``` lp15@60017 ` 1182` ``` have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" ``` lp15@60017 ` 1183` ``` using M [OF z1] by simp ``` lp15@60017 ` 1184` ``` 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 ` 1185` ``` by simp ``` lp15@60017 ` 1186` ``` 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 ` 1187` ``` by (blast intro: norm_triangle_le elim: ) ``` lp15@60017 ` 1188` ``` also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n" ``` lp15@60017 ` 1189` ``` by (simp add: norm_power norm_mult algebra_simps) ``` lp15@60017 ` 1190` ``` also have "... \ (e * norm z) * norm z ^ Suc n" ``` lp15@60017 ` 1191` ``` by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) ``` lp15@60017 ` 1192` ``` finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" ``` lp15@60162 ` 1193` ``` by simp ``` lp15@60017 ` 1194` ``` qed ``` lp15@60017 ` 1195` ```qed ``` lp15@60017 ` 1196` lp15@60017 ` 1197` ```lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*) ``` lp15@60017 ` 1198` ``` fixes c :: "nat \ 'a::real_normed_div_algebra" ``` lp15@60017 ` 1199` ``` assumes k: "c k \ 0" "1\k" and kn: "k\n" ``` lp15@60017 ` 1200` ``` shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity" ``` lp15@60017 ` 1201` ```using kn ``` lp15@60017 ` 1202` ```proof (induction n) ``` lp15@60017 ` 1203` ``` case 0 ``` lp15@60017 ` 1204` ``` then show ?case ``` lp15@60017 ` 1205` ``` using k by simp ``` lp15@60017 ` 1206` ```next ``` lp15@60017 ` 1207` ``` case (Suc m) ``` lp15@60017 ` 1208` ``` let ?even = ?case ``` lp15@60017 ` 1209` ``` show ?even ``` lp15@60017 ` 1210` ``` proof (cases "c (Suc m) = 0") ``` lp15@60017 ` 1211` ``` case True ``` lp15@60017 ` 1212` ``` then show ?even using Suc k ``` lp15@60017 ` 1213` ``` by auto (metis antisym_conv less_eq_Suc_le not_le) ``` lp15@60017 ` 1214` ``` next ``` lp15@60017 ` 1215` ``` case False ``` lp15@60017 ` 1216` ``` then obtain M where M: ``` lp15@60017 ` 1217` ``` "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m" ``` lp15@60017 ` 1218` ``` using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc ``` lp15@60017 ` 1219` ``` by auto ``` lp15@60017 ` 1220` ``` have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)" ``` lp15@60017 ` 1221` ``` proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc) ``` lp15@60017 ` 1222` ``` fix z::'a ``` lp15@60017 ` 1223` ``` assume z1: "M \ norm z" "1 \ norm z" ``` lp15@60017 ` 1224` ``` and "\B\ * 2 / norm (c (Suc m)) \ norm z" ``` lp15@60017 ` 1225` ``` then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2" ``` lp15@60017 ` 1226` ``` using False by (simp add: field_simps) ``` lp15@60017 ` 1227` ``` have nz: "norm z \ norm z ^ Suc m" ``` wenzelm@60420 ` 1228` ``` by (metis \1 \ norm z\ One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc) ``` lp15@60017 ` 1229` ``` have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)" ``` lp15@60017 ` 1230` ``` by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2) ``` lp15@60017 ` 1231` ``` have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i) ``` lp15@60017 ` 1232` ``` \ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m" ``` lp15@60017 ` 1233` ``` using M [of z] Suc z1 by auto ``` lp15@60017 ` 1234` ``` also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)" ``` lp15@60017 ` 1235` ``` using nz by (simp add: mult_mono del: power_Suc) ``` lp15@60017 ` 1236` ``` finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)" ``` lp15@60017 ` 1237` ``` using Suc.IH ``` lp15@60017 ` 1238` ``` apply (auto simp: eventually_at_infinity) ``` lp15@60017 ` 1239` ``` apply (rule *) ``` lp15@60017 ` 1240` ``` apply (simp add: field_simps norm_mult norm_power) ``` lp15@60017 ` 1241` ``` done ``` lp15@60017 ` 1242` ``` qed ``` lp15@60017 ` 1243` ``` then show ?even ``` lp15@60017 ` 1244` ``` by (simp add: eventually_at_infinity) ``` lp15@60017 ` 1245` ``` qed ``` lp15@60017 ` 1246` ```qed ``` lp15@60017 ` 1247` lp15@56215 ` 1248` ```end ```