src/HOL/Inequalities.thy
 author wenzelm Mon Mar 16 16:59:59 2015 +0100 (2015-03-16) changeset 59720 f893472fff31 parent 59712 6c013328b885 child 60150 bd773c47ad0b permissions -rw-r--r--
```     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_triangle_reindex:
```
```    11   fixes n :: nat
```
```    12   shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
```
```    13   apply (simp add: setsum.Sigma)
```
```    14   apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
```
```    15   apply auto
```
```    16   done
```
```    17
```
```    18 lemma gauss_sum_div2: "(2::'a::semiring_div) \<noteq> 0 \<Longrightarrow>
```
```    19   setsum of_nat {1..n} = of_nat n * (of_nat n + 1) div (2::'a)"
```
```    20 using gauss_sum[where n=n and 'a = 'a,symmetric] by auto
```
```    21
```
```    22 lemma Setsum_Icc_int: assumes "0 \<le> m" and "(m::int) \<le> n"
```
```    23 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
```
```    24 proof-
```
```    25   { fix k::int assume "k\<ge>0"
```
```    26     hence "\<Sum> {1..k::int} = k * (k+1) div 2"
```
```    27       by (rule gauss_sum_div2[where 'a = int, transferred]) simp
```
```    28   } note 1 = this
```
```    29   have "{m..n} = {0..n} - {0..m-1}" using `m\<ge>0` by auto
```
```    30   hence "\<Sum>{m..n} = \<Sum>{0..n} - \<Sum>{0..m-1}" using assms
```
```    31     by (force intro!: setsum_diff)
```
```    32   also have "{0..n} = {0} Un {1..n}" using assms by auto
```
```    33   also have "\<Sum>({0} \<union> {1..n}) = \<Sum>{1..n}" by(simp add: setsum.union_disjoint)
```
```    34   also have "\<dots> = n * (n+1) div 2" by(rule 1[OF order_trans[OF assms]])
```
```    35   also have "{0..m-1} = (if m=0 then {} else {0} Un {1..m-1})"
```
```    36     using assms by auto
```
```    37   also have "\<Sum> \<dots> = m*(m-1) div 2" using `m\<ge>0` by(simp add: 1 mult.commute)
```
```    38   also have "n*(n+1) div 2 - m*(m-1) div 2 = (n*(n+1) - m*(m-1)) div 2"
```
```    39     apply(subgoal_tac "even(n*(n+1)) \<and> even(m*(m-1))")
```
```    40     by (auto (*simp: even_def[symmetric]*))
```
```    41   finally show ?thesis .
```
```    42 qed
```
```    43
```
```    44 lemma Setsum_Icc_nat: assumes "(m::nat) \<le> n"
```
```    45 shows "\<Sum> {m..n} = (n*(n+1) - m*(m-1)) div 2"
```
```    46 proof -
```
```    47   have "m*(m-1) \<le> n*(n + 1)"
```
```    48    using assms by (meson diff_le_self order_trans le_add1 mult_le_mono)
```
```    49   hence "int(\<Sum> {m..n}) = int((n*(n+1) - m*(m-1)) div 2)" using assms
```
```    50     by (auto simp add: Setsum_Icc_int[transferred, OF _ assms] zdiv_int int_mult
```
```    51       split: zdiff_int_split)
```
```    52   thus ?thesis by simp
```
```    53 qed
```
```    54
```
```    55 lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
```
```    56 shows "\<Sum> {m..<n} = (n*(n-1) - m*(m-1)) div 2"
```
```    57 proof cases
```
```    58   assume "m < n"
```
```    59   hence "{m..<n} = {m..n-1}" by auto
```
```    60   hence "\<Sum>{m..<n} = \<Sum>{m..n-1}" by simp
```
```    61   also have "\<dots> = (n*(n-1) - m*(m-1)) div 2"
```
```    62     using assms `m < n` by (simp add: Setsum_Icc_nat mult.commute)
```
```    63   finally show ?thesis .
```
```    64 next
```
```    65   assume "\<not> m < n" with assms show ?thesis by simp
```
```    66 qed
```
```    67
```
```    68 lemma Chebyshev_sum_upper:
```
```    69   fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
```
```    70   assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
```
```    71   assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
```
```    72   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)"
```
```    73 proof -
```
```    74   let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
```
```    75   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"
```
```    76     unfolding one_add_one[symmetric] algebra_simps
```
```    77     by (simp add: algebra_simps setsum_subtractf setsum.distrib setsum.commute[of "\<lambda>i j. a i * b j"] setsum_right_distrib)
```
```    78   also
```
```    79   { fix i j::nat assume "i<n" "j<n"
```
```    80     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"
```
```    81       using assms by (cases "i \<le> j") (auto simp: algebra_simps)
```
```    82   } hence "?S \<le> 0"
```
```    83     by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
```
```    84        (auto simp: field_simps)
```
```    85   finally show ?thesis by (simp add: algebra_simps)
```
```    86 qed
```
```    87
```
```    88 lemma Chebyshev_sum_upper_nat:
```
```    89   fixes a b :: "nat \<Rightarrow> nat"
```
```    90   shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
```
```    91          (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
```
```    92     n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
```
```    93 using Chebyshev_sum_upper[where 'a=real, of n a b]
```
```    94 by (simp del: real_of_nat_mult real_of_nat_setsum
```
```    95   add: real_of_nat_mult[symmetric] real_of_nat_setsum[symmetric] real_of_nat_def[symmetric])
```
```    96
```
```    97 end
```