78 fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
82 fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
79 assumes "norm z < fps_conv_radius f" |
83 assumes "norm z < fps_conv_radius f" |
80 shows "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z" |
84 shows "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z" |
81 using assms unfolding eval_fps_def fps_conv_radius_def |
85 using assms unfolding eval_fps_def fps_conv_radius_def |
82 by (intro summable_sums summable_in_conv_radius) simp_all |
86 by (intro summable_sums summable_in_conv_radius) simp_all |
83 |
|
84 lemma |
|
85 fixes r :: ereal |
|
86 assumes "f holomorphic_on eball z0 r" |
|
87 shows conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r" |
|
88 and eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z" |
|
89 and eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)" |
|
90 proof - |
|
91 have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" |
|
92 if "z \<in> ball z0 r'" "ereal r' < r" for z r' |
|
93 proof - |
|
94 from that(2) have "ereal r' \<le> r" by simp |
|
95 from assms(1) and this have "f holomorphic_on ball z0 r'" |
|
96 by (rule holomorphic_on_subset[OF _ ball_eball_mono]) |
|
97 from holomorphic_power_series [OF this that(1)] |
|
98 show ?thesis by (simp add: fps_expansion_def) |
|
99 qed |
|
100 hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z" |
|
101 if "z \<in> eball z0 r" for z |
|
102 using that by (subst (asm) eball_conv_UNION_balls) blast |
|
103 show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def |
|
104 proof (rule conv_radius_geI_ex) |
|
105 fix r' :: real assume r': "r' > 0" "ereal r' < r" |
|
106 thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)" |
|
107 using *[of "z0 + of_real r'"] |
|
108 by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm) |
|
109 qed |
|
110 show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z |
|
111 using *[OF that] by (simp add: eval_fps_def sums_iff) |
|
112 show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z |
|
113 using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm) |
|
114 qed |
|
115 |
87 |
116 lemma continuous_on_eval_fps: |
88 lemma continuous_on_eval_fps: |
117 fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
89 fixes f :: "'a :: {banach, real_normed_div_algebra} fps" |
118 shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)" |
90 shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)" |
119 proof (subst continuous_on_eq_continuous_at [OF open_eball], safe) |
91 proof (subst continuous_on_eq_continuous_at [OF open_eball], safe) |
613 lemma eval_fps_exp [simp]: |
585 lemma eval_fps_exp [simp]: |
614 fixes c :: "'a :: {banach, real_normed_field}" |
586 fixes c :: "'a :: {banach, real_normed_field}" |
615 shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def |
587 shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def |
616 by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps power_mult_distrib) |
588 by (simp add: eval_fps_def exp_def scaleR_conv_of_real field_split_simps power_mult_distrib) |
617 |
589 |
618 lemma |
590 text \<open> |
619 fixes f :: "complex fps" and r :: ereal |
591 The case of division is more complicated and will therefore not be handled here. |
620 assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0" |
592 Handling division becomes much more easy using complex analysis, and we will do so once |
621 shows fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" |
593 that is available. |
622 and eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow> |
594 \<close> |
623 eval_fps (inverse f) z = inverse (eval_fps f z)" |
595 |
624 proof - |
596 |
625 define R where "R = min (fps_conv_radius f) r" |
597 subsection \<open>Power series expansions of analytic functions\<close> |
626 have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and> |
|
627 (\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))" |
|
628 proof (cases "min r (fps_conv_radius f) > 0") |
|
629 case True |
|
630 define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0" |
|
631 have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))" |
|
632 using assms by (intro holomorphic_intros) auto |
|
633 from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)" |
|
634 unfolding f'_def by (rule conv_radius_fps_expansion) |
|
635 have eval_f': "eval_fps f' z = inverse (eval_fps f z)" |
|
636 if "norm z < fps_conv_radius f" "norm z < r" for z |
|
637 using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto |
|
638 |
|
639 have "f * f' = 1" |
|
640 proof (rule eval_fps_eqD) |
|
641 from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')" |
|
642 by (auto simp: min_def split: if_splits) |
|
643 also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult) |
|
644 finally show "\<dots> > 0" . |
|
645 next |
|
646 from True have "R > 0" by (auto simp: R_def) |
|
647 hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)" |
|
648 by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def) |
|
649 thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)" |
|
650 proof eventually_elim |
|
651 case (elim z) |
|
652 hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z" |
|
653 using radius by (intro eval_fps_mult) |
|
654 (auto simp: R_def min_def split: if_splits intro: less_trans) |
|
655 also have "eval_fps f' z = inverse (eval_fps f z)" |
|
656 using elim by (intro eval_f') (auto simp: R_def) |
|
657 also from elim have "eval_fps f z \<noteq> 0" |
|
658 by (intro assms) (auto simp: R_def) |
|
659 hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z" |
|
660 by simp |
|
661 finally show "eval_fps (f * f') z = eval_fps 1 z" . |
|
662 qed |
|
663 qed simp_all |
|
664 hence "f' = inverse f" |
|
665 by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac) |
|
666 with eval_f' and radius show ?thesis by simp |
|
667 next |
|
668 case False |
|
669 hence *: "eball 0 R = {}" |
|
670 by (intro eball_empty) (auto simp: R_def min_def split: if_splits) |
|
671 show ?thesis |
|
672 proof safe |
|
673 from False have "min r (fps_conv_radius f) \<le> 0" |
|
674 by (simp add: min_def) |
|
675 also have "0 \<le> fps_conv_radius (inverse f)" |
|
676 by (simp add: fps_conv_radius_def conv_radius_nonneg) |
|
677 finally show "min r (fps_conv_radius f) \<le> \<dots>" . |
|
678 qed (unfold * [unfolded R_def], auto) |
|
679 qed |
|
680 |
|
681 from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast |
|
682 from * show "eval_fps (inverse f) z = inverse (eval_fps f z)" |
|
683 if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z |
|
684 using that by auto |
|
685 qed |
|
686 |
|
687 lemma |
|
688 fixes f g :: "complex fps" and r :: ereal |
|
689 defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" |
|
690 assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" |
|
691 assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0" |
|
692 shows fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R" |
|
693 and eval_fps_divide': |
|
694 "ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z" |
|
695 proof - |
|
696 from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0" |
|
697 by (auto simp: eval_fps_at_0 zero_ereal_def) |
|
698 have "R \<le> min r (fps_conv_radius g)" |
|
699 by (auto simp: R_def intro: min.coboundedI2) |
|
700 also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)" |
|
701 by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def) |
|
702 finally have radius: "fps_conv_radius (inverse g) \<ge> R" . |
|
703 have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))" |
|
704 by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
|
705 also have "\<dots> \<le> fps_conv_radius (f * inverse g)" |
|
706 by (rule fps_conv_radius_mult) |
|
707 also have "f * inverse g = f / g" |
|
708 by (intro fps_divide_unit [symmetric] nz') |
|
709 finally show "fps_conv_radius (f / g) \<ge> R" . |
|
710 |
|
711 assume z: "ereal (norm z) < R" |
|
712 have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z" |
|
713 using radius by (intro eval_fps_mult less_le_trans[OF z]) |
|
714 (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
|
715 also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close> |
|
716 by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz) |
|
717 (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
|
718 also have "f * inverse g = f / g" by fact |
|
719 finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: field_split_simps) |
|
720 qed |
|
721 |
|
722 lemma |
|
723 fixes f g :: "complex fps" and r :: ereal |
|
724 defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}" |
|
725 assumes "subdegree g \<le> subdegree f" |
|
726 assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0" |
|
727 assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0" |
|
728 shows fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R" |
|
729 and eval_fps_divide: |
|
730 "ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow> |
|
731 eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" |
|
732 proof - |
|
733 define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g" |
|
734 have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g" |
|
735 unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+ |
|
736 have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0" |
|
737 using assms(2) by (simp_all add: f'_def g'_def) |
|
738 have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g" |
|
739 by (simp_all add: f'_def g'_def) |
|
740 have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)" |
|
741 "fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def) |
|
742 have g_nz: "g \<noteq> 0" |
|
743 proof - |
|
744 define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))" |
|
745 from \<open>r > 0\<close> have "z \<in> eball 0 r" |
|
746 by (cases r) (auto simp: z_def eball_def) |
|
747 moreover have "z \<noteq> 0" using \<open>r > 0\<close> |
|
748 by (cases r) (auto simp: z_def) |
|
749 ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6)) |
|
750 thus "g \<noteq> 0" by auto |
|
751 qed |
|
752 have fg: "f / g = f' * inverse g'" |
|
753 by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit) |
|
754 |
|
755 have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z |
|
756 proof (cases "z = 0") |
|
757 case False |
|
758 with assms and z have "eval_fps g z \<noteq> 0" by auto |
|
759 also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g" |
|
760 by (subst g_eq) (auto simp: eval_fps_mult) |
|
761 finally show ?thesis by auto |
|
762 qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0) |
|
763 |
|
764 have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')" |
|
765 by (auto simp: R_def min.coboundedI1 min.coboundedI2) |
|
766 also have "\<dots> \<le> fps_conv_radius (inverse g')" |
|
767 using g'_nz by (rule fps_conv_radius_inverse) |
|
768 finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" . |
|
769 hence "R \<le> fps_conv_radius (f' * inverse g')" |
|
770 by (intro order.trans[OF _ fps_conv_radius_mult]) |
|
771 (auto simp: R_def intro: min.coboundedI1 min.coboundedI2) |
|
772 thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg) |
|
773 |
|
774 fix z c :: complex assume z: "ereal (norm z) < R" |
|
775 assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)" |
|
776 show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)" |
|
777 proof (cases "z = 0") |
|
778 case False |
|
779 from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')" |
|
780 by simp |
|
781 with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z" |
|
782 unfolding fg by (subst eval_fps_mult) (auto simp: R_def) |
|
783 also have "eval_fps (inverse g') z = inverse (eval_fps g' z)" |
|
784 using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def) |
|
785 also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z" |
|
786 using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def) |
|
787 finally show ?thesis using False by simp |
|
788 qed (simp_all add: eval_fps_at_0 fg field_simps c) |
|
789 qed |
|
790 |
|
791 |
|
792 subsection \<open>Power series expansion of complex functions\<close> |
|
793 |
598 |
794 text \<open> |
599 text \<open> |
795 This predicate contains the notion that the given formal power series converges |
600 This predicate contains the notion that the given formal power series converges |
796 in some disc of positive radius around the origin and is equal to the given complex |
601 in some disc of positive radius around the origin and is equal to the given complex |
797 function there. |
602 function there. |
827 have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n" |
632 have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n" |
828 using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def) |
633 using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def) |
829 also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0" |
634 also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0" |
830 using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def) |
635 using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def) |
831 finally show ?thesis . |
636 finally show ?thesis . |
832 qed |
|
833 |
|
834 lemma has_fps_expansion_fps_expansion [intro]: |
|
835 assumes "open A" "0 \<in> A" "f holomorphic_on A" |
|
836 shows "f has_fps_expansion fps_expansion f 0" |
|
837 proof - |
|
838 from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A" |
|
839 by (auto simp: open_contains_ball) |
|
840 have holo: "f holomorphic_on eball 0 (ereal r)" |
|
841 using r(2) and assms(3) by auto |
|
842 from r(1) have "0 < ereal r" by simp |
|
843 also have "r \<le> fps_conv_radius (fps_expansion f 0)" |
|
844 using holo by (intro conv_radius_fps_expansion) auto |
|
845 finally have "\<dots> > 0" . |
|
846 moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)" |
|
847 using r(1) by (intro eventually_nhds_in_open) auto |
|
848 hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)" |
|
849 by eventually_elim (subst eval_fps_expansion'[OF holo], auto) |
|
850 ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def) |
|
851 qed |
637 qed |
852 |
638 |
853 lemma has_fps_expansion_imp_continuous: |
639 lemma has_fps_expansion_imp_continuous: |
854 fixes F :: "'a::{real_normed_field,banach} fps" |
640 fixes F :: "'a::{real_normed_field,banach} fps" |
855 assumes "f has_fps_expansion F" |
641 assumes "f has_fps_expansion F" |