---

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

.....subterm..... T:t
1:n
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)|)))))
9. s : ℕ ─→ Outcome@i
10. q : ℚ@i
11. 0 < q@i
12. ∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s) - mean|))@i
13. n : ℕ@i
14. m : ℕ
15. n < m
16. q ≤ |Σ0 ≤ i < m. (1/m) * (X i s) - mean|
17. n < m
⊢ Σ0 ≤ i < m. (1/m) * (X i + -(mean) s) = (Σ0 ≤ i < m. (1/m) * (X i s) - mean) ∈ ℚ
BY
{ ((RWO "prod_sum_l_q<" 0
    THENM RepUR ``rv-add rv-const`` 0
    THENM RWO "sum_plus_q" 0
    THENM GenConcl ⌈Σ0 ≤ i < m. X i s = Z ∈ ℚ⌉⋅
    THENM RWO "qsum-const" 0
    THENM QNorm 0)
   THENA (Auto
          THEN Try ((Fold `random-variable` 0 THEN Auto))
          THEN Try ((Fold `p-outcome` 0 THEN Auto))
          THEN Try ((Dvar 0 THEN Complete (Auto)))
          THEN Try ((Assert ⌈¬(m = 0 ∈ ℤ)⌉⋅ THEN Auto)))
   )⋅ }

---

Latex:


.....subterm.....  T:t
1:n
1.  p  :  FinProbSpace@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  \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)
4.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
5.  rv-iid(p;n.f[n];n.X[n])@i
6.  mean  :  \mBbbQ{}@i
7.  E(f[0];X[0])  =  mean
8.  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]  +  -(mean)  s)|)))))
9.  s  :  \mBbbN{}  {}\mrightarrow{}  Outcome@i
10.  q  :  \mBbbQ{}@i
11.  0  <  q@i
12.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  s)  -  mean|))@i
13.  n  :  \mBbbN{}@i
14.  m  :  \mBbbN{}
15.  n  <  m
16.  q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  s)  -  mean|
17.  n  <  m
\mvdash{}  \mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  +  -(mean)  s)  =  (\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  s)  -  mean)


By

((RWO  "prod\_sum\_l\_q<"  0
    THENM  RepUR  ``rv-add  rv-const``  0
    THENM  RWO  "sum\_plus\_q"  0
    THENM  GenConcl  \mkleeneopen{}\mSigma{}0  \mleq{}  i  <  m.  X  i  s  =  Z\mkleeneclose{}\mcdot{}
    THENM  RWO  "qsum-const"  0
    THENM  QNorm  0)
  THENA  (Auto
                THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
                THEN  Try  ((Dvar  0  THEN  Complete  (Auto)))
                THEN  Try  ((Assert  \mkleeneopen{}\mneg{}(m  =  0)\mkleeneclose{}\mcdot{}  THEN  Auto)))
  )\mcdot{}

---

Home Index