| products/sources/formale Sprachen/PVS/probability/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ipat_tmp.v Sprache: PVSOriginal von: PVS© |
|
||||||
|
expectation[T:TYPE+, (IMPORTING measure_integration@subset_algebra_def[T])
S:sigma_algebra, (IMPORTING probability_measure[T,S]) P:probability_measure]: THEORY BEGIN IMPORTING probability_measure[T,S], measure_integration@measure_def[T,S], measure_integration@integral[T,S,to_measure(P)], measure_integration@indefinite_integral[T,S,to_measure(P)], % Proof only probability_space[T,S,P] X,Y: VAR integrable x,c: VAR real t: VAR T A: VAR (S) E(X):real = integral(X) E_zero: LEMMA E(zero) = 0 E_one: LEMMA E(one) = 1 E_phi: LEMMA E(phi(A)) = P(A) E_add: LEMMA E(X+Y) = E(X) + E(Y) E_scal: LEMMA E(c*X) = c*E(X) E_opp: LEMMA E(-X) = -E(X) E_diff: LEMMA E(X-Y) = E(X) - E(Y) E_nonneg: LEMMA (FORALL t: X(t) >= 0) => E(X) >= 0 px: VAR posreal markov_inequality: THEOREM P(px <= abs(X)) <= E(abs(X))/px markov_inequality_alt: LEMMA x*P(x <= abs(X)) <= E(abs(X)) END expectation ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
