author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 66804 | 3f9bb52082c4 |
child 66936 | cf8d8fc23891 |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: HOL/Inequalities.thy |
59712 | 2 |
Author: Tobias Nipkow |
3 |
Author: Johannes Hölzl |
|
4 |
*) |
|
5 |
||
6 |
theory Inequalities |
|
7 |
imports Real_Vector_Spaces |
|
8 |
begin |
|
9 |
||
64267 | 10 |
lemma Sum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2" |
60167 | 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 |
|
60758 | 19 |
also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close> |
60167 | 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 . |
|
59712 | 26 |
qed |
27 |
||
64267 | 28 |
lemma Sum_Icc_nat: assumes "(m::nat) \<le> n" |
59712 | 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 |
|
64267 | 34 |
by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60758
diff
changeset
|
35 |
split: zdiff_int_split) |
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
60758
diff
changeset
|
36 |
thus ?thesis |
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61649
diff
changeset
|
37 |
using of_nat_eq_iff by blast |
59712 | 38 |
qed |
39 |
||
64267 | 40 |
lemma Sum_Ico_nat: assumes "(m::nat) \<le> n" |
59712 | 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" |
|
64267 | 47 |
using assms \<open>m < n\<close> by (simp add: Sum_Icc_nat mult.commute) |
59712 | 48 |
finally show ?thesis . |
49 |
next |
|
50 |
assume "\<not> m < n" with assms show ?thesis by simp |
|
51 |
qed |
|
52 |
||
53 |
lemma Chebyshev_sum_upper: |
|
54 |
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" |
|
56 |
assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j" |
|
57 |
shows "of_nat n * (\<Sum>k=0..<n. a k * b k) \<le> (\<Sum>k=0..<n. a k) * (\<Sum>k=0..<n. b k)" |
|
58 |
proof - |
|
59 |
let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))" |
|
60 |
have "2 * (of_nat n * (\<Sum>j=0..<n. (a j * b j)) - (\<Sum>j=0..<n. b j) * (\<Sum>k=0..<n. a k)) = ?S" |
|
63170 | 61 |
by (simp only: one_add_one[symmetric] algebra_simps) |
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
64267
diff
changeset
|
62 |
(simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left) |
59712 | 63 |
also |
64 |
{ fix i j::nat assume "i<n" "j<n" |
|
65 |
hence "a i - a j \<le> 0 \<and> b i - b j \<ge> 0 \<or> a i - a j \<ge> 0 \<and> b i - b j \<le> 0" |
|
66 |
using assms by (cases "i \<le> j") (auto simp: algebra_simps) |
|
62348 | 67 |
} then have "?S \<le> 0" |
64267 | 68 |
by (auto intro!: sum_nonpos simp: mult_le_0_iff) |
59712 | 69 |
finally show ?thesis by (simp add: algebra_simps) |
70 |
qed |
|
71 |
||
72 |
lemma Chebyshev_sum_upper_nat: |
|
73 |
fixes a b :: "nat \<Rightarrow> nat" |
|
74 |
shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow> |
|
75 |
(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow> |
|
76 |
n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)" |
|
77 |
using Chebyshev_sum_upper[where 'a=real, of n a b] |
|
64267 | 78 |
by (simp del: of_nat_mult of_nat_sum add: of_nat_mult[symmetric] of_nat_sum[symmetric]) |
59712 | 79 |
|
80 |
end |