30 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field |
30 lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field |
31 |
31 |
32 lemma fact_cancel: |
32 lemma fact_cancel: |
33 fixes c :: "'a::real_field" |
33 fixes c :: "'a::real_field" |
34 shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" |
34 shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)" |
35 by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps) |
35 using of_nat_neq_0 by force |
36 |
36 |
37 lemma bilinear_times: |
37 lemma bilinear_times: |
38 fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)" |
38 fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)" |
39 by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) |
39 by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI) |
40 |
40 |
41 lemma linear_cnj: "linear cnj" |
41 lemma linear_cnj: "linear cnj" |
42 using bounded_linear.linear[OF bounded_linear_cnj] . |
42 using bounded_linear.linear[OF bounded_linear_cnj] . |
43 |
|
44 lemma tendsto_Re_upper: |
|
45 assumes "~ (trivial_limit F)" |
|
46 "(f \<longlongrightarrow> l) F" |
|
47 "eventually (\<lambda>x. Re(f x) \<le> b) F" |
|
48 shows "Re(l) \<le> b" |
|
49 by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Re) |
|
50 |
|
51 lemma tendsto_Re_lower: |
|
52 assumes "~ (trivial_limit F)" |
|
53 "(f \<longlongrightarrow> l) F" |
|
54 "eventually (\<lambda>x. b \<le> Re(f x)) F" |
|
55 shows "b \<le> Re(l)" |
|
56 by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Re) |
|
57 |
|
58 lemma tendsto_Im_upper: |
|
59 assumes "~ (trivial_limit F)" |
|
60 "(f \<longlongrightarrow> l) F" |
|
61 "eventually (\<lambda>x. Im(f x) \<le> b) F" |
|
62 shows "Im(l) \<le> b" |
|
63 by (metis assms tendsto_le [OF _ tendsto_const] tendsto_Im) |
|
64 |
|
65 lemma tendsto_Im_lower: |
|
66 assumes "~ (trivial_limit F)" |
|
67 "(f \<longlongrightarrow> l) F" |
|
68 "eventually (\<lambda>x. b \<le> Im(f x)) F" |
|
69 shows "b \<le> Im(l)" |
|
70 by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Im) |
|
71 |
43 |
72 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0" |
44 lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0" |
73 by auto |
45 by auto |
74 |
46 |
75 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1" |
47 lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1" |
114 |
86 |
115 subsection\<open>DERIV stuff\<close> |
87 subsection\<open>DERIV stuff\<close> |
116 |
88 |
117 lemma DERIV_zero_connected_constant: |
89 lemma DERIV_zero_connected_constant: |
118 fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a" |
90 fixes f :: "'a::{real_normed_field,euclidean_space} \<Rightarrow> 'a" |
119 assumes "connected s" |
91 assumes "connected S" |
120 and "open s" |
92 and "open S" |
121 and "finite k" |
93 and "finite K" |
122 and "continuous_on s f" |
94 and "continuous_on S f" |
123 and "\<forall>x\<in>(s - k). DERIV f x :> 0" |
95 and "\<forall>x\<in>(S - K). DERIV f x :> 0" |
124 obtains c where "\<And>x. x \<in> s \<Longrightarrow> f(x) = c" |
96 obtains c where "\<And>x. x \<in> S \<Longrightarrow> f(x) = c" |
125 using has_derivative_zero_connected_constant [OF assms(1-4)] assms |
97 using has_derivative_zero_connected_constant [OF assms(1-4)] assms |
126 by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def) |
98 by (metis DERIV_const has_derivative_const Diff_iff at_within_open frechet_derivative_at has_field_derivative_def) |
127 |
99 |
128 lemmas DERIV_zero_constant = has_field_derivative_zero_constant |
100 lemmas DERIV_zero_constant = has_field_derivative_zero_constant |
129 |
101 |
130 lemma DERIV_zero_unique: |
102 lemma DERIV_zero_unique: |
131 assumes "convex s" |
103 assumes "convex S" |
132 and d0: "\<And>x. x\<in>s \<Longrightarrow> (f has_field_derivative 0) (at x within s)" |
104 and d0: "\<And>x. x\<in>S \<Longrightarrow> (f has_field_derivative 0) (at x within S)" |
133 and "a \<in> s" |
105 and "a \<in> S" |
134 and "x \<in> s" |
106 and "x \<in> S" |
135 shows "f x = f a" |
107 shows "f x = f a" |
136 by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)]) |
108 by (rule has_derivative_zero_unique [OF assms(1) _ assms(4,3)]) |
137 (metis d0 has_field_derivative_imp_has_derivative lambda_zero) |
109 (metis d0 has_field_derivative_imp_has_derivative lambda_zero) |
138 |
110 |
139 lemma DERIV_zero_connected_unique: |
111 lemma DERIV_zero_connected_unique: |
140 assumes "connected s" |
112 assumes "connected S" |
141 and "open s" |
113 and "open S" |
142 and d0: "\<And>x. x\<in>s \<Longrightarrow> DERIV f x :> 0" |
114 and d0: "\<And>x. x\<in>S \<Longrightarrow> DERIV f x :> 0" |
143 and "a \<in> s" |
115 and "a \<in> S" |
144 and "x \<in> s" |
116 and "x \<in> S" |
145 shows "f x = f a" |
117 shows "f x = f a" |
146 by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)]) |
118 by (rule has_derivative_zero_unique_connected [OF assms(2,1) _ assms(5,4)]) |
147 (metis has_field_derivative_def lambda_zero d0) |
119 (metis has_field_derivative_def lambda_zero d0) |
148 |
120 |
149 lemma DERIV_transform_within: |
121 lemma DERIV_transform_within: |
150 assumes "(f has_field_derivative f') (at a within s)" |
122 assumes "(f has_field_derivative f') (at a within S)" |
151 and "0 < d" "a \<in> s" |
123 and "0 < d" "a \<in> S" |
152 and "\<And>x. x\<in>s \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x" |
124 and "\<And>x. x\<in>S \<Longrightarrow> dist x a < d \<Longrightarrow> f x = g x" |
153 shows "(g has_field_derivative f') (at a within s)" |
125 shows "(g has_field_derivative f') (at a within S)" |
154 using assms unfolding has_field_derivative_def |
126 using assms unfolding has_field_derivative_def |
155 by (blast intro: has_derivative_transform_within) |
127 by (blast intro: has_derivative_transform_within) |
156 |
128 |
157 lemma DERIV_transform_within_open: |
129 lemma DERIV_transform_within_open: |
158 assumes "DERIV f a :> f'" |
130 assumes "DERIV f a :> f'" |
159 and "open s" "a \<in> s" |
131 and "open S" "a \<in> S" |
160 and "\<And>x. x\<in>s \<Longrightarrow> f x = g x" |
132 and "\<And>x. x\<in>S \<Longrightarrow> f x = g x" |
161 shows "DERIV g a :> f'" |
133 shows "DERIV g a :> f'" |
162 using assms unfolding has_field_derivative_def |
134 using assms unfolding has_field_derivative_def |
163 by (metis has_derivative_transform_within_open) |
135 by (metis has_derivative_transform_within_open) |
164 |
136 |
165 lemma DERIV_transform_at: |
137 lemma DERIV_transform_at: |
453 "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk> |
423 "\<lbrakk>f field_differentiable at z; g field_differentiable at z\<rbrakk> |
454 \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z" |
424 \<Longrightarrow> deriv (\<lambda>w. f w * g w) z = f z * deriv g z + deriv f z * g z" |
455 unfolding DERIV_deriv_iff_field_differentiable[symmetric] |
425 unfolding DERIV_deriv_iff_field_differentiable[symmetric] |
456 by (auto intro!: DERIV_imp_deriv derivative_eq_intros) |
426 by (auto intro!: DERIV_imp_deriv derivative_eq_intros) |
457 |
427 |
458 lemma deriv_cmult [simp]: |
428 lemma deriv_cmult: |
459 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z" |
429 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. c * f w) z = c * deriv f z" |
|
430 by simp |
|
431 |
|
432 lemma deriv_cmult_right: |
|
433 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c" |
|
434 by simp |
|
435 |
|
436 lemma deriv_inverse [simp]: |
|
437 "\<lbrakk>f field_differentiable at z; f z \<noteq> 0\<rbrakk> |
|
438 \<Longrightarrow> deriv (\<lambda>w. inverse (f w)) z = - deriv f z / f z ^ 2" |
460 unfolding DERIV_deriv_iff_field_differentiable[symmetric] |
439 unfolding DERIV_deriv_iff_field_differentiable[symmetric] |
461 by (auto intro!: DERIV_imp_deriv derivative_eq_intros) |
440 by (safe intro!: DERIV_imp_deriv derivative_eq_intros) (auto simp: divide_simps power2_eq_square) |
462 |
441 |
463 lemma deriv_cmult_right [simp]: |
442 lemma deriv_divide [simp]: |
464 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w * c) z = deriv f z * c" |
443 "\<lbrakk>f field_differentiable at z; g field_differentiable at z; g z \<noteq> 0\<rbrakk> |
465 unfolding DERIV_deriv_iff_field_differentiable[symmetric] |
444 \<Longrightarrow> deriv (\<lambda>w. f w / g w) z = (deriv f z * g z - f z * deriv g z) / g z ^ 2" |
466 by (auto intro!: DERIV_imp_deriv derivative_eq_intros) |
445 by (simp add: field_class.field_divide_inverse field_differentiable_inverse) |
467 |
446 (simp add: divide_simps power2_eq_square) |
468 lemma deriv_cdivide_right [simp]: |
447 |
|
448 lemma deriv_cdivide_right: |
469 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c" |
449 "f field_differentiable at z \<Longrightarrow> deriv (\<lambda>w. f w / c) z = deriv f z / c" |
470 unfolding Fields.field_class.field_divide_inverse |
450 by (simp add: field_class.field_divide_inverse) |
471 by (blast intro: deriv_cmult_right) |
|
472 |
451 |
473 lemma complex_derivative_transform_within_open: |
452 lemma complex_derivative_transform_within_open: |
474 "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk> |
453 "\<lbrakk>f holomorphic_on s; g holomorphic_on s; open s; z \<in> s; \<And>w. w \<in> s \<Longrightarrow> f w = g w\<rbrakk> |
475 \<Longrightarrow> deriv f z = deriv g z" |
454 \<Longrightarrow> deriv f z = deriv g z" |
476 unfolding holomorphic_on_def |
455 unfolding holomorphic_on_def |
478 (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open) |
457 (metis DERIV_deriv_iff_field_differentiable DERIV_transform_within_open at_within_open) |
479 |
458 |
480 lemma deriv_compose_linear: |
459 lemma deriv_compose_linear: |
481 "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)" |
460 "f field_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)" |
482 apply (rule DERIV_imp_deriv) |
461 apply (rule DERIV_imp_deriv) |
483 apply (simp add: DERIV_deriv_iff_field_differentiable [symmetric]) |
462 unfolding DERIV_deriv_iff_field_differentiable [symmetric] |
484 apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id]) |
463 by (metis (full_types) DERIV_chain2 DERIV_cmult_Id mult.commute) |
485 apply (simp add: algebra_simps) |
464 |
486 done |
|
487 |
465 |
488 lemma nonzero_deriv_nonconstant: |
466 lemma nonzero_deriv_nonconstant: |
489 assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0" |
467 assumes df: "DERIV f \<xi> :> df" and S: "open S" "\<xi> \<in> S" and "df \<noteq> 0" |
490 shows "\<not> f constant_on S" |
468 shows "\<not> f constant_on S" |
491 unfolding constant_on_def |
469 unfolding constant_on_def |
492 by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique) |
470 by (metis \<open>df \<noteq> 0\<close> DERIV_transform_within_open [OF df S] DERIV_const DERIV_unique) |
493 |
471 |
494 lemma holomorphic_nonconstant: |
472 lemma holomorphic_nonconstant: |
495 assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0" |
473 assumes holf: "f holomorphic_on S" and "open S" "\<xi> \<in> S" "deriv f \<xi> \<noteq> 0" |
496 shows "\<not> f constant_on S" |
474 shows "\<not> f constant_on S" |
497 apply (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S]) |
475 by (rule nonzero_deriv_nonconstant [of f "deriv f \<xi>" \<xi> S]) |
498 using assms |
476 (use assms in \<open>auto simp: holomorphic_derivI\<close>) |
499 apply (auto simp: holomorphic_derivI) |
|
500 done |
|
501 |
477 |
502 subsection\<open>Caratheodory characterization\<close> |
478 subsection\<open>Caratheodory characterization\<close> |
503 |
479 |
504 lemma field_differentiable_caratheodory_at: |
480 lemma field_differentiable_caratheodory_at: |
505 "f field_differentiable (at z) \<longleftrightarrow> |
481 "f field_differentiable (at z) \<longleftrightarrow> |
514 by (simp add: field_differentiable_def has_field_derivative_def) |
490 by (simp add: field_differentiable_def has_field_derivative_def) |
515 |
491 |
516 subsection\<open>Analyticity on a set\<close> |
492 subsection\<open>Analyticity on a set\<close> |
517 |
493 |
518 definition analytic_on (infixl "(analytic'_on)" 50) |
494 definition analytic_on (infixl "(analytic'_on)" 50) |
519 where |
495 where "f analytic_on S \<equiv> \<forall>x \<in> S. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)" |
520 "f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)" |
|
521 |
496 |
522 named_theorems analytic_intros "introduction rules for proving analyticity" |
497 named_theorems analytic_intros "introduction rules for proving analyticity" |
523 |
498 |
524 lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s" |
499 lemma analytic_imp_holomorphic: "f analytic_on S \<Longrightarrow> f holomorphic_on S" |
525 by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def) |
500 by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def) |
526 (metis centre_in_ball field_differentiable_at_within) |
501 (metis centre_in_ball field_differentiable_at_within) |
527 |
502 |
528 lemma analytic_on_open: "open s \<Longrightarrow> f analytic_on s \<longleftrightarrow> f holomorphic_on s" |
503 lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S" |
529 apply (auto simp: analytic_imp_holomorphic) |
504 apply (auto simp: analytic_imp_holomorphic) |
530 apply (auto simp: analytic_on_def holomorphic_on_def) |
505 apply (auto simp: analytic_on_def holomorphic_on_def) |
531 by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball) |
506 by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball) |
532 |
507 |
533 lemma analytic_on_imp_differentiable_at: |
508 lemma analytic_on_imp_differentiable_at: |
534 "f analytic_on s \<Longrightarrow> x \<in> s \<Longrightarrow> f field_differentiable (at x)" |
509 "f analytic_on S \<Longrightarrow> x \<in> S \<Longrightarrow> f field_differentiable (at x)" |
535 apply (auto simp: analytic_on_def holomorphic_on_def) |
510 apply (auto simp: analytic_on_def holomorphic_on_def) |
536 by (metis open_ball centre_in_ball field_differentiable_within_open) |
511 by (metis open_ball centre_in_ball field_differentiable_within_open) |
537 |
512 |
538 lemma analytic_on_subset: "f analytic_on s \<Longrightarrow> t \<subseteq> s \<Longrightarrow> f analytic_on t" |
513 lemma analytic_on_subset: "f analytic_on S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> f analytic_on T" |
539 by (auto simp: analytic_on_def) |
514 by (auto simp: analytic_on_def) |
540 |
515 |
541 lemma analytic_on_Un: "f analytic_on (s \<union> t) \<longleftrightarrow> f analytic_on s \<and> f analytic_on t" |
516 lemma analytic_on_Un: "f analytic_on (S \<union> T) \<longleftrightarrow> f analytic_on S \<and> f analytic_on T" |
542 by (auto simp: analytic_on_def) |
517 by (auto simp: analytic_on_def) |
543 |
518 |
544 lemma analytic_on_Union: "f analytic_on (\<Union>s) \<longleftrightarrow> (\<forall>t \<in> s. f analytic_on t)" |
519 lemma analytic_on_Union: "f analytic_on (\<Union>\<T>) \<longleftrightarrow> (\<forall>T \<in> \<T>. f analytic_on T)" |
545 by (auto simp: analytic_on_def) |
520 by (auto simp: analytic_on_def) |
546 |
521 |
547 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. s i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (s i))" |
522 lemma analytic_on_UN: "f analytic_on (\<Union>i\<in>I. S i) \<longleftrightarrow> (\<forall>i\<in>I. f analytic_on (S i))" |
548 by (auto simp: analytic_on_def) |
523 by (auto simp: analytic_on_def) |
549 |
524 |
550 lemma analytic_on_holomorphic: |
525 lemma analytic_on_holomorphic: |
551 "f analytic_on s \<longleftrightarrow> (\<exists>t. open t \<and> s \<subseteq> t \<and> f holomorphic_on t)" |
526 "f analytic_on S \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f holomorphic_on T)" |
552 (is "?lhs = ?rhs") |
527 (is "?lhs = ?rhs") |
553 proof - |
528 proof - |
554 have "?lhs \<longleftrightarrow> (\<exists>t. open t \<and> s \<subseteq> t \<and> f analytic_on t)" |
529 have "?lhs \<longleftrightarrow> (\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T)" |
555 proof safe |
530 proof safe |
556 assume "f analytic_on s" |
531 assume "f analytic_on S" |
557 then show "\<exists>t. open t \<and> s \<subseteq> t \<and> f analytic_on t" |
532 then show "\<exists>T. open T \<and> S \<subseteq> T \<and> f analytic_on T" |
558 apply (simp add: analytic_on_def) |
533 apply (simp add: analytic_on_def) |
559 apply (rule exI [where x="\<Union>{u. open u \<and> f analytic_on u}"], auto) |
534 apply (rule exI [where x="\<Union>{U. open U \<and> f analytic_on U}"], auto) |
560 apply (metis open_ball analytic_on_open centre_in_ball) |
535 apply (metis open_ball analytic_on_open centre_in_ball) |
561 by (metis analytic_on_def) |
536 by (metis analytic_on_def) |
562 next |
537 next |
563 fix t |
538 fix T |
564 assume "open t" "s \<subseteq> t" "f analytic_on t" |
539 assume "open T" "S \<subseteq> T" "f analytic_on T" |
565 then show "f analytic_on s" |
540 then show "f analytic_on S" |
566 by (metis analytic_on_subset) |
541 by (metis analytic_on_subset) |
567 qed |
542 qed |
568 also have "... \<longleftrightarrow> ?rhs" |
543 also have "... \<longleftrightarrow> ?rhs" |
569 by (auto simp: analytic_on_open) |
544 by (auto simp: analytic_on_open) |
570 finally show ?thesis . |
545 finally show ?thesis . |
571 qed |
546 qed |
572 |
547 |
573 lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on s" |
548 lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on S" |
574 by (auto simp add: analytic_on_holomorphic) |
549 by (auto simp add: analytic_on_holomorphic) |
575 |
550 |
576 lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s" |
551 lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on S" |
577 by (metis analytic_on_def holomorphic_on_const zero_less_one) |
552 by (metis analytic_on_def holomorphic_on_const zero_less_one) |
578 |
553 |
579 lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s" |
554 lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on S" |
580 by (simp add: analytic_on_def gt_ex) |
555 by (simp add: analytic_on_def gt_ex) |
581 |
556 |
582 lemma analytic_on_id [analytic_intros]: "id analytic_on s" |
557 lemma analytic_on_id [analytic_intros]: "id analytic_on S" |
583 unfolding id_def by (rule analytic_on_ident) |
558 unfolding id_def by (rule analytic_on_ident) |
584 |
559 |
585 lemma analytic_on_compose: |
560 lemma analytic_on_compose: |
586 assumes f: "f analytic_on s" |
561 assumes f: "f analytic_on S" |
587 and g: "g analytic_on (f ` s)" |
562 and g: "g analytic_on (f ` S)" |
588 shows "(g o f) analytic_on s" |
563 shows "(g o f) analytic_on S" |
589 unfolding analytic_on_def |
564 unfolding analytic_on_def |
590 proof (intro ballI) |
565 proof (intro ballI) |
591 fix x |
566 fix x |
592 assume x: "x \<in> s" |
567 assume x: "x \<in> S" |
593 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f |
568 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball x e" using f |
594 by (metis analytic_on_def) |
569 by (metis analytic_on_def) |
595 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g |
570 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball (f x) e'" using g |
596 by (metis analytic_on_def g image_eqI x) |
571 by (metis analytic_on_def g image_eqI x) |
597 have "isCont f x" |
572 have "isCont f x" |
605 then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e" |
580 then show "\<exists>e>0. g \<circ> f holomorphic_on ball x e" |
606 by (metis d e min_less_iff_conj) |
581 by (metis d e min_less_iff_conj) |
607 qed |
582 qed |
608 |
583 |
609 lemma analytic_on_compose_gen: |
584 lemma analytic_on_compose_gen: |
610 "f analytic_on s \<Longrightarrow> g analytic_on t \<Longrightarrow> (\<And>z. z \<in> s \<Longrightarrow> f z \<in> t) |
585 "f analytic_on S \<Longrightarrow> g analytic_on T \<Longrightarrow> (\<And>z. z \<in> S \<Longrightarrow> f z \<in> T) |
611 \<Longrightarrow> g o f analytic_on s" |
586 \<Longrightarrow> g o f analytic_on S" |
612 by (metis analytic_on_compose analytic_on_subset image_subset_iff) |
587 by (metis analytic_on_compose analytic_on_subset image_subset_iff) |
613 |
588 |
614 lemma analytic_on_neg [analytic_intros]: |
589 lemma analytic_on_neg [analytic_intros]: |
615 "f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s" |
590 "f analytic_on S \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on S" |
616 by (metis analytic_on_holomorphic holomorphic_on_minus) |
591 by (metis analytic_on_holomorphic holomorphic_on_minus) |
617 |
592 |
618 lemma analytic_on_add [analytic_intros]: |
593 lemma analytic_on_add [analytic_intros]: |
619 assumes f: "f analytic_on s" |
594 assumes f: "f analytic_on S" |
620 and g: "g analytic_on s" |
595 and g: "g analytic_on S" |
621 shows "(\<lambda>z. f z + g z) analytic_on s" |
596 shows "(\<lambda>z. f z + g z) analytic_on S" |
622 unfolding analytic_on_def |
597 unfolding analytic_on_def |
623 proof (intro ballI) |
598 proof (intro ballI) |
624 fix z |
599 fix z |
625 assume z: "z \<in> s" |
600 assume z: "z \<in> S" |
626 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
601 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
627 by (metis analytic_on_def) |
602 by (metis analytic_on_def) |
628 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
603 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
629 by (metis analytic_on_def g z) |
604 by (metis analytic_on_def g z) |
630 have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')" |
605 have "(\<lambda>z. f z + g z) holomorphic_on ball z (min e e')" |
634 then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e" |
609 then show "\<exists>e>0. (\<lambda>z. f z + g z) holomorphic_on ball z e" |
635 by (metis e e' min_less_iff_conj) |
610 by (metis e e' min_less_iff_conj) |
636 qed |
611 qed |
637 |
612 |
638 lemma analytic_on_diff [analytic_intros]: |
613 lemma analytic_on_diff [analytic_intros]: |
639 assumes f: "f analytic_on s" |
614 assumes f: "f analytic_on S" |
640 and g: "g analytic_on s" |
615 and g: "g analytic_on S" |
641 shows "(\<lambda>z. f z - g z) analytic_on s" |
616 shows "(\<lambda>z. f z - g z) analytic_on S" |
642 unfolding analytic_on_def |
617 unfolding analytic_on_def |
643 proof (intro ballI) |
618 proof (intro ballI) |
644 fix z |
619 fix z |
645 assume z: "z \<in> s" |
620 assume z: "z \<in> S" |
646 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
621 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
647 by (metis analytic_on_def) |
622 by (metis analytic_on_def) |
648 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
623 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
649 by (metis analytic_on_def g z) |
624 by (metis analytic_on_def g z) |
650 have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')" |
625 have "(\<lambda>z. f z - g z) holomorphic_on ball z (min e e')" |
654 then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e" |
629 then show "\<exists>e>0. (\<lambda>z. f z - g z) holomorphic_on ball z e" |
655 by (metis e e' min_less_iff_conj) |
630 by (metis e e' min_less_iff_conj) |
656 qed |
631 qed |
657 |
632 |
658 lemma analytic_on_mult [analytic_intros]: |
633 lemma analytic_on_mult [analytic_intros]: |
659 assumes f: "f analytic_on s" |
634 assumes f: "f analytic_on S" |
660 and g: "g analytic_on s" |
635 and g: "g analytic_on S" |
661 shows "(\<lambda>z. f z * g z) analytic_on s" |
636 shows "(\<lambda>z. f z * g z) analytic_on S" |
662 unfolding analytic_on_def |
637 unfolding analytic_on_def |
663 proof (intro ballI) |
638 proof (intro ballI) |
664 fix z |
639 fix z |
665 assume z: "z \<in> s" |
640 assume z: "z \<in> S" |
666 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
641 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
667 by (metis analytic_on_def) |
642 by (metis analytic_on_def) |
668 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
643 obtain e' where e': "0 < e'" and gh: "g holomorphic_on ball z e'" using g |
669 by (metis analytic_on_def g z) |
644 by (metis analytic_on_def g z) |
670 have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')" |
645 have "(\<lambda>z. f z * g z) holomorphic_on ball z (min e e')" |
674 then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e" |
649 then show "\<exists>e>0. (\<lambda>z. f z * g z) holomorphic_on ball z e" |
675 by (metis e e' min_less_iff_conj) |
650 by (metis e e' min_less_iff_conj) |
676 qed |
651 qed |
677 |
652 |
678 lemma analytic_on_inverse [analytic_intros]: |
653 lemma analytic_on_inverse [analytic_intros]: |
679 assumes f: "f analytic_on s" |
654 assumes f: "f analytic_on S" |
680 and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)" |
655 and nz: "(\<And>z. z \<in> S \<Longrightarrow> f z \<noteq> 0)" |
681 shows "(\<lambda>z. inverse (f z)) analytic_on s" |
656 shows "(\<lambda>z. inverse (f z)) analytic_on S" |
682 unfolding analytic_on_def |
657 unfolding analytic_on_def |
683 proof (intro ballI) |
658 proof (intro ballI) |
684 fix z |
659 fix z |
685 assume z: "z \<in> s" |
660 assume z: "z \<in> S" |
686 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
661 then obtain e where e: "0 < e" and fh: "f holomorphic_on ball z e" using f |
687 by (metis analytic_on_def) |
662 by (metis analytic_on_def) |
688 have "continuous_on (ball z e) f" |
663 have "continuous_on (ball z e) f" |
689 by (metis fh holomorphic_on_imp_continuous_on) |
664 by (metis fh holomorphic_on_imp_continuous_on) |
690 then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0" |
665 then obtain e' where e': "0 < e'" and nz': "\<And>y. dist z y < e' \<Longrightarrow> f y \<noteq> 0" |
696 then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e" |
671 then show "\<exists>e>0. (\<lambda>z. inverse (f z)) holomorphic_on ball z e" |
697 by (metis e e' min_less_iff_conj) |
672 by (metis e e' min_less_iff_conj) |
698 qed |
673 qed |
699 |
674 |
700 lemma analytic_on_divide [analytic_intros]: |
675 lemma analytic_on_divide [analytic_intros]: |
701 assumes f: "f analytic_on s" |
676 assumes f: "f analytic_on S" |
702 and g: "g analytic_on s" |
677 and g: "g analytic_on S" |
703 and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)" |
678 and nz: "(\<And>z. z \<in> S \<Longrightarrow> g z \<noteq> 0)" |
704 shows "(\<lambda>z. f z / g z) analytic_on s" |
679 shows "(\<lambda>z. f z / g z) analytic_on S" |
705 unfolding divide_inverse |
680 unfolding divide_inverse |
706 by (metis analytic_on_inverse analytic_on_mult f g nz) |
681 by (metis analytic_on_inverse analytic_on_mult f g nz) |
707 |
682 |
708 lemma analytic_on_power [analytic_intros]: |
683 lemma analytic_on_power [analytic_intros]: |
709 "f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s" |
684 "f analytic_on S \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on S" |
710 by (induct n) (auto simp: analytic_on_mult) |
685 by (induct n) (auto simp: analytic_on_mult) |
711 |
686 |
712 lemma analytic_on_sum [analytic_intros]: |
687 lemma analytic_on_sum [analytic_intros]: |
713 "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s" |
688 "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S" |
714 by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add) |
689 by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add) |
715 |
690 |
716 lemma deriv_left_inverse: |
691 lemma deriv_left_inverse: |
717 assumes "f holomorphic_on S" and "g holomorphic_on T" |
692 assumes "f holomorphic_on S" and "g holomorphic_on T" |
718 and "open S" and "open T" |
693 and "open S" and "open T" |
809 |
784 |
810 subsection\<open>Complex differentiation of sequences and series\<close> |
785 subsection\<open>Complex differentiation of sequences and series\<close> |
811 |
786 |
812 (* TODO: Could probably be simplified using Uniform_Limit *) |
787 (* TODO: Could probably be simplified using Uniform_Limit *) |
813 lemma has_complex_derivative_sequence: |
788 lemma has_complex_derivative_sequence: |
814 fixes s :: "complex set" |
789 fixes S :: "complex set" |
815 assumes cvs: "convex s" |
790 assumes cvs: "convex S" |
816 and df: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)" |
791 and df: "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)" |
817 and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s \<longrightarrow> norm (f' n x - g' x) \<le> e" |
792 and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> S \<longrightarrow> norm (f' n x - g' x) \<le> e" |
818 and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially" |
793 and "\<exists>x l. x \<in> S \<and> ((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially" |
819 shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> |
794 shows "\<exists>g. \<forall>x \<in> S. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> |
820 (g has_field_derivative (g' x)) (at x within s)" |
795 (g has_field_derivative (g' x)) (at x within S)" |
821 proof - |
796 proof - |
822 from assms obtain x l where x: "x \<in> s" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially" |
797 from assms obtain x l where x: "x \<in> S" and tf: "((\<lambda>n. f n x) \<longlongrightarrow> l) sequentially" |
823 by blast |
798 by blast |
824 { fix e::real assume e: "e > 0" |
799 { fix e::real assume e: "e > 0" |
825 then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> s \<longrightarrow> cmod (f' n x - g' x) \<le> e" |
800 then obtain N where N: "\<forall>n\<ge>N. \<forall>x. x \<in> S \<longrightarrow> cmod (f' n x - g' x) \<le> e" |
826 by (metis conv) |
801 by (metis conv) |
827 have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h" |
802 have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h" |
828 proof (rule exI [of _ N], clarify) |
803 proof (rule exI [of _ N], clarify) |
829 fix n y h |
804 fix n y h |
830 assume "N \<le> n" "y \<in> s" |
805 assume "N \<le> n" "y \<in> S" |
831 then have "cmod (f' n y - g' y) \<le> e" |
806 then have "cmod (f' n y - g' y) \<le> e" |
832 by (metis N) |
807 by (metis N) |
833 then have "cmod h * cmod (f' n y - g' y) \<le> cmod h * e" |
808 then have "cmod h * cmod (f' n y - g' y) \<le> cmod h * e" |
834 by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) |
809 by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) |
835 then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h" |
810 then show "cmod (f' n y * h - g' y * h) \<le> e * cmod h" |
839 show ?thesis |
814 show ?thesis |
840 unfolding has_field_derivative_def |
815 unfolding has_field_derivative_def |
841 proof (rule has_derivative_sequence [OF cvs _ _ x]) |
816 proof (rule has_derivative_sequence [OF cvs _ _ x]) |
842 show "(\<lambda>n. f n x) \<longlonglongrightarrow> l" |
817 show "(\<lambda>n. f n x) \<longlonglongrightarrow> l" |
843 by (rule tf) |
818 by (rule tf) |
844 next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h" |
819 next show "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod (f' n x * h - g' x * h) \<le> e * cmod h" |
845 unfolding eventually_sequentially by (blast intro: **) |
820 unfolding eventually_sequentially by (blast intro: **) |
846 qed (metis has_field_derivative_def df) |
821 qed (metis has_field_derivative_def df) |
847 qed |
822 qed |
848 |
823 |
849 lemma has_complex_derivative_series: |
824 lemma has_complex_derivative_series: |
850 fixes s :: "complex set" |
825 fixes S :: "complex set" |
851 assumes cvs: "convex s" |
826 assumes cvs: "convex S" |
852 and df: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)" |
827 and df: "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x within S)" |
853 and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> s |
828 and conv: "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<longrightarrow> x \<in> S |
854 \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e" |
829 \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e" |
855 and "\<exists>x l. x \<in> s \<and> ((\<lambda>n. f n x) sums l)" |
830 and "\<exists>x l. x \<in> S \<and> ((\<lambda>n. f n x) sums l)" |
856 shows "\<exists>g. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((g has_field_derivative g' x) (at x within s))" |
831 shows "\<exists>g. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((g has_field_derivative g' x) (at x within S))" |
857 proof - |
832 proof - |
858 from assms obtain x l where x: "x \<in> s" and sf: "((\<lambda>n. f n x) sums l)" |
833 from assms obtain x l where x: "x \<in> S" and sf: "((\<lambda>n. f n x) sums l)" |
859 by blast |
834 by blast |
860 { fix e::real assume e: "e > 0" |
835 { fix e::real assume e: "e > 0" |
861 then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> s |
836 then obtain N where N: "\<forall>n x. n \<ge> N \<longrightarrow> x \<in> S |
862 \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e" |
837 \<longrightarrow> cmod ((\<Sum>i<n. f' i x) - g' x) \<le> e" |
863 by (metis conv) |
838 by (metis conv) |
864 have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h" |
839 have "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h" |
865 proof (rule exI [of _ N], clarify) |
840 proof (rule exI [of _ N], clarify) |
866 fix n y h |
841 fix n y h |
867 assume "N \<le> n" "y \<in> s" |
842 assume "N \<le> n" "y \<in> S" |
868 then have "cmod ((\<Sum>i<n. f' i y) - g' y) \<le> e" |
843 then have "cmod ((\<Sum>i<n. f' i y) - g' y) \<le> e" |
869 by (metis N) |
844 by (metis N) |
870 then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e" |
845 then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e" |
871 by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) |
846 by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2) |
872 then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h" |
847 then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h" |
875 } note ** = this |
850 } note ** = this |
876 show ?thesis |
851 show ?thesis |
877 unfolding has_field_derivative_def |
852 unfolding has_field_derivative_def |
878 proof (rule has_derivative_series [OF cvs _ _ x]) |
853 proof (rule has_derivative_series [OF cvs _ _ x]) |
879 fix n x |
854 fix n x |
880 assume "x \<in> s" |
855 assume "x \<in> S" |
881 then show "((f n) has_derivative (\<lambda>z. z * f' n x)) (at x within s)" |
856 then show "((f n) has_derivative (\<lambda>z. z * f' n x)) (at x within S)" |
882 by (metis df has_field_derivative_def mult_commute_abs) |
857 by (metis df has_field_derivative_def mult_commute_abs) |
883 next show " ((\<lambda>n. f n x) sums l)" |
858 next show " ((\<lambda>n. f n x) sums l)" |
884 by (rule sf) |
859 by (rule sf) |
885 next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h" |
860 next show "\<And>e. e>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<forall>h. cmod ((\<Sum>i<n. h * f' i x) - g' x * h) \<le> e * cmod h" |
886 unfolding eventually_sequentially by (blast intro: **) |
861 unfolding eventually_sequentially by (blast intro: **) |
887 qed |
862 qed |
888 qed |
863 qed |
889 |
864 |
890 |
865 |
891 lemma field_differentiable_series: |
866 lemma field_differentiable_series: |
892 fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a" |
867 fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach} \<Rightarrow> 'a" |
893 assumes "convex s" "open s" |
868 assumes "convex S" "open S" |
894 assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)" |
869 assumes "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative f' n x) (at x)" |
895 assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)" |
870 assumes "uniformly_convergent_on S (\<lambda>n x. \<Sum>i<n. f' i x)" |
896 assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s" |
871 assumes "x0 \<in> S" "summable (\<lambda>n. f n x0)" and x: "x \<in> S" |
897 shows "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" |
872 shows "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" |
898 proof - |
873 proof - |
899 from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially" |
874 from assms(4) obtain g' where A: "uniform_limit S (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially" |
900 unfolding uniformly_convergent_on_def by blast |
875 unfolding uniformly_convergent_on_def by blast |
901 from x and \<open>open s\<close> have s: "at x within s = at x" by (rule at_within_open) |
876 from x and \<open>open S\<close> have S: "at x within S = at x" by (rule at_within_open) |
902 have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)" |
877 have "\<exists>g. \<forall>x\<in>S. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within S)" |
903 by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within) |
878 by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within) |
904 then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x" |
879 then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x" |
905 "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast |
880 "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast |
906 from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)" |
881 from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)" |
907 by (simp add: has_field_derivative_def s) |
882 by (simp add: has_field_derivative_def S) |
908 have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)" |
883 have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)" |
909 by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x]) |
884 by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x]) |
910 (insert g, auto simp: sums_iff) |
885 (insert g, auto simp: sums_iff) |
911 thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def |
886 thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def |
912 by (auto simp: summable_def field_differentiable_def has_field_derivative_def) |
887 by (auto simp: summable_def field_differentiable_def has_field_derivative_def) |
913 qed |
888 qed |
914 |
889 |
915 subsection\<open>Bound theorem\<close> |
890 subsection\<open>Bound theorem\<close> |
916 |
891 |
917 lemma field_differentiable_bound: |
892 lemma field_differentiable_bound: |
918 fixes s :: "'a::real_normed_field set" |
893 fixes S :: "'a::real_normed_field set" |
919 assumes cvs: "convex s" |
894 assumes cvs: "convex S" |
920 and df: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z within s)" |
895 and df: "\<And>z. z \<in> S \<Longrightarrow> (f has_field_derivative f' z) (at z within S)" |
921 and dn: "\<And>z. z \<in> s \<Longrightarrow> norm (f' z) \<le> B" |
896 and dn: "\<And>z. z \<in> S \<Longrightarrow> norm (f' z) \<le> B" |
922 and "x \<in> s" "y \<in> s" |
897 and "x \<in> S" "y \<in> S" |
923 shows "norm(f x - f y) \<le> B * norm(x - y)" |
898 shows "norm(f x - f y) \<le> B * norm(x - y)" |
924 apply (rule differentiable_bound [OF cvs]) |
899 apply (rule differentiable_bound [OF cvs]) |
925 apply (erule df [unfolded has_field_derivative_def]) |
900 apply (erule df [unfolded has_field_derivative_def]) |
926 apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms) |
901 apply (rule onorm_le, simp_all add: norm_mult mult_right_mono assms) |
927 done |
902 done |
939 unfolding has_field_derivative_def |
914 unfolding has_field_derivative_def |
940 apply (rule has_derivative_inverse_basic) |
915 apply (rule has_derivative_inverse_basic) |
941 apply (auto simp: bounded_linear_mult_right) |
916 apply (auto simp: bounded_linear_mult_right) |
942 done |
917 done |
943 |
918 |
944 lemmas has_complex_derivative_inverse_basic = has_field_derivative_inverse_basic |
|
945 |
|
946 lemma has_field_derivative_inverse_strong: |
919 lemma has_field_derivative_inverse_strong: |
947 fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a" |
920 fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a" |
948 shows "DERIV f x :> f' \<Longrightarrow> |
921 shows "DERIV f x :> f' \<Longrightarrow> |
949 f' \<noteq> 0 \<Longrightarrow> |
922 f' \<noteq> 0 \<Longrightarrow> |
950 open s \<Longrightarrow> |
923 open S \<Longrightarrow> |
951 x \<in> s \<Longrightarrow> |
924 x \<in> S \<Longrightarrow> |
952 continuous_on s f \<Longrightarrow> |
925 continuous_on S f \<Longrightarrow> |
953 (\<And>z. z \<in> s \<Longrightarrow> g (f z) = z) |
926 (\<And>z. z \<in> S \<Longrightarrow> g (f z) = z) |
954 \<Longrightarrow> DERIV g (f x) :> inverse (f')" |
927 \<Longrightarrow> DERIV g (f x) :> inverse (f')" |
955 unfolding has_field_derivative_def |
928 unfolding has_field_derivative_def |
956 apply (rule has_derivative_inverse_strong [of s x f g ]) |
929 apply (rule has_derivative_inverse_strong [of S x f g ]) |
957 by auto |
930 by auto |
958 lemmas has_complex_derivative_inverse_strong = has_field_derivative_inverse_strong |
|
959 |
931 |
960 lemma has_field_derivative_inverse_strong_x: |
932 lemma has_field_derivative_inverse_strong_x: |
961 fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a" |
933 fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a" |
962 shows "DERIV f (g y) :> f' \<Longrightarrow> |
934 shows "DERIV f (g y) :> f' \<Longrightarrow> |
963 f' \<noteq> 0 \<Longrightarrow> |
935 f' \<noteq> 0 \<Longrightarrow> |
964 open s \<Longrightarrow> |
936 open S \<Longrightarrow> |
965 continuous_on s f \<Longrightarrow> |
937 continuous_on S f \<Longrightarrow> |
966 g y \<in> s \<Longrightarrow> f(g y) = y \<Longrightarrow> |
938 g y \<in> S \<Longrightarrow> f(g y) = y \<Longrightarrow> |
967 (\<And>z. z \<in> s \<Longrightarrow> g (f z) = z) |
939 (\<And>z. z \<in> S \<Longrightarrow> g (f z) = z) |
968 \<Longrightarrow> DERIV g y :> inverse (f')" |
940 \<Longrightarrow> DERIV g y :> inverse (f')" |
969 unfolding has_field_derivative_def |
941 unfolding has_field_derivative_def |
970 apply (rule has_derivative_inverse_strong_x [of s g y f]) |
942 apply (rule has_derivative_inverse_strong_x [of S g y f]) |
971 by auto |
943 by auto |
972 lemmas has_complex_derivative_inverse_strong_x = has_field_derivative_inverse_strong_x |
|
973 |
944 |
974 subsection \<open>Taylor on Complex Numbers\<close> |
945 subsection \<open>Taylor on Complex Numbers\<close> |
975 |
946 |
976 lemma sum_Suc_reindex: |
947 lemma sum_Suc_reindex: |
977 fixes f :: "nat \<Rightarrow> 'a::ab_group_add" |
948 fixes f :: "nat \<Rightarrow> 'a::ab_group_add" |
978 shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}" |
949 shows "sum f {0..n} = f 0 - f (Suc n) + sum (\<lambda>i. f (Suc i)) {0..n}" |
979 by (induct n) auto |
950 by (induct n) auto |
980 |
951 |
981 lemma field_taylor: |
952 lemma field_taylor: |
982 assumes s: "convex s" |
953 assumes S: "convex S" |
983 and f: "\<And>i x. x \<in> s \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within s)" |
954 and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)" |
984 and B: "\<And>x. x \<in> s \<Longrightarrow> norm (f (Suc n) x) \<le> B" |
955 and B: "\<And>x. x \<in> S \<Longrightarrow> norm (f (Suc n) x) \<le> B" |
985 and w: "w \<in> s" |
956 and w: "w \<in> S" |
986 and z: "z \<in> s" |
957 and z: "z \<in> S" |
987 shows "norm(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) |
958 shows "norm(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) |
988 \<le> B * norm(z - w)^(Suc n) / fact n" |
959 \<le> B * norm(z - w)^(Suc n) / fact n" |
989 proof - |
960 proof - |
990 have wzs: "closed_segment w z \<subseteq> s" using assms |
961 have wzs: "closed_segment w z \<subseteq> S" using assms |
991 by (metis convex_contains_segment) |
962 by (metis convex_contains_segment) |
992 { fix u |
963 { fix u |
993 assume "u \<in> closed_segment w z" |
964 assume "u \<in> closed_segment w z" |
994 then have "u \<in> s" |
965 then have "u \<in> S" |
995 by (metis wzs subsetD) |
966 by (metis wzs subsetD) |
996 have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) + |
967 have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) + |
997 f (Suc i) u * (z-u)^i / (fact i)) = |
968 f (Suc i) u * (z-u)^i / (fact i)) = |
998 f (Suc n) u * (z-u) ^ n / (fact n)" |
969 f (Suc n) u * (z-u) ^ n / (fact n)" |
999 proof (induction n) |
970 proof (induction n) |
1031 qed |
1002 qed |
1032 finally show ?case . |
1003 finally show ?case . |
1033 qed |
1004 qed |
1034 then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i))) |
1005 then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i))) |
1035 has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n)) |
1006 has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n)) |
1036 (at u within s)" |
1007 (at u within S)" |
1037 apply (intro derivative_eq_intros) |
1008 apply (intro derivative_eq_intros) |
1038 apply (blast intro: assms \<open>u \<in> s\<close>) |
1009 apply (blast intro: assms \<open>u \<in> S\<close>) |
1039 apply (rule refl)+ |
1010 apply (rule refl)+ |
1040 apply (auto simp: field_simps) |
1011 apply (auto simp: field_simps) |
1041 done |
1012 done |
1042 } note sum_deriv = this |
1013 } note sum_deriv = this |
1043 { fix u |
1014 { fix u |
1044 assume u: "u \<in> closed_segment w z" |
1015 assume u: "u \<in> closed_segment w z" |
1045 then have us: "u \<in> s" |
1016 then have us: "u \<in> S" |
1046 by (metis wzs subsetD) |
1017 by (metis wzs subsetD) |
1047 have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n" |
1018 have "norm (f (Suc n) u) * norm (z - u) ^ n \<le> norm (f (Suc n) u) * norm (u - z) ^ n" |
1048 by (metis norm_minus_commute order_refl) |
1019 by (metis norm_minus_commute order_refl) |
1049 also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n" |
1020 also have "... \<le> norm (f (Suc n) u) * norm (z - w) ^ n" |
1050 by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u]) |
1021 by (metis mult_left_mono norm_ge_zero power_mono segment_bound [OF u]) |
1061 (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))" |
1032 (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))" |
1062 by (simp add: norm_minus_commute) |
1033 by (simp add: norm_minus_commute) |
1063 also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)" |
1034 also have "... \<le> B * norm (z - w) ^ n / (fact n) * norm (w - z)" |
1064 apply (rule field_differentiable_bound |
1035 apply (rule field_differentiable_bound |
1065 [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)" |
1036 [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)" |
1066 and s = "closed_segment w z", OF convex_closed_segment]) |
1037 and S = "closed_segment w z", OF convex_closed_segment]) |
1067 apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs] |
1038 apply (auto simp: ends_in_segment DERIV_subset [OF sum_deriv wzs] |
1068 norm_divide norm_mult norm_power divide_le_cancel cmod_bound) |
1039 norm_divide norm_mult norm_power divide_le_cancel cmod_bound) |
1069 done |
1040 done |
1070 also have "... \<le> B * norm (z - w) ^ Suc n / (fact n)" |
1041 also have "... \<le> B * norm (z - w) ^ Suc n / (fact n)" |
1071 by (simp add: algebra_simps norm_minus_commute) |
1042 by (simp add: algebra_simps norm_minus_commute) |
1072 finally show ?thesis . |
1043 finally show ?thesis . |
1073 qed |
1044 qed |
1074 |
1045 |
1075 lemma complex_taylor: |
1046 lemma complex_taylor: |
1076 assumes s: "convex s" |
1047 assumes S: "convex S" |
1077 and f: "\<And>i x. x \<in> s \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within s)" |
1048 and f: "\<And>i x. x \<in> S \<Longrightarrow> i \<le> n \<Longrightarrow> (f i has_field_derivative f (Suc i) x) (at x within S)" |
1078 and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B" |
1049 and B: "\<And>x. x \<in> S \<Longrightarrow> cmod (f (Suc n) x) \<le> B" |
1079 and w: "w \<in> s" |
1050 and w: "w \<in> S" |
1080 and z: "z \<in> s" |
1051 and z: "z \<in> S" |
1081 shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) |
1052 shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i))) |
1082 \<le> B * cmod(z - w)^(Suc n) / fact n" |
1053 \<le> B * cmod(z - w)^(Suc n) / fact n" |
1083 using assms by (rule field_taylor) |
1054 using assms by (rule field_taylor) |
1084 |
1055 |
1085 |
1056 |