src/HOL/Inequalities.thy
 author nipkow Fri May 01 20:25:57 2015 +0200 (2015-05-01) changeset 60167 9a97407488cd parent 60150 bd773c47ad0b child 60758 d8d85a8172b5 permissions -rw-r--r--
simplified statement and proof
 wenzelm@59720 ` 1` ```(* Title: HOL/Inequalities.thy ``` hoelzl@59712 ` 2` ``` Author: Tobias Nipkow ``` hoelzl@59712 ` 3` ``` Author: Johannes Hölzl ``` hoelzl@59712 ` 4` ```*) ``` hoelzl@59712 ` 5` hoelzl@59712 ` 6` ```theory Inequalities ``` hoelzl@59712 ` 7` ``` imports Real_Vector_Spaces ``` hoelzl@59712 ` 8` ```begin ``` hoelzl@59712 ` 9` nipkow@60167 ` 10` ```lemma Setsum_Icc_int: "(m::int) \ n \ \ {m..n} = (n*(n+1) - m*(m-1)) div 2" ``` nipkow@60167 ` 11` ```proof(induct i == "nat(n-m)" arbitrary: m n) ``` nipkow@60167 ` 12` ``` case 0 ``` nipkow@60167 ` 13` ``` hence "m = n" by arith ``` nipkow@60167 ` 14` ``` thus ?case by (simp add: algebra_simps) ``` nipkow@60167 ` 15` ```next ``` nipkow@60167 ` 16` ``` case (Suc i) ``` nipkow@60167 ` 17` ``` have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+ ``` nipkow@60167 ` 18` ``` have "\ {m..n} = \ {m..1+(n-1)}" by simp ``` nipkow@60167 ` 19` ``` also have "\ = \ {m..n-1} + n" using `m \ n` ``` nipkow@60167 ` 20` ``` by(subst atLeastAtMostPlus1_int_conv) simp_all ``` nipkow@60167 ` 21` ``` also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" ``` nipkow@60167 ` 22` ``` by(simp add: Suc(1)[OF 0]) ``` nipkow@60167 ` 23` ``` also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp ``` nipkow@60167 ` 24` ``` also have "\ = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps) ``` nipkow@60167 ` 25` ``` finally show ?case . ``` hoelzl@59712 ` 26` ```qed ``` hoelzl@59712 ` 27` hoelzl@59712 ` 28` ```lemma Setsum_Icc_nat: assumes "(m::nat) \ n" ``` hoelzl@59712 ` 29` ```shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" ``` hoelzl@59712 ` 30` ```proof - ``` hoelzl@59712 ` 31` ``` have "m*(m-1) \ n*(n + 1)" ``` hoelzl@59712 ` 32` ``` using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) ``` hoelzl@59712 ` 33` ``` hence "int(\ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms ``` nipkow@60167 ` 34` ``` by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult ``` hoelzl@59712 ` 35` ``` split: zdiff_int_split) ``` hoelzl@59712 ` 36` ``` thus ?thesis by simp ``` hoelzl@59712 ` 37` ```qed ``` hoelzl@59712 ` 38` hoelzl@59712 ` 39` ```lemma Setsum_Ico_nat: assumes "(m::nat) \ n" ``` hoelzl@59712 ` 40` ```shows "\ {m..{m..{m..n-1}" by simp ``` hoelzl@59712 ` 45` ``` also have "\ = (n*(n-1) - m*(m-1)) div 2" ``` hoelzl@59712 ` 46` ``` using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute) ``` hoelzl@59712 ` 47` ``` finally show ?thesis . ``` hoelzl@59712 ` 48` ```next ``` hoelzl@59712 ` 49` ``` assume "\ m < n" with assms show ?thesis by simp ``` hoelzl@59712 ` 50` ```qed ``` hoelzl@59712 ` 51` hoelzl@59712 ` 52` ```lemma Chebyshev_sum_upper: ``` hoelzl@59712 ` 53` ``` fixes a b::"nat \ 'a::linordered_idom" ``` hoelzl@59712 ` 54` ``` assumes "\i j. i \ j \ j < n \ a i \ a j" ``` hoelzl@59712 ` 55` ``` assumes "\i j. i \ j \ j < n \ b i \ b j" ``` hoelzl@59712 ` 56` ``` shows "of_nat n * (\k=0.. (\k=0..k=0..j=0..j=0..k=0..i j. a i * b j"] setsum_right_distrib) ``` hoelzl@59712 ` 62` ``` also ``` hoelzl@59712 ` 63` ``` { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" ``` hoelzl@59712 ` 65` ``` using assms by (cases "i \ j") (auto simp: algebra_simps) ``` hoelzl@59712 ` 66` ``` } hence "?S \ 0" ``` hoelzl@59712 ` 67` ``` by (auto intro!: setsum_nonpos simp: mult_le_0_iff) ``` hoelzl@59712 ` 68` ``` (auto simp: field_simps) ``` hoelzl@59712 ` 69` ``` finally show ?thesis by (simp add: algebra_simps) ``` hoelzl@59712 ` 70` ```qed ``` hoelzl@59712 ` 71` hoelzl@59712 ` 72` ```lemma Chebyshev_sum_upper_nat: ``` hoelzl@59712 ` 73` ``` fixes a b :: "nat \ nat" ``` hoelzl@59712 ` 74` ``` shows "(\i j. \ i\j; j \ a i \ a j) \ ``` hoelzl@59712 ` 75` ``` (\i j. \ i\j; j \ b i \ b j) \ ``` hoelzl@59712 ` 76` ``` n * (\i=0.. (\i=0..i=0..