src/HOL/Inequalities.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (19 months ago) changeset 67003 49850a679c2c parent 66936 cf8d8fc23891 permissions -rw-r--r--
more robust sorted_entries;
```     1 (*  Title:     HOL/Inequalities.thy
```
```     2     Author:    Tobias Nipkow
```
```     3     Author:    Johannes Hölzl
```
```     4 *)
```
```     5
```
```     6 theory Inequalities
```
```     7   imports Real_Vector_Spaces
```
```     8 begin
```
```     9
```
```    10 lemma 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)"
```
```    15 proof -
```
```    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)
```
```    27 qed
```
```    28
```
```    29 lemma 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)"
```
```    34 using Chebyshev_sum_upper[where 'a=real, of n a b]
```
```    35 by (simp del: of_nat_mult of_nat_sum  add: of_nat_mult[symmetric] of_nat_sum[symmetric])
```
```    36
```
```    37 end
```