---

Step * of Lemma slln-lemma4

∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
  ⇒ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|))))) 
     supposing E(f[0];X[0]) = 0 ∈ ℚ)
BY
{ (InstLemma `slln-lemma3` []
   THEN RepeatFor 3 ((ParallelLast THEN (Thin (-3))))
   THEN Auto
   THEN (D (-2))
   THEN Unfold `rv-identically-distributed` -3
   THEN InstHyp [⌈E(f[0];(x.x * x) o X[0])⌉; ⌈E(f[0];(x.(x * x) * x * x) o X[0])⌉ ] 4⋅
   THEN Auto
   THEN (InstHyp [⌈0⌉;⌈n⌉] (-4))⋅
   THEN Auto) }

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).
    (rv-iid(p;n.f[n];n.X[n])
    {}\mRightarrow{}  nullset(p;\mlambda{}s.\mexists{}q:\mBbbQ{}.  (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X[i]  s)|))))) 
          supposing  E(f[0];X[0])  =  0)


By

(InstLemma  `slln-lemma3`  []
  THEN  RepeatFor  3  ((ParallelLast  THEN  (Thin  (-3))))
  THEN  Auto
  THEN  (D  (-2))
  THEN  Unfold  `rv-identically-distributed`  -3
  THEN  InstHyp  [\mkleeneopen{}E(f[0];(x.x  *  x)  o  X[0])\mkleeneclose{};  \mkleeneopen{}E(f[0];(x.(x  *  x)  *  x  *  x)  o  X[0])\mkleeneclose{}  ]  4\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  (-4))\mcdot{}
  THEN  Auto)

---

Home Index