---

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
{ ((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)))) }

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

---

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

((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))))

---

Home Index