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