---

Step * 1 1 of Lemma bounded-expectation

.....assertion..... 
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)
⊢ ∀q:ℚ. (0 < q ⇒ (∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q))
BY
{ (Auto
   THEN skip{(Assert 0 < (B/q) BY
                    (QMul ⌈(1/q)⌉ 7⋅
                     THEN (Auto THEN Try ((BLemma `qinv-positive` THEN Auto)))
                     THEN All (Unfold `qdiv`)
                     THEN (QNorm (0) THENM QNorm (-1))
                     THEN Auto
                     THEN RW assert_pushdownC 0
                     THEN Auto))}
   ) }

1
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 : ℚ@i
10. 0 < q@i
⊢ ∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q

---

Latex:


.....assertion..... 
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)
\mvdash{}  \mforall{}q:\mBbbQ{}.  (0  <  q  {}\mRightarrow{}  (\mexists{}b:\mBbbQ{}.  \mforall{}n:\mBbbN{}.  E(f[n];b  \mleq{}  X[n])  <  q))


By

(Auto
  THEN  skip\{(Assert  0  <  (B/q)  BY
                                    (QMul  \mkleeneopen{}(1/q)\mkleeneclose{}  7\mcdot{}
                                      THEN  (Auto  THEN  Try  ((BLemma  `qinv-positive`  THEN  Auto)))
                                      THEN  All  (Unfold  `qdiv`)
                                      THEN  (QNorm  (0)  THENM  QNorm  (-1))
                                      THEN  Auto
                                      THEN  RW  assert\_pushdownC  0
                                      THEN  Auto))\}
  )

---

Home Index