5 |
5 |
6 theory Inequalities |
6 theory Inequalities |
7 imports Real_Vector_Spaces |
7 imports Real_Vector_Spaces |
8 begin |
8 begin |
9 |
9 |
10 lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow> |
10 lemma Setsum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
11 setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" |
11 proof(induct i == "nat(n-m)" arbitrary: m n) |
12 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto |
12 case 0 |
13 |
13 hence "m = n" by arith |
14 lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n" |
14 thus ?case by (simp add: algebra_simps) |
15 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
15 next |
16 proof- |
16 case (Suc i) |
17 { fix k::int assume "k\<ge>0" |
17 have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+ |
18 hence "\<Sum> {1..k::int} = k * (k+1) div 2" |
18 have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp |
19 by (rule gauss_sum_div2[where 'a = int, transferred]) simp |
19 also have "\<dots> = \<Sum> {m..n-1} + n" using `m \<le> n` |
20 } note 1 = this |
20 by(subst atLeastAtMostPlus1_int_conv) simp_all |
21 have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto |
21 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" |
22 hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms |
22 by(simp add: Suc(1)[OF 0]) |
23 by (force intro!: setsum_diff) |
23 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp |
24 also have "{0..n} = {0} Un {1..n}" using assms by auto |
24 also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) |
25 also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint) |
25 finally show ?case . |
26 also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]]) |
|
27 also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})" |
|
28 using assms by auto |
|
29 also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute) |
|
30 also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2" |
|
31 apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))") |
|
32 by (auto (*simp: even_def[symmetric]*)) |
|
33 finally show ?thesis . |
|
34 qed |
26 qed |
35 |
27 |
36 lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n" |
28 lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n" |
37 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
29 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
38 proof - |
30 proof - |
39 have "m*(m-1) \<le> n*(n + 1)" |
31 have "m*(m-1) \<le> n*(n + 1)" |
40 using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) |
32 using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) |
41 hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms |
33 hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms |
42 by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult |
34 by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult |
43 split: zdiff_int_split) |
35 split: zdiff_int_split) |
44 thus ?thesis by simp |
36 thus ?thesis by simp |
45 qed |
37 qed |
46 |
38 |
47 lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n" |
39 lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n" |