1(* Title: HOL/Inequalities.thy 2 Author: Tobias Nipkow 3 Author: Johannes H��lzl 4*) 5 6theory Inequalities 7 imports Real_Vector_Spaces 8begin 9 10lemma Chebyshev_sum_upper: 11 fixes a b::"nat \<Rightarrow> 'a::linordered_idom" 12 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j" 13 assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j" 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)" 15proof - 16 let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))" 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" 18 by (simp only: one_add_one[symmetric] algebra_simps) 19 (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left) 20 also 21 { fix i j::nat assume "i<n" "j<n" 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" 23 using assms by (cases "i \<le> j") (auto simp: algebra_simps) 24 } then have "?S \<le> 0" 25 by (auto intro!: sum_nonpos simp: mult_le_0_iff) 26 finally show ?thesis by (simp add: algebra_simps) 27qed 28 29lemma Chebyshev_sum_upper_nat: 30 fixes a b :: "nat \<Rightarrow> nat" 31 shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow> 32 (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow> 33 n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)" 34using Chebyshev_sum_upper[where 'a=real, of n a b] 35by (simp del: of_nat_mult of_nat_sum add: of_nat_mult[symmetric] of_nat_sum[symmetric]) 36 37end 38