---

Step * of Lemma strong-law-of-large-numbers

∀p:FinProbSpace. ∀f:ℕ ⟶ ℕ. ∀X:n:ℕ ⟶ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
  ⇒ (∀mean:ℚ
        nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s) - mean|))))) 
        supposing E(f[0];X[0]) = mean ∈ ℚ))
BY
{ xxx(InstLemma `slln-lemma4` []
      THEN RepeatFor 2 ((ParallelLast THEN (Thin (-3))))
      THEN Auto
      THEN ((InstHyp [⌜λ2i.X[i] + -(mean)⌝] (3))⋅ THENA Auto)
      THEN Try ((BLemma `rv-iid-add-const` THEN Auto))
      THEN Try (((RWO "expectation-rv-add" 0 THENA Auto)
                 THEN (RWO "expectation-rv-const" 0 THENA Auto)
                 THEN (HypSubst' -1 0 THENA Auto)
                 THEN QNorm 0)))xxx }

1
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. ∀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 ∈ ℚ)
4. X : n:ℕ ⟶ RandomVariable(p;f[n])
5. rv-iid(p;n.f[n];n.X[n])
6. mean : ℚ
7. E(f[0];X[0]) = mean ∈ ℚ
8. nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] + -(mean) s)|)))))
⊢ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s) - mean|)))))

---

Latex:

---

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{}  (\mforall{}mean:\mBbbQ{}
                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)  -  mean|))))) 
                supposing  E(f[0];X[0])  =  mean))


By

---

Latex:
xxx(InstLemma  `slln-lemma4`  []
        THEN  RepeatFor  2  ((ParallelLast  THEN  (Thin  (-3))))
        THEN  Auto
        THEN  ((InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}i.X[i]  +  -(mean)\mkleeneclose{}]  (3))\mcdot{}  THENA  Auto)
        THEN  Try  ((BLemma  `rv-iid-add-const`  THEN  Auto))
        THEN  Try  (((RWO  "expectation-rv-add"  0  THENA  Auto)
                              THEN  (RWO  "expectation-rv-const"  0  THENA  Auto)
                              THEN  (HypSubst'  -1  0  THENA  Auto)
                              THEN  QNorm  0)))xxx

---

Home Index