--- a/src/HOL/Analysis/FPS_Convergence.thy Tue Apr 22 22:06:52 2025 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Wed Apr 23 01:38:06 2025 +0200
@@ -691,6 +691,10 @@
finally show ?thesis .
qed
+lemma eval_fps_has_fps_expansion:
+ "fps_conv_radius F > 0 \<Longrightarrow> eval_fps F has_fps_expansion F"
+ unfolding has_fps_expansion_def by simp
+
lemma has_fps_expansion_imp_continuous:
fixes F :: "'a::{real_normed_field,banach} fps"
assumes "f has_fps_expansion F"
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Apr 22 22:06:52 2025 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Wed Apr 23 01:38:06 2025 +0200
@@ -280,6 +280,7 @@
by linarith
qed
+
subsection\<open>Absolutely convergent products\<close>
definition\<^marker>\<open>tag important\<close> abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
@@ -1777,6 +1778,26 @@
by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)
qed
+lemma has_prod_imp_sums_ln_real':
+ fixes P :: real
+ assumes "f has_prod P" "\<And>n. f n > 0"
+ shows "(\<lambda>n. ln (f n)) sums (ln P)"
+proof -
+ have nz: "f n \<noteq> 0" for n
+ using assms(2)[of n] by simp
+ have "P \<noteq> 0"
+ using has_prod_eq_0_iff[OF assms(1)] by (auto simp: nz)
+
+ have "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> P"
+ using has_prod_imp_tendsto'[OF assms(1)] by simp
+ hence "(\<lambda>n. ln (\<Prod>k<n. f k)) \<longlonglongrightarrow> ln P"
+ by (intro tendsto_intros \<open>P \<noteq> 0\<close>)
+ also have "(\<lambda>n. ln (\<Prod>k<n. f k)) = (\<lambda>n. \<Sum>k<n. ln (f k))"
+ by (subst ln_prod) (auto simp: nz)
+ finally show ?thesis
+ by (simp add: sums_def)
+qed
+
lemma summable_ln_real:
fixes f :: "nat \<Rightarrow> real"
assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
--- a/src/HOL/Analysis/Summation_Tests.thy Tue Apr 22 22:06:52 2025 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Wed Apr 23 01:38:06 2025 +0200
@@ -287,6 +287,20 @@
finally show ?thesis .
qed
+lemma summable_power_int_real_iff:
+ "summable (\<lambda>n. real n powi c) \<longleftrightarrow> c < -1"
+proof -
+ have "summable (\<lambda>n. real n powi c) \<longleftrightarrow> summable (\<lambda>n. real (Suc n) powi c)"
+ by (subst summable_Suc_iff) auto
+ also have "(\<lambda>n. real (Suc n) powi c) = (\<lambda>n. real (Suc n) powr of_int c)"
+ by (subst powr_real_of_int') auto
+ also have "summable \<dots> \<longleftrightarrow> summable (\<lambda>n. real n powr of_int c)"
+ by (subst summable_Suc_iff) auto
+ also have "\<dots> \<longleftrightarrow> c < -1"
+ by (subst summable_real_powr_iff) auto
+ finally show ?thesis .
+qed
+
lemma inverse_power_summable:
assumes s: "s \<ge> 2"
shows "summable (\<lambda>n. inverse (of_nat n ^ s :: 'a :: {real_normed_div_algebra,banach}))"
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Tue Apr 22 22:06:52 2025 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Wed Apr 23 01:38:06 2025 +0200
@@ -1555,6 +1555,19 @@
using assms unfolding fps_eq_iff
by (auto simp: fps_eq_iff fps_nth_fps_expansion fps_expansion_def)
+lemma holomorphic_on_imp_fps_conv_radius_ge:
+ assumes "f has_fps_expansion F" "f holomorphic_on eball 0 r"
+ shows "fps_conv_radius F \<ge> r"
+proof -
+ define n where "n = subdegree F"
+ have "fps_conv_radius (fps_expansion f 0) \<ge> r"
+ by (intro conv_radius_fps_expansion assms)
+ also have "fps_expansion f 0 = F"
+ using assms by (intro fps_expansion_eqI)
+ finally show ?thesis
+ by simp
+qed
+
lemma has_fps_expansion_imp_eval_fps_eq:
assumes "f has_fps_expansion F" "norm z < r"
assumes "f holomorphic_on ball 0 r"
@@ -1572,6 +1585,31 @@
by simp
qed
+lemma has_fps_expansion_imp_sums_complex:
+ fixes F :: "complex fps"
+ assumes "f has_fps_expansion F" "f holomorphic_on eball 0 r" "ereal (norm z) < r"
+ shows "(\<lambda>n. fps_nth F n * z ^ n) sums f z"
+proof -
+ have r: "fps_conv_radius F \<ge> r"
+ using assms(1,2) by (rule holomorphic_on_imp_fps_conv_radius_ge)
+ from assms obtain R where R: "norm z < R" "ereal R < r"
+ using ereal_dense2 less_ereal.simps(1) by blast
+ have z: "norm z < fps_conv_radius F"
+ using r R assms(3) by order
+
+ have "summable (\<lambda>n. fps_nth F n * z ^ n)"
+ by (rule summable_fps) (use z in auto)
+ moreover have "eval_fps F z = f z"
+ proof (rule has_fps_expansion_imp_eval_fps_eq[where r = R])
+ have *: "ereal (norm z) < r" if "norm z < R" for z :: complex
+ using that R ereal_le_less less_imp_le by blast
+ show "f holomorphic_on ball 0 R"
+ using assms(2) by (rule holomorphic_on_subset) (use * in auto)
+ qed (use R assms(1) in auto)
+ ultimately show ?thesis
+ unfolding eval_fps_def sums_iff by simp
+qed
+
lemma fls_conv_radius_ge:
assumes "f has_laurent_expansion F"
assumes "f holomorphic_on eball 0 r - {0}"