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