44 |
44 |
45 arctan :: "real => real" |
45 arctan :: "real => real" |
46 "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)" |
46 "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)" |
47 |
47 |
48 |
48 |
49 |
|
50 subsection{*Exponential Function*} |
49 subsection{*Exponential Function*} |
51 |
50 |
52 lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" |
51 lemma summable_exp: "summable (%n. inverse (real (fact n)) * x ^ n)" |
53 apply (cut_tac 'a = real in zero_less_one [THEN dense], safe) |
52 apply (cut_tac 'a = real in zero_less_one [THEN dense], safe) |
54 apply (cut_tac x = r in reals_Archimedean3, auto) |
53 apply (cut_tac x = r in reals_Archimedean3, auto) |
55 apply (drule_tac x = "\<bar>x\<bar>" in spec, safe) |
54 apply (drule_tac x = "\<bar>x\<bar>" in spec, safe) |
56 apply (rule_tac N = n and c = r in ratio_test) |
55 apply (rule_tac N = n and c = r in ratio_test) |
57 apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc) |
56 apply (safe, simp add: abs_mult mult_assoc [symmetric] del: fact_Suc) |
58 apply (rule mult_right_mono) |
57 apply (rule mult_right_mono) |
59 apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst]) |
58 apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst]) |
60 apply (subst fact_Suc) |
59 apply (subst fact_Suc) |
61 apply (subst real_of_nat_mult) |
60 apply (subst real_of_nat_mult) |
62 apply (auto) |
61 apply (auto) |
63 apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive) |
62 apply (simp add: mult_assoc [symmetric] positive_imp_inverse_positive) |
64 apply (rule order_less_imp_le) |
63 apply (rule order_less_imp_le) |
65 apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1]) |
64 apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1]) |
66 apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc) |
65 apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc) |
67 apply (erule order_less_trans) |
66 apply (erule order_less_trans) |
68 apply (auto simp add: mult_less_cancel_left mult_ac) |
67 apply (auto simp add: mult_less_cancel_left mult_ac) |
174 |
173 |
175 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
174 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term |
176 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
175 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*} |
177 |
176 |
178 lemma powser_insidea: |
177 lemma powser_insidea: |
179 fixes f :: "nat \<Rightarrow> real" |
178 fixes x z :: real |
180 shows |
179 assumes 1: "summable (\<lambda>n. f n * x ^ n)" |
181 "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |] |
180 assumes 2: "\<bar>z\<bar> < \<bar>x\<bar>" |
182 ==> summable (%n. \<bar>f(n)\<bar> * (z ^ n))" |
181 shows "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)" |
183 apply (drule summable_LIMSEQ_zero) |
182 proof - |
184 apply (drule convergentI) |
183 from 2 have x_neq_0: "x \<noteq> 0" by clarsimp |
185 apply (simp add: Cauchy_convergent_iff [symmetric]) |
184 from 1 have "(\<lambda>n. f n * x ^ n) ----> 0" |
186 apply (drule Cauchy_Bseq) |
185 by (rule summable_LIMSEQ_zero) |
187 apply (simp add: Bseq_def, safe) |
186 hence "convergent (\<lambda>n. f n * x ^ n)" |
188 apply (rule_tac g = "%n. K * \<bar>z ^ n\<bar> * inverse (\<bar>x ^ n\<bar>)" in summable_comparison_test) |
187 by (rule convergentI) |
189 apply (rule_tac x = 0 in exI, safe) |
188 hence "Cauchy (\<lambda>n. f n * x ^ n)" |
190 apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ") |
189 by (simp add: Cauchy_convergent_iff) |
191 apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) |
190 hence "Bseq (\<lambda>n. f n * x ^ n)" |
192 apply (auto simp add: mult_assoc power_abs abs_mult) |
191 by (rule Cauchy_Bseq) |
193 prefer 2 |
192 then obtain K where 3: "0 < K" and 4: "\<forall>n. \<bar>f n * x ^ n\<bar> \<le> K" |
194 apply (drule_tac x = 0 in spec, force) |
193 by (simp add: Bseq_def, safe) |
195 apply (auto simp add: power_abs mult_ac) |
194 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>" |
196 apply (rule_tac a2 = "z ^ n" |
195 proof (intro exI allI impI) |
197 in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE]) |
196 fix n::nat assume "0 \<le> n" |
198 apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left) |
197 have "norm (\<bar>f n\<bar> * z ^ n) * \<bar>x ^ n\<bar> = \<bar>f n * x ^ n\<bar> * \<bar>z ^ n\<bar>" |
199 apply (rule_tac x = "K * inverse (1 - (\<bar>z\<bar> * inverse (\<bar>x\<bar>)))" in exI) |
198 by (simp add: abs_mult) |
200 apply (auto intro!: sums_mult simp add: mult_assoc) |
199 also have "\<dots> \<le> K * \<bar>z ^ n\<bar>" |
201 apply (subgoal_tac "\<bar>z ^ n\<bar> * inverse (\<bar>x\<bar> ^ n) = (\<bar>z\<bar> * inverse (\<bar>x\<bar>)) ^ n") |
200 by (simp only: mult_right_mono 4 abs_ge_zero) |
202 apply (auto simp add: power_abs [symmetric]) |
201 also have "\<dots> = K * \<bar>z ^ n\<bar> * (inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>)" |
203 apply (subgoal_tac "x \<noteq> 0") |
202 by (simp add: x_neq_0) |
204 apply (subgoal_tac [3] "x \<noteq> 0") |
203 also have "\<dots> = K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar> * \<bar>x ^ n\<bar>" |
205 apply (auto simp del: abs_inverse |
204 by (simp only: mult_assoc) |
206 simp add: abs_inverse [symmetric] realpow_not_zero |
205 finally show "norm (\<bar>f n\<bar> * z ^ n) \<le> K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>" |
207 abs_mult [symmetric] power_inverse power_mult_distrib [symmetric]) |
206 by (simp add: mult_le_cancel_right x_neq_0) |
208 apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide) |
207 qed |
209 done |
208 moreover have "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)" |
|
209 proof - |
|
210 from 2 have "norm \<bar>z * inverse x\<bar> < 1" |
|
211 by (simp add: abs_mult divide_inverse [symmetric]) |
|
212 hence "summable (\<lambda>n. \<bar>z * inverse x\<bar> ^ n)" |
|
213 by (rule summable_geometric) |
|
214 hence "summable (\<lambda>n. K * \<bar>z * inverse x\<bar> ^ n)" |
|
215 by (rule summable_mult) |
|
216 thus "summable (\<lambda>n. K * \<bar>z ^ n\<bar> * inverse \<bar>x ^ n\<bar>)" |
|
217 by (simp add: abs_mult power_mult_distrib power_abs |
|
218 power_inverse mult_assoc) |
|
219 qed |
|
220 ultimately show "summable (\<lambda>n. \<bar>f n\<bar> * z ^ n)" |
|
221 by (rule summable_comparison_test) |
|
222 qed |
210 |
223 |
211 lemma powser_inside: |
224 lemma powser_inside: |
212 fixes f :: "nat \<Rightarrow> real" |
225 fixes f :: "nat \<Rightarrow> real" shows |
213 shows |
|
214 "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |] |
226 "[| summable (%n. f(n) * (x ^ n)); \<bar>z\<bar> < \<bar>x\<bar> |] |
215 ==> summable (%n. f(n) * (z ^ n))" |
227 ==> summable (%n. f(n) * (z ^ n))" |
216 apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea) |
228 apply (drule_tac z = "\<bar>z\<bar>" in powser_insidea, simp) |
217 apply (auto intro: summable_rabs_cancel simp add: abs_mult power_abs [symmetric]) |
229 apply (rule summable_rabs_cancel) |
|
230 apply (simp add: abs_mult power_abs [symmetric]) |
218 done |
231 done |
219 |
232 |
220 |
233 |
221 subsection{*Differentiation of Power Series*} |
234 subsection{*Differentiation of Power Series*} |
222 |
235 |
368 done |
381 done |
369 |
382 |
370 |
383 |
371 text{* FIXME: Long proofs*} |
384 text{* FIXME: Long proofs*} |
372 |
385 |
373 ML {* fast_arith_split_limit := 0; *} (* FIXME: rewrite proofs *) |
|
374 |
|
375 lemma termdiffs_aux: |
386 lemma termdiffs_aux: |
376 "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |] |
387 assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)" |
377 ==> (\<lambda>h. \<Sum>n. c n * |
388 assumes 2: "\<bar>x\<bar> < \<bar>K\<bar>" |
|
389 shows "(\<lambda>h. \<Sum>n. c n * |
378 (((x + h) ^ n - x ^ n) * inverse h - |
390 (((x + h) ^ n - x ^ n) * inverse h - |
379 real n * x ^ (n - Suc 0))) |
391 real n * x ^ (n - Suc 0))) |
380 -- 0 --> 0" |
392 -- 0 --> 0" |
381 apply (drule dense, safe) |
393 proof - |
382 apply (frule real_less_sum_gt_zero) |
394 from dense [OF 2] obtain r where 3: "\<bar>x\<bar> < r" and 4: "r < \<bar>K\<bar>" by fast |
383 apply (drule_tac |
395 from 3 have r_neq_0: "r \<noteq> 0" by auto |
384 f = "%n. \<bar>c n\<bar> * real n * real (n - Suc 0) * (r ^ (n - 2))" |
396 show "(\<lambda>h. suminf (\<lambda>n. c n * (((x + h) ^ n - x ^ n) * inverse h - real n * x ^ (n - Suc 0)))) -- 0 --> 0" |
385 and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) |
397 proof (rule lemma_termdiff5) |
386 - (real n * (x ^ (n - Suc 0))))" |
398 show "0 < r + - \<bar>x\<bar>" using 3 by simp |
387 in lemma_termdiff5) |
399 next |
388 apply (auto simp add: add_commute) |
400 have A: "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))" |
389 apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))") |
401 apply (rule powser_insidea [OF 1]) |
390 apply (rule_tac [2] x = K in powser_insidea, auto) |
402 apply (subgoal_tac "\<bar>r\<bar> = r", erule ssubst, rule 4) |
391 apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto) |
403 apply (rule_tac y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg]) |
392 apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto) |
404 apply (rule abs_ge_zero) |
393 apply (simp add: diffs_def mult_assoc [symmetric]) |
405 apply (rule order_less_imp_le [OF 3]) |
394 apply (subgoal_tac |
406 done |
395 "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) |
407 have B: "\<forall>n. real (Suc n) * real (Suc (Suc n)) * |
396 = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") |
408 \<bar>c (Suc (Suc n))\<bar> * (r ^ n) = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n)" |
397 apply (auto simp add: abs_mult) |
409 by (simp add: diffs_def mult_assoc) |
398 apply (drule diffs_equiv) |
410 have C: "(%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) |
399 apply (drule sums_summable) |
411 = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))" |
400 apply (simp_all add: diffs_def) |
412 apply (rule ext) |
401 apply (simp add: diffs_def mult_ac) |
413 apply (simp add: diffs_def) |
402 apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))") |
414 apply (case_tac n, simp_all add: r_neq_0) |
403 apply auto |
415 done |
404 prefer 2 |
416 have D: |
405 apply (rule ext) |
417 "(\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * |
406 apply (simp add: diffs_def) |
|
407 apply (case_tac "n", auto) |
|
408 txt{*23*} |
|
409 apply (drule abs_ge_zero [THEN order_le_less_trans]) |
|
410 apply (simp add: mult_ac) |
|
411 apply (drule abs_ge_zero [THEN order_le_less_trans]) |
|
412 apply (simp add: mult_ac) |
|
413 apply (drule diffs_equiv) |
|
414 apply (drule sums_summable) |
|
415 apply (subgoal_tac |
|
416 "summable |
|
417 (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) * |
|
418 r ^ (n - Suc 0)) = |
418 r ^ (n - Suc 0)) = |
419 summable |
419 (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))" |
420 (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))") |
420 apply (rule ext) |
421 apply simp |
421 apply (case_tac "n", simp) |
422 apply (rule_tac f = summable in arg_cong, rule ext) |
422 apply (case_tac "nat", simp) |
423 txt{*33*} |
423 apply (simp add: r_neq_0) |
424 apply (case_tac "n", auto) |
424 done |
425 apply (case_tac "nat", auto) |
425 show "summable (\<lambda>n. \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2))" |
426 apply (drule abs_ge_zero [THEN order_le_less_trans], auto) |
426 apply (cut_tac A) |
427 apply (drule abs_ge_zero [THEN order_le_less_trans]) |
427 apply (simp add: diffs_def mult_assoc [symmetric]) |
428 apply (simp add: mult_assoc) |
428 apply (simp only: abs_mult abs_real_of_nat_cancel B) |
429 apply (rule mult_left_mono) |
429 apply (drule diffs_equiv) |
430 prefer 2 apply arith |
430 apply (drule sums_summable) |
431 apply (subst add_commute) |
431 apply (simp only: diffs_def mult_ac) |
432 apply (simp (no_asm) add: mult_assoc [symmetric]) |
432 apply (simp only: C) |
433 apply (rule lemma_termdiff3) |
433 apply (drule diffs_equiv) |
434 apply (auto intro: abs_triangle_ineq [THEN order_trans], arith) |
434 apply (drule sums_summable) |
435 done |
435 apply (simp only: D) |
436 |
436 done |
437 ML {* fast_arith_split_limit := 9; *} (* FIXME *) |
437 next |
|
438 show "\<forall>h. 0 < \<bar>h\<bar> \<and> \<bar>h\<bar> < r + - \<bar>x\<bar> \<longrightarrow> (\<forall>n. \<bar>c n * (((x + h) ^ n - x ^ n) * inverse h - real n * x ^ (n - Suc 0))\<bar> \<le> \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2) * \<bar>h\<bar>)" |
|
439 proof (clarify) |
|
440 fix h::real and n::nat |
|
441 assume A: "0 < \<bar>h\<bar>" and B: "\<bar>h\<bar> < r + - \<bar>x\<bar>" |
|
442 from A have C: "h \<noteq> 0" by simp |
|
443 show "\<bar>c n * (((x + h) ^ n - x ^ n) * inverse h - real n * x ^ (n - Suc 0))\<bar> \<le> \<bar>c n\<bar> * real n * real (n - Suc 0) * r ^ (n - 2) * \<bar>h\<bar>" |
|
444 apply (cut_tac 3 B C) |
|
445 apply (subst abs_mult) |
|
446 apply (drule abs_ge_zero [THEN order_le_less_trans]) |
|
447 apply (simp only: mult_assoc) |
|
448 apply (rule mult_left_mono) |
|
449 prefer 2 apply arith |
|
450 apply (simp (no_asm) add: mult_assoc [symmetric]) |
|
451 apply (rule lemma_termdiff3) |
|
452 apply assumption |
|
453 apply (rule 3 [THEN order_less_imp_le]) |
|
454 apply (rule abs_triangle_ineq [THEN order_trans]) |
|
455 apply arith |
|
456 done |
|
457 qed |
|
458 qed |
|
459 qed |
438 |
460 |
439 lemma termdiffs: |
461 lemma termdiffs: |
440 "[| summable(%n. c(n) * (K ^ n)); |
462 "[| summable(%n. c(n) * (K ^ n)); |
441 summable(%n. (diffs c)(n) * (K ^ n)); |
463 summable(%n. (diffs c)(n) * (K ^ n)); |
442 summable(%n. (diffs(diffs c))(n) * (K ^ n)); |
464 summable(%n. (diffs(diffs c))(n) * (K ^ n)); |