src/HOL/Inequalities.thy
author wenzelm
Fri, 05 Apr 2019 17:05:32 +0200
changeset 70067 9b34dbeb1103
parent 66936 cf8d8fc23891
permissions -rw-r--r--
auxiliary operation for common uses of 'compile_generated_files';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 59712
diff changeset
     1
(*  Title:     HOL/Inequalities.thy
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     2
    Author:    Tobias Nipkow
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     3
    Author:    Johannes Hölzl
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     4
*)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     5
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     6
theory Inequalities
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     7
  imports Real_Vector_Spaces
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     8
begin
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
     9
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    10
lemma Chebyshev_sum_upper:
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    11
  fixes a b::"nat \<Rightarrow> 'a::linordered_idom"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    12
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> a i \<le> a j"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    13
  assumes "\<And>i j. i \<le> j \<Longrightarrow> j < n \<Longrightarrow> b i \<ge> b j"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    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)"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    15
proof -
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    16
  let ?S = "(\<Sum>j=0..<n. (\<Sum>k=0..<n. (a j - a k) * (b j - b k)))"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    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"
63170
eae6549dbea2 tuned proofs, to allow unfold_abs_def;
wenzelm
parents: 62348
diff changeset
    18
    by (simp only: one_add_one[symmetric] algebra_simps)
66804
3f9bb52082c4 avoid name clashes on interpretation of abstract locales
haftmann
parents: 64267
diff changeset
    19
      (simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "\<lambda>i j. a i * b j"] sum_distrib_left)
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    20
  also
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    21
  { fix i j::nat assume "i<n" "j<n"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    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"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    23
      using assms by (cases "i \<le> j") (auto simp: algebra_simps)
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61762
diff changeset
    24
  } then have "?S \<le> 0"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
    25
    by (auto intro!: sum_nonpos simp: mult_le_0_iff)
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    26
  finally show ?thesis by (simp add: algebra_simps)
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    27
qed
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    28
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    29
lemma Chebyshev_sum_upper_nat:
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    30
  fixes a b :: "nat \<Rightarrow> nat"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    31
  shows "(\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> a i \<le> a j) \<Longrightarrow>
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    32
         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    33
    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    34
using Chebyshev_sum_upper[where 'a=real, of n a b]
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63918
diff changeset
    35
by (simp del: of_nat_mult of_nat_sum  add: of_nat_mult[symmetric] of_nat_sum[symmetric])
59712
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    36
6c013328b885 add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
diff changeset
    37
end