---

Step * 2 2 1 3 of Lemma slln-lemma1

.....wf..... 
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 : ℤ@i
14. 0 < n@i
⊢ (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1)))
  ∧ (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (B * (n - 1))) ∈ ℙ
BY
{ ((Subst' rv-partial-sum(0;i.X[i]) = 0 ∈ RandomVariable(p;f[0]) 0 THEN Auto)
   THEN Try ((RepUR ``rv-compose rv-const`` 0
              THEN Subst' E(f[0];λs.0) = 0 ∈ ℚ 0
              THEN Auto
              THEN Try (((BLemma `expectation-constant` THEN Auto)
                         THEN Reduce 0
                         THEN Auto
                         THEN Fold `rv-const` 0
                         THEN Auto))
              THEN QNorm 0))
   THEN Try (((RepUR ``rv-partial-sum rv-const random-variable`` 0 THEN Try (Fold `p-outcome` 0))
              THEN Ext
              THEN Reduce 0
              THEN Auto
              THEN RepUR ``qsum rng_sum mon_itop`` 0
              THEN RecUnfold `itop` 0
              THEN Reduce 0
              THEN Auto)))⋅ }

---

Latex:


.....wf..... 
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.  n  :  \mBbbZ{}@i
14.  0  <  n@i
\mvdash{}  (E(f[n  -  1];(x.(x  *  x)  *  x  *  x)  o  rv-partial-sum(n  -  1;i.X[i]))  \mleq{}  (((3  *  s)  +  1)
    *  B
    *  (n  -  1)
    *  (n  -  1)))
    \mwedge{}  (E(f[n  -  1];(x.x  *  x)  o  rv-partial-sum(n  -  1;i.X[i]))  \mleq{}  (B  *  (n  -  1)))  \mmember{}  \mBbbP{}


By

((Subst'  rv-partial-sum(0;i.X[i])  =  0  0  THEN  Auto)
  THEN  Try  ((RepUR  ``rv-compose  rv-const``  0
                        THEN  Subst'  E(f[0];\mlambda{}s.0)  =  0  0
                        THEN  Auto
                        THEN  Try  (((BLemma  `expectation-constant`  THEN  Auto)
                                              THEN  Reduce  0
                                              THEN  Auto
                                              THEN  Fold  `rv-const`  0
                                              THEN  Auto))
                        THEN  QNorm  0))
  THEN  Try  (((RepUR  ``rv-partial-sum  rv-const  random-variable``  0  THEN  Try  (Fold  `p-outcome`  0))
                        THEN  Ext
                        THEN  Reduce  0
                        THEN  Auto
                        THEN  RepUR  ``qsum  rng\_sum  mon\_itop``  0
                        THEN  RecUnfold  `itop`  0
                        THEN  Reduce  0
                        THEN  Auto)))\mcdot{}

---

Home Index