Theory Inequalities

(*  Title:     HOL/Inequalities.thy
    Author:    Tobias Nipkow
    Author:    Johannes Hölzl

theory Inequalities
  imports Real_Vector_Spaces

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..<n. a k * b k)  (k=0..<n. a k) * (k=0..<n. b k)"
proof -
  let ?S = "(j=0..<n. (k=0..<n. (a j - a k) * (b j - b k)))"
  have "2 * (of_nat n * (j=0..<n. (a j * b j)) - (j=0..<n. b j) * (k=0..<n. a k)) = ?S"
    by (simp only: one_add_one[symmetric] algebra_simps)
      (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "λi j. a i * b j"] sum_distrib_left)
  { fix i j::nat assume "i<n" "j<n"
    hence "a i - a j  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)
  } then have "?S  0"
    by (auto intro!: sum_nonpos simp: mult_le_0_iff)
  finally show ?thesis by (simp add: algebra_simps)

lemma Chebyshev_sum_upper_nat:
  fixes a b :: "nat  nat"
  shows "(i j.  ij; j<n   a i  a j) 
         (i j.  ij; j<n   b i  b j) 
    n * (i=0..<n. a i * b i)  (i=0..<n. a i) * (i=0..<n. b i)"
using Chebyshev_sum_upper[where 'a=real, of n a b]
by (simp del: of_nat_mult of_nat_sum  add: of_nat_mult[symmetric] of_nat_sum[symmetric])