src/HOL/Inequalities.thy
 author paulson Tue Apr 28 16:23:38 2015 +0100 (2015-04-28) changeset 60150 bd773c47ad0b parent 59720 f893472fff31 child 60167 9a97407488cd permissions -rw-r--r--
New material about complex transcendental functions (especially Ln, Arg) and polynomials
 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 hoelzl@59712 10 lemma gauss_sum_div2: "(2::'a::semiring_div) \ 0 \ hoelzl@59712 11 setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" hoelzl@59712 12 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto hoelzl@59712 13 hoelzl@59712 14 lemma Setsum_Icc_int: assumes "0 \ m" and "(m::int) \ n" hoelzl@59712 15 shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" hoelzl@59712 16 proof- hoelzl@59712 17 { fix k::int assume "k\0" hoelzl@59712 18 hence "\ {1..k::int} = k * (k+1) div 2" hoelzl@59712 19 by (rule gauss_sum_div2[where 'a = int, transferred]) simp hoelzl@59712 20 } note 1 = this hoelzl@59712 21 have "{m..n} = {0..n} - {0..m-1}" using `m\0` by auto hoelzl@59712 22 hence "\{m..n} = \{0..n} - \{0..m-1}" using assms hoelzl@59712 23 by (force intro!: setsum_diff) hoelzl@59712 24 also have "{0..n} = {0} Un {1..n}" using assms by auto hoelzl@59712 25 also have "\({0} \ {1..n}) = \{1..n}" by(simp add: setsum.union_disjoint) hoelzl@59712 26 also have "\ = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]]) hoelzl@59712 27 also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})" hoelzl@59712 28 using assms by auto hoelzl@59712 29 also have "\ \ = m*(m-1) div 2" using `m\0` by(simp add: 1 mult.commute) hoelzl@59712 30 also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2" hoelzl@59712 31 apply(subgoal_tac "even(n*(n+1)) \ even(m*(m-1))") hoelzl@59712 32 by (auto (*simp: even_def[symmetric]*)) hoelzl@59712 33 finally show ?thesis . hoelzl@59712 34 qed hoelzl@59712 35 hoelzl@59712 36 lemma Setsum_Icc_nat: assumes "(m::nat) \ n" hoelzl@59712 37 shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" hoelzl@59712 38 proof - hoelzl@59712 39 have "m*(m-1) \ n*(n + 1)" hoelzl@59712 40 using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) hoelzl@59712 41 hence "int(\ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms hoelzl@59712 42 by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult hoelzl@59712 43 split: zdiff_int_split) hoelzl@59712 44 thus ?thesis by simp hoelzl@59712 45 qed hoelzl@59712 46 hoelzl@59712 47 lemma Setsum_Ico_nat: assumes "(m::nat) \ n" hoelzl@59712 48 shows "\ {m..{m..{m..n-1}" by simp hoelzl@59712 53 also have "\ = (n*(n-1) - m*(m-1)) div 2" hoelzl@59712 54 using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute) hoelzl@59712 55 finally show ?thesis . hoelzl@59712 56 next hoelzl@59712 57 assume "\ m < n" with assms show ?thesis by simp hoelzl@59712 58 qed hoelzl@59712 59 hoelzl@59712 60 lemma Chebyshev_sum_upper: hoelzl@59712 61 fixes a b::"nat \ 'a::linordered_idom" hoelzl@59712 62 assumes "\i j. i \ j \ j < n \ a i \ a j" hoelzl@59712 63 assumes "\i j. i \ j \ j < n \ b i \ b j" hoelzl@59712 64 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 70 also hoelzl@59712 71 { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" hoelzl@59712 73 using assms by (cases "i \ j") (auto simp: algebra_simps) hoelzl@59712 74 } hence "?S \ 0" hoelzl@59712 75 by (auto intro!: setsum_nonpos simp: mult_le_0_iff) hoelzl@59712 76 (auto simp: field_simps) hoelzl@59712 77 finally show ?thesis by (simp add: algebra_simps) hoelzl@59712 78 qed hoelzl@59712 79 hoelzl@59712 80 lemma Chebyshev_sum_upper_nat: hoelzl@59712 81 fixes a b :: "nat \ nat" hoelzl@59712 82 shows "(\i j. \ i\j; j \ a i \ a j) \ hoelzl@59712 83 (\i j. \ i\j; j \ b i \ b j) \ hoelzl@59712 84 n * (\i=0.. (\i=0..i=0..