---

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


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 ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s) - mean|)))@i
⊢ 0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i + -(mean) s)|)))
BY
{ ((RepeatFor 3 (ParallelLast)
    THEN Try ((Fold `random-variable` 0 THEN Auto))
    THEN Try ((Fold `p-outcome` 0 THEN Auto))
    THEN Try ((Dvar 0 THEN Complete (Auto))))
   THEN Auto
   THEN (NthHypEq (-2) THEN RepeatFor 2 ((EqCD THEN Auto)))⋅) }

1
.....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) ∈ ℚ

---

Latex:



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  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  s)  -  mean|)))@i
\mvdash{}  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)|)))


By

((RepeatFor  3  (ParallelLast)
    THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
    THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
    THEN  Try  ((Dvar  0  THEN  Complete  (Auto))))
  THEN  Auto
  THEN  (NthHypEq  (-2)  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))\mcdot{})

---

Home Index