14 begin |
14 begin |
15 |
15 |
16 declare atLeastLessThan_iff[iff] |
16 declare atLeastLessThan_iff[iff] |
17 declare setsum_op_ivl_Suc[simp] |
17 declare setsum_op_ivl_Suc[simp] |
18 |
18 |
19 constdefs |
19 definition |
20 sums :: "(nat => real) => real => bool" (infixr "sums" 80) |
20 sums :: "(nat => real) => real => bool" (infixr "sums" 80) |
21 "f sums s == (%n. setsum f {0..<n}) ----> s" |
21 "f sums s = (%n. setsum f {0..<n}) ----> s" |
22 |
22 |
23 summable :: "(nat=>real) => bool" |
23 summable :: "(nat=>real) => bool" |
24 "summable f == (\<exists>s. f sums s)" |
24 "summable f = (\<exists>s. f sums s)" |
25 |
25 |
26 suminf :: "(nat=>real) => real" |
26 suminf :: "(nat=>real) => real" |
27 "suminf f == SOME s. f sums s" |
27 "suminf f = (SOME s. f sums s)" |
28 |
28 |
29 syntax |
29 syntax |
30 "_suminf" :: "idt => real => real" ("\<Sum>_. _" [0, 10] 10) |
30 "_suminf" :: "idt => real => real" ("\<Sum>_. _" [0, 10] 10) |
31 translations |
31 translations |
32 "\<Sum>i. b" == "suminf (%i. b)" |
32 "\<Sum>i. b" == "suminf (%i. b)" |
498 --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" |
498 --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)" |
499 apply (induct "n") |
499 apply (induct "n") |
500 apply (auto intro: DERIV_add) |
500 apply (auto intro: DERIV_add) |
501 done |
501 done |
502 |
502 |
503 ML |
|
504 {* |
|
505 val sums_def = thm"sums_def"; |
|
506 val summable_def = thm"summable_def"; |
|
507 val suminf_def = thm"suminf_def"; |
|
508 |
|
509 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; |
|
510 val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero"; |
|
511 val sumr_group = thm "sumr_group"; |
|
512 val sums_summable = thm "sums_summable"; |
|
513 val summable_sums = thm "summable_sums"; |
|
514 val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf"; |
|
515 val sums_unique = thm "sums_unique"; |
|
516 val series_zero = thm "series_zero"; |
|
517 val sums_mult = thm "sums_mult"; |
|
518 val sums_divide = thm "sums_divide"; |
|
519 val sums_diff = thm "sums_diff"; |
|
520 val suminf_mult = thm "suminf_mult"; |
|
521 val suminf_mult2 = thm "suminf_mult2"; |
|
522 val suminf_diff = thm "suminf_diff"; |
|
523 val sums_minus = thm "sums_minus"; |
|
524 val sums_group = thm "sums_group"; |
|
525 val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma"; |
|
526 val sumr_pos_lt_pair = thm "sumr_pos_lt_pair"; |
|
527 val series_pos_le = thm "series_pos_le"; |
|
528 val series_pos_less = thm "series_pos_less"; |
|
529 val sumr_geometric = thm "sumr_geometric"; |
|
530 val geometric_sums = thm "geometric_sums"; |
|
531 val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff"; |
|
532 val summable_Cauchy = thm "summable_Cauchy"; |
|
533 val summable_comparison_test = thm "summable_comparison_test"; |
|
534 val summable_rabs_comparison_test = thm "summable_rabs_comparison_test"; |
|
535 val summable_le = thm "summable_le"; |
|
536 val summable_le2 = thm "summable_le2"; |
|
537 val summable_rabs_cancel = thm "summable_rabs_cancel"; |
|
538 val summable_rabs = thm "summable_rabs"; |
|
539 val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma"; |
|
540 val le_Suc_ex = thm "le_Suc_ex"; |
|
541 val le_Suc_ex_iff = thm "le_Suc_ex_iff"; |
|
542 val ratio_test_lemma2 = thm "ratio_test_lemma2"; |
|
543 val ratio_test = thm "ratio_test"; |
|
544 val DERIV_sumr = thm "DERIV_sumr"; |
|
545 *} |
|
546 |
|
547 end |
503 end |