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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: matrix_props.prf   Sprache: Isabelle

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff