src/HOL/Inequalities.thy
author haftmann
Mon Oct 30 13:18:41 2017 +0000 (20 months ago)
changeset 66936 cf8d8fc23891
parent 66804 3f9bb52082c4
permissions -rw-r--r--
tuned some proofs and added some lemmas
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 Chebyshev_sum_upper:
hoelzl@59712
    11
  fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
hoelzl@59712
    12
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
hoelzl@59712
    13
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
hoelzl@59712
    14
  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
    15
proof -
hoelzl@59712
    16
  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
hoelzl@59712
    17
  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"
wenzelm@63170
    18
    by (simp only: one_add_one[symmetric] algebra_simps)
haftmann@66804
    19
      (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left)
hoelzl@59712
    20
  also
hoelzl@59712
    21
  { fix i j::nat assume "i<n" "j<n"
hoelzl@59712
    22
    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
    23
      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
haftmann@62348
    24
  } then have "?S \<le> 0"
nipkow@64267
    25
    by (auto intro!: sum_nonpos simp: mult_le_0_iff)
hoelzl@59712
    26
  finally show ?thesis by (simp add: algebra_simps)
hoelzl@59712
    27
qed
hoelzl@59712
    28
hoelzl@59712
    29
lemma Chebyshev_sum_upper_nat:
hoelzl@59712
    30
  fixes a b :: "nat \<Rightarrow> nat"
hoelzl@59712
    31
  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
hoelzl@59712
    32
         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
hoelzl@59712
    33
    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
hoelzl@59712
    34
using Chebyshev_sum_upper[where 'a=real, of n a b]
nipkow@64267
    35
by (simp del: of_nat_mult of_nat_sum  add: of_nat_mult[symmetric] of_nat_sum[symmetric])
hoelzl@59712
    36
hoelzl@59712
    37
end