52 |
52 |
53 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
53 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
54 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
54 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
55 |
55 |
56 lemma powser_insidea: |
56 lemma powser_insidea: |
57 fixes x z :: "'a::{real_normed_field,banach}" |
57 fixes x z :: "'a::real_normed_field" |
58 assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
58 assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
59 assumes 2: "norm z < norm x" |
59 assumes 2: "norm z < norm x" |
60 shows "summable (\<lambda>n. norm (f n * z ^ n))" |
60 shows "summable (\<lambda>n. norm (f n * z ^ n))" |
61 proof - |
61 proof - |
62 from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
62 from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
63 from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
63 from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
64 by (rule summable_LIMSEQ_zero) |
64 by (rule summable_LIMSEQ_zero) |
65 hence "convergent (\<lambda>n. f n * x ^ n)" |
65 hence "convergent (\<lambda>n. f n * x ^ n)" |
66 by (rule convergentI) |
66 by (rule convergentI) |
67 hence "Cauchy (\<lambda>n. f n * x ^ n)" |
67 hence "Cauchy (\<lambda>n. f n * x ^ n)" |
68 by (simp add: Cauchy_convergent_iff) |
68 by (rule convergent_Cauchy) |
69 hence "Bseq (\<lambda>n. f n * x ^ n)" |
69 hence "Bseq (\<lambda>n. f n * x ^ n)" |
70 by (rule Cauchy_Bseq) |
70 by (rule Cauchy_Bseq) |
71 then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K" |
71 then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K" |
72 by (simp add: Bseq_def, safe) |
72 by (simp add: Bseq_def, safe) |
73 have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> |
73 have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> |