| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/probability/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle expectation.pvs Sprache: 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.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28