---

Step * 1 2 1 1 2 1 2 of Lemma bounded-expectation


1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. B : ℚ@i
5. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
6. ∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]
7. 0 < B
8. ∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)
9. ∀q:ℚ. (0 < q ⇒ (∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q))
10. q : ℚ@i
11. 0 < q@i
12. b : ℚ
13. ∀n:ℕ. E(f[n];b ≤ X[n]) < q
14. g : ∀n:ℕ. ∀s:ℕn ─→ Outcome.  Dec(∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
⊢ ∀n:ℕ. ∀s:ℕn ─→ Outcome.  (((λp.case g (fst(p)) (snd(p)) of inl(x) => 1 | inr(x) => 0) <n, s>) = 1 ∈ ℤ ⇐⇒ ∃i:ℕn. (f[i]\000C < n c∧ (b ≤ (X[i] s))))
BY
{ (Reduce 0
   THEN (UnivCD THENA Auto)
   THEN ((GenConclAtAddr [1; 2; 1])
         THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Try ((Fold `p-outcome` 0 THEN Auto)))
         )
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN Try ((Fold `random-variable` 0 THEN Auto))
   THEN Try ((Fold `p-outcome` 0 THEN Auto))) }

---

Latex:



1.  p  :  FinProbSpace@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
4.  B  :  \mBbbQ{}@i
5.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]
6.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    X[i]  \mleq{}  X[n]
7.  0  <  B
8.  \mforall{}n:\mBbbN{}.  (0  \mleq{}  X[n]  \mwedge{}  E(f[n];X[n])  <  B)
9.  \mforall{}q:\mBbbQ{}.  (0  <  q  {}\mRightarrow{}  (\mexists{}b:\mBbbQ{}.  \mforall{}n:\mBbbN{}.  E(f[n];b  \mleq{}  X[n])  <  q))
10.  q  :  \mBbbQ{}@i
11.  0  <  q@i
12.  b  :  \mBbbQ{}
13.  \mforall{}n:\mBbbN{}.  E(f[n];b  \mleq{}  X[n])  <  q
14.  g  :  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.    Dec(\mexists{}i:\mBbbN{}n.  (f[i]  <  n  c\mwedge{}  (b  \mleq{}  (X[i]  s))))
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.    (((\mlambda{}p.case  g  (fst(p))  (snd(p))  of  inl(x)  =>  1  |  inr(x)  =>  0)  <n,  s>)  =  1  \000C\mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (f[i]  <  n  c\mwedge{}  (b  \mleq{}  (X[i]  s))))


By

(Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  ((GenConclAtAddr  [1;  2;  1])
              THENA  (Auto
                            THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                            THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))
              )
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
  THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))

---

Home Index