11 imports NthRoot Fact Series EvenOdd Deriv |
11 imports NthRoot Fact Series EvenOdd Deriv |
12 begin |
12 begin |
13 |
13 |
14 subsection{*Properties of Power Series*} |
14 subsection{*Properties of Power Series*} |
15 |
15 |
16 lemma lemma_realpow_diff [rule_format (no_asm)]: |
16 lemma lemma_realpow_diff: |
17 "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y" |
17 fixes y :: "'a::recpower" |
18 apply (induct "n", auto) |
18 shows "p \<le> n \<Longrightarrow> y ^ (Suc n - p) = (y ^ (n - p)) * y" |
19 apply (subgoal_tac "p = Suc n") |
19 proof - |
20 apply (simp (no_asm_simp), auto) |
20 assume "p \<le> n" |
21 apply (drule sym) |
21 hence "Suc n - p = Suc (n - p)" by (rule Suc_diff_le) |
22 apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric] |
22 thus ?thesis by (simp add: power_Suc power_commutes) |
23 del: realpow_Suc) |
23 qed |
24 done |
|
25 |
24 |
26 lemma lemma_realpow_diff_sumr: |
25 lemma lemma_realpow_diff_sumr: |
27 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) = |
26 fixes y :: "'a::{recpower,comm_semiring_0}" shows |
28 y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)" |
27 "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) = |
|
28 y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))" |
29 by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac |
29 by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac |
30 simp del: setsum_op_ivl_Suc cong: strong_setsum_cong) |
30 simp del: setsum_op_ivl_Suc cong: strong_setsum_cong) |
31 |
31 |
32 lemma lemma_realpow_diff_sumr2: |
32 lemma lemma_realpow_diff_sumr2: |
|
33 fixes y :: "'a::{recpower,comm_ring}" shows |
33 "x ^ (Suc n) - y ^ (Suc n) = |
34 "x ^ (Suc n) - y ^ (Suc n) = |
34 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)" |
35 (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))" |
35 apply (induct "n", simp) |
36 apply (induct "n", simp add: power_Suc) |
36 apply (auto simp del: setsum_op_ivl_Suc) |
37 apply (simp add: power_Suc del: setsum_op_ivl_Suc) |
37 apply (subst setsum_op_ivl_Suc) |
38 apply (subst setsum_op_ivl_Suc) |
38 apply (drule sym) |
39 apply (subst lemma_realpow_diff_sumr) |
39 apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_op_ivl_Suc) |
40 apply (simp add: right_distrib del: setsum_op_ivl_Suc) |
|
41 apply (subst mult_left_commute [where a="x - y"]) |
|
42 apply (erule subst) |
|
43 apply (simp add: power_Suc ring_eq_simps) |
40 done |
44 done |
41 |
45 |
42 lemma lemma_realpow_rev_sumr: |
46 lemma lemma_realpow_rev_sumr: |
43 "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) = |
47 "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) = |
44 (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)" |
48 (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))" |
45 apply (case_tac "x = y") |
49 apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"]) |
46 apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_op_ivl_Suc) |
50 apply (rule inj_onI, simp) |
47 apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1]) |
51 apply auto |
48 apply (rule_tac [2] minus_minus [THEN subst], simp) |
52 apply (rule_tac x="n - x" in image_eqI, simp, simp) |
49 apply (subst minus_mult_left) |
|
50 apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_op_ivl_Suc) |
|
51 done |
53 done |
52 |
54 |
53 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
55 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>"}.*} |
56 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
55 |
57 |
56 lemma powser_insidea: |
58 lemma powser_insidea: |
57 fixes x z :: real |
59 fixes x z :: "'a::{real_normed_field,banach,recpower}" |
58 assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
60 assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
59 assumes 2: "\<bar>z\<bar> < \<bar>x\<bar>" |
61 assumes 2: "norm z < norm x" |
60 shows "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)" |
62 shows "summable (\<lambda>n. norm (f n * z ^ n))" |
61 proof - |
63 proof - |
62 from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
64 from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
63 from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
65 from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
64 by (rule summable_LIMSEQ_zero) |
66 by (rule summable_LIMSEQ_zero) |
65 hence "convergent (\<lambda>n. f n * x ^ n)" |
67 hence "convergent (\<lambda>n. f n * x ^ n)" |
66 by (rule convergentI) |
68 by (rule convergentI) |
67 hence "Cauchy (\<lambda>n. f n * x ^ n)" |
69 hence "Cauchy (\<lambda>n. f n * x ^ n)" |
68 by (simp add: Cauchy_convergent_iff) |
70 by (simp add: Cauchy_convergent_iff) |
69 hence "Bseq (\<lambda>n. f n * x ^ n)" |
71 hence "Bseq (\<lambda>n. f n * x ^ n)" |
70 by (rule Cauchy_Bseq) |
72 by (rule Cauchy_Bseq) |
71 then obtain K where 3: "0 < K" and 4: "\<forall>n. \<bar>f n * x ^ n\<bar> \<le> K" |
73 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) |
74 by (simp add: Bseq_def, safe) |
73 have "\<exists>N. \<forall>n\<ge>N. norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>" |
75 have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le> |
|
76 K * norm (z ^ n) * inverse (norm (x ^ n))" |
74 proof (intro exI allI impI) |
77 proof (intro exI allI impI) |
75 fix n::nat assume "0 \<le> n" |
78 fix n::nat assume "0 \<le> n" |
76 have "norm (\<bar>f n\<bar> * z ^ n) * \<bar>x ^ n\<bar> = \<bar>f n * x ^ n\<bar> * \<bar>z ^ n\<bar>" |
79 have "norm (norm (f n * z ^ n)) * norm (x ^ n) = |
77 by (simp add: abs_mult) |
80 norm (f n * x ^ n) * norm (z ^ n)" |
78 also have "\<dots> \<le> K * \<bar>z ^ n\<bar>" |
81 by (simp add: norm_mult abs_mult) |
79 by (simp only: mult_right_mono 4 abs_ge_zero) |
82 also have "\<dots> \<le> K * norm (z ^ n)" |
80 also have "\<dots> = K * \<bar>z ^ n\<bar> * (inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>)" |
83 by (simp only: mult_right_mono 4 norm_ge_zero) |
|
84 also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))" |
81 by (simp add: x_neq_0) |
85 by (simp add: x_neq_0) |
82 also have "\<dots> = K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>" |
86 also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)" |
83 by (simp only: mult_assoc) |
87 by (simp only: mult_assoc) |
84 finally show "norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>" |
88 finally show "norm (norm (f n * z ^ n)) \<le> |
|
89 K * norm (z ^ n) * inverse (norm (x ^ n))" |
85 by (simp add: mult_le_cancel_right x_neq_0) |
90 by (simp add: mult_le_cancel_right x_neq_0) |
86 qed |
91 qed |
87 moreover have "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)" |
92 moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" |
88 proof - |
93 proof - |
89 from 2 have "norm \<bar>z * inverse x\<bar> < 1" |
94 from 2 have "norm (norm (z * inverse x)) < 1" |
90 by (simp add: abs_mult divide_inverse [symmetric]) |
95 using x_neq_0 |
91 hence "summable (\<lambda>n. \<bar>z * inverse x\<bar> ^ n)" |
96 by (simp add: nonzero_norm_divide divide_inverse [symmetric]) |
|
97 hence "summable (\<lambda>n. norm (z * inverse x) ^ n)" |
92 by (rule summable_geometric) |
98 by (rule summable_geometric) |
93 hence "summable (\<lambda>n. K * \<bar>z * inverse x\<bar> ^ n)" |
99 hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)" |
94 by (rule summable_mult) |
100 by (rule summable_mult) |
95 thus "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)" |
101 thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))" |
96 by (simp add: abs_mult power_mult_distrib power_abs |
102 using x_neq_0 |
97 power_inverse mult_assoc) |
103 by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib |
|
104 power_inverse norm_power mult_assoc) |
98 qed |
105 qed |
99 ultimately show "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)" |
106 ultimately show "summable (\<lambda>n. norm (f n * z ^ n))" |
100 by (rule summable_comparison_test) |
107 by (rule summable_comparison_test) |
101 qed |
108 qed |
102 |
109 |
103 lemma powser_inside: |
110 lemma powser_inside: |
104 fixes f :: "nat \<Rightarrow> real" shows |
111 fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach,recpower}" shows |
105 "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |] |
112 "[| summable (%n. f(n) * (x ^ n)); norm z < norm x |] |
106 ==> summable (%n. f(n) * (z ^ n))" |
113 ==> summable (%n. f(n) * (z ^ n))" |
107 apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea, simp) |
114 by (rule powser_insidea [THEN summable_norm_cancel]) |
108 apply (rule summable_rabs_cancel) |
|
109 apply (simp add: abs_mult power_abs [symmetric]) |
|
110 done |
|
111 |
115 |
112 |
116 |
113 subsection{*Term-by-Term Differentiability of Power Series*} |
117 subsection{*Term-by-Term Differentiability of Power Series*} |
114 |
118 |
115 definition |
119 definition |
116 diffs :: "(nat => real) => nat => real" where |
120 diffs :: "(nat => 'a::ring_1) => nat => 'a" where |
117 "diffs c = (%n. real (Suc n) * c(Suc n))" |
121 "diffs c = (%n. of_nat (Suc n) * c(Suc n))" |
118 |
122 |
119 text{*Lemma about distributing negation over it*} |
123 text{*Lemma about distributing negation over it*} |
120 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)" |
124 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)" |
121 by (simp add: diffs_def) |
125 by (simp add: diffs_def) |
122 |
126 |
123 text{*Show that we can shift the terms down one*} |
127 text{*Show that we can shift the terms down one*} |
124 lemma lemma_diffs: |
128 lemma lemma_diffs: |
125 "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) = |
129 "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) = |
126 (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) + |
130 (\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) + |
127 (real n * c(n) * x ^ (n - Suc 0))" |
131 (of_nat n * c(n) * x ^ (n - Suc 0))" |
128 apply (induct "n") |
132 apply (induct "n") |
129 apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def) |
133 apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def) |
130 done |
134 done |
131 |
135 |
132 lemma lemma_diffs2: |
136 lemma lemma_diffs2: |
133 "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) = |
137 "(\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) = |
134 (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) - |
138 (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) - |
135 (real n * c(n) * x ^ (n - Suc 0))" |
139 (of_nat n * c(n) * x ^ (n - Suc 0))" |
136 by (auto simp add: lemma_diffs) |
140 by (auto simp add: lemma_diffs) |
137 |
141 |
138 |
142 |
139 lemma diffs_equiv: |
143 lemma diffs_equiv: |
140 "summable (%n. (diffs c)(n) * (x ^ n)) ==> |
144 "summable (%n. (diffs c)(n) * (x ^ n)) ==> |
141 (%n. real n * c(n) * (x ^ (n - Suc 0))) sums |
145 (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums |
142 (\<Sum>n. (diffs c)(n) * (x ^ n))" |
146 (\<Sum>n. (diffs c)(n) * (x ^ n))" |
143 apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0") |
147 apply (subgoal_tac " (%n. of_nat n * c (n) * (x ^ (n - Suc 0))) ----> 0") |
144 apply (rule_tac [2] LIMSEQ_imp_Suc) |
148 apply (rule_tac [2] LIMSEQ_imp_Suc) |
145 apply (drule summable_sums) |
149 apply (drule summable_sums) |
146 apply (auto simp add: sums_def) |
150 apply (auto simp add: sums_def) |
147 apply (drule_tac X="(\<lambda>n. \<Sum>n = 0..<n. diffs c n * x ^ n)" in LIMSEQ_diff) |
151 apply (drule_tac X="(\<lambda>n. \<Sum>n = 0..<n. diffs c n * x ^ n)" in LIMSEQ_diff) |
148 apply (auto simp add: lemma_diffs2 [symmetric] diffs_def [symmetric]) |
152 apply (auto simp add: lemma_diffs2 [symmetric] diffs_def [symmetric]) |
149 apply (simp add: diffs_def summable_LIMSEQ_zero) |
153 apply (simp add: diffs_def summable_LIMSEQ_zero) |
150 done |
154 done |
151 |
155 |
152 lemma lemma_termdiff1: |
156 lemma lemma_termdiff1: |
|
157 fixes z :: "'a :: {recpower,comm_ring}" shows |
153 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = |
158 "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) = |
154 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)" |
159 (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))" |
155 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac |
160 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac |
156 cong: strong_setsum_cong) |
161 cong: strong_setsum_cong) |
157 |
162 |
158 lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)" |
163 lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)" |
159 by (simp add: less_iff_Suc_add) |
164 by (simp add: less_iff_Suc_add) |
160 |
165 |
161 lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)" |
166 lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)" |
162 by arith |
167 by arith |
163 |
168 |
|
169 lemma sumr_diff_mult_const2: |
|
170 "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)" |
|
171 by (simp add: setsum_subtractf) |
|
172 |
164 lemma lemma_termdiff2: |
173 lemma lemma_termdiff2: |
|
174 fixes h :: "'a :: {recpower,field,division_by_zero}" |
165 assumes h: "h \<noteq> 0" shows |
175 assumes h: "h \<noteq> 0" shows |
166 "((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0) = |
176 "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) = |
167 h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p. |
177 h * (\<Sum>p=0..< n - Suc 0. \<Sum>q=0..< n - Suc 0 - p. |
168 (z + h) ^ q * z ^ (n - 2 - q))" |
178 (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs") |
169 apply (rule real_mult_left_cancel [OF h, THEN iffD1]) |
179 apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h) |
170 apply (simp add: right_diff_distrib diff_divide_distrib h) |
180 apply (simp add: right_diff_distrib diff_divide_distrib h) |
171 apply (simp add: mult_assoc [symmetric]) |
181 apply (simp add: mult_assoc [symmetric]) |
172 apply (cases "n", simp) |
182 apply (cases "n", simp) |
173 apply (simp add: lemma_realpow_diff_sumr2 h |
183 apply (simp add: lemma_realpow_diff_sumr2 h |
174 right_diff_distrib [symmetric] mult_assoc |
184 right_diff_distrib [symmetric] mult_assoc |
175 del: realpow_Suc setsum_op_ivl_Suc) |
185 del: realpow_Suc setsum_op_ivl_Suc of_nat_Suc) |
176 apply (subst lemma_realpow_rev_sumr) |
186 apply (subst lemma_realpow_rev_sumr) |
177 apply (subst sumr_diff_mult_const) |
187 apply (subst sumr_diff_mult_const2) |
178 apply simp |
188 apply simp |
179 apply (simp only: lemma_termdiff1 setsum_right_distrib) |
189 apply (simp only: lemma_termdiff1 setsum_right_distrib) |
180 apply (rule setsum_cong [OF refl]) |
190 apply (rule setsum_cong [OF refl]) |
181 apply (simp add: diff_minus [symmetric] less_iff_Suc_add) |
191 apply (simp add: diff_minus [symmetric] less_iff_Suc_add) |
182 apply (clarify) |
192 apply (clarify) |
185 apply (subst mult_assoc [symmetric], subst power_add [symmetric]) |
195 apply (subst mult_assoc [symmetric], subst power_add [symmetric]) |
186 apply (simp add: mult_ac) |
196 apply (simp add: mult_ac) |
187 done |
197 done |
188 |
198 |
189 lemma real_setsum_nat_ivl_bounded2: |
199 lemma real_setsum_nat_ivl_bounded2: |
190 "\<lbrakk>\<And>p::nat. p < n \<Longrightarrow> f p \<le> K; 0 \<le> K\<rbrakk> |
200 fixes K :: "'a::ordered_semidom" |
191 \<Longrightarrow> setsum f {0..<n-k} \<le> real n * K" |
201 assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" |
192 apply (rule order_trans [OF real_setsum_nat_ivl_bounded mult_right_mono]) |
202 assumes K: "0 \<le> K" |
193 apply simp_all |
203 shows "setsum f {0..<n-k} \<le> of_nat n * K" |
|
204 apply (rule order_trans [OF setsum_mono]) |
|
205 apply (rule f, simp) |
|
206 apply (simp add: mult_right_mono K) |
194 done |
207 done |
195 |
208 |
196 lemma lemma_termdiff3: |
209 lemma lemma_termdiff3: |
|
210 fixes h z :: "'a::{real_normed_field,recpower,division_by_zero}" |
197 assumes 1: "h \<noteq> 0" |
211 assumes 1: "h \<noteq> 0" |
198 assumes 2: "\<bar>z\<bar> \<le> K" |
212 assumes 2: "norm z \<le> K" |
199 assumes 3: "\<bar>z + h\<bar> \<le> K" |
213 assumes 3: "norm (z + h) \<le> K" |
200 shows "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar> |
214 shows "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) |
201 \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>" |
215 \<le> of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" |
202 proof - |
216 proof - |
203 have "\<bar>((z + h) ^ n - z ^ n) / h - real n * z ^ (n - Suc 0)\<bar> = |
217 have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) = |
204 \<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
218 norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
205 (z + h) ^ q * z ^ (n - 2 - q)\<bar> * \<bar>h\<bar>" |
219 (z + h) ^ q * z ^ (n - 2 - q)) * norm h" |
206 apply (subst lemma_termdiff2 [OF 1]) |
220 apply (subst lemma_termdiff2 [OF 1]) |
207 apply (subst abs_mult) |
221 apply (subst norm_mult) |
208 apply (rule mult_commute) |
222 apply (rule mult_commute) |
209 done |
223 done |
210 also have "\<dots> \<le> real n * (real (n - Suc 0) * K ^ (n - 2)) * \<bar>h\<bar>" |
224 also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h" |
211 proof (rule mult_right_mono [OF _ abs_ge_zero]) |
225 proof (rule mult_right_mono [OF _ norm_ge_zero]) |
212 from abs_ge_zero 2 have K: "0 \<le> K" by (rule order_trans) |
226 from norm_ge_zero 2 have K: "0 \<le> K" by (rule order_trans) |
213 have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> \<bar>(z + h) ^ i * z ^ j\<bar> \<le> K ^ n" |
227 have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n" |
214 apply (erule subst) |
228 apply (erule subst) |
215 apply (simp only: abs_mult power_abs power_add) |
229 apply (simp only: norm_mult norm_power power_add) |
216 apply (intro mult_mono power_mono 2 3 abs_ge_zero zero_le_power K) |
230 apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K) |
217 done |
231 done |
218 show "\<bar>\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
232 show "norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p. |
219 (z + h) ^ q * z ^ (n - 2 - q)\<bar> |
233 (z + h) ^ q * z ^ (n - 2 - q)) |
220 \<le> real n * (real (n - Suc 0) * K ^ (n - 2))" |
234 \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))" |
221 apply (intro |
235 apply (intro |
222 order_trans [OF setsum_abs] |
236 order_trans [OF norm_setsum] |
223 real_setsum_nat_ivl_bounded2 |
237 real_setsum_nat_ivl_bounded2 |
224 mult_nonneg_nonneg |
238 mult_nonneg_nonneg |
225 real_of_nat_ge_zero |
239 zero_le_imp_of_nat |
226 zero_le_power K) |
240 zero_le_power K) |
227 apply (rule le_Kn, simp) |
241 apply (rule le_Kn, simp) |
228 done |
242 done |
229 qed |
243 qed |
230 also have "\<dots> = real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>" |
244 also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h" |
231 by (simp only: mult_assoc) |
245 by (simp only: mult_assoc) |
232 finally show ?thesis . |
246 finally show ?thesis . |
233 qed |
247 qed |
234 |
248 |
235 lemma lemma_termdiff4: |
249 lemma lemma_termdiff4: |
|
250 fixes f :: "'a::{real_normed_field,recpower,division_by_zero} \<Rightarrow> |
|
251 'b::real_normed_vector" |
236 assumes k: "0 < (k::real)" |
252 assumes k: "0 < (k::real)" |
237 assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>f h\<bar> \<le> K * \<bar>h\<bar>" |
253 assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h" |
238 shows "f -- 0 --> 0" |
254 shows "f -- 0 --> 0" |
239 proof (simp add: LIM_def, safe) |
255 proof (simp add: LIM_def, safe) |
240 fix r::real assume r: "0 < r" |
256 fix r::real assume r: "0 < r" |
241 have zero_le_K: "0 \<le> K" |
257 have zero_le_K: "0 \<le> K" |
242 apply (cut_tac k) |
258 apply (cut_tac k) |
243 apply (cut_tac h="k/2" in le, simp, simp) |
259 apply (cut_tac h="of_real (k/2)" in le, simp) |
244 apply (subgoal_tac "0 \<le> K*k", simp add: zero_le_mult_iff) |
260 apply (simp del: of_real_divide) |
245 apply (force intro: order_trans [of _ "\<bar>f (k / 2)\<bar> * 2"]) |
261 apply (drule order_trans [OF norm_ge_zero]) |
|
262 apply (simp add: zero_le_mult_iff) |
246 done |
263 done |
247 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)" |
264 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" |
248 proof (cases) |
265 proof (cases) |
249 assume "K = 0" |
266 assume "K = 0" |
250 with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < k \<longrightarrow> \<bar>f x\<bar> < r)" |
267 with k r le have "0 < k \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < k \<longrightarrow> norm (f x) < r)" |
251 by simp |
268 by simp |
252 thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)" .. |
269 thus "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" .. |
253 next |
270 next |
254 assume K_neq_zero: "K \<noteq> 0" |
271 assume K_neq_zero: "K \<noteq> 0" |
255 with zero_le_K have K: "0 < K" by simp |
272 with zero_le_K have K: "0 < K" by simp |
256 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>f x\<bar> < r)" |
273 show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)" |
257 proof (rule exI, safe) |
274 proof (rule exI, safe) |
258 from k r K show "0 < min k (r * inverse K / 2)" |
275 from k r K show "0 < min k (r * inverse K / 2)" |
259 by (simp add: mult_pos_pos positive_imp_inverse_positive) |
276 by (simp add: mult_pos_pos positive_imp_inverse_positive) |
260 next |
277 next |
261 fix x::real |
278 fix x::'a |
262 assume x1: "x \<noteq> 0" and x2: "\<bar>x\<bar> < min k (r * inverse K / 2)" |
279 assume x1: "x \<noteq> 0" and x2: "norm x < min k (r * inverse K / 2)" |
263 from x2 have x3: "\<bar>x\<bar> < k" and x4: "\<bar>x\<bar> < r * inverse K / 2" |
280 from x2 have x3: "norm x < k" and x4: "norm x < r * inverse K / 2" |
264 by simp_all |
281 by simp_all |
265 from x1 x3 le have "\<bar>f x\<bar> \<le> K * \<bar>x\<bar>" by simp |
282 from x1 x3 le have "norm (f x) \<le> K * norm x" by simp |
266 also from x4 K have "K * \<bar>x\<bar> < K * (r * inverse K / 2)" |
283 also from x4 K have "K * norm x < K * (r * inverse K / 2)" |
267 by (rule mult_strict_left_mono) |
284 by (rule mult_strict_left_mono) |
268 also have "\<dots> = r / 2" |
285 also have "\<dots> = r / 2" |
269 using K_neq_zero by simp |
286 using K_neq_zero by simp |
270 also have "r / 2 < r" |
287 also have "r / 2 < r" |
271 using r by simp |
288 using r by simp |
272 finally show "\<bar>f x\<bar> < r" . |
289 finally show "norm (f x) < r" . |
273 qed |
290 qed |
274 qed |
291 qed |
275 qed |
292 qed |
276 |
293 |
277 lemma lemma_termdiff5: |
294 lemma lemma_termdiff5: |
|
295 fixes g :: "'a::{recpower,real_normed_field,division_by_zero} \<Rightarrow> |
|
296 nat \<Rightarrow> 'b::banach" |
278 assumes k: "0 < (k::real)" |
297 assumes k: "0 < (k::real)" |
279 assumes f: "summable f" |
298 assumes f: "summable f" |
280 assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; \<bar>h\<bar> < k\<rbrakk> \<Longrightarrow> \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>" |
299 assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h" |
281 shows "(\<lambda>h. suminf (g h)) -- 0 --> 0" |
300 shows "(\<lambda>h. suminf (g h)) -- 0 --> 0" |
282 proof (rule lemma_termdiff4 [OF k]) |
301 proof (rule lemma_termdiff4 [OF k]) |
283 fix h assume "h \<noteq> 0" and "\<bar>h\<bar> < k" |
302 fix h::'a assume "h \<noteq> 0" and "norm h < k" |
284 hence A: "\<forall>n. \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>" |
303 hence A: "\<forall>n. norm (g h n) \<le> f n * norm h" |
285 by (simp add: le) |
304 by (simp add: le) |
286 hence "\<exists>N. \<forall>n\<ge>N. norm \<bar>g h n\<bar> \<le> f n * \<bar>h\<bar>" |
305 hence "\<exists>N. \<forall>n\<ge>N. norm (norm (g h n)) \<le> f n * norm h" |
287 by simp |
306 by simp |
288 moreover from f have B: "summable (\<lambda>n. f n * \<bar>h\<bar>)" |
307 moreover from f have B: "summable (\<lambda>n. f n * norm h)" |
289 by (rule summable_mult2) |
308 by (rule summable_mult2) |
290 ultimately have C: "summable (\<lambda>n. \<bar>g h n\<bar>)" |
309 ultimately have C: "summable (\<lambda>n. norm (g h n))" |
291 by (rule summable_comparison_test) |
310 by (rule summable_comparison_test) |
292 hence "\<bar>suminf (g h)\<bar> \<le> (\<Sum>n. \<bar>g h n\<bar>)" |
311 hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))" |
293 by (rule summable_rabs) |
312 by (rule summable_norm) |
294 also from A C B have "(\<Sum>n. \<bar>g h n\<bar>) \<le> (\<Sum>n. f n * \<bar>h\<bar>)" |
313 also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)" |
295 by (rule summable_le) |
314 by (rule summable_le) |
296 also from f have "(\<Sum>n. f n * \<bar>h\<bar>) = suminf f * \<bar>h\<bar>" |
315 also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h" |
297 by (rule suminf_mult2 [symmetric]) |
316 by (rule suminf_mult2 [symmetric]) |
298 finally show "\<bar>suminf (g h)\<bar> \<le> suminf f * \<bar>h\<bar>" . |
317 finally show "norm (suminf (g h)) \<le> suminf f * norm h" . |
299 qed |
318 qed |
300 |
319 |
301 |
320 |
302 text{* FIXME: Long proofs*} |
321 text{* FIXME: Long proofs*} |
303 |
322 |
304 lemma termdiffs_aux: |
323 lemma termdiffs_aux: |
|
324 fixes x :: "'a::{recpower,real_normed_field,division_by_zero,banach}" |
305 assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" |
325 assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" |
306 assumes 2: "\<bar>x\<bar> < \<bar>K\<bar>" |
326 assumes 2: "norm x < norm K" |
307 shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h |
327 shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h |
308 - real n * x ^ (n - Suc 0))) -- 0 --> 0" |
328 - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0" |
309 proof - |
329 proof - |
310 from dense [OF 2] |
330 from dense [OF 2] |
311 obtain r where r1: "\<bar>x\<bar> < r" and r2: "r < \<bar>K\<bar>" by fast |
331 obtain r where r1: "norm x < r" and r2: "r < norm K" by fast |
312 from abs_ge_zero r1 have r: "0 < r" |
332 from norm_ge_zero r1 have r: "0 < r" |
313 by (rule order_le_less_trans) |
333 by (rule order_le_less_trans) |
314 hence r_neq_0: "r \<noteq> 0" by simp |
334 hence r_neq_0: "r \<noteq> 0" by simp |
315 show ?thesis |
335 show ?thesis |
316 proof (rule lemma_termdiff5) |
336 proof (rule lemma_termdiff5) |
317 show "0 < r - \<bar>x\<bar>" using r1 by simp |
337 show "0 < r - norm x" using r1 by simp |
318 next |
338 next |
319 from r r2 have "\<bar>r\<bar> < \<bar>K\<bar>" |
339 from r r2 have "norm (of_real r::'a) < norm K" |
320 by (simp only: abs_of_nonneg order_less_imp_le) |
340 by simp |
321 with 1 have "summable (\<lambda>n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))" |
341 with 1 have "summable (\<lambda>n. norm (diffs (diffs c) n * (of_real r ^ n)))" |
322 by (rule powser_insidea) |
342 by (rule powser_insidea) |
323 hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. \<bar>c n\<bar>)) n * r ^ n)" |
343 hence "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)" |
324 by (simp only: diffs_def abs_mult abs_real_of_nat_cancel) |
344 using r |
325 hence "summable (\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0))" |
345 by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc) |
|
346 hence "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))" |
326 by (rule diffs_equiv [THEN sums_summable]) |
347 by (rule diffs_equiv [THEN sums_summable]) |
327 also have "(\<lambda>n. real n * diffs (\<lambda>n. \<bar>c n\<bar>) n * r ^ (n - Suc 0)) |
348 also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) |
328 = (\<lambda>n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))" |
349 = (\<lambda>n. diffs (%m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))" |
329 apply (rule ext) |
350 apply (rule ext) |
330 apply (simp add: diffs_def) |
351 apply (simp add: diffs_def) |
331 apply (case_tac n, simp_all add: r_neq_0) |
352 apply (case_tac n, simp_all add: r_neq_0) |
332 done |
353 done |
333 finally have "summable |
354 finally have "summable |
334 (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * r ^ (n - Suc 0))" |
355 (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))" |
335 by (rule diffs_equiv [THEN sums_summable]) |
356 by (rule diffs_equiv [THEN sums_summable]) |
336 also have |
357 also have |
337 "(\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * |
358 "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * |
338 r ^ (n - Suc 0)) = |
359 r ^ (n - Suc 0)) = |
339 (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))" |
360 (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" |
340 apply (rule ext) |
361 apply (rule ext) |
341 apply (case_tac "n", simp) |
362 apply (case_tac "n", simp) |
342 apply (case_tac "nat", simp) |
363 apply (case_tac "nat", simp) |
343 apply (simp add: r_neq_0) |
364 apply (simp add: r_neq_0) |
344 done |
365 done |
345 finally show |
366 finally show |
346 "summable (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))" . |
367 "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" . |
347 next |
368 next |
348 fix h::real and n::nat |
369 fix h::'a and n::nat |
349 assume h: "h \<noteq> 0" |
370 assume h: "h \<noteq> 0" |
350 assume "\<bar>h\<bar> < r - \<bar>x\<bar>" |
371 assume "norm h < r - norm x" |
351 hence "\<bar>x\<bar> + \<bar>h\<bar> < r" by simp |
372 hence "norm x + norm h < r" by simp |
352 with abs_triangle_ineq have xh: "\<bar>x + h\<bar> < r" |
373 with norm_triangle_ineq have xh: "norm (x + h) < r" |
353 by (rule order_le_less_trans) |
374 by (rule order_le_less_trans) |
354 show "\<bar>c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0))\<bar> |
375 show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) |
355 \<le> \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2) * \<bar>h\<bar>" |
376 \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h" |
356 apply (simp only: abs_mult mult_assoc) |
377 apply (simp only: norm_mult mult_assoc) |
357 apply (rule mult_left_mono [OF _ abs_ge_zero]) |
378 apply (rule mult_left_mono [OF _ norm_ge_zero]) |
358 apply (simp (no_asm) add: mult_assoc [symmetric]) |
379 apply (simp (no_asm) add: mult_assoc [symmetric]) |
359 apply (rule lemma_termdiff3) |
380 apply (rule lemma_termdiff3) |
360 apply (rule h) |
381 apply (rule h) |
361 apply (rule r1 [THEN order_less_imp_le]) |
382 apply (rule r1 [THEN order_less_imp_le]) |
362 apply (rule xh [THEN order_less_imp_le]) |
383 apply (rule xh [THEN order_less_imp_le]) |
363 done |
384 done |
364 qed |
385 qed |
365 qed |
386 qed |
366 |
387 |
367 lemma termdiffs: |
388 lemma termdiffs: |
|
389 fixes K x :: "'a::{recpower,real_normed_field,division_by_zero,banach}" |
368 assumes 1: "summable (\<lambda>n. c n * K ^ n)" |
390 assumes 1: "summable (\<lambda>n. c n * K ^ n)" |
369 assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" |
391 assumes 2: "summable (\<lambda>n. (diffs c) n * K ^ n)" |
370 assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" |
392 assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)" |
371 assumes 4: "\<bar>x\<bar> < \<bar>K\<bar>" |
393 assumes 4: "norm x < norm K" |
372 shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" |
394 shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)" |
373 proof (simp add: deriv_def, rule LIM_zero_cancel) |
395 proof (simp add: deriv_def, rule LIM_zero_cancel) |
374 show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h |
396 show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h |
375 - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0" |
397 - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0" |
376 proof (rule LIM_equal2) |
398 proof (rule LIM_equal2) |
377 show "0 < \<bar>K\<bar> - \<bar>x\<bar>" by (simp add: less_diff_eq 4) |
399 show "0 < norm K - norm x" by (simp add: less_diff_eq 4) |
378 next |
400 next |
379 fix h :: real |
401 fix h :: 'a |
380 assume "h \<noteq> 0" |
402 assume "h \<noteq> 0" |
381 assume "norm (h - 0) < \<bar>K\<bar> - \<bar>x\<bar>" |
403 assume "norm (h - 0) < norm K - norm x" |
382 hence "\<bar>x\<bar> + \<bar>h\<bar> < \<bar>K\<bar>" by simp |
404 hence "norm x + norm h < norm K" by simp |
383 hence 5: "\<bar>x + h\<bar> < \<bar>K\<bar>" |
405 hence 5: "norm (x + h) < norm K" |
384 by (rule abs_triangle_ineq [THEN order_le_less_trans]) |
406 by (rule norm_triangle_ineq [THEN order_le_less_trans]) |
385 have A: "summable (\<lambda>n. c n * x ^ n)" |
407 have A: "summable (\<lambda>n. c n * x ^ n)" |
386 by (rule powser_inside [OF 1 4]) |
408 by (rule powser_inside [OF 1 4]) |
387 have B: "summable (\<lambda>n. c n * (x + h) ^ n)" |
409 have B: "summable (\<lambda>n. c n * (x + h) ^ n)" |
388 by (rule powser_inside [OF 1 5]) |
410 by (rule powser_inside [OF 1 5]) |
389 have C: "summable (\<lambda>n. diffs c n * x ^ n)" |
411 have C: "summable (\<lambda>n. diffs c n * x ^ n)" |
390 by (rule powser_inside [OF 2 4]) |
412 by (rule powser_inside [OF 2 4]) |
391 show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h |
413 show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h |
392 - (\<Sum>n. diffs c n * x ^ n) = |
414 - (\<Sum>n. diffs c n * x ^ n) = |
393 (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - real n * x ^ (n - Suc 0)))" |
415 (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))" |
394 apply (subst sums_unique [OF diffs_equiv [OF C]]) |
416 apply (subst sums_unique [OF diffs_equiv [OF C]]) |
395 apply (subst suminf_diff [OF B A]) |
417 apply (subst suminf_diff [OF B A]) |
396 apply (subst suminf_divide [symmetric]) |
418 apply (subst suminf_divide [symmetric]) |
397 apply (rule summable_diff [OF B A]) |
419 apply (rule summable_diff [OF B A]) |
398 apply (subst suminf_diff) |
420 apply (subst suminf_diff) |