---

Step * 1 2 2 2 2 2 1 1 1 of Lemma slln-lemma3

.....antecedent..... 
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. s : ℚ
5. k : ℚ
6. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
7. ∀n:ℕ. ((E(f[n];X[n]) = 0 ∈ ℚ) ∧ (E(f[n];(x.x * x) o X[n]) = s ∈ ℚ) ∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = k ∈ ℚ))
8. ∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n])
9. B : ℚ
10. ∀n:ℕ
      (E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
11. ∀n:ℕ
      (rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
       ∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
      rv-partial-sum(i;k.if (k =z 0)
      then 0
      else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
      fi ) ≤ rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
15. ∀s:ℕ ⟶ Outcome. ∀n:ℕ+.  (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ⟶ Outcome) ⟶ ℙ].  ((∀s:ℕ ⟶ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ⟶ Outcome
18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))
19. B1 : ℚ
⊢ ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ ((λx.((x * x) * x * x)) |Σ0 ≤ i < m. (1/m) * (X i s1)|)))))
BY
{ (ExRepD THEN (InstConcl [⌜(q * q) * q * q⌝]⋅ THENA Auto)) }

1
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. s : ℚ
5. k : ℚ
6. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
7. ∀n:ℕ. ((E(f[n];X[n]) = 0 ∈ ℚ) ∧ (E(f[n];(x.x * x) o X[n]) = s ∈ ℚ) ∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = k ∈ ℚ))
8. ∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n])
9. B : ℚ
10. ∀n:ℕ
      (E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
11. ∀n:ℕ
      (rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
       ∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
      rv-partial-sum(i;k.if (k =z 0)
      then 0
      else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
      fi ) ≤ rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
15. ∀s:ℕ ⟶ Outcome. ∀n:ℕ+.  (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ⟶ Outcome) ⟶ ℙ].  ((∀s:ℕ ⟶ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ⟶ Outcome
18. q : ℚ
19. 0 < q
20. ∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))
21. B1 : ℚ
⊢ 0 < (q * q) * q * q
∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (((q * q) * q * q) ≤ ((λx.((x * x) * x * x)) |Σ0 ≤ i < m. (1/m) * (X i s1)|))))

---

Latex:

---

Latex:
.....antecedent..... 
1.  p  :  FinProbSpace
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])
4.  s  :  \mBbbQ{}
5.  k  :  \mBbbQ{}
6.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]
7.  \mforall{}n:\mBbbN{}
          ((E(f[n];X[n])  =  0)
          \mwedge{}  (E(f[n];(x.x  *  x)  o  X[n])  =  s)
          \mwedge{}  (E(f[n];(x.(x  *  x)  *  x  *  x)  o  X[n])  =  k))
8.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    rv-disjoint(p;f[n];X[i];X[n])
9.  B  :  \mBbbQ{}
10.  \mforall{}n:\mBbbN{}
            (E(f[n];rv-partial-sum(n;k.if  (k  =\msubz{}  0)
            then  0
            else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
            fi  ))  \mleq{}  B)
11.  \mforall{}n:\mBbbN{}
            (rv-partial-sum(n;k.if  (k  =\msubz{}  0)
              then  0
              else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
              fi  )  \mmember{}  RandomVariable(p;f[n]))
12.  0  \mleq{}  B
13.  B  <  B  +  1
14.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.
            rv-partial-sum(i;k.if  (k  =\msubz{}  0)
            then  0
            else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
            fi  )  \mleq{}  rv-partial-sum(n;k.if  (k  =\msubz{}  0)
            then  0
            else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
            fi  )
15.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}\msupplus{}.    (\mSigma{}0  \mleq{}  i  <  n.  (1/n)  *  (X  i  s)  \mmember{}  \mBbbQ{})
16.  \mforall{}p:FinProbSpace
            \mforall{}[P,Q:(\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}].
                ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  (Q[s]  {}\mRightarrow{}  P[s]))  {}\mRightarrow{}  \{nullset(p;P)  {}\mRightarrow{}  nullset(p;Q)\})
17.  s1  :  \mBbbN{}  {}\mrightarrow{}  Outcome
18.  \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  s1)|))))
19.  B1  :  \mBbbQ{}
\mvdash{}  \mexists{}q:\mBbbQ{}
      (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  ((\mlambda{}x.((x  *  x)  *  x  *  x))  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X  i  s1)|)))))


By

---

Latex:
(ExRepD  THEN  (InstConcl  [\mkleeneopen{}(q  *  q)  *  q  *  q\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index