---

Step * of Lemma bounded-expectation

∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀B:ℚ.
  (nullset(p;(X[n]─→∞ as n─→∞))) supposing 
     ((∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)) and 
     0 < B and 
     (∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))
BY
{ 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)
⊢ nullset(p;(X[n]─→∞ as n─→∞))

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).  \mforall{}B:\mBbbQ{}.
    (nullset(p;(X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{})))  supposing 
          ((\mforall{}n:\mBbbN{}.  (0  \mleq{}  X[n]  \mwedge{}  E(f[n];X[n])  <  B))  and 
          0  <  B  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    X[i]  \mleq{}  X[n])  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))


By

Auto

---

Home Index