---

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

.....wf..... 
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. 0 < n
16. (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)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
18. x : ℕf[n] ⟶ Outcome
⊢ (Σ0 ≤ i < n - 1. X[i] x + (X[n - 1] x)) = (Σ0 ≤ i < n - 1. X[i] x + (X[n - 1] x)) ∈ ℚ
BY
{ (Fold `member` 0 THEN MemCD) }

1
.....subterm..... T:t
1:n
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. 0 < n
16. (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)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
18. x : ℕf[n] ⟶ Outcome
⊢ Σ0 ≤ i < n - 1. X[i] x ∈ ℚ

2
.....subterm..... T:t
2:n
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. 0 < n
16. (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)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
18. x : ℕf[n] ⟶ Outcome
⊢ X[n - 1] x ∈ ℚ

---

Latex:

---

Latex:
.....wf..... 
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.  0  \mleq{}  s
10.  B  :  \mBbbQ{}
11.  k  \mleq{}  B
12.  s  \mleq{}  B
13.  n  :  \mBbbZ{}
14.  f[n  -  1]  <  f[n]
15.  0  <  n
16.  (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)))
17.  rv-partial-sum(n  -  1;i.X[i])  \mmember{}  RandomVariable(p;f[n  -  1])
18.  x  :  \mBbbN{}f[n]  {}\mrightarrow{}  Outcome
\mvdash{}  (\mSigma{}0  \mleq{}  i  <  n  -  1.  X[i]  x  +  (X[n  -  1]  x))  =  (\mSigma{}0  \mleq{}  i  <  n  -  1.  X[i]  x  +  (X[n  -  1]  x))


By

---

Latex:
(Fold  `member`  0  THEN  MemCD)

---

Home Index