---

Step * of Lemma expectation-monotone

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  E(n;X) ≤ E(n;Y) supposing X ≤ Y
BY
{ (InductionOnNat
   THEN RecUnfold `expectation` 0
   THEN Reduce 0
   THEN Try ((SplitOnConclITE THENA Auto))
   THEN Auto'
   THEN Auto
   THEN Try (Complete ((DVar `p' THEN Auto)))) }

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
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) ≤ weighted-sum(p;λx.E(n - 1;rv-shift(x;Y)))

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(p;n)].    E(n;X)  \mleq{}  E(n;Y)  supposing  X  \mleq{}  Y


By

(InductionOnNat
  THEN  RecUnfold  `expectation`  0
  THEN  Reduce  0
  THEN  Try  ((SplitOnConclITE  THENA  Auto))
  THEN  Auto'
  THEN  Auto
  THEN  Try  (Complete  ((DVar  `p'  THEN  Auto))))

---

Home Index