Quelle Inequalities.thy Sprache: Isabelle

(*  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)
  } then have "?S \ 0"
    by (auto intro!: sum_nonpos simp: mult_le_0_iff)
  finally show ?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) \
         (\<And>i j. \<lbrakk> i\<le>j; j<n \<rbrakk> \<Longrightarrow> b i \<ge> b j) \<Longrightarrow>
    n * (\<Sum>i=0..<n. a i * b i) \<le> (\<Sum>i=0..<n. a i) * (\<Sum>i=0..<n. b i)"
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

quality88%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 ist noch experimentell.