equal
deleted
inserted
replaced
689 also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0" |
689 also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0" |
690 using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def) |
690 using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def) |
691 finally show ?thesis . |
691 finally show ?thesis . |
692 qed |
692 qed |
693 |
693 |
|
694 lemma eval_fps_has_fps_expansion: |
|
695 "fps_conv_radius F > 0 \<Longrightarrow> eval_fps F has_fps_expansion F" |
|
696 unfolding has_fps_expansion_def by simp |
|
697 |
694 lemma has_fps_expansion_imp_continuous: |
698 lemma has_fps_expansion_imp_continuous: |
695 fixes F :: "'a::{real_normed_field,banach} fps" |
699 fixes F :: "'a::{real_normed_field,banach} fps" |
696 assumes "f has_fps_expansion F" |
700 assumes "f has_fps_expansion F" |
697 shows "continuous (at 0 within A) f" |
701 shows "continuous (at 0 within A) f" |
698 proof - |
702 proof - |