src/HOL/Inequalities.thy
 author wenzelm Fri Oct 27 13:50:08 2017 +0200 (21 months ago) changeset 66924 b4d4027f743b parent 66804 3f9bb52082c4 child 66936 cf8d8fc23891 permissions -rw-r--r--
more permissive;
 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@64267 ` 10` ```lemma Sum_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 ``` wenzelm@60758 ` 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` nipkow@64267 ` 28` ```lemma Sum_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@64267 ` 34` ``` by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum ``` lp15@61609 ` 35` ``` split: zdiff_int_split) ``` lp15@61609 ` 36` ``` thus ?thesis ``` lp15@61694 ` 37` ``` using of_nat_eq_iff by blast ``` hoelzl@59712 ` 38` ```qed ``` hoelzl@59712 ` 39` nipkow@64267 ` 40` ```lemma Sum_Ico_nat: assumes "(m::nat) \ n" ``` hoelzl@59712 ` 41` ```shows "\ {m..{m..{m..n-1}" by simp ``` hoelzl@59712 ` 46` ``` also have "\ = (n*(n-1) - m*(m-1)) div 2" ``` nipkow@64267 ` 47` ``` using assms \m < n\ by (simp add: Sum_Icc_nat mult.commute) ``` hoelzl@59712 ` 48` ``` finally show ?thesis . ``` hoelzl@59712 ` 49` ```next ``` hoelzl@59712 ` 50` ``` assume "\ m < n" with assms show ?thesis by simp ``` hoelzl@59712 ` 51` ```qed ``` hoelzl@59712 ` 52` hoelzl@59712 ` 53` ```lemma Chebyshev_sum_upper: ``` hoelzl@59712 ` 54` ``` fixes a b::"nat \ 'a::linordered_idom" ``` hoelzl@59712 ` 55` ``` assumes "\i j. i \ j \ j < n \ a i \ a j" ``` hoelzl@59712 ` 56` ``` assumes "\i j. i \ j \ j < n \ b i \ b j" ``` hoelzl@59712 ` 57` ``` shows "of_nat n * (\k=0.. (\k=0..k=0..j=0..j=0..k=0..i j. a i * b j"] sum_distrib_left) ``` hoelzl@59712 ` 63` ``` also ``` hoelzl@59712 ` 64` ``` { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" ``` hoelzl@59712 ` 66` ``` using assms by (cases "i \ j") (auto simp: algebra_simps) ``` haftmann@62348 ` 67` ``` } then have "?S \ 0" ``` nipkow@64267 ` 68` ``` by (auto intro!: sum_nonpos simp: mult_le_0_iff) ``` 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..