---

Step * 1 of Lemma open-expectation-monotone


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
⊢ E(0;λs.(C <0, s>)) ≤ E(m;λs.(C <m, s>))
BY
{ (RW (AddrC [1] (RecUnfoldC `expectation`)) 0 THEN Reduce 0) }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
⊢ (C <0, null>) ≤ E(m;λs.(C <m, s>))

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}@i
4.  0  \mleq{}  m@i
5.  C  :  p-open(p)@i
\mvdash{}  E(0;\mlambda{}s.(C  ɘ,  s>))  \mleq{}  E(m;\mlambda{}s.(C  <m,  s>))


By

(RW  (AddrC  [1]  (RecUnfoldC  `expectation`))  0  THEN  Reduce  0)

---

Home Index