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