|
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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
