# HG changeset patch
# User Manuel Eberl <manuel@pruvisto.org>
# Date 1744971964 -7200
# Node ID 904589510439e559a0f3996003b6a70429233c21
# Parent  ff4b062aae573d061e92a4a24c35f4929c31d9c7
some facts about power series

diff -r ff4b062aae57 -r 904589510439 src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Fri Apr 18 10:58:16 2025 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy	Fri Apr 18 12:26:04 2025 +0200
@@ -2392,4 +2392,64 @@
   shows   "(\<lambda>y. \<Prod>x\<in>#I. f x y) has_laurent_expansion (\<Prod>x\<in>#I. F x)"
   using assms by (induction I) (auto intro!: laurent_expansion_intros)
 
+
+subsection \<open>Formal convergence versus analytic convergence\<close>
+
+
+text \<open>
+  The convergence of a sequence of formal power series and the convergence of the functions
+  in the complex plane do not imply each other:
+
+  \<^item> If we have the sequence of constant power series $(1/n)_{n\geq 0}$, this clearly converges 
+    to the zero function analytically, but as a series of formal power series it is divergent 
+    (since the 0-th coefficient never stabilises).
+
+  \<^item> Conversely, the sequence of series $(n! x^n)_{n\geq 0}$ converges formally to $0$,
+    but the corresponding sequence of functions diverges for every $x \neq 0$.
+
+  However, if the sequence of series converges to some limit series $h$ and the corresponding
+  series of functions converges uniformly to some limit function $g(x)$, then $h$ is also a
+  series expansion of $g(x)$, i.e.\ in that case, formal and analytic convergence agree.
+\<close>
+proposition uniform_limit_imp_fps_expansion_eq:
+  fixes f :: "'a \<Rightarrow> complex fps"
+  assumes lim1: "(f \<longlongrightarrow> h) F"
+  assumes lim2: "uniform_limit A (\<lambda>x z. f' x z) g' F"
+  assumes expansions: "eventually (\<lambda>x. f' x has_fps_expansion f x) F" "g' has_fps_expansion g"
+  assumes holo: "eventually (\<lambda>x. f' x holomorphic_on A) F"
+  assumes A: "open A" "0 \<in> A"
+  assumes nontriv [simp]: "F \<noteq> bot"
+  shows "g = h"
+proof (rule fps_ext)
+  fix n :: nat
+  have "eventually (\<lambda>x. fps_nth (f x) n = fps_nth h n) F"
+    using lim1 unfolding tendsto_fps_iff by blast
+  hence "eventually (\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n = fps_nth h n) F"
+    using expansions(1)
+  proof eventually_elim
+    case (elim x)
+    have "fps_nth (f x) n = (deriv ^^ n) (f' x) 0 / fact n"
+      by (rule fps_nth_fps_expansion) (use elim in auto)
+    with elim show ?case
+      by simp
+  qed
+  hence "((\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n) \<longlongrightarrow> fps_nth h n) F"
+    by (simp add: tendsto_eventually)
+
+  moreover have "((\<lambda>x. (deriv ^^ n) (f' x) 0) \<longlongrightarrow> (deriv ^^ n) g' 0) F"
+    using lim2
+  proof (rule higher_deriv_complex_uniform_limit)
+    show "eventually (\<lambda>x. f' x holomorphic_on A) F"
+      using holo by eventually_elim auto
+  qed (use A in auto)
+  hence "((\<lambda>x. (deriv ^^ n) (f' x) 0 / fact n) \<longlongrightarrow> (deriv ^^ n) g' 0 / fact n) F"
+    by (intro tendsto_divide) auto
+
+  ultimately have "fps_nth h n = (deriv ^^ n) g' 0 / fact n"
+    using tendsto_unique[OF nontriv] by blast
+  also have "\<dots> = fps_nth g n"
+    by (rule fps_nth_fps_expansion [symmetric]) fact
+  finally show "fps_nth g n = fps_nth h n" ..
+qed
+
 end
diff -r ff4b062aae57 -r 904589510439 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 18 10:58:16 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Fri Apr 18 12:26:04 2025 +0200
@@ -996,25 +996,6 @@
 qed simp_all
 
 
-subsection \<open>Truncation\<close>
-
-text \<open>
-  Truncation of formal power series: all monomials $cx^k$ with $k\geq n$ are removed;
-  the remainder is a polynomial of degree at most $n-1$.
-\<close>
-definition truncate_fps :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a :: zero fps" where
-  "truncate_fps n F = Abs_fps (\<lambda>k. if k \<ge> n then 0 else fps_nth F k)"
-
-lemma fps_nth_truncate' [simp]:
-  "k \<ge> n \<Longrightarrow> fps_nth (truncate_fps n F) k = 0"
-  "k < n \<Longrightarrow> fps_nth (truncate_fps n F) k = fps_nth F k"
-  by (auto simp: truncate_fps_def)
-
-lemma truncate_fps_eq_truncate_fps_iff:
-  "truncate_fps N F = truncate_fps N G \<longleftrightarrow> (\<forall>n<N. fps_nth F n = fps_nth G n)"
-  by (auto simp: fps_eq_iff truncate_fps_def)
-
-
 subsection \<open>Shifting and slicing\<close>
 
 definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
@@ -1364,6 +1345,15 @@
   "k < n \<Longrightarrow> (fps_cutoff n f * g) $ k = (f * g) $ k"
   by (simp add: fps_mult_nth)
 
+lemma fps_cutoff_add: "fps_cutoff n (f + g :: 'a :: monoid_add fps) = fps_cutoff n f + fps_cutoff n g"
+  by (auto simp: fps_eq_iff)
+
+lemma fps_cutoff_diff: "fps_cutoff n (f - g :: 'a :: group_add fps) = fps_cutoff n f - fps_cutoff n g"
+  by (auto simp: fps_eq_iff)
+
+lemma fps_cutoff_uminus: "fps_cutoff n (-f :: 'a :: group_add fps) = -fps_cutoff n f"
+  by (auto simp: fps_eq_iff)
+
 lemma fps_cutoff_right_mult_nth:
   assumes "k < n"
   shows   "(f * fps_cutoff n g) $ k = (f * g) $ k"
@@ -1372,6 +1362,22 @@
   thus ?thesis by (simp add: fps_mult_nth)
 qed
 
+lemma fps_cutoff_eq_fps_cutoff_iff:
+  "fps_cutoff n f = fps_cutoff n g \<longleftrightarrow> (\<forall>k<n. fps_nth f k = fps_nth g k)"
+  by (subst fps_eq_iff) auto
+
+lemma fps_conv_fps_X_power_mult_fps_shift: 
+  assumes "f = 0 \<or> subdegree f \<ge> n"
+  shows   "f = fps_X ^ n * fps_shift n f"
+proof -
+  have "f = fps_X ^ n * fps_shift n f + fps_cutoff n f"
+    by (auto simp: fps_eq_iff fps_X_power_mult_nth)
+  also have "fps_cutoff n f = 0"
+    by (subst fps_cutoff_zero_iff) (use assms in auto)
+  finally show ?thesis by simp
+qed
+
+
 subsection \<open>Metrizability\<close>
 
 instantiation fps :: ("{minus,zero}") dist
@@ -1452,10 +1458,10 @@
   also in it.
 \<close>
 lemma open_fps_iff:
-  "open A \<longleftrightarrow> (\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A)"
+  "open A \<longleftrightarrow> (\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A)"
 proof
   assume "open A"
-  show "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+  show "\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
   proof
     fix F :: "'a fps"
     assume F: "F \<in> A"
@@ -1468,9 +1474,9 @@
       by (simp add: power_divide)
     then obtain n where n: "1 / 2 ^ n < e"
       by (auto simp: eventually_sequentially)
-    show "\<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+    show "\<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
     proof (rule exI[of _ n], safe)
-      fix G assume *: "truncate_fps n G = truncate_fps n F"
+      fix G assume *: "fps_cutoff n G = fps_cutoff n F"
       show "G \<in> A"
       proof (cases "G = F")
         case False
@@ -1479,7 +1485,7 @@
         also have "subdegree (G - F) \<ge> n"
         proof (rule subdegree_geI)
           fix i assume "i < n"
-          hence "fps_nth (G - F) i = fps_nth (truncate_fps n G - truncate_fps n F) i"
+          hence "fps_nth (G - F) i = fps_nth (fps_cutoff n G - fps_cutoff n F) i"
             by (auto simp: fps_eq_iff)
           also from * have "\<dots> = 0"
             by simp
@@ -1495,12 +1501,12 @@
     qed
   qed
 next
-  assume *: "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+  assume *: "\<forall>F\<in>A. \<exists>n. {G. fps_cutoff n G = fps_cutoff n F} \<subseteq> A"
   show "open A"
     unfolding open_fps_def
   proof safe
     fix F assume F: "F \<in> A"
-    with * obtain n where n: "\<And>G. truncate_fps n G = truncate_fps n F \<Longrightarrow> G \<in> A"
+    with * obtain n where n: "\<And>G. fps_cutoff n G = fps_cutoff n F \<Longrightarrow> G \<in> A"
       by blast
     show "\<exists>r>0. {G. dist G F < r} \<subseteq> A"
     proof (rule exI[of _ "1 / 2 ^ n"], safe)
@@ -1514,8 +1520,8 @@
           by (auto simp: field_simps)
         hence "fps_nth (F - G) i = 0" if "i \<le> n" for i
           using that nth_less_subdegree_zero[of i "F - G"] by simp
-        hence "truncate_fps n G = truncate_fps n F"
-          by (auto simp: fps_eq_iff truncate_fps_def)
+        hence "fps_cutoff n G = fps_cutoff n F"
+          by (auto simp: fps_eq_iff fps_cutoff_def)
         thus "G \<in> A"
           by (rule n)
       qed (use \<open>F \<in> A\<close> in auto)
@@ -1523,12 +1529,12 @@
   qed
 qed
 
-lemma open_truncate_fps: "open {H. truncate_fps N H = truncate_fps N G}"
+lemma open_fps_cutoff: "open {H. fps_cutoff N H = fps_cutoff N G}"
   unfolding open_fps_iff
 proof safe
-  fix F assume F: "truncate_fps N F = truncate_fps N G"
-  show "\<exists>n. {G. truncate_fps n G = truncate_fps n F}
-             \<subseteq> {H. truncate_fps N H = truncate_fps N G}"
+  fix F assume F: "fps_cutoff N F = fps_cutoff N G"
+  show "\<exists>n. {G. fps_cutoff n G = fps_cutoff n F}
+             \<subseteq> {H. fps_cutoff N H = fps_cutoff N G}"
     by (rule exI[of _ N]) (use F in \<open>auto simp: fps_eq_iff\<close>)
 qed
 
@@ -1548,13 +1554,13 @@
   assume lim: "filterlim f (nhds (g :: 'a :: group_add fps)) F"
   show "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F" for n
   proof -
-    define S where "S = {H. truncate_fps (n+1) H = truncate_fps (n+1) g}"
+    define S where "S = {H. fps_cutoff (n+1) H = fps_cutoff (n+1) g}"
     have S: "open S" "g \<in> S"
-      unfolding S_def using open_truncate_fps[of "n+1" g] by (auto simp: S_def)
+      unfolding S_def using open_fps_cutoff[of "n+1" g] by (auto simp: S_def)
     from lim and S have "eventually (\<lambda>x. f x \<in> S) F"
       using topological_tendstoD by blast
     thus "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
-      by eventually_elim (auto simp: S_def truncate_fps_eq_truncate_fps_iff)
+      by eventually_elim (auto simp: S_def fps_cutoff_eq_fps_cutoff_iff)
   qed
 next
   assume *: "\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
@@ -1562,12 +1568,12 @@
   proof (rule topological_tendstoI)
     fix S :: "'a fps set"
     assume S: "open S" "g \<in> S"
-    then obtain N where N: "{H. truncate_fps N H = truncate_fps N g} \<subseteq> S"
+    then obtain N where N: "{H. fps_cutoff N H = fps_cutoff N g} \<subseteq> S"
       unfolding open_fps_iff by blast
     have "eventually (\<lambda>x. \<forall>n\<in>{..<N}. fps_nth (f x) n = fps_nth g n) F"
       by (subst eventually_ball_finite_distrib) (use * in auto)
-    hence "eventually (\<lambda>x. f x \<in> {H. truncate_fps N H = truncate_fps N g}) F"
-      by eventually_elim (auto simp: truncate_fps_eq_truncate_fps_iff)
+    hence "eventually (\<lambda>x. f x \<in> {H. fps_cutoff N H = fps_cutoff N g}) F"
+      by eventually_elim (auto simp: fps_cutoff_eq_fps_cutoff_iff)
     thus "eventually (\<lambda>x. f x \<in> S) F"
       by eventually_elim (use N in auto)
   qed
@@ -3040,6 +3046,105 @@
 end
 
 
+subsection \<open>Computing reciprocals via Hensel lifting\<close>
+
+lemma inverse_fps_hensel_lifting:
+  fixes F G :: "'a :: field fps" and n :: nat
+  assumes G_eq: "fps_cutoff n G = fps_cutoff n (inverse F)"
+  assumes unit: "fps_nth F 0 \<noteq> 0"
+  shows "fps_cutoff (2*n) (inverse F) = fps_cutoff (2*n) (G * (2 - F * G))"
+proof -
+  define R where "R = inverse F - G"
+  have eq: "G = inverse F - R"
+    by (simp add: R_def)
+  from assms have "fps_cutoff n R = 0"
+    by (simp add: R_def fps_cutoff_diff)
+  hence R: "R = 0 \<or> subdegree R \<ge> n"
+    by (simp add: fps_cutoff_zero_iff)
+
+  have "G * (2 - F * G) - inverse F = 
+         inverse F + F * inverse F * R * 2 - F * R\<^sup>2 - R * 2 - F * inverse F * inverse F"
+    by (simp add: eq algebra_simps power2_eq_square)
+  also have "F * inverse F = 1"
+    using unit by (simp add: inverse_mult_eq_1')
+  also have "inverse F + 1 * R * 2 - F * R\<^sup>2 - R * 2 - 1 * inverse F = -F * R\<^sup>2"
+    by (simp add: algebra_simps)
+  finally have "fps_cutoff (2*n) (G * (2 - F * G) - inverse F) = fps_cutoff (2*n) (-F * R\<^sup>2)"
+    by (rule arg_cong)
+  also have "\<dots> = 0"
+  proof (cases "-F * R\<^sup>2 = 0")
+    case False
+    have "2 * n \<le> subdegree (-F * R\<^sup>2)"
+      using False R unit by simp
+    thus ?thesis
+      by (simp add: fps_cutoff_zero_iff)
+  qed auto
+  finally show ?thesis
+    by (simp add: fps_cutoff_diff)
+qed
+
+lemma inverse_fps_hensel_lifting':
+  fixes F G :: "'a :: field fps" and n :: nat
+  assumes G_eq: "fps_cutoff n G = fps_cutoff n (inverse F)"
+  assumes unit: "fps_nth F 0 \<noteq> 0"
+  defines "P \<equiv> fps_shift n (F * G - 1)"
+  shows "fps_cutoff (2*n) (inverse F) = fps_cutoff (2*n) (G * (1 - fps_X ^ n * P))"
+proof -
+  define R where "R = inverse F - G"
+  have eq: "G = inverse F - R"
+    by (simp add: R_def)
+  from assms have "fps_cutoff n R = 0"
+    by (simp add: R_def fps_cutoff_diff)
+  hence R: "R = 0 \<or> subdegree R \<ge> n"
+    by (simp add: fps_cutoff_zero_iff)
+
+  have FG_eq: "F * G = 1 + fps_X ^ n * P"
+  proof (cases "F * G - 1 = 0")
+    case False
+    have eq: "F * G - 1 = F * (G - inverse F)"
+      using unit by (simp add: inverse_mult_eq_1' ring_distribs)
+    have "subdegree (F * (G - inverse F)) \<ge> n"
+    proof -
+      have "fps_cutoff n (G - inverse F) = 0"
+        using G_eq by (simp add: fps_cutoff_diff)
+      hence "n \<le> subdegree (G - inverse F)"
+        using False unfolding eq by (simp add: fps_cutoff_zero_iff)
+      also have "subdegree (G - inverse F) = subdegree (F * (G - inverse F))"
+        by (subst subdegree_mult) (use unit False in \<open>auto simp: eq\<close>)
+      finally have "n \<le> subdegree (F * (G - inverse F))" .
+      thus ?thesis
+        by blast
+    qed
+    hence "F * G - 1 = fps_X ^ n * P"
+      unfolding eq P_def by (intro fps_conv_fps_X_power_mult_fps_shift) auto
+    thus ?thesis
+      by (simp add: algebra_simps)
+  qed (auto simp: P_def)
+
+  have "G * (1 - fps_X ^ n * P) - inverse F = G * (2 - F * G) - inverse F"
+    by (auto simp: FG_eq)
+  also have "G * (2 - F * G) - inverse F = 
+         inverse F + F * inverse F * R * 2 - F * R\<^sup>2 - R * 2 - F * inverse F * inverse F"
+    by (simp add: eq algebra_simps power2_eq_square)
+  also have "F * inverse F = 1"
+    using unit by (simp add: inverse_mult_eq_1')
+  also have "inverse F + 1 * R * 2 - F * R\<^sup>2 - R * 2 - 1 * inverse F = -F * R\<^sup>2"
+    by (simp add: algebra_simps)
+  finally have "fps_cutoff (2*n) (G * (1 - fps_X ^ n * P) - inverse F) = fps_cutoff (2*n) (-F * R\<^sup>2)"
+    by (rule arg_cong)
+  also have "\<dots> = 0"
+  proof (cases "-F * R\<^sup>2 = 0")
+    case False
+    have "2 * n \<le> subdegree (-F * R\<^sup>2)"
+      using False R unit by simp
+    thus ?thesis
+      by (simp add: fps_cutoff_zero_iff)
+  qed auto
+  finally show ?thesis
+    by (simp add: fps_cutoff_diff)
+qed
+
+
 subsection \<open>Euclidean division\<close>
 
 instantiation fps :: (field) euclidean_ring_cancel
diff -r ff4b062aae57 -r 904589510439 src/HOL/Computational_Algebra/Polynomial_FPS.thy
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 18 10:58:16 2025 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Fri Apr 18 12:26:04 2025 +0200
@@ -313,4 +313,48 @@
 
 end
 
+
+text \<open>
+  Truncation of formal power series: all monomials $cx^k$ with $k\geq n$ are removed;
+  the remainder is a polynomial of degree at most $n-1$.
+\<close>
+lift_definition truncate_fps :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a :: zero poly" is
+  "\<lambda>n F k. if k \<ge> n then 0 else fps_nth F k"
+proof goal_cases
+  case (1 n F)
+  have "eventually (\<lambda>k. (if n \<le> k then 0 else fps_nth F k) = 0) at_top"
+    using eventually_ge_at_top[of n] by eventually_elim auto
+  thus ?case
+    by (simp add: cofinite_eq_sequentially)
+qed
+
+lemma coeff_truncate_fps' [simp]:
+  "k \<ge> n \<Longrightarrow> coeff (truncate_fps n F) k = 0"
+  "k < n \<Longrightarrow> coeff (truncate_fps n F) k = fps_nth F k"
+  by (transfer; simp; fail)+
+
+lemma coeff_truncate_fps: "coeff (truncate_fps n F) k = (if k < n then fps_nth F k else 0)"
+  by auto
+
+lemma truncate_0_fps [simp]: "truncate_fps 0 F = 0"
+  by (rule poly_eqI) auto
+
+lemma degree_truncate_fps: "n > 0 \<Longrightarrow> degree (truncate_fps n F) < n"
+  by (rule degree_lessI) auto
+
+lemma truncate_fps_0 [simp]: "truncate_fps n 0 = 0"
+  by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_add: "truncate_fps n (f + g) = truncate_fps n f + truncate_fps n g"
+  by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_diff: "truncate_fps n (f - g) = truncate_fps n f - truncate_fps n g"
+  by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma truncate_fps_uminus: "truncate_fps n (-f) = -truncate_fps n f"
+  by (rule poly_eqI) (auto simp: coeff_truncate_fps)
+
+lemma fps_of_poly_truncate [simp]: "fps_of_poly (truncate_fps n f) = fps_cutoff n f"
+  by (rule fps_ext) auto
+
 end