src/HOL/Analysis/FPS_Convergence.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69517 dc20f278e8f3 child 69597 ff784d5a5bfb permissions -rw-r--r--
capitalize proper names in lemma names
```     1 (*
```
```     2   Title:    HOL/Analysis/FPS_Convergence.thy
```
```     3   Author:   Manuel Eberl, TU München
```
```     4
```
```     5   Connection of formal power series and actual convergent power series on Banach spaces
```
```     6   (most notably the complex numbers).
```
```     7 *)
```
```     8 section \<open>Convergence of Formal Power Series\<close>
```
```     9
```
```    10 theory FPS_Convergence
```
```    11 imports
```
```    12   Conformal_Mappings
```
```    13   Generalised_Binomial_Theorem
```
```    14   "HOL-Computational_Algebra.Formal_Power_Series"
```
```    15 begin
```
```    16
```
```    17 subsection%unimportant \<open>Balls with extended real radius\<close>
```
```    18
```
```    19 text \<open>
```
```    20   The following is a variant of @{const ball} that also allows an infinite radius.
```
```    21 \<close>
```
```    22 definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where
```
```    23   "eball z r = {z'. ereal (dist z z') < r}"
```
```    24
```
```    25 lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r"
```
```    26   by (simp add: eball_def)
```
```    27
```
```    28 lemma eball_ereal [simp]: "eball z (ereal r) = ball z r"
```
```    29   by auto
```
```    30
```
```    31 lemma eball_inf [simp]: "eball z \<infinity> = UNIV"
```
```    32   by auto
```
```    33
```
```    34 lemma eball_empty [simp]: "r \<le> 0 \<Longrightarrow> eball z r = {}"
```
```    35 proof safe
```
```    36   fix x assume "r \<le> 0" "x \<in> eball z r"
```
```    37   hence "dist z x < r" by simp
```
```    38   also have "\<dots> \<le> ereal 0" using \<open>r \<le> 0\<close> by (simp add: zero_ereal_def)
```
```    39   finally show "x \<in> {}" by simp
```
```    40 qed
```
```    41
```
```    42 lemma eball_conv_UNION_balls:
```
```    43   "eball z r = (\<Union>r'\<in>{r'. ereal r' < r}. ball z r')"
```
```    44   by (cases r) (use dense gt_ex in force)+
```
```    45
```
```    46 lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'"
```
```    47   by auto
```
```    48
```
```    49 lemma ball_eball_mono: "ereal r \<le> r' \<Longrightarrow> ball z r \<le> eball z r'"
```
```    50   using eball_mono[of "ereal r" r'] by simp
```
```    51
```
```    52 lemma open_eball [simp, intro]: "open (eball z r)"
```
```    53   by (cases r) auto
```
```    54
```
```    55
```
```    56 subsection \<open>Basic properties of convergent power series\<close>
```
```    57
```
```    58 definition%important fps_conv_radius :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> ereal" where
```
```    59   "fps_conv_radius f = conv_radius (fps_nth f)"
```
```    60
```
```    61 definition%important eval_fps :: "'a :: {banach, real_normed_div_algebra} fps \<Rightarrow> 'a \<Rightarrow> 'a" where
```
```    62   "eval_fps f z = (\<Sum>n. fps_nth f n * z ^ n)"
```
```    63
```
```    64 definition%important fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
```
```    65   "fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
```
```    66
```
```    67 lemma norm_summable_fps:
```
```    68   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
```
```    69   shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fps_nth f n * z ^ n))"
```
```    70   by (rule abs_summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
```
```    71
```
```    72 lemma summable_fps:
```
```    73   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
```
```    74   shows "norm z < fps_conv_radius f \<Longrightarrow> summable (\<lambda>n. fps_nth f n * z ^ n)"
```
```    75   by (rule summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
```
```    76
```
```    77 theorem sums_eval_fps:
```
```    78   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
```
```    79   assumes "norm z < fps_conv_radius f"
```
```    80   shows   "(\<lambda>n. fps_nth f n * z ^ n) sums eval_fps f z"
```
```    81   using assms unfolding eval_fps_def fps_conv_radius_def
```
```    82   by (intro summable_sums summable_in_conv_radius) simp_all
```
```    83
```
```    84 lemma
```
```    85   fixes r :: ereal
```
```    86   assumes "f holomorphic_on eball z0 r"
```
```    87   shows   conv_radius_fps_expansion: "fps_conv_radius (fps_expansion f z0) \<ge> r"
```
```    88     and   eval_fps_expansion: "\<And>z. z \<in> eball z0 r \<Longrightarrow> eval_fps (fps_expansion f z0) (z - z0) = f z"
```
```    89     and   eval_fps_expansion': "\<And>z. norm z < r \<Longrightarrow> eval_fps (fps_expansion f z0) z = f (z0 + z)"
```
```    90 proof -
```
```    91   have "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
```
```    92     if "z \<in> ball z0 r'" "ereal r' < r" for z r'
```
```    93   proof -
```
```    94     from that(2) have "ereal r' \<le> r" by simp
```
```    95     from assms(1) and this have "f holomorphic_on ball z0 r'"
```
```    96       by (rule holomorphic_on_subset[OF _ ball_eball_mono])
```
```    97     from holomorphic_power_series [OF this that(1)]
```
```    98       show ?thesis by (simp add: fps_expansion_def)
```
```    99   qed
```
```   100   hence *: "(\<lambda>n. fps_nth (fps_expansion f z0) n * (z - z0) ^ n) sums f z"
```
```   101     if "z \<in> eball z0 r" for z
```
```   102     using that by (subst (asm) eball_conv_UNION_balls) blast
```
```   103   show "fps_conv_radius (fps_expansion f z0) \<ge> r" unfolding fps_conv_radius_def
```
```   104   proof (rule conv_radius_geI_ex)
```
```   105     fix r' :: real assume r': "r' > 0" "ereal r' < r"
```
```   106     thus "\<exists>z. norm z = r' \<and> summable (\<lambda>n. fps_nth (fps_expansion f z0) n * z ^ n)"
```
```   107       using *[of "z0 + of_real r'"]
```
```   108       by (intro exI[of _ "of_real r'"]) (auto simp: summable_def dist_norm)
```
```   109   qed
```
```   110   show "eval_fps (fps_expansion f z0) (z - z0) = f z" if "z \<in> eball z0 r" for z
```
```   111     using *[OF that] by (simp add: eval_fps_def sums_iff)
```
```   112   show "eval_fps (fps_expansion f z0) z = f (z0 + z)" if "ereal (norm z) < r" for z
```
```   113     using *[of "z0 + z"] and that by (simp add: eval_fps_def sums_iff dist_norm)
```
```   114 qed
```
```   115
```
```   116 lemma continuous_on_eval_fps:
```
```   117   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
```
```   118   shows "continuous_on (eball 0 (fps_conv_radius f)) (eval_fps f)"
```
```   119 proof (subst continuous_on_eq_continuous_at [OF open_eball], safe)
```
```   120   fix x :: 'a assume x: "x \<in> eball 0 (fps_conv_radius f)"
```
```   121   define r where "r = (if fps_conv_radius f = \<infinity> then norm x + 1 else
```
```   122                         (norm x + real_of_ereal (fps_conv_radius f)) / 2)"
```
```   123   have r: "norm x < r \<and> ereal r < fps_conv_radius f"
```
```   124     using x by (cases "fps_conv_radius f")
```
```   125                (auto simp: r_def eball_def split: if_splits)
```
```   126
```
```   127   have "continuous_on (cball 0 r) (\<lambda>x. \<Sum>i. fps_nth f i * (x - 0) ^ i)"
```
```   128     by (rule powser_continuous_suminf) (insert r, auto simp: fps_conv_radius_def)
```
```   129   hence "continuous_on (cball 0 r) (eval_fps f)"
```
```   130     by (simp add: eval_fps_def)
```
```   131   thus "isCont (eval_fps f) x"
```
```   132     by (rule continuous_on_interior) (use r in auto)
```
```   133 qed
```
```   134
```
```   135 lemma continuous_on_eval_fps' [continuous_intros]:
```
```   136   assumes "continuous_on A g"
```
```   137   assumes "g ` A \<subseteq> eball 0 (fps_conv_radius f)"
```
```   138   shows   "continuous_on A (\<lambda>x. eval_fps f (g x))"
```
```   139   using continuous_on_compose2[OF continuous_on_eval_fps assms] .
```
```   140
```
```   141 lemma has_field_derivative_powser:
```
```   142   fixes z :: "'a :: {banach, real_normed_field}"
```
```   143   assumes "ereal (norm z) < conv_radius f"
```
```   144   shows   "((\<lambda>z. \<Sum>n. f n * z ^ n) has_field_derivative (\<Sum>n. diffs f n * z ^ n)) (at z within A)"
```
```   145 proof -
```
```   146   define K where "K = (if conv_radius f = \<infinity> then norm z + 1
```
```   147                          else (norm z + real_of_ereal (conv_radius f)) / 2)"
```
```   148   have K: "norm z < K \<and> ereal K < conv_radius f"
```
```   149     using assms by (cases "conv_radius f") (auto simp: K_def)
```
```   150   have "0 \<le> norm z" by simp
```
```   151   also from K have "\<dots> < K" by simp
```
```   152   finally have K_pos: "K > 0" by simp
```
```   153
```
```   154   have "summable (\<lambda>n. f n * of_real K ^ n)"
```
```   155     using K and K_pos by (intro summable_in_conv_radius) auto
```
```   156   moreover from K and K_pos have "norm z < norm (of_real K :: 'a)" by auto
```
```   157   ultimately show ?thesis
```
```   158     by (rule has_field_derivative_at_within [OF termdiffs_strong])
```
```   159 qed
```
```   160
```
```   161 lemma has_field_derivative_eval_fps:
```
```   162   fixes z :: "'a :: {banach, real_normed_field}"
```
```   163   assumes "norm z < fps_conv_radius f"
```
```   164   shows   "(eval_fps f has_field_derivative eval_fps (fps_deriv f) z) (at z within A)"
```
```   165 proof -
```
```   166   have "(eval_fps f has_field_derivative eval_fps (Abs_fps (diffs (fps_nth f))) z) (at z within A)"
```
```   167     using assms unfolding eval_fps_def fps_nth_Abs_fps fps_conv_radius_def
```
```   168     by (intro has_field_derivative_powser) auto
```
```   169   also have "Abs_fps (diffs (fps_nth f)) = fps_deriv f"
```
```   170     by (simp add: fps_eq_iff diffs_def)
```
```   171   finally show ?thesis .
```
```   172 qed
```
```   173
```
```   174 lemma holomorphic_on_eval_fps [holomorphic_intros]:
```
```   175   fixes z :: "'a :: {banach, real_normed_field}"
```
```   176   assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
```
```   177   shows   "eval_fps f holomorphic_on A"
```
```   178 proof (rule holomorphic_on_subset [OF _ assms])
```
```   179   show "eval_fps f holomorphic_on eball 0 (fps_conv_radius f)"
```
```   180   proof (subst holomorphic_on_open [OF open_eball], safe, goal_cases)
```
```   181     case (1 x)
```
```   182     thus ?case
```
```   183       by (intro exI[of _ "eval_fps (fps_deriv f) x"]) (auto intro: has_field_derivative_eval_fps)
```
```   184   qed
```
```   185 qed
```
```   186
```
```   187 lemma analytic_on_eval_fps:
```
```   188   fixes z :: "'a :: {banach, real_normed_field}"
```
```   189   assumes "A \<subseteq> eball 0 (fps_conv_radius f)"
```
```   190   shows   "eval_fps f analytic_on A"
```
```   191 proof (rule analytic_on_subset [OF _ assms])
```
```   192   show "eval_fps f analytic_on eball 0 (fps_conv_radius f)"
```
```   193     using holomorphic_on_eval_fps[of "eball 0 (fps_conv_radius f)"]
```
```   194     by (subst analytic_on_open) auto
```
```   195 qed
```
```   196
```
```   197 lemma continuous_eval_fps [continuous_intros]:
```
```   198   fixes z :: "'a::{real_normed_field,banach}"
```
```   199   assumes "norm z < fps_conv_radius F"
```
```   200   shows   "continuous (at z within A) (eval_fps F)"
```
```   201 proof -
```
```   202   from ereal_dense2[OF assms] obtain K :: real where K: "norm z < K" "K < fps_conv_radius F"
```
```   203     by auto
```
```   204   have "0 \<le> norm z" by simp
```
```   205   also have "norm z < K" by fact
```
```   206   finally have "K > 0" .
```
```   207   from K and \<open>K > 0\<close> have "summable (\<lambda>n. fps_nth F n * of_real K ^ n)"
```
```   208     by (intro summable_fps) auto
```
```   209   from this have "isCont (eval_fps F) z" unfolding eval_fps_def
```
```   210     by (rule isCont_powser) (use K in auto)
```
```   211   thus "continuous (at z within A)  (eval_fps F)"
```
```   212     by (simp add: continuous_at_imp_continuous_within)
```
```   213 qed
```
```   214
```
```   215
```
```   216 subsection%unimportant \<open>Lower bounds on radius of convergence\<close>
```
```   217
```
```   218 lemma fps_conv_radius_deriv:
```
```   219   fixes f :: "'a :: {banach, real_normed_field} fps"
```
```   220   shows "fps_conv_radius (fps_deriv f) \<ge> fps_conv_radius f"
```
```   221   unfolding fps_conv_radius_def
```
```   222 proof (rule conv_radius_geI_ex)
```
```   223   fix r :: real assume r: "r > 0" "ereal r < conv_radius (fps_nth f)"
```
```   224   define K where "K = (if conv_radius (fps_nth f) = \<infinity> then r + 1
```
```   225                          else (real_of_ereal (conv_radius (fps_nth f)) + r) / 2)"
```
```   226   have K: "r < K \<and> ereal K < conv_radius (fps_nth f)"
```
```   227     using r by (cases "conv_radius (fps_nth f)") (auto simp: K_def)
```
```   228   have "summable (\<lambda>n. diffs (fps_nth f) n * of_real r ^ n)"
```
```   229   proof (rule termdiff_converges)
```
```   230     fix x :: 'a assume "norm x < K"
```
```   231     hence "ereal (norm x) < ereal K" by simp
```
```   232     also have "\<dots> < conv_radius (fps_nth f)" using K by simp
```
```   233     finally show "summable (\<lambda>n. fps_nth f n * x ^ n)"
```
```   234       by (intro summable_in_conv_radius) auto
```
```   235   qed (insert K r, auto)
```
```   236   also have "\<dots> = (\<lambda>n. fps_nth (fps_deriv f) n * of_real r ^ n)"
```
```   237     by (simp add: fps_deriv_def diffs_def)
```
```   238   finally show "\<exists>z::'a. norm z = r \<and> summable (\<lambda>n. fps_nth (fps_deriv f) n * z ^ n)"
```
```   239     using r by (intro exI[of _ "of_real r"]) auto
```
```   240 qed
```
```   241
```
```   242 lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"
```
```   243   by (simp add: eval_fps_def)
```
```   244
```
```   245 lemma fps_conv_radius_norm [simp]:
```
```   246   "fps_conv_radius (Abs_fps (\<lambda>n. norm (fps_nth f n))) = fps_conv_radius f"
```
```   247   by (simp add: fps_conv_radius_def)
```
```   248
```
```   249 lemma fps_conv_radius_const [simp]: "fps_conv_radius (fps_const c) = \<infinity>"
```
```   250 proof -
```
```   251   have "fps_conv_radius (fps_const c) = conv_radius (\<lambda>_. 0 :: 'a)"
```
```   252     unfolding fps_conv_radius_def
```
```   253     by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]]) auto
```
```   254   thus ?thesis by simp
```
```   255 qed
```
```   256
```
```   257 lemma fps_conv_radius_0 [simp]: "fps_conv_radius 0 = \<infinity>"
```
```   258   by (simp only: fps_const_0_eq_0 [symmetric] fps_conv_radius_const)
```
```   259
```
```   260 lemma fps_conv_radius_1 [simp]: "fps_conv_radius 1 = \<infinity>"
```
```   261   by (simp only: fps_const_1_eq_1 [symmetric] fps_conv_radius_const)
```
```   262
```
```   263 lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>"
```
```   264   by (simp add: numeral_fps_const)
```
```   265
```
```   266 lemma fps_conv_radius_fps_X_power [simp]: "fps_conv_radius (fps_X ^ n) = \<infinity>"
```
```   267 proof -
```
```   268   have "fps_conv_radius (fps_X ^ n :: 'a fps) = conv_radius (\<lambda>_. 0 :: 'a)"
```
```   269     unfolding fps_conv_radius_def
```
```   270     by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of n]])
```
```   271        (auto simp: fps_X_power_iff)
```
```   272   thus ?thesis by simp
```
```   273 qed
```
```   274
```
```   275 lemma fps_conv_radius_fps_X [simp]: "fps_conv_radius fps_X = \<infinity>"
```
```   276   using fps_conv_radius_fps_X_power[of 1] by (simp only: power_one_right)
```
```   277
```
```   278 lemma fps_conv_radius_shift [simp]:
```
```   279   "fps_conv_radius (fps_shift n f) = fps_conv_radius f"
```
```   280   by (simp add: fps_conv_radius_def fps_shift_def conv_radius_shift)
```
```   281
```
```   282 lemma fps_conv_radius_cmult_left:
```
```   283   "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (fps_const c * f) = fps_conv_radius f"
```
```   284   unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_left)
```
```   285
```
```   286 lemma fps_conv_radius_cmult_right:
```
```   287   "c \<noteq> 0 \<Longrightarrow> fps_conv_radius (f * fps_const c) = fps_conv_radius f"
```
```   288   unfolding fps_conv_radius_def by (simp add: conv_radius_cmult_right)
```
```   289
```
```   290 lemma fps_conv_radius_uminus [simp]:
```
```   291   "fps_conv_radius (-f) = fps_conv_radius f"
```
```   292   using fps_conv_radius_cmult_left[of "-1" f]
```
```   293   by (simp flip: fps_const_neg)
```
```   294
```
```   295 lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
```
```   296   unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
```
```   297   by simp
```
```   298
```
```   299 lemma fps_conv_radius_diff: "fps_conv_radius (f - g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
```
```   300   using fps_conv_radius_add[of f "-g"] by simp
```
```   301
```
```   302 lemma fps_conv_radius_mult: "fps_conv_radius (f * g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
```
```   303   using conv_radius_mult_ge[of "fps_nth f" "fps_nth g"]
```
```   304   by (simp add: fps_mult_nth fps_conv_radius_def atLeast0AtMost)
```
```   305
```
```   306 lemma fps_conv_radius_power: "fps_conv_radius (f ^ n) \<ge> fps_conv_radius f"
```
```   307 proof (induction n)
```
```   308   case (Suc n)
```
```   309   hence "fps_conv_radius f \<le> min (fps_conv_radius f) (fps_conv_radius (f ^ n))"
```
```   310     by simp
```
```   311   also have "\<dots> \<le> fps_conv_radius (f * f ^ n)"
```
```   312     by (rule fps_conv_radius_mult)
```
```   313   finally show ?case by simp
```
```   314 qed simp_all
```
```   315
```
```   316 context
```
```   317 begin
```
```   318
```
```   319 lemma natfun_inverse_bound:
```
```   320   fixes f :: "'a :: {real_normed_field} fps"
```
```   321   assumes "fps_nth f 0 = 1" and "\<delta> > 0"
```
```   322       and summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
```
```   323       and le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
```
```   324   shows   "norm (natfun_inverse f n) \<le> inverse (\<delta> ^ n)"
```
```   325 proof (induction n rule: less_induct)
```
```   326   case (less m)
```
```   327   show ?case
```
```   328   proof (cases m)
```
```   329     case 0
```
```   330     thus ?thesis using assms by (simp add: divide_simps norm_inverse norm_divide)
```
```   331   next
```
```   332     case [simp]: (Suc n)
```
```   333     have "norm (natfun_inverse f (Suc n)) =
```
```   334             norm (\<Sum>i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))"
```
```   335       (is "_ = norm ?S") using assms
```
```   336       by (simp add: field_simps norm_mult norm_divide del: sum_cl_ivl_Suc)
```
```   337     also have "norm ?S \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))"
```
```   338       by (rule norm_sum)
```
```   339     also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (Suc n - i))"
```
```   340     proof (intro sum_mono, goal_cases)
```
```   341       case (1 i)
```
```   342       have "norm (fps_nth f i * natfun_inverse f (Suc n - i)) =
```
```   343               norm (fps_nth f i) * norm (natfun_inverse f (Suc n - i))"
```
```   344         by (simp add: norm_mult)
```
```   345       also have "\<dots> \<le> norm (fps_nth f i) * inverse (\<delta> ^ (Suc n - i))"
```
```   346         using 1 by (intro mult_left_mono less.IH) auto
```
```   347       also have "\<dots> = norm (fps_nth f i) / \<delta> ^ (Suc n - i)"
```
```   348         by (simp add: divide_simps)
```
```   349       finally show ?case .
```
```   350     qed
```
```   351     also have "\<dots> = (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) / \<delta> ^ Suc n"
```
```   352       by (subst sum_divide_distrib, rule sum.cong)
```
```   353          (insert \<open>\<delta> > 0\<close>, auto simp: field_simps power_diff)
```
```   354     also have "(\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) * \<delta> ^ i) =
```
```   355                  (\<Sum>i=0..n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i))"
```
```   356       by (subst sum.atLeast_Suc_atMost_Suc_shift) simp_all
```
```   357     also have "{0..n} = {..<Suc n}" by auto
```
```   358     also have "(\<Sum>i< Suc n. norm (fps_nth f (Suc i)) * \<delta> ^ (Suc i)) \<le>
```
```   359                  (\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ (Suc n))"
```
```   360       using \<open>\<delta> > 0\<close> by (intro sum_le_suminf ballI mult_nonneg_nonneg zero_le_power summable) auto
```
```   361     also have "\<dots> \<le> 1" by fact
```
```   362     finally show ?thesis using \<open>\<delta> > 0\<close>
```
```   363       by (simp add: divide_right_mono divide_simps)
```
```   364   qed
```
```   365 qed
```
```   366
```
```   367 private lemma fps_conv_radius_inverse_pos_aux:
```
```   368   fixes f :: "'a :: {banach, real_normed_field} fps"
```
```   369   assumes "fps_nth f 0 = 1" "fps_conv_radius f > 0"
```
```   370   shows   "fps_conv_radius (inverse f) > 0"
```
```   371 proof -
```
```   372   let ?R = "fps_conv_radius f"
```
```   373   define h where "h = Abs_fps (\<lambda>n. norm (fps_nth f n))"
```
```   374   have [simp]: "fps_conv_radius h = ?R" by (simp add: h_def)
```
```   375   have "continuous_on (eball 0 (fps_conv_radius h)) (eval_fps h)"
```
```   376     by (intro continuous_on_eval_fps)
```
```   377   hence *: "open (eval_fps h -` A \<inter> eball 0 ?R)" if "open A" for A
```
```   378     using that by (subst (asm) continuous_on_open_vimage) auto
```
```   379   have "open (eval_fps h -` {..<2} \<inter> eball 0 ?R)"
```
```   380     by (rule *) auto
```
```   381   moreover have "0 \<in> eval_fps h -` {..<2} \<inter> eball 0 ?R"
```
```   382     using assms by (auto simp: eball_def zero_ereal_def eval_fps_at_0 h_def)
```
```   383   ultimately obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "ball 0 \<epsilon> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R"
```
```   384     by (subst (asm) open_contains_ball_eq) blast+
```
```   385
```
```   386   define \<delta> where "\<delta> = real_of_ereal (min (ereal \<epsilon> / 2) (?R / 2))"
```
```   387   have \<delta>: "0 < \<delta> \<and> \<delta> < \<epsilon> \<and> ereal \<delta> < ?R"
```
```   388     using \<open>\<epsilon> > 0\<close> and assms by (cases ?R) (auto simp: \<delta>_def min_def)
```
```   389
```
```   390   have summable: "summable (\<lambda>n. norm (fps_nth f n) * \<delta> ^ n)"
```
```   391     using \<delta> by (intro summable_in_conv_radius) (simp_all add: fps_conv_radius_def)
```
```   392   hence "(\<lambda>n. norm (fps_nth f n) * \<delta> ^ n) sums eval_fps h \<delta>"
```
```   393     by (simp add: eval_fps_def summable_sums h_def)
```
```   394   hence "(\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) sums (eval_fps h \<delta> - 1)"
```
```   395     by (subst sums_Suc_iff) (auto simp: assms)
```
```   396   moreover {
```
```   397     from \<delta> have "\<delta> \<in> ball 0 \<epsilon>" by auto
```
```   398     also have "\<dots> \<subseteq> eval_fps h -` {..<2} \<inter> eball 0 ?R" by fact
```
```   399     finally have "eval_fps h \<delta> < 2" by simp
```
```   400   }
```
```   401   ultimately have le: "(\<Sum>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n) \<le> 1"
```
```   402     by (simp add: sums_iff)
```
```   403   from summable have summable: "summable (\<lambda>n. norm (fps_nth f (Suc n)) * \<delta> ^ Suc n)"
```
```   404     by (subst summable_Suc_iff)
```
```   405
```
```   406   have "0 < \<delta>" using \<delta> by blast
```
```   407   also have "\<delta> = inverse (limsup (\<lambda>n. ereal (inverse \<delta>)))"
```
```   408     using \<delta> by (subst Limsup_const) auto
```
```   409   also have "\<dots> \<le> conv_radius (natfun_inverse f)"
```
```   410     unfolding conv_radius_def
```
```   411   proof (intro ereal_inverse_antimono Limsup_mono
```
```   412            eventually_mono[OF eventually_gt_at_top[of 0]])
```
```   413     fix n :: nat assume n: "n > 0"
```
```   414     have "root n (norm (natfun_inverse f n)) \<le> root n (inverse (\<delta> ^ n))"
```
```   415       using n assms \<delta> le summable
```
```   416       by (intro real_root_le_mono natfun_inverse_bound) auto
```
```   417     also have "\<dots> = inverse \<delta>"
```
```   418       using n \<delta> by (simp add: power_inverse [symmetric] real_root_pos2)
```
```   419     finally show "ereal (inverse \<delta>) \<ge> ereal (root n (norm (natfun_inverse f n)))"
```
```   420       by (subst ereal_less_eq)
```
```   421   next
```
```   422     have "0 = limsup (\<lambda>n. 0::ereal)"
```
```   423       by (rule Limsup_const [symmetric]) auto
```
```   424     also have "\<dots> \<le> limsup (\<lambda>n. ereal (root n (norm (natfun_inverse f n))))"
```
```   425       by (intro Limsup_mono) (auto simp: real_root_ge_zero)
```
```   426     finally show "0 \<le> \<dots>" by simp
```
```   427   qed
```
```   428   also have "\<dots> = fps_conv_radius (inverse f)"
```
```   429     using assms by (simp add: fps_conv_radius_def fps_inverse_def)
```
```   430   finally show ?thesis by (simp add: zero_ereal_def)
```
```   431 qed
```
```   432
```
```   433 lemma fps_conv_radius_inverse_pos:
```
```   434   fixes f :: "'a :: {banach, real_normed_field} fps"
```
```   435   assumes "fps_nth f 0 \<noteq> 0" and "fps_conv_radius f > 0"
```
```   436   shows   "fps_conv_radius (inverse f) > 0"
```
```   437 proof -
```
```   438   let ?c = "fps_nth f 0"
```
```   439   have "fps_conv_radius (inverse f) = fps_conv_radius (fps_const ?c * inverse f)"
```
```   440     using assms by (subst fps_conv_radius_cmult_left) auto
```
```   441   also have "fps_const ?c * inverse f = inverse (fps_const (inverse ?c) * f)"
```
```   442     using assms by (simp add: fps_inverse_mult fps_const_inverse)
```
```   443   also have "fps_conv_radius \<dots> > 0" using assms
```
```   444     by (intro fps_conv_radius_inverse_pos_aux)
```
```   445        (auto simp: fps_conv_radius_cmult_left)
```
```   446   finally show ?thesis .
```
```   447 qed
```
```   448
```
```   449 end
```
```   450
```
```   451 lemma fps_conv_radius_exp [simp]:
```
```   452   fixes c :: "'a :: {banach, real_normed_field}"
```
```   453   shows "fps_conv_radius (fps_exp c) = \<infinity>"
```
```   454   unfolding fps_conv_radius_def
```
```   455 proof (rule conv_radius_inftyI'')
```
```   456   fix z :: 'a
```
```   457   have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) sums exp (norm (c * z))"
```
```   458     by (rule exp_converges)
```
```   459   also have "(\<lambda>n. norm (c * z) ^ n /\<^sub>R fact n) = (\<lambda>n. norm (fps_nth (fps_exp c) n * z ^ n))"
```
```   460     by (rule ext) (simp add: norm_divide norm_mult norm_power divide_simps power_mult_distrib)
```
```   461   finally have "summable \<dots>" by (simp add: sums_iff)
```
```   462   thus "summable (\<lambda>n. fps_nth (fps_exp c) n * z ^ n)"
```
```   463     by (rule summable_norm_cancel)
```
```   464 qed
```
```   465
```
```   466
```
```   467 subsection \<open>Evaluating power series\<close>
```
```   468
```
```   469 theorem eval_fps_deriv:
```
```   470   assumes "norm z < fps_conv_radius f"
```
```   471   shows   "eval_fps (fps_deriv f) z = deriv (eval_fps f) z"
```
```   472   by (intro DERIV_imp_deriv [symmetric] has_field_derivative_eval_fps assms)
```
```   473
```
```   474 theorem fps_nth_conv_deriv:
```
```   475   fixes f :: "complex fps"
```
```   476   assumes "fps_conv_radius f > 0"
```
```   477   shows   "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
```
```   478   using assms
```
```   479 proof (induction n arbitrary: f)
```
```   480   case 0
```
```   481   thus ?case by (simp add: eval_fps_def)
```
```   482 next
```
```   483   case (Suc n f)
```
```   484   have "(deriv ^^ Suc n) (eval_fps f) 0 = (deriv ^^ n) (deriv (eval_fps f)) 0"
```
```   485     unfolding funpow_Suc_right o_def ..
```
```   486   also have "eventually (\<lambda>z::complex. z \<in> eball 0 (fps_conv_radius f)) (nhds 0)"
```
```   487     using Suc.prems by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
```
```   488   hence "eventually (\<lambda>z. deriv (eval_fps f) z = eval_fps (fps_deriv f) z) (nhds 0)"
```
```   489     by eventually_elim (simp add: eval_fps_deriv)
```
```   490   hence "(deriv ^^ n) (deriv (eval_fps f)) 0 = (deriv ^^ n) (eval_fps (fps_deriv f)) 0"
```
```   491     by (intro higher_deriv_cong_ev refl)
```
```   492   also have "\<dots> / fact n = fps_nth (fps_deriv f) n"
```
```   493     using Suc.prems fps_conv_radius_deriv[of f]
```
```   494     by (intro Suc.IH [symmetric]) auto
```
```   495   also have "\<dots> / of_nat (Suc n) = fps_nth f (Suc n)"
```
```   496     by (simp add: fps_deriv_def del: of_nat_Suc)
```
```   497   finally show ?case by (simp add: divide_simps)
```
```   498 qed
```
```   499
```
```   500 theorem eval_fps_eqD:
```
```   501   fixes f g :: "complex fps"
```
```   502   assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0"
```
```   503   assumes "eventually (\<lambda>z. eval_fps f z = eval_fps g z) (nhds 0)"
```
```   504   shows   "f = g"
```
```   505 proof (rule fps_ext)
```
```   506   fix n :: nat
```
```   507   have "fps_nth f n = (deriv ^^ n) (eval_fps f) 0 / fact n"
```
```   508     using assms by (intro fps_nth_conv_deriv)
```
```   509   also have "(deriv ^^ n) (eval_fps f) 0 = (deriv ^^ n) (eval_fps g) 0"
```
```   510     by (intro higher_deriv_cong_ev refl assms)
```
```   511   also have "\<dots> / fact n = fps_nth g n"
```
```   512     using assms by (intro fps_nth_conv_deriv [symmetric])
```
```   513   finally show "fps_nth f n = fps_nth g n" .
```
```   514 qed
```
```   515
```
```   516 lemma eval_fps_const [simp]:
```
```   517   fixes c :: "'a :: {banach, real_normed_div_algebra}"
```
```   518   shows "eval_fps (fps_const c) z = c"
```
```   519 proof -
```
```   520   have "(\<lambda>n::nat. if n \<in> {0} then c else 0) sums (\<Sum>n\<in>{0::nat}. c)"
```
```   521     by (rule sums_If_finite_set) auto
```
```   522   also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_const c) n * z ^ n) sums (\<Sum>n\<in>{0::nat}. c)"
```
```   523     by (intro sums_cong) auto
```
```   524   also have "(\<Sum>n\<in>{0::nat}. c) = c"
```
```   525     by simp
```
```   526   finally show ?thesis
```
```   527     by (simp add: eval_fps_def sums_iff)
```
```   528 qed
```
```   529
```
```   530 lemma eval_fps_0 [simp]:
```
```   531   "eval_fps (0 :: 'a :: {banach, real_normed_div_algebra} fps) z = 0"
```
```   532   by (simp only: fps_const_0_eq_0 [symmetric] eval_fps_const)
```
```   533
```
```   534 lemma eval_fps_1 [simp]:
```
```   535   "eval_fps (1 :: 'a :: {banach, real_normed_div_algebra} fps) z = 1"
```
```   536   by (simp only: fps_const_1_eq_1 [symmetric] eval_fps_const)
```
```   537
```
```   538 lemma eval_fps_numeral [simp]:
```
```   539   "eval_fps (numeral n :: 'a :: {banach, real_normed_div_algebra} fps) z = numeral n"
```
```   540   by (simp only: numeral_fps_const eval_fps_const)
```
```   541
```
```   542 lemma eval_fps_X_power [simp]:
```
```   543   "eval_fps (fps_X ^ m :: 'a :: {banach, real_normed_div_algebra} fps) z = z ^ m"
```
```   544 proof -
```
```   545   have "(\<lambda>n::nat. if n \<in> {m} then z ^ n else 0 :: 'a) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
```
```   546     by (rule sums_If_finite_set) auto
```
```   547   also have "?this \<longleftrightarrow> (\<lambda>n::nat. fps_nth (fps_X ^ m) n * z ^ n) sums (\<Sum>n\<in>{m::nat}. z ^ n)"
```
```   548     by (intro sums_cong) (auto simp: fps_X_power_iff)
```
```   549   also have "(\<Sum>n\<in>{m::nat}. z ^ n) = z ^ m"
```
```   550     by simp
```
```   551   finally show ?thesis
```
```   552     by (simp add: eval_fps_def sums_iff)
```
```   553 qed
```
```   554
```
```   555 lemma eval_fps_X [simp]:
```
```   556   "eval_fps (fps_X :: 'a :: {banach, real_normed_div_algebra} fps) z = z"
```
```   557   using eval_fps_X_power[of 1 z] by (simp only: power_one_right)
```
```   558
```
```   559 lemma eval_fps_minus:
```
```   560   fixes f :: "'a :: {banach, real_normed_div_algebra} fps"
```
```   561   assumes "norm z < fps_conv_radius f"
```
```   562   shows   "eval_fps (-f) z = -eval_fps f z"
```
```   563   using assms unfolding eval_fps_def
```
```   564   by (subst suminf_minus [symmetric]) (auto intro!: summable_fps)
```
```   565
```
```   566 lemma eval_fps_add:
```
```   567   fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
```
```   568   assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
```
```   569   shows   "eval_fps (f + g) z = eval_fps f z + eval_fps g z"
```
```   570   using assms unfolding eval_fps_def
```
```   571   by (subst suminf_add) (auto simp: ring_distribs intro!: summable_fps)
```
```   572
```
```   573 lemma eval_fps_diff:
```
```   574   fixes f g :: "'a :: {banach, real_normed_div_algebra} fps"
```
```   575   assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
```
```   576   shows   "eval_fps (f - g) z = eval_fps f z - eval_fps g z"
```
```   577   using assms unfolding eval_fps_def
```
```   578   by (subst suminf_diff) (auto simp: ring_distribs intro!: summable_fps)
```
```   579
```
```   580 lemma eval_fps_mult:
```
```   581   fixes f g :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
```
```   582   assumes "norm z < fps_conv_radius f" "norm z < fps_conv_radius g"
```
```   583   shows   "eval_fps (f * g) z = eval_fps f z * eval_fps g z"
```
```   584 proof -
```
```   585   have "eval_fps f z * eval_fps g z =
```
```   586           (\<Sum>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i)))"
```
```   587     unfolding eval_fps_def
```
```   588   proof (subst Cauchy_product)
```
```   589     show "summable (\<lambda>k. norm (fps_nth f k * z ^ k))" "summable (\<lambda>k. norm (fps_nth g k * z ^ k))"
```
```   590       by (rule norm_summable_fps assms)+
```
```   591   qed (simp_all add: algebra_simps)
```
```   592   also have "(\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * (z ^ i * z ^ (k - i))) =
```
```   593                (\<lambda>k. \<Sum>i\<le>k. fps_nth f i * fps_nth g (k - i) * z ^ k)"
```
```   594     by (intro ext sum.cong refl) (simp add: power_add [symmetric])
```
```   595   also have "suminf \<dots> = eval_fps (f * g) z"
```
```   596     by (simp add: eval_fps_def fps_mult_nth atLeast0AtMost sum_distrib_right)
```
```   597   finally show ?thesis ..
```
```   598 qed
```
```   599
```
```   600 lemma eval_fps_shift:
```
```   601   fixes f :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
```
```   602   assumes "n \<le> subdegree f" "norm z < fps_conv_radius f"
```
```   603   shows   "eval_fps (fps_shift n f) z = (if z = 0 then fps_nth f n else eval_fps f z / z ^ n)"
```
```   604 proof (cases "z = 0")
```
```   605   case False
```
```   606   have "eval_fps (fps_shift n f * fps_X ^ n) z = eval_fps (fps_shift n f) z * z ^ n"
```
```   607     using assms by (subst eval_fps_mult) simp_all
```
```   608   also from assms have "fps_shift n f * fps_X ^ n = f"
```
```   609     by (simp add: fps_shift_times_fps_X_power)
```
```   610   finally show ?thesis using False by (simp add: field_simps)
```
```   611 qed (simp_all add: eval_fps_at_0)
```
```   612
```
```   613 lemma eval_fps_exp [simp]:
```
```   614   fixes c :: "'a :: {banach, real_normed_field}"
```
```   615   shows "eval_fps (fps_exp c) z = exp (c * z)" unfolding eval_fps_def exp_def
```
```   616   by (simp add: eval_fps_def exp_def scaleR_conv_of_real divide_simps power_mult_distrib)
```
```   617
```
```   618 lemma
```
```   619   fixes f :: "complex fps" and r :: ereal
```
```   620   assumes "\<And>z. ereal (norm z) < r \<Longrightarrow> eval_fps f z \<noteq> 0"
```
```   621   shows   fps_conv_radius_inverse: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)"
```
```   622     and   eval_fps_inverse: "\<And>z. ereal (norm z) < fps_conv_radius f \<Longrightarrow> ereal (norm z) < r \<Longrightarrow>
```
```   623                                eval_fps (inverse f) z = inverse (eval_fps f z)"
```
```   624 proof -
```
```   625   define R where "R = min (fps_conv_radius f) r"
```
```   626   have *: "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f) \<and>
```
```   627           (\<forall>z\<in>eball 0 (min (fps_conv_radius f) r). eval_fps (inverse f) z = inverse (eval_fps f z))"
```
```   628   proof (cases "min r (fps_conv_radius f) > 0")
```
```   629     case True
```
```   630     define f' where "f' = fps_expansion (\<lambda>z. inverse (eval_fps f z)) 0"
```
```   631     have holo: "(\<lambda>z. inverse (eval_fps f z)) holomorphic_on eball 0 (min r (fps_conv_radius f))"
```
```   632       using assms by (intro holomorphic_intros) auto
```
```   633     from holo have radius: "fps_conv_radius f' \<ge> min r (fps_conv_radius f)"
```
```   634       unfolding f'_def by (rule conv_radius_fps_expansion)
```
```   635     have eval_f': "eval_fps f' z = inverse (eval_fps f z)"
```
```   636       if "norm z < fps_conv_radius f" "norm z < r" for z
```
```   637       using that unfolding f'_def by (subst eval_fps_expansion'[OF holo]) auto
```
```   638
```
```   639     have "f * f' = 1"
```
```   640     proof (rule eval_fps_eqD)
```
```   641       from radius and True have "0 < min (fps_conv_radius f) (fps_conv_radius f')"
```
```   642         by (auto simp: min_def split: if_splits)
```
```   643       also have "\<dots> \<le> fps_conv_radius (f * f')" by (rule fps_conv_radius_mult)
```
```   644       finally show "\<dots> > 0" .
```
```   645     next
```
```   646       from True have "R > 0" by (auto simp: R_def)
```
```   647       hence "eventually (\<lambda>z. z \<in> eball 0 R) (nhds 0)"
```
```   648         by (intro eventually_nhds_in_open) (auto simp: zero_ereal_def)
```
```   649       thus "eventually (\<lambda>z. eval_fps (f * f') z = eval_fps 1 z) (nhds 0)"
```
```   650       proof eventually_elim
```
```   651         case (elim z)
```
```   652         hence "eval_fps (f * f') z = eval_fps f z * eval_fps f' z"
```
```   653           using radius by (intro eval_fps_mult)
```
```   654                           (auto simp: R_def min_def split: if_splits intro: less_trans)
```
```   655         also have "eval_fps f' z = inverse (eval_fps f z)"
```
```   656           using elim by (intro eval_f') (auto simp: R_def)
```
```   657         also from elim have "eval_fps f z \<noteq> 0"
```
```   658           by (intro assms) (auto simp: R_def)
```
```   659         hence "eval_fps f z * inverse (eval_fps f z) = eval_fps 1 z"
```
```   660           by simp
```
```   661         finally show "eval_fps (f * f') z = eval_fps 1 z" .
```
```   662       qed
```
```   663     qed simp_all
```
```   664     hence "f' = inverse f"
```
```   665       by (intro fps_inverse_unique [symmetric]) (simp_all add: mult_ac)
```
```   666     with eval_f' and radius show ?thesis by simp
```
```   667   next
```
```   668     case False
```
```   669     hence *: "eball 0 R = {}"
```
```   670       by (intro eball_empty) (auto simp: R_def min_def split: if_splits)
```
```   671     show ?thesis
```
```   672     proof safe
```
```   673       from False have "min r (fps_conv_radius f) \<le> 0"
```
```   674         by (simp add: min_def)
```
```   675       also have "0 \<le> fps_conv_radius (inverse f)"
```
```   676         by (simp add: fps_conv_radius_def conv_radius_nonneg)
```
```   677       finally show "min r (fps_conv_radius f) \<le> \<dots>" .
```
```   678     qed (unfold * [unfolded R_def], auto)
```
```   679   qed
```
```   680
```
```   681   from * show "fps_conv_radius (inverse f) \<ge> min r (fps_conv_radius f)" by blast
```
```   682   from * show "eval_fps (inverse f) z = inverse (eval_fps f z)"
```
```   683     if "ereal (norm z) < fps_conv_radius f" "ereal (norm z) < r" for z
```
```   684     using that by auto
```
```   685 qed
```
```   686
```
```   687 lemma
```
```   688   fixes f g :: "complex fps" and r :: ereal
```
```   689   defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
```
```   690   assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
```
```   691   assumes nz: "\<And>z. z \<in> eball 0 r \<Longrightarrow> eval_fps g z \<noteq> 0"
```
```   692   shows   fps_conv_radius_divide': "fps_conv_radius (f / g) \<ge> R"
```
```   693     and   eval_fps_divide':
```
```   694             "ereal (norm z) < R \<Longrightarrow> eval_fps (f / g) z = eval_fps f z / eval_fps g z"
```
```   695 proof -
```
```   696   from nz[of 0] and \<open>r > 0\<close> have nz': "fps_nth g 0 \<noteq> 0"
```
```   697     by (auto simp: eval_fps_at_0 zero_ereal_def)
```
```   698   have "R \<le> min r (fps_conv_radius g)"
```
```   699     by (auto simp: R_def intro: min.coboundedI2)
```
```   700   also have "min r (fps_conv_radius g) \<le> fps_conv_radius (inverse g)"
```
```   701     by (intro fps_conv_radius_inverse assms) (auto simp: zero_ereal_def)
```
```   702   finally have radius: "fps_conv_radius (inverse g) \<ge> R" .
```
```   703   have "R \<le> min (fps_conv_radius f) (fps_conv_radius (inverse g))"
```
```   704     by (intro radius min.boundedI) (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
```
```   705   also have "\<dots> \<le> fps_conv_radius (f * inverse g)"
```
```   706     by (rule fps_conv_radius_mult)
```
```   707   also have "f * inverse g = f / g"
```
```   708     by (intro fps_divide_unit [symmetric] nz')
```
```   709   finally show "fps_conv_radius (f / g) \<ge> R" .
```
```   710
```
```   711   assume z: "ereal (norm z) < R"
```
```   712   have "eval_fps (f * inverse g) z = eval_fps f z * eval_fps (inverse g) z"
```
```   713     using radius by (intro eval_fps_mult less_le_trans[OF z])
```
```   714                     (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
```
```   715   also have "eval_fps (inverse g) z = inverse (eval_fps g z)" using \<open>r > 0\<close>
```
```   716     by (intro eval_fps_inverse[where r = r] less_le_trans[OF z] nz)
```
```   717        (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
```
```   718   also have "f * inverse g = f / g" by fact
```
```   719   finally show "eval_fps (f / g) z = eval_fps f z / eval_fps g z" by (simp add: divide_simps)
```
```   720 qed
```
```   721
```
```   722 lemma
```
```   723   fixes f g :: "complex fps" and r :: ereal
```
```   724   defines "R \<equiv> Min {r, fps_conv_radius f, fps_conv_radius g}"
```
```   725   assumes "subdegree g \<le> subdegree f"
```
```   726   assumes "fps_conv_radius f > 0" "fps_conv_radius g > 0" "r > 0"
```
```   727   assumes "\<And>z. z \<in> eball 0 r \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> eval_fps g z \<noteq> 0"
```
```   728   shows   fps_conv_radius_divide: "fps_conv_radius (f / g) \<ge> R"
```
```   729     and   eval_fps_divide:
```
```   730             "ereal (norm z) < R \<Longrightarrow> c = fps_nth f (subdegree g) / fps_nth g (subdegree g) \<Longrightarrow>
```
```   731                eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
```
```   732 proof -
```
```   733   define f' g' where "f' = fps_shift (subdegree g) f" and "g' = fps_shift (subdegree g) g"
```
```   734   have f_eq: "f = f' * fps_X ^ subdegree g" and g_eq: "g = g' * fps_X ^ subdegree g"
```
```   735     unfolding f'_def g'_def by (rule subdegree_decompose' le_refl | fact)+
```
```   736   have subdegree: "subdegree f' = subdegree f - subdegree g" "subdegree g' = 0"
```
```   737     using assms(2) by (simp_all add: f'_def g'_def)
```
```   738   have [simp]: "fps_conv_radius f' = fps_conv_radius f" "fps_conv_radius g' = fps_conv_radius g"
```
```   739     by (simp_all add: f'_def g'_def)
```
```   740   have [simp]: "fps_nth f' 0 = fps_nth f (subdegree g)"
```
```   741                "fps_nth g' 0 = fps_nth g (subdegree g)" by (simp_all add: f'_def g'_def)
```
```   742   have g_nz: "g \<noteq> 0"
```
```   743   proof -
```
```   744     define z :: complex where "z = (if r = \<infinity> then 1 else of_real (real_of_ereal r / 2))"
```
```   745     from \<open>r > 0\<close> have "z \<in> eball 0 r"
```
```   746       by (cases r) (auto simp: z_def eball_def)
```
```   747     moreover have "z \<noteq> 0" using \<open>r > 0\<close>
```
```   748       by (cases r) (auto simp: z_def)
```
```   749     ultimately have "eval_fps g z \<noteq> 0" by (rule assms(6))
```
```   750     thus "g \<noteq> 0" by auto
```
```   751   qed
```
```   752   have fg: "f / g = f' * inverse g'"
```
```   753     by (subst f_eq, subst (2) g_eq) (insert g_nz, simp add: fps_divide_unit)
```
```   754
```
```   755   have g'_nz: "eval_fps g' z \<noteq> 0" if z: "norm z < min r (fps_conv_radius g)" for z
```
```   756   proof (cases "z = 0")
```
```   757     case False
```
```   758     with assms and z have "eval_fps g z \<noteq> 0" by auto
```
```   759     also from z have "eval_fps g z = eval_fps g' z * z ^ subdegree g"
```
```   760       by (subst g_eq) (auto simp: eval_fps_mult)
```
```   761     finally show ?thesis by auto
```
```   762   qed (insert \<open>g \<noteq> 0\<close>, auto simp: g'_def eval_fps_at_0)
```
```   763
```
```   764   have "R \<le> min (min r (fps_conv_radius g)) (fps_conv_radius g')"
```
```   765     by (auto simp: R_def min.coboundedI1 min.coboundedI2)
```
```   766   also have "\<dots> \<le> fps_conv_radius (inverse g')"
```
```   767     using g'_nz by (rule fps_conv_radius_inverse)
```
```   768   finally have conv_radius_inv: "R \<le> fps_conv_radius (inverse g')" .
```
```   769   hence "R \<le> fps_conv_radius (f' * inverse g')"
```
```   770     by (intro order.trans[OF _ fps_conv_radius_mult])
```
```   771        (auto simp: R_def intro: min.coboundedI1 min.coboundedI2)
```
```   772   thus "fps_conv_radius (f / g) \<ge> R" by (simp add: fg)
```
```   773
```
```   774   fix z c :: complex assume z: "ereal (norm z) < R"
```
```   775   assume c: "c = fps_nth f (subdegree g) / fps_nth g (subdegree g)"
```
```   776   show "eval_fps (f / g) z = (if z = 0 then c else eval_fps f z / eval_fps g z)"
```
```   777   proof (cases "z = 0")
```
```   778     case False
```
```   779     from z and conv_radius_inv have "ereal (norm z) < fps_conv_radius (inverse g')"
```
```   780       by simp
```
```   781     with z have "eval_fps (f / g) z = eval_fps f' z * eval_fps (inverse g') z"
```
```   782       unfolding fg by (subst eval_fps_mult) (auto simp: R_def)
```
```   783     also have "eval_fps (inverse g') z = inverse (eval_fps g' z)"
```
```   784       using z by (intro eval_fps_inverse[of "min r (fps_conv_radius g')"] g'_nz) (auto simp: R_def)
```
```   785     also have "eval_fps f' z * \<dots> = eval_fps f z / eval_fps g z"
```
```   786       using z False assms(2) by (simp add: f'_def g'_def eval_fps_shift R_def)
```
```   787     finally show ?thesis using False by simp
```
```   788   qed (simp_all add: eval_fps_at_0 fg field_simps c)
```
```   789 qed
```
```   790
```
```   791
```
```   792 subsection \<open>Power series expansion of complex functions\<close>
```
```   793
```
```   794 text \<open>
```
```   795   This predicate contains the notion that the given formal power series converges
```
```   796   in some disc of positive radius around the origin and is equal to the given complex
```
```   797   function there.
```
```   798
```
```   799   This relationship is unique in the sense that no complex function can have more than
```
```   800   one formal power series to which it expands, and if two holomorphic functions that are
```
```   801   holomorphic on a connected open set around the origin and have the same power series
```
```   802   expansion, they must be equal on that set.
```
```   803
```
```   804   More concrete statements about the radius of convergence can usually be made, but for
```
```   805   many purposes, the statment that the series converges to the function in some neighbourhood
```
```   806   of the origin is enough, and that can be shown almost fully automatically in most cases,
```
```   807   as there are straightforward introduction rules to show this.
```
```   808
```
```   809   In particular, when one wants to relate the coefficients of the power series to the
```
```   810   values of the derivatives of the function at the origin, or if one wants to approximate
```
```   811   the coefficients of the series with the singularities of the function, this predicate
```
```   812   is enough.
```
```   813 \<close>
```
```   814 definition%important
```
```   815   has_fps_expansion :: "('a :: {banach,real_normed_div_algebra} \<Rightarrow> 'a) \<Rightarrow> 'a fps \<Rightarrow> bool"
```
```   816   (infixl "has'_fps'_expansion" 60)
```
```   817   where "(f has_fps_expansion F) \<longleftrightarrow>
```
```   818             fps_conv_radius F > 0 \<and> eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
```
```   819
```
```   820 named_theorems fps_expansion_intros
```
```   821
```
```   822 lemma fps_nth_fps_expansion:
```
```   823   fixes f :: "complex \<Rightarrow> complex"
```
```   824   assumes "f has_fps_expansion F"
```
```   825   shows   "fps_nth F n = (deriv ^^ n) f 0 / fact n"
```
```   826 proof -
```
```   827   have "fps_nth F n = (deriv ^^ n) (eval_fps F) 0 / fact n"
```
```   828     using assms by (intro fps_nth_conv_deriv) (auto simp: has_fps_expansion_def)
```
```   829   also have "(deriv ^^ n) (eval_fps F) 0 = (deriv ^^ n) f 0"
```
```   830     using assms by (intro higher_deriv_cong_ev) (auto simp: has_fps_expansion_def)
```
```   831   finally show ?thesis .
```
```   832 qed
```
```   833
```
```   834 lemma has_fps_expansion_fps_expansion [intro]:
```
```   835   assumes "open A" "0 \<in> A" "f holomorphic_on A"
```
```   836   shows   "f has_fps_expansion fps_expansion f 0"
```
```   837 proof -
```
```   838   from assms(1,2) obtain r where r: "r > 0 " "ball 0 r \<subseteq> A"
```
```   839     by (auto simp: open_contains_ball)
```
```   840   have holo: "f holomorphic_on eball 0 (ereal r)"
```
```   841     using r(2) and assms(3) by auto
```
```   842   from r(1) have "0 < ereal r" by simp
```
```   843   also have "r \<le> fps_conv_radius (fps_expansion f 0)"
```
```   844     using holo by (intro conv_radius_fps_expansion) auto
```
```   845   finally have "\<dots> > 0" .
```
```   846   moreover have "eventually (\<lambda>z. z \<in> ball 0 r) (nhds 0)"
```
```   847     using r(1) by (intro eventually_nhds_in_open) auto
```
```   848   hence "eventually (\<lambda>z. eval_fps (fps_expansion f 0) z = f z) (nhds 0)"
```
```   849     by eventually_elim (subst eval_fps_expansion'[OF holo], auto)
```
```   850   ultimately show ?thesis using r(1) by (auto simp: has_fps_expansion_def)
```
```   851 qed
```
```   852
```
```   853 lemma has_fps_expansion_imp_continuous:
```
```   854   fixes F :: "'a::{real_normed_field,banach} fps"
```
```   855   assumes "f has_fps_expansion F"
```
```   856   shows   "continuous (at 0 within A) f"
```
```   857 proof -
```
```   858   from assms have "isCont (eval_fps F) 0"
```
```   859     by (intro continuous_eval_fps) (auto simp: has_fps_expansion_def zero_ereal_def)
```
```   860   also have "?this \<longleftrightarrow> isCont f 0" using assms
```
```   861     by (intro isCont_cong) (auto simp: has_fps_expansion_def)
```
```   862   finally have "isCont f 0" .
```
```   863   thus "continuous (at 0 within A) f"
```
```   864     by (simp add: continuous_at_imp_continuous_within)
```
```   865 qed
```
```   866
```
```   867 lemma has_fps_expansion_const [simp, intro, fps_expansion_intros]:
```
```   868   "(\<lambda>_. c) has_fps_expansion fps_const c"
```
```   869   by (auto simp: has_fps_expansion_def)
```
```   870
```
```   871 lemma has_fps_expansion_0 [simp, intro, fps_expansion_intros]:
```
```   872   "(\<lambda>_. 0) has_fps_expansion 0"
```
```   873   by (auto simp: has_fps_expansion_def)
```
```   874
```
```   875 lemma has_fps_expansion_1 [simp, intro, fps_expansion_intros]:
```
```   876   "(\<lambda>_. 1) has_fps_expansion 1"
```
```   877   by (auto simp: has_fps_expansion_def)
```
```   878
```
```   879 lemma has_fps_expansion_numeral [simp, intro, fps_expansion_intros]:
```
```   880   "(\<lambda>_. numeral n) has_fps_expansion numeral n"
```
```   881   by (auto simp: has_fps_expansion_def)
```
```   882
```
```   883 lemma has_fps_expansion_fps_X_power [fps_expansion_intros]:
```
```   884   "(\<lambda>x. x ^ n) has_fps_expansion (fps_X ^ n)"
```
```   885   by (auto simp: has_fps_expansion_def)
```
```   886
```
```   887 lemma has_fps_expansion_fps_X [fps_expansion_intros]:
```
```   888   "(\<lambda>x. x) has_fps_expansion fps_X"
```
```   889   by (auto simp: has_fps_expansion_def)
```
```   890
```
```   891 lemma has_fps_expansion_cmult_left [fps_expansion_intros]:
```
```   892   fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
```
```   893   assumes "f has_fps_expansion F"
```
```   894   shows   "(\<lambda>x. c * f x) has_fps_expansion fps_const c * F"
```
```   895 proof (cases "c = 0")
```
```   896   case False
```
```   897   from assms have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```   898     by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
```
```   899   moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
```
```   900     by (auto simp: has_fps_expansion_def)
```
```   901   ultimately have "eventually (\<lambda>z. eval_fps (fps_const c * F) z = c * f z) (nhds 0)"
```
```   902     by eventually_elim (simp_all add: eval_fps_mult)
```
```   903   with assms and False show ?thesis
```
```   904     by (auto simp: has_fps_expansion_def fps_conv_radius_cmult_left)
```
```   905 qed auto
```
```   906
```
```   907 lemma has_fps_expansion_cmult_right [fps_expansion_intros]:
```
```   908   fixes c :: "'a :: {banach, real_normed_div_algebra, comm_ring_1}"
```
```   909   assumes "f has_fps_expansion F"
```
```   910   shows   "(\<lambda>x. f x * c) has_fps_expansion F * fps_const c"
```
```   911 proof -
```
```   912   have "F * fps_const c = fps_const c * F"
```
```   913     by (intro fps_ext) (auto simp: mult.commute)
```
```   914   with has_fps_expansion_cmult_left [OF assms] show ?thesis
```
```   915     by (simp add: mult.commute)
```
```   916 qed
```
```   917
```
```   918 lemma has_fps_expansion_minus [fps_expansion_intros]:
```
```   919   assumes "f has_fps_expansion F"
```
```   920   shows   "(\<lambda>x. - f x) has_fps_expansion -F"
```
```   921 proof -
```
```   922   from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```   923     by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
```
```   924   moreover from assms have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
```
```   925     by (auto simp: has_fps_expansion_def)
```
```   926   ultimately have "eventually (\<lambda>x. eval_fps (-F) x = -f x) (nhds 0)"
```
```   927     by eventually_elim (auto simp: eval_fps_minus)
```
```   928   thus ?thesis using assms by (auto simp: has_fps_expansion_def)
```
```   929 qed
```
```   930
```
```   931 lemma has_fps_expansion_add [fps_expansion_intros]:
```
```   932   assumes "f has_fps_expansion F" "g has_fps_expansion G"
```
```   933   shows   "(\<lambda>x. f x + g x) has_fps_expansion F + G"
```
```   934 proof -
```
```   935   from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
```
```   936     by (auto simp: has_fps_expansion_def)
```
```   937   also have "\<dots> \<le> fps_conv_radius (F + G)"
```
```   938     by (rule fps_conv_radius_add)
```
```   939   finally have radius: "\<dots> > 0" .
```
```   940
```
```   941   from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```   942                   "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
```
```   943     by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
```
```   944   moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
```
```   945             and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
```
```   946     using assms by (auto simp: has_fps_expansion_def)
```
```   947   ultimately have "eventually (\<lambda>x. eval_fps (F + G) x = f x + g x) (nhds 0)"
```
```   948     by eventually_elim (auto simp: eval_fps_add)
```
```   949   with radius show ?thesis by (auto simp: has_fps_expansion_def)
```
```   950 qed
```
```   951
```
```   952 lemma has_fps_expansion_diff [fps_expansion_intros]:
```
```   953   assumes "f has_fps_expansion F" "g has_fps_expansion G"
```
```   954   shows   "(\<lambda>x. f x - g x) has_fps_expansion F - G"
```
```   955   using has_fps_expansion_add[of f F "\<lambda>x. - g x" "-G"] assms
```
```   956   by (simp add: has_fps_expansion_minus)
```
```   957
```
```   958 lemma has_fps_expansion_mult [fps_expansion_intros]:
```
```   959   fixes F G :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps"
```
```   960   assumes "f has_fps_expansion F" "g has_fps_expansion G"
```
```   961   shows   "(\<lambda>x. f x * g x) has_fps_expansion F * G"
```
```   962 proof -
```
```   963   from assms have "0 < min (fps_conv_radius F) (fps_conv_radius G)"
```
```   964     by (auto simp: has_fps_expansion_def)
```
```   965   also have "\<dots> \<le> fps_conv_radius (F * G)"
```
```   966     by (rule fps_conv_radius_mult)
```
```   967   finally have radius: "\<dots> > 0" .
```
```   968
```
```   969   from assms have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```   970                   "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius G)) (nhds 0)"
```
```   971     by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
```
```   972   moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
```
```   973             and "eventually (\<lambda>x. eval_fps G x = g x) (nhds 0)"
```
```   974     using assms by (auto simp: has_fps_expansion_def)
```
```   975   ultimately have "eventually (\<lambda>x. eval_fps (F * G) x = f x * g x) (nhds 0)"
```
```   976     by eventually_elim (auto simp: eval_fps_mult)
```
```   977   with radius show ?thesis by (auto simp: has_fps_expansion_def)
```
```   978 qed
```
```   979
```
```   980 lemma has_fps_expansion_inverse [fps_expansion_intros]:
```
```   981   fixes F :: "'a :: {banach, real_normed_field} fps"
```
```   982   assumes "f has_fps_expansion F"
```
```   983   assumes "fps_nth F 0 \<noteq> 0"
```
```   984   shows   "(\<lambda>x. inverse (f x)) has_fps_expansion inverse F"
```
```   985 proof -
```
```   986   have radius: "fps_conv_radius (inverse F) > 0"
```
```   987     using assms unfolding has_fps_expansion_def
```
```   988     by (intro fps_conv_radius_inverse_pos) auto
```
```   989   let ?R = "min (fps_conv_radius F) (fps_conv_radius (inverse F))"
```
```   990   from assms radius
```
```   991     have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```   992          "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius (inverse F))) (nhds 0)"
```
```   993     by (intro eventually_nhds_in_open; force simp: has_fps_expansion_def zero_ereal_def)+
```
```   994   moreover have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
```
```   995     using assms by (auto simp: has_fps_expansion_def)
```
```   996   ultimately have "eventually (\<lambda>z. eval_fps (inverse F) z = inverse (f z)) (nhds 0)"
```
```   997   proof eventually_elim
```
```   998     case (elim z)
```
```   999     hence "eval_fps (inverse F * F) z = eval_fps (inverse F) z * f z"
```
```  1000       by (subst eval_fps_mult) auto
```
```  1001     also have "eval_fps (inverse F * F) z = 1"
```
```  1002       using assms by (simp add: inverse_mult_eq_1)
```
```  1003     finally show ?case by (auto simp: divide_simps)
```
```  1004   qed
```
```  1005   with radius show ?thesis by (auto simp: has_fps_expansion_def)
```
```  1006 qed
```
```  1007
```
```  1008 lemma has_fps_expansion_exp [fps_expansion_intros]:
```
```  1009   fixes c :: "'a :: {banach, real_normed_field}"
```
```  1010   shows "(\<lambda>x. exp (c * x)) has_fps_expansion fps_exp c"
```
```  1011   by (auto simp: has_fps_expansion_def)
```
```  1012
```
```  1013 lemma has_fps_expansion_exp1 [fps_expansion_intros]:
```
```  1014   "(\<lambda>x::'a :: {banach, real_normed_field}. exp x) has_fps_expansion fps_exp 1"
```
```  1015   using has_fps_expansion_exp[of 1] by simp
```
```  1016
```
```  1017 lemma has_fps_expansion_exp_neg1 [fps_expansion_intros]:
```
```  1018   "(\<lambda>x::'a :: {banach, real_normed_field}. exp (-x)) has_fps_expansion fps_exp (-1)"
```
```  1019   using has_fps_expansion_exp[of "-1"] by simp
```
```  1020
```
```  1021 lemma has_fps_expansion_deriv [fps_expansion_intros]:
```
```  1022   assumes "f has_fps_expansion F"
```
```  1023   shows   "deriv f has_fps_expansion fps_deriv F"
```
```  1024 proof -
```
```  1025   have "eventually (\<lambda>z. z \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```  1026     using assms by (intro eventually_nhds_in_open)
```
```  1027                    (auto simp: has_fps_expansion_def zero_ereal_def)
```
```  1028   moreover from assms have "eventually (\<lambda>z. eval_fps F z = f z) (nhds 0)"
```
```  1029     by (auto simp: has_fps_expansion_def)
```
```  1030   then obtain s where "open s" "0 \<in> s" and s: "\<And>w. w \<in> s \<Longrightarrow> eval_fps F w = f w"
```
```  1031     by (auto simp: eventually_nhds)
```
```  1032   hence "eventually (\<lambda>w. w \<in> s) (nhds 0)"
```
```  1033     by (intro eventually_nhds_in_open) auto
```
```  1034   ultimately have "eventually (\<lambda>z. eval_fps (fps_deriv F) z = deriv f z) (nhds 0)"
```
```  1035   proof eventually_elim
```
```  1036     case (elim z)
```
```  1037     hence "eval_fps (fps_deriv F) z = deriv (eval_fps F) z"
```
```  1038       by (simp add: eval_fps_deriv)
```
```  1039     also have "eventually (\<lambda>w. w \<in> s) (nhds z)"
```
```  1040       using elim and \<open>open s\<close> by (intro eventually_nhds_in_open) auto
```
```  1041     hence "eventually (\<lambda>w. eval_fps F w = f w) (nhds z)"
```
```  1042       by eventually_elim (simp add: s)
```
```  1043     hence "deriv (eval_fps F) z = deriv f z"
```
```  1044       by (intro deriv_cong_ev refl)
```
```  1045     finally show ?case .
```
```  1046   qed
```
```  1047   with assms and fps_conv_radius_deriv[of F] show ?thesis
```
```  1048     by (auto simp: has_fps_expansion_def)
```
```  1049 qed
```
```  1050
```
```  1051 lemma fps_conv_radius_binomial:
```
```  1052   fixes c :: "'a :: {real_normed_field,banach}"
```
```  1053   shows "fps_conv_radius (fps_binomial c) = (if c \<in> \<nat> then \<infinity> else 1)"
```
```  1054   unfolding fps_conv_radius_def by (simp add: conv_radius_gchoose)
```
```  1055
```
```  1056 lemma fps_conv_radius_ln:
```
```  1057   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1058   shows "fps_conv_radius (fps_ln c) = (if c = 0 then \<infinity> else 1)"
```
```  1059 proof (cases "c = 0")
```
```  1060   case False
```
```  1061   have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) = 1"
```
```  1062   proof (rule conv_radius_ratio_limit_nonzero)
```
```  1063     show "(\<lambda>n. norm (1 / of_nat n :: 'a) / norm (1 / of_nat (Suc n) :: 'a)) \<longlonglongrightarrow> 1"
```
```  1064       using LIMSEQ_Suc_n_over_n by (simp add: norm_divide del: of_nat_Suc)
```
```  1065   qed auto
```
```  1066   also have "conv_radius (\<lambda>n. 1 / of_nat n :: 'a) =
```
```  1067                conv_radius (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n :: 'a)"
```
```  1068     by (intro conv_radius_cong eventually_mono[OF eventually_gt_at_top[of 0]])
```
```  1069        (simp add: norm_mult norm_divide norm_power)
```
```  1070   finally show ?thesis using False unfolding fps_ln_def
```
```  1071     by (subst  fps_conv_radius_cmult_left) (simp_all add: fps_conv_radius_def)
```
```  1072 qed (auto simp: fps_ln_def)
```
```  1073
```
```  1074 lemma fps_conv_radius_ln_nonzero [simp]:
```
```  1075   assumes "c \<noteq> (0 :: 'a :: {banach,real_normed_field,field_char_0})"
```
```  1076   shows   "fps_conv_radius (fps_ln c) = 1"
```
```  1077   using assms by (simp add: fps_conv_radius_ln)
```
```  1078
```
```  1079 lemma fps_conv_radius_sin [simp]:
```
```  1080   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1081   shows "fps_conv_radius (fps_sin c) = \<infinity>"
```
```  1082 proof (cases "c = 0")
```
```  1083   case False
```
```  1084   have "\<infinity> = conv_radius (\<lambda>n. of_real (sin_coeff n) :: 'a)"
```
```  1085   proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
```
```  1086     case (1 z)
```
```  1087     show ?case using summable_norm_sin[of z] by (simp add: norm_mult)
```
```  1088   qed
```
```  1089   also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (sin_coeff n) :: 'a)"
```
```  1090     using False by (subst conv_radius_mult_power) auto
```
```  1091   also have "\<dots> = fps_conv_radius (fps_sin c)" unfolding fps_conv_radius_def
```
```  1092     by (rule conv_radius_cong_weak) (auto simp add: fps_sin_def sin_coeff_def)
```
```  1093   finally show ?thesis by simp
```
```  1094 qed simp_all
```
```  1095
```
```  1096 lemma fps_conv_radius_cos [simp]:
```
```  1097   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1098   shows "fps_conv_radius (fps_cos c) = \<infinity>"
```
```  1099 proof (cases "c = 0")
```
```  1100   case False
```
```  1101   have "\<infinity> = conv_radius (\<lambda>n. of_real (cos_coeff n) :: 'a)"
```
```  1102   proof (rule sym, rule conv_radius_inftyI'', rule summable_norm_cancel, goal_cases)
```
```  1103     case (1 z)
```
```  1104     show ?case using summable_norm_cos[of z] by (simp add: norm_mult)
```
```  1105   qed
```
```  1106   also have "\<dots> / norm c = conv_radius (\<lambda>n. c ^ n * of_real (cos_coeff n) :: 'a)"
```
```  1107     using False by (subst conv_radius_mult_power) auto
```
```  1108   also have "\<dots> = fps_conv_radius (fps_cos c)" unfolding fps_conv_radius_def
```
```  1109     by (rule conv_radius_cong_weak) (auto simp add: fps_cos_def cos_coeff_def)
```
```  1110   finally show ?thesis by simp
```
```  1111 qed simp_all
```
```  1112
```
```  1113 lemma eval_fps_sin [simp]:
```
```  1114   fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1115   shows "eval_fps (fps_sin c) z = sin (c * z)"
```
```  1116 proof -
```
```  1117   have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) sums sin (c * z)" by (rule sin_converges)
```
```  1118   also have "(\<lambda>n. sin_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_sin c) n * z ^ n)"
```
```  1119     by (rule ext) (auto simp: sin_coeff_def fps_sin_def power_mult_distrib scaleR_conv_of_real)
```
```  1120   finally show ?thesis by (simp add: sums_iff eval_fps_def)
```
```  1121 qed
```
```  1122
```
```  1123 lemma eval_fps_cos [simp]:
```
```  1124   fixes z :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1125   shows "eval_fps (fps_cos c) z = cos (c * z)"
```
```  1126 proof -
```
```  1127   have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) sums cos (c * z)" by (rule cos_converges)
```
```  1128   also have "(\<lambda>n. cos_coeff n *\<^sub>R (c * z) ^ n) = (\<lambda>n. fps_nth (fps_cos c) n * z ^ n)"
```
```  1129     by (rule ext) (auto simp: cos_coeff_def fps_cos_def power_mult_distrib scaleR_conv_of_real)
```
```  1130   finally show ?thesis by (simp add: sums_iff eval_fps_def)
```
```  1131 qed
```
```  1132
```
```  1133 lemma cos_eq_zero_imp_norm_ge:
```
```  1134   assumes "cos (z :: complex) = 0"
```
```  1135   shows   "norm z \<ge> pi / 2"
```
```  1136 proof -
```
```  1137   from assms obtain n where "z = complex_of_real ((of_int n + 1 / 2) * pi)"
```
```  1138     by (auto simp: cos_eq_0 algebra_simps)
```
```  1139   also have "norm \<dots> = \<bar>real_of_int n + 1 / 2\<bar> * pi"
```
```  1140     by (subst norm_of_real) (simp_all add: abs_mult)
```
```  1141   also have "real_of_int n + 1 / 2 = of_int (2 * n + 1) / 2" by simp
```
```  1142   also have "\<bar>\<dots>\<bar> = of_int \<bar>2 * n + 1\<bar> / 2" by (subst abs_divide) simp_all
```
```  1143   also have "\<dots> * pi = of_int \<bar>2 * n + 1\<bar> * (pi / 2)" by simp
```
```  1144   also have "\<dots> \<ge> of_int 1 * (pi / 2)"
```
```  1145     by (intro mult_right_mono, subst of_int_le_iff) (auto simp: abs_if)
```
```  1146   finally show ?thesis by simp
```
```  1147 qed
```
```  1148
```
```  1149 lemma fps_conv_radius_tan:
```
```  1150   fixes c :: complex
```
```  1151   assumes "c \<noteq> 0"
```
```  1152   shows   "fps_conv_radius (fps_tan c) \<ge> pi / (2 * norm c)"
```
```  1153 proof -
```
```  1154   have "fps_conv_radius (fps_tan c) \<ge>
```
```  1155           Min {pi / (2 * norm c), fps_conv_radius (fps_sin c), fps_conv_radius (fps_cos c)}"
```
```  1156     unfolding fps_tan_def
```
```  1157   proof (rule fps_conv_radius_divide)
```
```  1158     fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
```
```  1159     with cos_eq_zero_imp_norm_ge[of "c*z"] assms
```
```  1160       show "eval_fps (fps_cos  c) z \<noteq> 0" by (auto simp: norm_mult field_simps)
```
```  1161   qed (insert assms, auto)
```
```  1162   thus ?thesis by (simp add: min_def)
```
```  1163 qed
```
```  1164
```
```  1165 lemma eval_fps_tan:
```
```  1166   fixes c :: complex
```
```  1167   assumes "norm z < pi / (2 * norm c)"
```
```  1168   shows   "eval_fps (fps_tan c) z = tan (c * z)"
```
```  1169 proof (cases "c = 0")
```
```  1170   case False
```
```  1171   show ?thesis unfolding fps_tan_def
```
```  1172   proof (subst eval_fps_divide'[where r = "pi / (2 * norm c)"])
```
```  1173     fix z :: complex assume "z \<in> eball 0 (pi / (2 * norm c))"
```
```  1174     with cos_eq_zero_imp_norm_ge[of "c*z"] assms
```
```  1175       show "eval_fps (fps_cos  c) z \<noteq> 0" using False by (auto simp: norm_mult field_simps)
```
```  1176     qed (insert False assms, auto simp: field_simps tan_def)
```
```  1177 qed simp_all
```
```  1178
```
```  1179 lemma eval_fps_binomial:
```
```  1180   fixes c :: complex
```
```  1181   assumes "norm z < 1"
```
```  1182   shows   "eval_fps (fps_binomial c) z = (1 + z) powr c"
```
```  1183   using gen_binomial_complex[OF assms] by (simp add: sums_iff eval_fps_def)
```
```  1184
```
```  1185 lemma has_fps_expansion_binomial_complex [fps_expansion_intros]:
```
```  1186   fixes c :: complex
```
```  1187   shows "(\<lambda>x. (1 + x) powr c) has_fps_expansion fps_binomial c"
```
```  1188 proof -
```
```  1189   have *: "eventually (\<lambda>z::complex. z \<in> eball 0 1) (nhds 0)"
```
```  1190     by (intro eventually_nhds_in_open) auto
```
```  1191   thus ?thesis
```
```  1192     by (auto simp: has_fps_expansion_def eval_fps_binomial fps_conv_radius_binomial
```
```  1193              intro!: eventually_mono [OF *])
```
```  1194 qed
```
```  1195
```
```  1196 lemma has_fps_expansion_sin [fps_expansion_intros]:
```
```  1197   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1198   shows "(\<lambda>x. sin (c * x)) has_fps_expansion fps_sin c"
```
```  1199   by (auto simp: has_fps_expansion_def)
```
```  1200
```
```  1201 lemma has_fps_expansion_sin' [fps_expansion_intros]:
```
```  1202   "(\<lambda>x::'a :: {banach, real_normed_field}. sin x) has_fps_expansion fps_sin 1"
```
```  1203   using has_fps_expansion_sin[of 1] by simp
```
```  1204
```
```  1205 lemma has_fps_expansion_cos [fps_expansion_intros]:
```
```  1206   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1207   shows "(\<lambda>x. cos (c * x)) has_fps_expansion fps_cos c"
```
```  1208   by (auto simp: has_fps_expansion_def)
```
```  1209
```
```  1210 lemma has_fps_expansion_cos' [fps_expansion_intros]:
```
```  1211   "(\<lambda>x::'a :: {banach, real_normed_field}. cos x) has_fps_expansion fps_cos 1"
```
```  1212   using has_fps_expansion_cos[of 1] by simp
```
```  1213
```
```  1214 lemma has_fps_expansion_shift [fps_expansion_intros]:
```
```  1215   fixes F :: "'a :: {banach, real_normed_field} fps"
```
```  1216   assumes "f has_fps_expansion F" and "n \<le> subdegree F"
```
```  1217   assumes "c = fps_nth F n"
```
```  1218   shows   "(\<lambda>x. if x = 0 then c else f x / x ^ n) has_fps_expansion (fps_shift n F)"
```
```  1219 proof -
```
```  1220   have "eventually (\<lambda>x. x \<in> eball 0 (fps_conv_radius F)) (nhds 0)"
```
```  1221     using assms by (intro eventually_nhds_in_open) (auto simp: has_fps_expansion_def zero_ereal_def)
```
```  1222   moreover have "eventually (\<lambda>x. eval_fps F x = f x) (nhds 0)"
```
```  1223     using assms by (auto simp: has_fps_expansion_def)
```
```  1224   ultimately have "eventually (\<lambda>x. eval_fps (fps_shift n F) x =
```
```  1225                      (if x = 0 then c else f x / x ^ n)) (nhds 0)"
```
```  1226     by eventually_elim (auto simp: eval_fps_shift assms)
```
```  1227   with assms show ?thesis by (auto simp: has_fps_expansion_def)
```
```  1228 qed
```
```  1229
```
```  1230 lemma has_fps_expansion_divide [fps_expansion_intros]:
```
```  1231   fixes F G :: "'a :: {banach, real_normed_field} fps"
```
```  1232   assumes "f has_fps_expansion F" and "g has_fps_expansion G" and
```
```  1233           "subdegree G \<le> subdegree F" "G \<noteq> 0"
```
```  1234           "c = fps_nth F (subdegree G) / fps_nth G (subdegree G)"
```
```  1235   shows   "(\<lambda>x. if x = 0 then c else f x / g x) has_fps_expansion (F / G)"
```
```  1236 proof -
```
```  1237   define n where "n = subdegree G"
```
```  1238   define F' and G' where "F' = fps_shift n F" and "G' = fps_shift n G"
```
```  1239   have "F = F' * fps_X ^ n" "G = G' * fps_X ^ n" unfolding F'_def G'_def n_def
```
```  1240     by (rule fps_shift_times_fps_X_power [symmetric] le_refl | fact)+
```
```  1241   moreover from assms have "fps_nth G' 0 \<noteq> 0"
```
```  1242     by (simp add: G'_def n_def)
```
```  1243   ultimately have FG: "F / G = F' * inverse G'"
```
```  1244     by (simp add: fps_divide_unit)
```
```  1245
```
```  1246   have "(\<lambda>x. (if x = 0 then fps_nth F n else f x / x ^ n) *
```
```  1247           inverse (if x = 0 then fps_nth G n else g x / x ^ n)) has_fps_expansion F / G"
```
```  1248     (is "?h has_fps_expansion _") unfolding FG F'_def G'_def n_def using \<open>G \<noteq> 0\<close>
```
```  1249     by (intro has_fps_expansion_mult has_fps_expansion_inverse
```
```  1250               has_fps_expansion_shift assms) auto
```
```  1251   also have "?h = (\<lambda>x. if x = 0 then c else f x / g x)"
```
```  1252     using assms(5) unfolding n_def
```
```  1253     by (intro ext) (auto split: if_splits simp: field_simps)
```
```  1254   finally show ?thesis .
```
```  1255 qed
```
```  1256
```
```  1257 lemma has_fps_expansion_divide' [fps_expansion_intros]:
```
```  1258   fixes F G :: "'a :: {banach, real_normed_field} fps"
```
```  1259   assumes "f has_fps_expansion F" and "g has_fps_expansion G" and "fps_nth G 0 \<noteq> 0"
```
```  1260   shows   "(\<lambda>x. f x / g x) has_fps_expansion (F / G)"
```
```  1261 proof -
```
```  1262   have "(\<lambda>x. if x = 0 then fps_nth F 0 / fps_nth G 0 else f x / g x) has_fps_expansion (F / G)"
```
```  1263     (is "?h has_fps_expansion _") using assms(3) by (intro has_fps_expansion_divide assms) auto
```
```  1264   also from assms have "fps_nth F 0 = f 0" "fps_nth G 0 = g 0"
```
```  1265     by (auto simp: has_fps_expansion_def eval_fps_at_0 dest: eventually_nhds_x_imp_x)
```
```  1266   hence "?h = (\<lambda>x. f x / g x)" by auto
```
```  1267   finally show ?thesis .
```
```  1268 qed
```
```  1269
```
```  1270 lemma has_fps_expansion_tan [fps_expansion_intros]:
```
```  1271   fixes c :: "'a :: {banach, real_normed_field, field_char_0}"
```
```  1272   shows "(\<lambda>x. tan (c * x)) has_fps_expansion fps_tan c"
```
```  1273 proof -
```
```  1274   have "(\<lambda>x. sin (c * x) / cos (c * x)) has_fps_expansion fps_sin c / fps_cos c"
```
```  1275     by (intro fps_expansion_intros) auto
```
```  1276   thus ?thesis by (simp add: tan_def fps_tan_def)
```
```  1277 qed
```
```  1278
```
```  1279 lemma has_fps_expansion_tan' [fps_expansion_intros]:
```
```  1280   "tan has_fps_expansion fps_tan (1 :: 'a :: {banach, real_normed_field, field_char_0})"
```
```  1281   using has_fps_expansion_tan[of 1] by simp
```
```  1282
```
```  1283 lemma has_fps_expansion_imp_holomorphic:
```
```  1284   assumes "f has_fps_expansion F"
```
```  1285   obtains s where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
```
```  1286 proof -
```
```  1287   from assms obtain s where s: "open s" "0 \<in> s" "\<And>z. z \<in> s \<Longrightarrow> eval_fps F z = f z"
```
```  1288     unfolding has_fps_expansion_def eventually_nhds by blast
```
```  1289   let ?s' = "eball 0 (fps_conv_radius F) \<inter> s"
```
```  1290   have "eval_fps F holomorphic_on ?s'"
```
```  1291     by (intro holomorphic_intros) auto
```
```  1292   also have "?this \<longleftrightarrow> f holomorphic_on ?s'"
```
```  1293     using s by (intro holomorphic_cong) auto
```
```  1294   finally show ?thesis using s assms
```
```  1295     by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
```
```  1296 qed
```
```  1297
```
```  1298 theorem residue_fps_expansion_over_power_at_0:
```
```  1299   assumes "f has_fps_expansion F"
```
```  1300   shows   "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
```
```  1301 proof -
```
```  1302   from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
```
```  1303   have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
```
```  1304     using assms s unfolding has_fps_expansion_def
```
```  1305     by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
```
```  1306   also from assms have "\<dots> = fps_nth F n"
```
```  1307     by (subst fps_nth_fps_expansion) auto
```
```  1308   finally show ?thesis by simp
```
```  1309 qed
```
```  1310
```
```  1311 end
```