--- a/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 18 16:51:23 2025 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 18 16:51:31 2025 +0200
@@ -846,6 +846,17 @@
with radius show ?thesis by (auto simp: has_fps_expansion_def)
qed
+lemma has_fps_expansion_sum [fps_expansion_intros]:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x has_fps_expansion F x"
+ shows "(\<lambda>z. \<Sum>x\<in>A. f x z) has_fps_expansion (\<Sum>x\<in>A. F x)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: fps_expansion_intros)
+
+lemma has_fps_expansion_prod [fps_expansion_intros]:
+ fixes F :: "'a \<Rightarrow> 'b :: {banach, real_normed_div_algebra, comm_ring_1} fps"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x has_fps_expansion F x"
+ shows "(\<lambda>z. \<Prod>x\<in>A. f x z) has_fps_expansion (\<Prod>x\<in>A. F x)"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: fps_expansion_intros)
+
lemma has_fps_expansion_exp [fps_expansion_intros]:
fixes c :: "'a :: {banach, real_normed_field}"
shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c"