---

Step * 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
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) ≤ weighted-sum(p;λx.E(n - 1;rv-shift(x;Y)))
BY
{ (BLemma `ws-monotone`
   THEN Auto
   THEN (All (Fold `p-outcome`) THEN Auto)
   THEN Try (((DVar `p' THEN Unhide) THEN Auto THEN RWO "l_all_iff" 3 THEN Complete (Auto)))
   THEN Reduce 0) }

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
⊢ E(n - 1;rv-shift(x;X)) ≤ E(n - 1;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
\mvdash{}  weighted-sum(p;\mlambda{}x.E(n  -  1;rv-shift(x;X)))  \mleq{}  weighted-sum(p;\mlambda{}x.E(n  -  1;rv-shift(x;Y)))


By

(BLemma  `ws-monotone`
  THEN  Auto
  THEN  (All  (Fold  `p-outcome`)  THEN  Auto)
  THEN  Try  (((DVar  `p'  THEN  Unhide)  THEN  Auto  THEN  RWO  "l\_all\_iff"  3  THEN  Complete  (Auto)))
  THEN  Reduce  0)

---

Home Index