author  haftmann 
Wed, 17 Feb 2016 21:51:57 +0100  
changeset 62348  9a5f43dac883 
parent 61762  d50b993b4fb9 
child 63170  eae6549dbea2 
permissions  rwrr 
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 

60167  10 
lemma Setsum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1)  m*(m1)) div 2" 
11 
proof(induct i == "nat(nm)" 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((n1)  m)" "m \<le> n1" using Suc(2,3) by arith+ 

18 
have "\<Sum> {m..n} = \<Sum> {m..1+(n1)}" by simp 

60758  19 
also have "\<dots> = \<Sum> {m..n1} + n" using \<open>m \<le> n\<close> 
60167  20 
by(subst atLeastAtMostPlus1_int_conv) simp_all 
21 
also have "\<dots> = ((n1)*(n1+1)  m*(m1)) div 2 + n" 

22 
by(simp add: Suc(1)[OF 0]) 

23 
also have "\<dots> = ((n1)*(n1+1)  m*(m1) + 2*n) div 2" by simp 

24 
also have "\<dots> = (n*(n+1)  m*(m1)) div 2" by(simp add: algebra_simps) 

25 
finally show ?case . 

59712  26 
qed 
27 

28 
lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n" 

29 
shows "\<Sum> {m..n} = (n*(n+1)  m*(m1)) div 2" 

30 
proof  

31 
have "m*(m1) \<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*(m1)) div 2)" using assms 

62348  34 
by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_setsum 
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 

40 
lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n" 

41 
shows "\<Sum> {m..<n} = (n*(n1)  m*(m1)) div 2" 

42 
proof cases 

43 
assume "m < n" 

44 
hence "{m..<n} = {m..n1}" by auto 

45 
hence "\<Sum>{m..<n} = \<Sum>{m..n1}" by simp 

46 
also have "\<dots> = (n*(n1)  m*(m1)) div 2" 

60758  47 
using assms \<open>m < n\<close> by (simp add: Setsum_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" 

61 
unfolding one_add_one[symmetric] algebra_simps 

62 
by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib) 

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" 
59712  68 
by (auto intro!: setsum_nonpos simp: mult_le_0_iff) 
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] 

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

78 
by (simp del: of_nat_mult of_nat_setsum add: of_nat_mult[symmetric] of_nat_setsum[symmetric]) 
59712  79 

80 
end 