src/HOL/Analysis/FPS_Convergence.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
child 70113 c8deb8ba6d05
permissions -rw-r--r--
more strict AFP properties;
     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>\<open>ball\<close> 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