(* Title: HOL/Inequalities.thy Author: Tobias Nipkow Author: Johannes Hölzl *)
theory Inequalities imports Real_Vector_Spaces begin
lemma Chebyshev_sum_upper: fixes a b::"nat ==> 'a::linordered_idom" assumes"∧i j. i ≤ j ==> j < n ==> a i ≤ a j" assumes"∧i j. i ≤ j ==> j < n ==> b i ≥ b j" shows"of_nat n * (∑k=0..≤ (∑k=0..∑k=0.. proof - let ?S = "(∑j=0..∑k=0.. have"2 * (of_nat n * (∑j=0..∑j=0..∑k=0.. by (simp only: one_add_one[symmetric] algebra_simps)
(simp add: algebra_simps sum_subtractf sum.distrib sum.swap[of "λi j. a i * b j"] sum_distrib_left) also
{ fix i j::nat assume"i"j hence"a i - a j ≤ 0 ∧ b i - b j ≥ 0 ∨ a i - a j ≥ 0 ∧ b i - b j ≤ 0" using assms by (cases "i ≤ j") (auto simp: algebra_simps)
} thenhave"?S ≤ 0" by (auto intro!: sum_nonpos simp: mult_le_0_iff) finallyshow ?thesis by (simp add: algebra_simps) qed
lemma Chebyshev_sum_upper_nat: fixes a b :: "nat ==> nat" shows"(∧i j. [ i≤j; j]==> a i ≤ a j) ==> (∧i j. [ i≤j; j]==> b i ≥ b j) ==> n * (∑i=0..≤ (∑i=0..∑i=0.. using Chebyshev_sum_upper[where 'a=real, of n a b] by (simp del: of_nat_mult of_nat_sum add: of_nat_mult[symmetric] of_nat_sum[symmetric])
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
