# HG changeset patch # User hoelzl # Date 1426513954 -3600 # Node ID 6c013328b885371f0ba06f49c18f2c4475337c31 # Parent 5b0003211207747af7eae48ada7e0fddb4c18960 add inequalities (move from AFP/Amortized_Complexity) diff -r 5b0003211207 -r 6c013328b885 src/HOL/Inequalities.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Inequalities.thy Mon Mar 16 14:52:34 2015 +0100 @@ -0,0 +1,97 @@ +(* Title: Inequalities + Author: Tobias Nipkow + Author: Johannes Hölzl +*) + +theory Inequalities + imports Real_Vector_Spaces +begin + +lemma setsum_triangle_reindex: + fixes n :: nat + shows "(\(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" + apply (simp add: setsum.Sigma) + apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) + apply auto + done + +lemma gauss_sum_div2: "(2::'a::semiring_div) \ 0 \ + setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)" +using gauss_sum[where n=n and 'a = 'a,symmetric] by auto + +lemma Setsum_Icc_int: assumes "0 \ m" and "(m::int) \ n" +shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" +proof- + { fix k::int assume "k\0" + hence "\ {1..k::int} = k * (k+1) div 2" + by (rule gauss_sum_div2[where 'a = int, transferred]) simp + } note 1 = this + have "{m..n} = {0..n} - {0..m-1}" using `m\0` by auto + hence "\{m..n} = \{0..n} - \{0..m-1}" using assms + by (force intro!: setsum_diff) + also have "{0..n} = {0} Un {1..n}" using assms by auto + also have "\({0} \ {1..n}) = \{1..n}" by(simp add: setsum.union_disjoint) + also have "\ = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]]) + also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})" + using assms by auto + also have "\ \ = m*(m-1) div 2" using `m\0` by(simp add: 1 mult.commute) + also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2" + apply(subgoal_tac "even(n*(n+1)) \ even(m*(m-1))") + by (auto (*simp: even_def[symmetric]*)) + finally show ?thesis . +qed + +lemma Setsum_Icc_nat: assumes "(m::nat) \ n" +shows "\ {m..n} = (n*(n+1) - m*(m-1)) div 2" +proof - + have "m*(m-1) \ n*(n + 1)" + using assms by (meson diff_le_self order_trans le_add1 mult_le_mono) + hence "int(\ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms + by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult + split: zdiff_int_split) + thus ?thesis by simp +qed + +lemma Setsum_Ico_nat: assumes "(m::nat) \ n" +shows "\ {m..{m..{m..n-1}" by simp + also have "\ = (n*(n-1) - m*(m-1)) div 2" + using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute) + finally show ?thesis . +next + assume "\ m < n" with assms show ?thesis by simp +qed + +lemma Chebyshev_sum_upper: + fixes a b::"nat \ 'a::linordered_idom" + assumes "\i j. i \ j \ j < n \ a i \ a j" + assumes "\i j. i \ j \ j < n \ b i \ b j" + 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) + also + { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" + using assms by (cases "i \ j") (auto simp: algebra_simps) + } hence "?S \ 0" + by (auto intro!: setsum_nonpos simp: mult_le_0_iff) + (auto simp: field_simps) + finally show ?thesis by (simp add: algebra_simps) +qed + +lemma Chebyshev_sum_upper_nat: + fixes a b :: "nat \ nat" + shows "(\i j. \ i\j; j \ a i \ a j) \ + (\i j. \ i\j; j \ b i \ b j) \ + n * (\i=0.. (\i=0..i=0..(i,j)\{(i,j). i+j < n}. f i j) = (\ki\k. f i (k - i))" - apply (simp add: setsum.Sigma) - apply (rule setsum.reindex_bij_witness[where j="\(i, j). (i+j, i)" and i="\(k, i). (i, k - i)"]) - apply auto - done - lemma Cauchy_product_sums: fixes a b :: "nat \ 'a::{real_normed_algebra,banach}" assumes a: "summable (\k. norm (a k))"