---

Step * 1 of Lemma open-expectation-monotone


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index