---

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


1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. s : ℚ@i
5. k : ℚ@i
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])@i
9. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. ∀n:ℕ
      ((E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n;i.X[i])) ≤ (((3 * s) + 1) * B * n * n))
      ∧ (E(f[n];(x.x * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n)))
⊢ 0 ≤ ((3 * s) + 1)
BY
{ ((QMul ⌈3⌉ 9⋅ THENA Auto) THEN QAdd ⌈1⌉ 9⋅ THEN Auto THEN QNorm 0 THEN (Assert 0 ≤ 1 BY Auto) THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
4.  s  :  \mBbbQ{}@i
5.  k  :  \mBbbQ{}@i
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])@i
9.  0  \mleq{}  s
10.  B  :  \mBbbQ{}
11.  k  \mleq{}  B
12.  s  \mleq{}  B
13.  \mforall{}n:\mBbbN{}
            ((E(f[n];(x.(x  *  x)  *  x  *  x)  o  rv-partial-sum(n;i.X[i]))  \mleq{}  (((3  *  s)  +  1)  *  B  *  n  *  n))
            \mwedge{}  (E(f[n];(x.x  *  x)  o  rv-partial-sum(n;i.X[i]))  \mleq{}  (B  *  n)))
\mvdash{}  0  \mleq{}  ((3  *  s)  +  1)


By

((QMul  \mkleeneopen{}3\mkleeneclose{}  9\mcdot{}  THENA  Auto)
  THEN  QAdd  \mkleeneopen{}1\mkleeneclose{}  9\mcdot{}
  THEN  Auto
  THEN  QNorm  0
  THEN  (Assert  0  \mleq{}  1  BY
                          Auto)
  THEN  Auto)

---

Home Index