49 Goal "n < p ==> sumr 0 p f + \ |
49 Goal "n < p ==> sumr 0 p f + \ |
50 \ - sumr 0 n f = sumr n p f"; |
50 \ - sumr 0 n f = sumr n p f"; |
51 by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
51 by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
52 by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
52 by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
53 qed "sumr_split_add_minus"; |
53 qed "sumr_split_add_minus"; |
|
54 |
|
55 Goal "0 < n --> n < p --> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"; |
|
56 by (induct_tac "p" 1); |
|
57 by (auto_tac (claset() addSDs [CLAIM "[| m < Suc n; n <= m |] ==> m = n"], |
|
58 simpset())); |
|
59 qed_spec_mp "sumr_split_add2"; |
|
60 |
|
61 Goal "[| 0<n; n <= p |] ==> sumr (Suc 0) n f + sumr n p f = sumr (Suc 0) p f"; |
|
62 by (dtac le_imp_less_or_eq 1 THEN Auto_tac); |
|
63 by (blast_tac (claset() addIs [sumr_split_add2]) 1); |
|
64 qed "sumr_split_add3"; |
54 |
65 |
55 Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; |
66 Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; |
56 by (induct_tac "n" 1); |
67 by (induct_tac "n" 1); |
57 by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans, |
68 by (auto_tac (claset() addIs [abs_triangle_ineq RS order_trans, |
58 real_add_le_mono1], |
69 real_add_le_mono1], |
586 |
597 |
587 Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ |
598 Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ |
588 \ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; |
599 \ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; |
589 by (induct_tac "n" 1); |
600 by (induct_tac "n" 1); |
590 by (auto_tac (claset() addIs [DERIV_add], simpset())); |
601 by (auto_tac (claset() addIs [DERIV_add], simpset())); |
591 qed "DERIV_sumr"; |
602 qed_spec_mp "DERIV_sumr"; |