src/HOL/Inequalities.thy
author paulson <lp15@cam.ac.uk>
Fri, 13 Nov 2015 12:27:13 +0000
changeset 61649 268d88ec9087
parent 61609 77b453bd616f
child 61694 6571c78c9667
permissions -rw-r--r--
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 59712
diff changeset
     1
(*  Title:     HOL/Inequalities.thy
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     2
    Author:    Tobias Nipkow
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     3
    Author:    Johannes Hölzl
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     4
*)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     5
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     6
theory Inequalities
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     7
  imports Real_Vector_Spaces
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     8
begin
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     9
60167
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    10
lemma Setsum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    11
proof(induct i == "nat(n-m)" arbitrary: m n)
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    12
  case 0
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    13
  hence "m = n" by arith
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    14
  thus ?case by (simp add: algebra_simps)
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    15
next
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    16
  case (Suc i)
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    17
  have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    18
  have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60167
diff changeset
    19
  also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
60167
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    20
    by(subst atLeastAtMostPlus1_int_conv) simp_all
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    21
  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    22
    by(simp add: Suc(1)[OF 0])
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    23
  also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    24
  also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
9a97407488cd simplified statement and proof
nipkow
parents: 60150
diff changeset
    25
  finally show ?case .
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    26
qed
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    27
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    28
lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    29
shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    30
proof -
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    31
  have "m*(m-1) \<le> n*(n + 1)"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    32
   using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    33
  hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60758
diff changeset
    34
    by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60758
diff changeset
    35
          split: zdiff_int_split)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60758
diff changeset
    36
  thus ?thesis
61649
268d88ec9087 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents: 61609
diff changeset
    37
    using int_int_eq by blast
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    38
qed
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    39
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    40
lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    41
shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    42
proof cases
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    43
  assume "m < n"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    44
  hence "{m..<n} = {m..n-1}" by auto
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    45
  hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    46
  also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60167
diff changeset
    47
    using assms \<open>m < n\<close> by (simp add: Setsum_Icc_nat mult.commute)
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    48
  finally show ?thesis .
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    49
next
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    50
  assume "\<not> m < n" with assms show ?thesis by simp
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    51
qed
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    52
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    53
lemma Chebyshev_sum_upper:
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    54
  fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    55
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    56
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    57
  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)"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    58
proof -
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    59
  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    60
  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"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    61
    unfolding one_add_one[symmetric] algebra_simps
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    62
    by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    63
  also
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    64
  { fix i j::nat assume "i<n" "j<n"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    65
    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"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    66
      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    67
  } hence "?S \<le> 0"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    68
    by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    69
       (auto simp: field_simps)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    70
  finally show ?thesis by (simp add: algebra_simps)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    71
qed
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    72
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    73
lemma Chebyshev_sum_upper_nat:
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    74
  fixes a b :: "nat \<Rightarrow> nat"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    75
  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    76
         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    77
    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    78
using Chebyshev_sum_upper[where 'a=real, of n a b]
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60758
diff changeset
    79
by (simp del: of_nat_mult of_nat_setsum  add: of_nat_mult[symmetric] of_nat_setsum[symmetric])
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    80
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    81
end