---

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


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 : ℕ
15. i : ℕn
16. n1 : ℕ
⊢ 0 ≤ if (n1 =z 0) then 0 else (x.(x * x) * x * x) o (1/n1)*rv-partial-sum(n1;i.X[i]) fi 
BY
{ ((InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜n1⌝]⋅ THENA Auto)
   THEN (SplitOnConclITE THENA Auto)
   THEN RepUR ``rv-le rv-scale rv-const rv-compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:

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.  n  :  \mBbbN{}
15.  i  :  \mBbbN{}n
16.  n1  :  \mBbbN{}
\mvdash{}  0  \mleq{}  if  (n1  =\msubz{}  0)  then  0  else  (x.(x  *  x)  *  x  *  x)  o  (1/n1)*rv-partial-sum(n1;i.X[i])  fi 


By

---

Latex:
((InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}n1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  RepUR  ``rv-le  rv-scale  rv-const  rv-compose``  0
  THEN  Auto)

---

Home Index