---

Step * 1 1 of Lemma open-expectation-monotone


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>))
BY
{ ((Subst' (C <0, null>) = E(m;λs.(C <0, null>)) ∈ ℚ 0 THEN Auto)
   THEN Try ((Symmetry THEN BLemma `expectation-constant` THEN Reduce 0 THEN Auto))
   THEN Try ((BLemma `expectation-monotone` THEN Auto))
   THEN Try ((Try ((DVar `C' THEN Reduce 0))
              THEN Try (Unfold `random-variable` 0)
              THEN All (Fold `p-outcome`)⋅
              THEN Auto
              THEN (DVar `p' THEN Auto THEN Unhide THEN Complete (Auto))⋅))) }

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


By

((Subst'  (C  ɘ,  null>)  =  E(m;\mlambda{}s.(C  ɘ,  null>))  0  THEN  Auto)
  THEN  Try  ((Symmetry  THEN  BLemma  `expectation-constant`  THEN  Reduce  0  THEN  Auto))
  THEN  Try  ((BLemma  `expectation-monotone`  THEN  Auto))
  THEN  Try  ((Try  ((DVar  `C'  THEN  Reduce  0))
                        THEN  Try  (Unfold  `random-variable`  0)
                        THEN  All  (Fold  `p-outcome`)\mcdot{}
                        THEN  Auto
                        THEN  (DVar  `p'  THEN  Auto  THEN  Unhide  THEN  Complete  (Auto))\mcdot{})))

---

Home Index