---

Step * 1 2 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:ℚ. (0 < q ⇒ (∃b:ℚ. ∃C:p-open(p). (measure(C) ≤ q ∧ (∀s:ℕ ─→ Outcome. ((∃n:ℕ. (b ≤ (X[n] s))) ⇒ s ∈ C)))))
⊢ nullset(p;(X[n]─→∞ as n─→∞))
BY
{ (Unfold `nullset` 0
   THEN ParallelLast
   THEN (D -1 THENA (DVar `q' THEN Unhide THEN Auto))
   THEN D -1
   THEN ((InstLemma `rv-unbounded_wf` [⌈p⌉; ⌈f⌉; ⌈X⌉])⋅ THENA Auto)
   THEN ParallelOp -2
   THEN ExRepD
   THEN D 0
   THEN Try (Trivial)
   THEN ParallelOp -2
   THEN ParallelLast) }

1
.....antecedent..... 
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:ℚ. (0 < q ⇒ (∃b:ℚ. ∃C:p-open(p). (measure(C) ≤ q ∧ (∀s:ℕ ─→ Outcome. ((∃n:ℕ. (b ≤ (X[n] s))) ⇒ s ∈ C)))))
11. q : {q:ℚ| 0 < q} @i
12. b : ℚ
13. C : p-open(p)
14. measure(C) ≤ q
15. ∀s:ℕ ─→ Outcome. ((∃n:ℕ. (b ≤ (X[n] s))) ⇒ s ∈ C)
16. (X[n]─→∞ as n─→∞) ∈ (ℕ ─→ Outcome) ─→ ℙ
17. s : ℕ ─→ Outcome@i
18. (X[n]─→∞ as n─→∞) s@i
⊢ ∃n:ℕ. (b ≤ (X[n] s))

---

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.  \mforall{}q:\mBbbQ{}
            (0  <  q
            {}\mRightarrow{}  (\mexists{}b:\mBbbQ{}
                      \mexists{}C:p-open(p).  (measure(C)  \mleq{}  q  \mwedge{}  (\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  ((\mexists{}n:\mBbbN{}.  (b  \mleq{}  (X[n]  s)))  {}\mRightarrow{}  s  \mmember{}  C)))))
\mvdash{}  nullset(p;(X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{}))


By

(Unfold  `nullset`  0
  THEN  ParallelLast
  THEN  (D  -1  THENA  (DVar  `q'  THEN  Unhide  THEN  Auto))
  THEN  D  -1
  THEN  ((InstLemma  `rv-unbounded\_wf`  [\mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}X\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  ExRepD
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  ParallelOp  -2
  THEN  ParallelLast)

---

Home Index