equal
deleted
inserted
replaced
64 { fix i j::nat assume "i<n" "j<n" |
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" |
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) |
66 using assms by (cases "i \<le> j") (auto simp: algebra_simps) |
67 } hence "?S \<le> 0" |
67 } hence "?S \<le> 0" |
68 by (auto intro!: setsum_nonpos simp: mult_le_0_iff) |
68 by (auto intro!: setsum_nonpos simp: mult_le_0_iff) |
69 (auto simp: field_simps) |
|
70 finally show ?thesis by (simp add: algebra_simps) |
69 finally show ?thesis by (simp add: algebra_simps) |
71 qed |
70 qed |
72 |
71 |
73 lemma Chebyshev_sum_upper_nat: |
72 lemma Chebyshev_sum_upper_nat: |
74 fixes a b :: "nat \<Rightarrow> nat" |
73 fixes a b :: "nat \<Rightarrow> nat" |