---

Step * 1 2 of Lemma slln-lemma2


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. B : ℚ
10. 0 ≤ B
11. ∀n:ℕ. (E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n * n))
12. n : ℕ@i
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[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 )) ≤ (2 * B)
BY
{ ((RW (AddrC [1;3] (UnfoldTopC `rv-partial-sum`)) 0)
   THEN (InstLemma `expectation-qsum` [⌈n⌉;⌈p⌉;⌈f[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 ⌉]⋅
         THENA (Auto THEN Try ((Unfold `label` 0 THEN (RWO "int-eq-in-rationals" (-1)) THEN Auto)))
         )
   THEN (Reduce (-1))
   THEN ((HypSubst (-1) 0) THENA Auto)
   THEN (Thin (-1))) }

1
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. B : ℚ
10. 0 ≤ B
11. ∀n:ℕ. (E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n * n))
12. n : ℕ@i
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n]))
⊢ Σ0 ≤ i < n. E(f[n];if (i =z 0) then 0 else (x.(x * x) * x * x) o (1/i)*rv-partial-sum(i;i.X[i]) fi ) ≤ (2 * B)

---

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


By

((RW  (AddrC  [1;3]  (UnfoldTopC  `rv-partial-sum`))  0)
  THEN  (InstLemma  `expectation-qsum`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f[n]\mkleeneclose{};\mkleeneopen{}\mlambda{}k.if  (k  =\msubz{}  0)
                                                                                                                then  0
                                                                                                                else  (x.(x  *  x)
                                                                                                                          *  x
                                                                                                                          *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
                                                                                                                fi  \mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((Unfold  `label`  0  THEN  (RWO  "int-eq-in-rationals"  (-1))  THEN  Auto)))
              )
  THEN  (Reduce  (-1))
  THEN  ((HypSubst  (-1)  0)  THENA  Auto)
  THEN  (Thin  (-1)))

---

Home Index