---

Step * 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)|)))))
⊢ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s) - mean|)))))
BY
{ (Using [`P',⌈λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] + -(mean) s)|))))⌉
   ] (BLemma `nullset-monotone` )⋅
   THEN RepUR ``so_apply`` 0
   THEN (Auto THEN Try (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 Try ((Assert ⌈¬(m = 0 ∈ ℤ)⌉⋅ THEN Auto))) }

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

---

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)|)))))
\mvdash{}  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|)))))


By

(Using  [`P',\mkleeneopen{}\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)|))))\mkleeneclose{}
  ]  (BLemma  `nullset-monotone`  )\mcdot{}
  THEN  RepUR  ``so\_apply``  0
  THEN  (Auto  THEN  Try  (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  Try  ((Assert  \mkleeneopen{}\mneg{}(m  =  0)\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index