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