src/HOL/Inequalities.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63170 eae6549dbea2 child 63918 6bf55e6e0b75 permissions -rw-r--r--
tuned proofs;
```     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 Setsum_Icc_int: "(m::int) \<le> n \<Longrightarrow> \<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
```
```    11 proof(induct i == "nat(n-m)" arbitrary: m n)
```
```    12   case 0
```
```    13   hence "m = n" by arith
```
```    14   thus ?case by (simp add: algebra_simps)
```
```    15 next
```
```    16   case (Suc i)
```
```    17   have 0: "i = nat((n-1) - m)" "m \<le> n-1" using Suc(2,3) by arith+
```
```    18   have "\<Sum> {m..n} = \<Sum> {m..1+(n-1)}" by simp
```
```    19   also have "\<dots> = \<Sum> {m..n-1} + n" using \<open>m \<le> n\<close>
```
```    20     by(subst atLeastAtMostPlus1_int_conv) simp_all
```
```    21   also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n"
```
```    22     by(simp add: Suc(1)[OF 0])
```
```    23   also have "\<dots> = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp
```
```    24   also have "\<dots> = (n*(n+1) - m*(m-1)) div 2" by(simp add: algebra_simps)
```
```    25   finally show ?case .
```
```    26 qed
```
```    27
```
```    28 lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
```
```    29 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
```
```    30 proof -
```
```    31   have "m*(m-1) \<le> n*(n + 1)"
```
```    32    using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
```
```    33   hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
```
```    34     by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int of_nat_mult simp del: of_nat_setsum
```
```    35           split: zdiff_int_split)
```
```    36   thus ?thesis
```
```    37     using of_nat_eq_iff by blast
```
```    38 qed
```
```    39
```
```    40 lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
```
```    41 shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
```
```    42 proof cases
```
```    43   assume "m < n"
```
```    44   hence "{m..<n} = {m..n-1}" by auto
```
```    45   hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
```
```    46   also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
```
```    47     using assms \<open>m < n\<close> by (simp add: Setsum_Icc_nat mult.commute)
```
```    48   finally show ?thesis .
```
```    49 next
```
```    50   assume "\<not> m < n" with assms show ?thesis by simp
```
```    51 qed
```
```    52
```
```    53 lemma Chebyshev_sum_upper:
```
```    54   fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
```
```    55   assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
```
```    56   assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
```
```    57   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)"
```
```    58 proof -
```
```    59   let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
```
```    60   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"
```
```    61     by (simp only: one_add_one[symmetric] algebra_simps)
```
```    62       (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
```
```    63   also
```
```    64   { fix i j::nat assume "i<n" "j<n"
```
```    65     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"
```
```    66       using assms by (cases "i \<le> j") (auto simp: algebra_simps)
```
```    67   } then have "?S \<le> 0"
```
```    68     by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
```
```    69   finally show ?thesis by (simp add: algebra_simps)
```
```    70 qed
```
```    71
```
```    72 lemma Chebyshev_sum_upper_nat:
```
```    73   fixes a b :: "nat \<Rightarrow> nat"
```
```    74   shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
```
```    75          (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
```
```    76     n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
```
```    77 using Chebyshev_sum_upper[where 'a=real, of n a b]
```
```    78 by (simp del: of_nat_mult of_nat_setsum  add: of_nat_mult[symmetric] of_nat_setsum[symmetric])
```
```    79
```
```    80 end
```