products/sources/formale Sprachen/Isabelle/Pure/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: more_pattern.ML   Sprache: Isabelle

Untersuchung 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

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.18Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff