---

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


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. 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 : ℕ
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n]))
14. i : ℤ
15. 0 ≤ i
16. i < n
17. ¬(i = 0 ∈ ℤ)
18. E(f[n];(x.(x * x) * x * x) o rv-partial-sum(i;i.X[i])) ≤ (B * i * i)
19. Z : (ℕf[n] ⟶ Outcome) ⟶ ℚ
20. rv-partial-sum(i;i.X[i]) = Z ∈ RandomVariable(p;f[n])
⊢ (λs.((((1/i) * (Z s)) * (1/i) * (Z s)) * ((1/i) * (Z s)) * (1/i) * (Z s)))
= (λs.((1/(i * i) * i * i) * ((Z s) * (Z s)) * (Z s) * (Z s)))
∈ ((ℕf[n] ⟶ Outcome) ⟶ ℚ)
BY
{ xxx((Assert ¬(i = 0 ∈ ℚ) BY Auto) THEN (Ext THEN Reduce 0)⋅ THEN Auto)xxx }

1
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. 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 : ℕ
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n]))
14. i : ℤ
15. 0 ≤ i
16. i < n
17. ¬(i = 0 ∈ ℤ)
18. E(f[n];(x.(x * x) * x * x) o rv-partial-sum(i;i.X[i])) ≤ (B * i * i)
19. Z : (ℕf[n] ⟶ Outcome) ⟶ ℚ
20. rv-partial-sum(i;i.X[i]) = Z ∈ RandomVariable(p;f[n])
21. ¬(i = 0 ∈ ℚ)
22. x : ℕf[n] ⟶ Outcome
⊢ ((((1/i) * (Z x)) * (1/i) * (Z x)) * ((1/i) * (Z x)) * (1/i) * (Z x))
= ((1/(i * i) * i * i) * ((Z x) * (Z x)) * (Z x) * (Z x))
∈ ℚ

---

Latex:

---

Latex:

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.  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{}
13.  \mforall{}k:\mBbbN{}n.  (rv-partial-sum(k;i.X[i])  \mmember{}  RandomVariable(p;f[n]))
14.  i  :  \mBbbZ{}
15.  0  \mleq{}  i
16.  i  <  n
17.  \mneg{}(i  =  0)
18.  E(f[n];(x.(x  *  x)  *  x  *  x)  o  rv-partial-sum(i;i.X[i]))  \mleq{}  (B  *  i  *  i)
19.  Z  :  (\mBbbN{}f[n]  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbQ{}
20.  rv-partial-sum(i;i.X[i])  =  Z
\mvdash{}  (\mlambda{}s.((((1/i)  *  (Z  s))  *  (1/i)  *  (Z  s))  *  ((1/i)  *  (Z  s))  *  (1/i)  *  (Z  s)))
=  (\mlambda{}s.((1/(i  *  i)  *  i  *  i)  *  ((Z  s)  *  (Z  s))  *  (Z  s)  *  (Z  s)))


By

---

Latex:
xxx((Assert  \mneg{}(i  =  0)  BY  Auto)  THEN  (Ext  THEN  Reduce  0)\mcdot{}  THEN  Auto)xxx

---

Home Index