equal
deleted
inserted
replaced
379 apply (subst mult_assoc [symmetric], subst power_add [symmetric]) |
379 apply (subst mult_assoc [symmetric], subst power_add [symmetric]) |
380 apply (simp add: mult_ac) |
380 apply (simp add: mult_ac) |
381 done |
381 done |
382 |
382 |
383 lemma real_setsum_nat_ivl_bounded2: |
383 lemma real_setsum_nat_ivl_bounded2: |
384 fixes K :: "'a::ordered_semidom" |
384 fixes K :: "'a::linordered_semidom" |
385 assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" |
385 assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" |
386 assumes K: "0 \<le> K" |
386 assumes K: "0 \<le> K" |
387 shows "setsum f {0..<n-k} \<le> of_nat n * K" |
387 shows "setsum f {0..<n-k} \<le> of_nat n * K" |
388 apply (rule order_trans [OF setsum_mono]) |
388 apply (rule order_trans [OF setsum_mono]) |
389 apply (rule f, simp) |
389 apply (rule f, simp) |