---

Step * 1 1 of Lemma expectation-monotone-in-first


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. X : RandomVariable(p;0)
⊢ (X null) = E(m;X) ∈ ℚ
BY
{ xxx((Subst' E(m;X) = (X null) ∈ ℚ 0 THEN Try (BLemma `expectation-constant`))
      THEN Auto
      THEN Try ((Fold `random-variable` 0 THEN Auto))
      THEN Try ((DVar `p' THEN Complete (Auto))))xxx }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. X : RandomVariable(p;0)
6. s : ℕm ⟶ Outcome
⊢ (X s) = (X null) ∈ ℚ

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}
4.  0  \mleq{}  m
5.  X  :  RandomVariable(p;0)
\mvdash{}  (X  null)  =  E(m;X)


By

---

Latex:
xxx((Subst'  E(m;X)  =  (X  null)  0  THEN  Try  (BLemma  `expectation-constant`))
        THEN  Auto
        THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
        THEN  Try  ((DVar  `p'  THEN  Complete  (Auto))))xxx

---

Home Index