equal
deleted
inserted
replaced
41 have "?int 0 (Suc n) = ?int 0 n + ?int n (Suc n)" |
41 have "?int 0 (Suc n) = ?int 0 n + ?int n (Suc n)" |
42 by (intro integral_combine[symmetric] int) simp_all |
42 by (intro integral_combine[symmetric] int) simp_all |
43 with Suc show ?case by simp |
43 with Suc show ?case by simp |
44 qed simp_all |
44 qed simp_all |
45 also have "... \<le> (\<Sum>k<n. integral {of_nat k..of_nat (Suc k)} (\<lambda>_::real. f (of_nat k)))" |
45 also have "... \<le> (\<Sum>k<n. integral {of_nat k..of_nat (Suc k)} (\<lambda>_::real. f (of_nat k)))" |
46 by (intro setsum_mono integral_le int) (auto intro: dec) |
46 by (intro sum_mono integral_le int) (auto intro: dec) |
47 also have "... = (\<Sum>k<n. f (of_nat k))" by simp |
47 also have "... = (\<Sum>k<n. f (of_nat k))" by simp |
48 also have "\<dots> - (\<Sum>k\<le>n. f (of_nat k)) = -(\<Sum>k\<in>{..n} - {..<n}. f (of_nat k))" |
48 also have "\<dots> - (\<Sum>k\<le>n. f (of_nat k)) = -(\<Sum>k\<in>{..n} - {..<n}. f (of_nat k))" |
49 by (subst setsum_diff) auto |
49 by (subst sum_diff) auto |
50 also have "\<dots> \<le> 0" by (auto intro!: setsum_nonneg nonneg) |
50 also have "\<dots> \<le> 0" by (auto intro!: sum_nonneg nonneg) |
51 finally show "sum_integral_diff_series n \<ge> 0" by simp |
51 finally show "sum_integral_diff_series n \<ge> 0" by simp |
52 qed |
52 qed |
53 |
53 |
54 lemma sum_integral_diff_series_antimono: |
54 lemma sum_integral_diff_series_antimono: |
55 assumes "m \<le> n" |
55 assumes "m \<le> n" |