---

Step * 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
⊢ E(n - 1;rv-shift(x;X)) ≤ E(n - 1;rv-shift(x;Y))
BY
{ BackThruSomeHyp }

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

---

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{}  E(n  -  1;rv-shift(x;X))  \mleq{}  E(n  -  1;rv-shift(x;Y))


By

BackThruSomeHyp

---

Home Index