---

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

.....equality..... 
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
15. Z : RandomVariable(p;f[n - 1])@i
16. rv-partial-sum(n - 1;i.X[i]) = Z ∈ RandomVariable(p;f[n - 1])@i
17. E(f[n - 1];(x.(x * x) * x * x) o Z) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1))@i
18. E(f[n - 1];(x.x * x) o Z) ≤ (B * (n - 1))@i
⊢ E(f[n];(x.(x * x) * x * x) o Z + X[n - 1])
= E(f[n];(x.(x * x) * x * x) o Z + (x.(x * x) * x) o Z * 4*X[n - 1] + (x.(x * x) * x) o X[n - 1] * 4*Z + 6*(x.x
  * x) o Z * (x.x * x) o X[n - 1] + (x.(x * x) * x * x) o X[n - 1])
∈ ℚ
BY
{ ((EqCD THEN Auto)
   THEN RepUR ``rv-compose rv-mul rv-add rv-scale random-variable`` 0
   THEN Try (Fold `p-outcome` 0)
   THEN Ext
   THEN Reduce 0
   THEN Auto
   THEN (GenConcl ⌈(X[n - 1] x) = a ∈ ℚ⌉⋅ THENA Auto)
   THEN (GenConcl ⌈(Z x) = b ∈ ℚ⌉⋅ THENA Auto))⋅ }

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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ@i
14. 0 < n@i
15. Z : RandomVariable(p;f[n - 1])@i
16. rv-partial-sum(n - 1;i.X[i]) = Z ∈ RandomVariable(p;f[n - 1])@i
17. E(f[n - 1];(x.(x * x) * x * x) o Z) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1))@i
18. E(f[n - 1];(x.x * x) o Z) ≤ (B * (n - 1))@i
19. x : ℕf[n] ─→ Outcome
20. a : ℚ@i
21. (X[n - 1] x) = a ∈ ℚ@i
22. b : ℚ@i
23. (Z x) = b ∈ ℚ@i
⊢ (((b + a) * (b + a)) * (b + a) * (b + a))
= (((b * b) * b * b) + ((((b * b) * b) * 4 * a) + (((a * a) * a) * 4 * b) + (6 * (b * b) * a * a)) + ((a * a) * a * a))
∈ ℚ

---

Latex:


.....equality..... 
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
15.  Z  :  RandomVariable(p;f[n  -  1])@i
16.  rv-partial-sum(n  -  1;i.X[i])  =  Z@i
17.  E(f[n  -  1];(x.(x  *  x)  *  x  *  x)  o  Z)  \mleq{}  (((3  *  s)  +  1)  *  B  *  (n  -  1)  *  (n  -  1))@i
18.  E(f[n  -  1];(x.x  *  x)  o  Z)  \mleq{}  (B  *  (n  -  1))@i
\mvdash{}  E(f[n];(x.(x  *  x)  *  x  *  x)  o  Z  +  X[n  -  1])
=  E(f[n];(x.(x  *  x)  *  x  *  x)  o  Z  +  (x.(x  *  x)  *  x)  o  Z  *  4*X[n  -  1]  +  (x.(x  *  x)  *  x)  o  X[n 
    -  1]  *  4*Z  +  6*(x.x  *  x)  o  Z  *  (x.x  *  x)  o  X[n  -  1]  +  (x.(x  *  x)  *  x  *  x)  o  X[n  -  1])


By

((EqCD  THEN  Auto)
  THEN  RepUR  ``rv-compose  rv-mul  rv-add  rv-scale  random-variable``  0
  THEN  Try  (Fold  `p-outcome`  0)
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}(X[n  -  1]  x)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(Z  x)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index