---

Step * 1 1 1 of Lemma expectation-monotone


1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀[X,Y:RandomVariable(p;n - 1)].  E(n - 1;X) ≤ E(n - 1;Y) supposing X ≤ Y
5. ¬(n = 0 ∈ ℤ)
6. X : RandomVariable(p;n)
7. Y : RandomVariable(p;n)
8. X ≤ Y
9. x : Outcome@i
⊢ rv-shift(x;X) ≤ rv-shift(x;Y)
BY
{ (All (Unfolds ``rv-le rv-shift``) THEN Reduce 0 THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[X,Y:RandomVariable(p;n  -  1)].    E(n  -  1;X)  \mleq{}  E(n  -  1;Y)  supposing  X  \mleq{}  Y
5.  \mneg{}(n  =  0)
6.  X  :  RandomVariable(p;n)
7.  Y  :  RandomVariable(p;n)
8.  X  \mleq{}  Y
9.  x  :  Outcome@i
\mvdash{}  rv-shift(x;X)  \mleq{}  rv-shift(x;Y)


By

(All  (Unfolds  ``rv-le  rv-shift``)  THEN  Reduce  0  THEN  Auto)

---

Home Index