src/HOL/Inequalities.thy
author paulson <lp15@cam.ac.uk>
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) \<noteq> 0 \<Longrightarrow>
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 \<le> m" and "(m::int) \<le> n"
hoelzl@59712
    15
shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
hoelzl@59712
    16
proof-
hoelzl@59712
    17
  { fix k::int assume "k\<ge>0"
hoelzl@59712
    18
    hence "\<Sum> {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\<ge>0` by auto
hoelzl@59712
    22
  hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{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 "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
hoelzl@59712
    26
  also have "\<dots> = 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 "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>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)) \<and> 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) \<le> n"
hoelzl@59712
    37
shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
hoelzl@59712
    38
proof -
hoelzl@59712
    39
  have "m*(m-1) \<le> 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(\<Sum> {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) \<le> n"
hoelzl@59712
    48
shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
hoelzl@59712
    49
proof cases
hoelzl@59712
    50
  assume "m < n"
hoelzl@59712
    51
  hence "{m..<n} = {m..n-1}" by auto
hoelzl@59712
    52
  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
hoelzl@59712
    53
  also have "\<dots> = (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 "\<not> 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 \<Rightarrow> 'a::linordered_idom"
hoelzl@59712
    62
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
hoelzl@59712
    63
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
hoelzl@59712
    64
  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)"
hoelzl@59712
    65
proof -
hoelzl@59712
    66
  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
hoelzl@59712
    67
  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"
hoelzl@59712
    68
    unfolding one_add_one[symmetric] algebra_simps
hoelzl@59712
    69
    by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
hoelzl@59712
    70
  also
hoelzl@59712
    71
  { fix i j::nat assume "i<n" "j<n"
hoelzl@59712
    72
    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"
hoelzl@59712
    73
      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
hoelzl@59712
    74
  } hence "?S \<le> 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 \<Rightarrow> nat"
hoelzl@59712
    82
  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
hoelzl@59712
    83
         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
hoelzl@59712
    84
    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
hoelzl@59712
    85
using Chebyshev_sum_upper[where 'a=real, of n a b]
hoelzl@59712
    86
by (simp del: real_of_nat_mult real_of_nat_setsum
hoelzl@59712
    87
  add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
hoelzl@59712
    88
hoelzl@59712
    89
end