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

.....equality..... 
1. FinProbSpace@i
2. : ℕ ─→ ℕ@i
3. n:ℕ ─→ RandomVariable(p;f[n])@i
4. : ℚ@i
5. : ℚ@i
6. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
7. ∀n:ℕ((E(f[n];X[n]) 0 ∈ ℚ) ∧ (E(f[n];(x.x x) X[n]) s ∈ ℚ) ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))
8. ∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n])@i
9. : ℚ
10. 0 ≤ B
11. ∀n:ℕ(E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (B n))
12. : ℕ@i
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n]))
14. : ℤ@i
15. 0 ≤ i@i
16. i < n@i
17. ¬(i 0 ∈ ℤ)
18. E(f[n];(x.(x x) x) rv-partial-sum(i;i.X[i])) ≤ (B i)
⊢ E(f[n];(x.(x x) x) (1/i)*rv-partial-sum(i;i.X[i]))
E(f[n];(1/(i i) i)*(x.(x x) x) rv-partial-sum(i;i.X[i]))
∈ ℚ
BY
(EqCD
   THEN Auto
   THEN (GenConcl ⌈rv-partial-sum(i;i.X[i]) Z ∈ RandomVariable(p;f[n])⌉⋅ THENA Auto)
   THEN RepUR ``random-variable rv-compose rv-scale`` 0
   THEN Unfold `random-variable` -2
   THEN (All (Fold `p-outcome`))) }

1
1. FinProbSpace@i
2. : ℕ ─→ ℕ@i
3. n:ℕ ─→ RandomVariable(p;f[n])@i
4. : ℚ@i
5. : ℚ@i
6. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
7. ∀n:ℕ((E(f[n];X[n]) 0 ∈ ℚ) ∧ (E(f[n];(x.x x) X[n]) s ∈ ℚ) ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))
8. ∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n])@i
9. : ℚ
10. 0 ≤ B
11. ∀n:ℕ(E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (B n))
12. : ℕ@i
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n]))
14. : ℤ@i
15. 0 ≤ i@i
16. i < n@i
17. ¬(i 0 ∈ ℤ)
18. E(f[n];(x.(x x) x) rv-partial-sum(i;i.X[i])) ≤ (B i)
19. (ℕf[n] ─→ Outcome) ─→ ℚ@i
20. rv-partial-sum(i;i.X[i]) Z ∈ RandomVariable(p;f[n])@i
⊢ s.((((1/i) (Z s)) (1/i) (Z s)) ((1/i) (Z s)) (1/i) (Z s)))
s.((1/(i i) i) ((Z s) (Z s)) (Z s) (Z s)))
∈ ((ℕf[n] ─→ Outcome) ─→ ℚ)


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.  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]))
14.  i  :  \mBbbZ{}@i
15.  0  \mleq{}  i@i
16.  i  <  n@i
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)
\mvdash{}  E(f[n];(x.(x  *  x)  *  x  *  x)  o  (1/i)*rv-partial-sum(i;i.X[i]))
=  E(f[n];(1/(i  *  i)  *  i  *  i)*(x.(x  *  x)  *  x  *  x)  o  rv-partial-sum(i;i.X[i]))


By

(EqCD
  THEN  Auto
  THEN  (GenConcl  \mkleeneopen{}rv-partial-sum(i;i.X[i])  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``random-variable  rv-compose  rv-scale``  0
  THEN  Unfold  `random-variable`  -2
  THEN  (All  (Fold  `p-outcome`)))




Home Index