equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 theory Inequalities |
6 theory Inequalities |
7 imports Real_Vector_Spaces |
7 imports Real_Vector_Spaces |
8 begin |
8 begin |
9 |
|
10 lemma setsum_triangle_reindex: |
|
11 fixes n :: nat |
|
12 shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))" |
|
13 apply (simp add: setsum.Sigma) |
|
14 apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"]) |
|
15 apply auto |
|
16 done |
|
17 |
9 |
18 lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow> |
10 lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow> |
19 setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" |
11 setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" |
20 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto |
12 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto |
21 |
13 |