---

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


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. X : RandomVariable(p;0)
⊢ E(0;X) = E(m;X) ∈ ℚ
BY
{ (RW (AddrC [2] (RecUnfoldC `expectation`)) 0 THEN Reduce 0)⋅ }

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

---

Latex:



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


By

(RW  (AddrC  [2]  (RecUnfoldC  `expectation`))  0  THEN  Reduce  0)\mcdot{}

---

Home Index