summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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

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>

10 theory FPS_Convergence

11 imports

12 Conformal_Mappings

13 Generalised_Binomial_Theorem

14 "HOL-Computational_Algebra.Formal_Power_Series"

15 begin

17 subsection%unimportant \<open>Balls with extended real radius\<close>

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}"

25 lemma in_eball_iff [simp]: "z \<in> eball z0 r \<longleftrightarrow> ereal (dist z0 z) < r"

26 by (simp add: eball_def)

28 lemma eball_ereal [simp]: "eball z (ereal r) = ball z r"

29 by auto

31 lemma eball_inf [simp]: "eball z \<infinity> = UNIV"

32 by auto

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

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)+

46 lemma eball_mono: "r \<le> r' \<Longrightarrow> eball z r \<le> eball z r'"

47 by auto

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

52 lemma open_eball [simp, intro]: "open (eball z r)"

53 by (cases r) auto

56 subsection \<open>Basic properties of convergent power series\<close>

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)"

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)"

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)"

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)

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)

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

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

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)

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

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] .

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

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

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

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

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

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

216 subsection%unimportant \<open>Lower bounds on radius of convergence\<close>

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

242 lemma eval_fps_at_0: "eval_fps f 0 = fps_nth f 0"

243 by (simp add: eval_fps_def)

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)

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

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)

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)

263 lemma fps_conv_radius_numeral [simp]: "fps_conv_radius (numeral n) = \<infinity>"

264 by (simp add: numeral_fps_const)

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

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)

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)

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)

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)

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)

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

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

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)

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

316 context

317 begin

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

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+

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)

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)

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

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

449 end

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

467 subsection \<open>Evaluating power series\<close>

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)

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

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

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

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)

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)

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)

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

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)

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)

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)

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)

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

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)

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)

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

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

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

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" .

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

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)

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)

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)

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

792 subsection \<open>Power series expansion of complex functions\<close>

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.

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.

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.

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)"

820 named_theorems fps_expansion_intros

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

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

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

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)

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)

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)

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)

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)

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)

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

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

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

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" .

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

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)

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" .

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

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

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)

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

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

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

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)

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)

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)

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

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

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

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

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

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

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

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)

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

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)

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

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)

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

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

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)

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

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

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

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

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

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

1311 end