---

Step * of Lemma expectation-non-neg

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[Y:RandomVariable(p;n)].  0 ≤ E(n;Y) supposing 0 ≤ Y
BY
{ (InstLemma `expectation-monotone` []
   THEN RepeatFor 2 (ParallelLast)
   THEN ((InstHyp [⌈0⌉] (-1))⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (RWO "expectation-rv-const" (-1))
   THEN Auto) }

---

Latex:


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


By

(InstLemma  `expectation-monotone`  []
  THEN  RepeatFor  2  (ParallelLast)
  THEN  ((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RWO  "expectation-rv-const"  (-1))
  THEN  Auto)

---

Home Index