src/HOL/Inequalities.thy
changeset 59712 6c013328b885
child 59720 f893472fff31
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Inequalities.thy	Mon Mar 16 14:52:34 2015 +0100
     1.3 @@ -0,0 +1,97 @@
     1.4 +(*  Title:     Inequalities
     1.5 +    Author:    Tobias Nipkow
     1.6 +    Author:    Johannes Hölzl
     1.7 +*)
     1.8 +
     1.9 +theory Inequalities
    1.10 +  imports Real_Vector_Spaces
    1.11 +begin
    1.12 +
    1.13 +lemma setsum_triangle_reindex:
    1.14 +  fixes n :: nat
    1.15 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
    1.16 +  apply (simp add: setsum.Sigma)
    1.17 +  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
    1.18 +  apply auto
    1.19 +  done
    1.20 +
    1.21 +lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
    1.22 +  setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
    1.23 +using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
    1.24 +
    1.25 +lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n"
    1.26 +shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    1.27 +proof-
    1.28 +  { fix k::int assume "k\<ge>0"
    1.29 +    hence "\<Sum> {1..k::int} = k * (k+1) div 2"
    1.30 +      by (rule gauss_sum_div2[where 'a = int, transferred]) simp
    1.31 +  } note 1 = this
    1.32 +  have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto
    1.33 +  hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms
    1.34 +    by (force intro!: setsum_diff)
    1.35 +  also have "{0..n} = {0} Un {1..n}" using assms by auto
    1.36 +  also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
    1.37 +  also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]])
    1.38 +  also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})"
    1.39 +    using assms by auto
    1.40 +  also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute)
    1.41 +  also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2"
    1.42 +    apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))")
    1.43 +    by (auto (*simp: even_def[symmetric]*))
    1.44 +  finally show ?thesis .
    1.45 +qed
    1.46 +
    1.47 +lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
    1.48 +shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
    1.49 +proof -
    1.50 +  have "m*(m-1) \<le> n*(n + 1)"
    1.51 +   using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
    1.52 +  hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
    1.53 +    by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult
    1.54 +      split: zdiff_int_split)
    1.55 +  thus ?thesis by simp
    1.56 +qed
    1.57 +
    1.58 +lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
    1.59 +shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
    1.60 +proof cases
    1.61 +  assume "m < n"
    1.62 +  hence "{m..<n} = {m..n-1}" by auto
    1.63 +  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
    1.64 +  also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
    1.65 +    using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute)
    1.66 +  finally show ?thesis .
    1.67 +next
    1.68 +  assume "\<not> m < n" with assms show ?thesis by simp
    1.69 +qed
    1.70 +
    1.71 +lemma Chebyshev_sum_upper:
    1.72 +  fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
    1.73 +  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
    1.74 +  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
    1.75 +  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)"
    1.76 +proof -
    1.77 +  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
    1.78 +  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"
    1.79 +    unfolding one_add_one[symmetric] algebra_simps
    1.80 +    by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
    1.81 +  also
    1.82 +  { fix i j::nat assume "i<n" "j<n"
    1.83 +    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"
    1.84 +      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
    1.85 +  } hence "?S \<le> 0"
    1.86 +    by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
    1.87 +       (auto simp: field_simps)
    1.88 +  finally show ?thesis by (simp add: algebra_simps)
    1.89 +qed
    1.90 +
    1.91 +lemma Chebyshev_sum_upper_nat:
    1.92 +  fixes a b :: "nat \<Rightarrow> nat"
    1.93 +  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
    1.94 +         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
    1.95 +    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
    1.96 +using Chebyshev_sum_upper[where 'a=real, of n a b]
    1.97 +by (simp del: real_of_nat_mult real_of_nat_setsum
    1.98 +  add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
    1.99 +
   1.100 +end