# HG changeset patch # User Manuel Eberl # Date 1745365086 -7200 # Node ID 5160b68e78a959613eaccab7f933772593a29a64 # Parent ad31be996dcbfa3ec4c595177cc85e3042013955 some material on power series and infinite products diff -r ad31be996dcb -r 5160b68e78a9 src/HOL/Analysis/FPS_Convergence.thy --- 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 \ 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" diff -r ad31be996dcb -r 5160b68e78a9 src/HOL/Analysis/Infinite_Products.thy --- 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\Absolutely convergent products\ definition\<^marker>\tag important\ abs_convergent_prod :: "(nat \ _) \ 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" "\n. f n > 0" + shows "(\n. ln (f n)) sums (ln P)" +proof - + have nz: "f n \ 0" for n + using assms(2)[of n] by simp + have "P \ 0" + using has_prod_eq_0_iff[OF assms(1)] by (auto simp: nz) + + have "(\n. \k P" + using has_prod_imp_tendsto'[OF assms(1)] by simp + hence "(\n. ln (\k ln P" + by (intro tendsto_intros \P \ 0\) + also have "(\n. ln (\kn. \k real" assumes f: "convergent_prod f" and 0: "\x. f x > 0" diff -r ad31be996dcb -r 5160b68e78a9 src/HOL/Analysis/Summation_Tests.thy --- 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 (\n. real n powi c) \ c < -1" +proof - + have "summable (\n. real n powi c) \ summable (\n. real (Suc n) powi c)" + by (subst summable_Suc_iff) auto + also have "(\n. real (Suc n) powi c) = (\n. real (Suc n) powr of_int c)" + by (subst powr_real_of_int') auto + also have "summable \ \ summable (\n. real n powr of_int c)" + by (subst summable_Suc_iff) auto + also have "\ \ c < -1" + by (subst summable_real_powr_iff) auto + finally show ?thesis . +qed + lemma inverse_power_summable: assumes s: "s \ 2" shows "summable (\n. inverse (of_nat n ^ s :: 'a :: {real_normed_div_algebra,banach}))" diff -r ad31be996dcb -r 5160b68e78a9 src/HOL/Complex_Analysis/Laurent_Convergence.thy --- 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 \ r" +proof - + define n where "n = subdegree F" + have "fps_conv_radius (fps_expansion f 0) \ 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 "(\n. fps_nth F n * z ^ n) sums f z" +proof - + have r: "fps_conv_radius F \ 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 (\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}"