# Theory Inequalities

theory Inequalities
imports Real_Vector_Spaces
```(*  Title:     HOL/Inequalities.thy
Author:    Tobias Nipkow
Author:    Johannes Hölzl
*)

theory Inequalities
imports Real_Vector_Spaces
begin

lemma Sum_Icc_int: "(m::int) ≤ n ⟹ ∑ {m..n} = (n*(n+1) - m*(m-1)) div 2"
proof(induct i == "nat(n-m)" arbitrary: m n)
case 0
hence "m = n" by arith
thus ?case by (simp add: algebra_simps)
next
case (Suc i)
have 0: "i = nat((n-1) - m)" "m ≤ n-1" using Suc(2,3) by arith+
have "∑ {m..n} = ∑ {m..1+(n-1)}" by simp
also have "… = ∑ {m..n-1} + n" using ‹m ≤ n›
by(subst atLeastAtMostPlus1_int_conv) simp_all
also have "… = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
also have "… = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
also have "… = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
finally show ?case .
qed

lemma Sum_Icc_nat: assumes "(m::nat) ≤ n"
shows "∑ {m..n} = (n*(n+1) - m*(m-1)) div 2"
proof -
have "m*(m-1) ≤ n*(n + 1)"
using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
hence "int(∑ {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
by (auto simp: Sum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_sum
split: zdiff_int_split)
thus ?thesis
using of_nat_eq_iff by blast
qed

lemma Sum_Ico_nat: assumes "(m::nat) ≤ n"
shows "∑ {m..<n} = (n*(n-1) - m*(m-1)) div 2"
proof cases
assume "m < n"
hence "{m..<n} = {m..n-1}" by auto
hence "∑{m..<n} = ∑{m..n-1}" by simp
also have "… = (n*(n-1) - m*(m-1)) div 2"
using assms ‹m < n› by (simp add: Sum_Icc_nat mult.commute)
finally show ?thesis .
next
assume "¬ m < n" with assms show ?thesis by simp
qed

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"
(simp add: algebra_simps sum_subtractf sum.distrib sum.commute[of "λi j. a i * b j"] sum_distrib_left)
also
{ 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)
qed

lemma Chebyshev_sum_upper_nat:
fixes a b :: "nat ⇒ nat"
shows "(⋀i j. ⟦ i≤j; j<n ⟧ ⟹ a i ≤ a j) ⟹
(⋀i j. ⟦ i≤j; 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])

end
```