---

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
{ (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))) }

1
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
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])@i
5. rv-iid(p;n.f[n];n.X[n])@i
6. mean : ℚ@i
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:


\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

(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)))

---

Home Index