src/HOL/Inequalities.thy
 author haftmann Mon Oct 30 13:18:41 2017 +0000 (20 months ago) changeset 66936 cf8d8fc23891 parent 66804 3f9bb52082c4 permissions -rw-r--r--
tuned some proofs and added some lemmas
 wenzelm@59720 ` 1` ```(* Title: HOL/Inequalities.thy ``` hoelzl@59712 ` 2` ``` Author: Tobias Nipkow ``` hoelzl@59712 ` 3` ``` Author: Johannes Hölzl ``` hoelzl@59712 ` 4` ```*) ``` hoelzl@59712 ` 5` hoelzl@59712 ` 6` ```theory Inequalities ``` hoelzl@59712 ` 7` ``` imports Real_Vector_Spaces ``` hoelzl@59712 ` 8` ```begin ``` hoelzl@59712 ` 9` hoelzl@59712 ` 10` ```lemma Chebyshev_sum_upper: ``` hoelzl@59712 ` 11` ``` fixes a b::"nat \ 'a::linordered_idom" ``` hoelzl@59712 ` 12` ``` assumes "\i j. i \ j \ j < n \ a i \ a j" ``` hoelzl@59712 ` 13` ``` assumes "\i j. i \ j \ j < n \ b i \ b j" ``` hoelzl@59712 ` 14` ``` shows "of_nat n * (\k=0.. (\k=0..k=0..j=0..j=0..k=0..i j. a i * b j"] sum_distrib_left) ``` hoelzl@59712 ` 20` ``` also ``` hoelzl@59712 ` 21` ``` { fix i j::nat assume "i 0 \ b i - b j \ 0 \ a i - a j \ 0 \ b i - b j \ 0" ``` hoelzl@59712 ` 23` ``` using assms by (cases "i \ j") (auto simp: algebra_simps) ``` haftmann@62348 ` 24` ``` } then have "?S \ 0" ``` nipkow@64267 ` 25` ``` by (auto intro!: sum_nonpos simp: mult_le_0_iff) ``` hoelzl@59712 ` 26` ``` finally show ?thesis by (simp add: algebra_simps) ``` hoelzl@59712 ` 27` ```qed ``` hoelzl@59712 ` 28` hoelzl@59712 ` 29` ```lemma Chebyshev_sum_upper_nat: ``` hoelzl@59712 ` 30` ``` fixes a b :: "nat \ nat" ``` hoelzl@59712 ` 31` ``` shows "(\i j. \ i\j; j \ a i \ a j) \ ``` hoelzl@59712 ` 32` ``` (\i j. \ i\j; j \ b i \ b j) \ ``` hoelzl@59712 ` 33` ``` n * (\i=0.. (\i=0..i=0..