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 Sum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
|
11 proof(induct i == "nat(n-m)" arbitrary: m n) |
|
12 case 0 |
|
13 hence "m = n" by arith |
|
14 thus ?case by (simp add: algebra_simps) |
|
15 next |
|
16 case (Suc i) |
|
17 have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+ |
|
18 have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp |
|
19 also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close> |
|
20 by(subst atLeastAtMostPlus1_int_conv) simp_all |
|
21 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" |
|
22 by(simp add: Suc(1)[OF 0]) |
|
23 also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp |
|
24 also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) |
|
25 finally show ?case . |
|
26 qed |
|
27 |
|
28 lemma Sum_Icc_nat: assumes "(m::nat) \<le> n" |
|
29 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
|
30 proof - |
|
31 have "m*(m-1) \<le> n*(n + 1)" |
|
32 using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) |
|
33 hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms |
|
34 by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum |
|
35 split: zdiff_int_split) |
|
36 thus ?thesis |
|
37 using of_nat_eq_iff by blast |
|
38 qed |
|
39 |
|
40 lemma Sum_Ico_nat: assumes "(m::nat) \<le> n" |
|
41 shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2" |
|
42 proof cases |
|
43 assume "m < n" |
|
44 hence "{m..<n} = {m..n-1}" by auto |
|
45 hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp |
|
46 also have "\<dots> = (n*(n-1) - m*(m-1)) div 2" |
|
47 using assms \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute) |
|
48 finally show ?thesis . |
|
49 next |
|
50 assume "\<not> m < n" with assms show ?thesis by simp |
|
51 qed |
|
52 |
9 |
53 lemma Chebyshev_sum_upper: |
10 lemma Chebyshev_sum_upper: |
54 fixes a b::"nat \<Rightarrow> 'a::linordered_idom" |
11 fixes a b::"nat \<Rightarrow> 'a::linordered_idom" |
55 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j" |
12 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j" |
56 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j" |
13 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j" |