# HG changeset patch # User Manuel Eberl # Date 1744987891 -7200 # Node ID 42964a5121a9d5cf937f7d5d008395e85d640fda # Parent b4d4ad6fb9bdffb321a14ef73b5d2bc50ec26000 more about formal convergence of power series diff -r b4d4ad6fb9bd -r 42964a5121a9 src/HOL/Analysis/FPS_Convergence.thy --- 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 "\x. x \ A \ f x has_fps_expansion F x" + shows "(\z. \x\A. f x z) has_fps_expansion (\x\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 \ 'b :: {banach, real_normed_div_algebra, comm_ring_1} fps" + assumes "\x. x \ A \ f x has_fps_expansion F x" + shows "(\z. \x\A. f x z) has_fps_expansion (\x\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 "(\x. exp (c * x)) has_fps_expansion fps_exp c" diff -r b4d4ad6fb9bd -r 42964a5121a9 src/HOL/Computational_Algebra/Formal_Power_Series.thy --- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Apr 18 16:51:23 2025 +0200 +++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Apr 18 16:51:31 2025 +0200 @@ -1538,6 +1538,18 @@ by (rule exI[of _ N]) (use F in \auto simp: fps_eq_iff\) qed +lemma eventually_fps_nth_eq_nhds_fps_strong: + "eventually (\g. \k\n. fps_nth g k = fps_nth f k) (nhds f)" +proof - + have "eventually (\g. g \ {g. fps_cutoff (n+1) g = fps_cutoff (n+1) f}) (nhds f)" + by (rule eventually_nhds_in_open, rule open_fps_cutoff) auto + thus ?thesis + by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff) +qed + +lemma eventually_fps_nth_eq_nhds_fps: "eventually (\g. fps_nth g k = fps_nth f k) (nhds f)" + using eventually_fps_nth_eq_nhds_fps_strong[of k] by eventually_elim auto + text \ A family of formal power series $f_x$ tends to a limit series $g$ at some filter $F$ iff for any $N\geq 0$, the set of $x$ for which $f_x$ and $G$ agree on the first $N$ coefficients @@ -2213,6 +2225,9 @@ lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g" by (simp add: fps_inverse_mult_divring) +lemma inverse_prod_fps: "inverse (prod f A) = (\x\A. inverse (f x) :: 'a :: field fps)" + by (induction A rule: infinite_finite_induct) (auto simp: fps_inverse_mult) + lemma fps_lr_inverse_gp_ring1: fixes ones ones_inv :: "'a :: ring_1 fps" defines "ones \ Abs_fps (\n. 1)" @@ -2435,6 +2450,92 @@ using subdegree_lr_inverse(2) by (simp add: fps_inverse_def) +lemma fps_right_inverse_constructor_rec: + "n > 0 \ fps_right_inverse_constructor f a n = + -a * sum (\i. fps_nth f i * fps_right_inverse_constructor f a (n - i)) {1..n}" + by (cases n) auto + +lemma fps_right_inverse_constructor_cong: + assumes "\k. k \ n \ fps_nth f k = fps_nth g k" + shows "fps_right_inverse_constructor f c n = fps_right_inverse_constructor g c n" + using assms +proof (induction n rule: less_induct) + case (less n) + show ?case + proof (cases "n > 0") + case n: True + have "fps_right_inverse_constructor f c n = + -c * sum (\i. fps_nth f i * fps_right_inverse_constructor f c (n - i)) {1..n}" + by (subst fps_right_inverse_constructor_rec) (use n in auto) + also have "sum (\i. fps_nth f i * fps_right_inverse_constructor f c (n - i)) {1..n} = + sum (\i. fps_nth g i * fps_right_inverse_constructor g c (n - i)) {1..n}" + by (intro sum.cong refl arg_cong2[of _ _ _ _ "(*)"] less) (use assms in auto) + also have "-c * \ = fps_right_inverse_constructor g c n" + by (subst (2) fps_right_inverse_constructor_rec) (use n in auto) + finally show ?thesis . + qed auto +qed + +lemma fps_cutoff_inverse: + fixes f :: "'a :: field fps" + assumes "fps_nth f 0 \ 0" + shows "fps_cutoff n (inverse (fps_cutoff n f)) = fps_cutoff n (inverse f)" +proof (cases "n = 0") + case True + show ?thesis + by (simp add: True) +next + case False + show ?thesis + proof (subst fps_cutoff_eq_fps_cutoff_iff, safe) + fix k assume "k < n" + have "fps_nth (inverse (fps_cutoff n f)) k = + fps_right_inverse_constructor (fps_cutoff n f) (inverse (fps_nth f 0)) k" + using False by (simp add: fps_inverse_def) + also have "\ = fps_right_inverse_constructor f (inverse (fps_nth f 0)) k" + by (rule fps_right_inverse_constructor_cong) (use \k < n\ in auto) + also have "\ = fps_nth (inverse f) k" + using False by (simp add: fps_inverse_def) + finally show "fps_nth (inverse (fps_cutoff n f)) k = fps_nth (inverse f) k" . + qed +qed + +lemma tendsto_inverse_fps_aux: + fixes f :: "'a :: field fps" + assumes "fps_nth f 0 \ 0" + shows "((\f. inverse f) \ inverse f) (at f)" + unfolding tendsto_fps_iff +proof + fix n :: nat + have "eventually (\g. \k\n. fps_nth g k = fps_nth f k) (nhds f)" + by (rule eventually_fps_nth_eq_nhds_fps_strong) + hence "eventually (\g. \k\n. fps_nth g k = fps_nth f k) (at f)" + using eventually_nhds_conv_at by blast + thus "eventually (\g. fps_nth (inverse g) n = fps_nth (inverse f) n) (at f)" + proof eventually_elim + case (elim g) + from elim have "fps_nth g 0 = fps_nth f 0" + by auto + with assms have [simp]: "fps_nth g 0 \ 0" + by simp + have "fps_cutoff (n+1) (inverse f) = fps_cutoff (n+1) (inverse (fps_cutoff (n+1) f))" + by (rule fps_cutoff_inverse [symmetric]) fact + also have "fps_cutoff (n+1) f = fps_cutoff (n+1) g" + by (subst fps_cutoff_eq_fps_cutoff_iff) (use elim in auto) + also have "fps_cutoff (n+1) (inverse \) = fps_cutoff (n+1) (inverse g)" + by (rule fps_cutoff_inverse) auto + finally show ?case + by (subst (asm) fps_cutoff_eq_fps_cutoff_iff) auto + qed +qed + +lemma tendsto_inverse_fps [tendsto_intros]: + fixes g :: "'a :: field fps" + assumes "(f \ g) F" + assumes "fps_nth g 0 \ 0" + shows "((\x. inverse (f x)) \ inverse g) F" + by (rule tendsto_compose[OF tendsto_inverse_fps_aux assms(1)]) fact + lemma fps_div_zero [simp]: "0 div (g :: 'a :: {comm_monoid_add,inverse,mult_zero,uminus} fps) = 0" by (simp add: fps_divide_def)