Step * 2 2 1 of Lemma slln-lemma1

.....assertion..... 
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. 0 ≤ s
10. : ℚ
11. k ≤ B
12. s ≤ B
⊢ ∀n:ℕ
    ((E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (((3 s) 1) n))
    ∧ (E(f[n];(x.x x) rv-partial-sum(n;i.X[i])) ≤ (B n)))
BY
InductionOnNat
⋅ }

1
.....basecase..... 
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. 0 ≤ s
10. : ℚ
11. k ≤ B
12. s ≤ B
⊢ (E(f[0];(x.(x x) x) rv-partial-sum(0;i.X[i])) ≤ (((3 s) 1) 0))
∧ (E(f[0];(x.x x) rv-partial-sum(0;i.X[i])) ≤ (B 0))

2
.....upcase..... 
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. 0 ≤ s
10. : ℚ
11. k ≤ B
12. s ≤ B
13. : ℤ@i
14. \\%9 0 < n@i
15. (E(f[n 1];(x.(x x) x) rv-partial-sum(n 1;i.X[i])) ≤ (((3 s) 1) (n 1) (n 1)))
∧ (E(f[n 1];(x.x x) rv-partial-sum(n 1;i.X[i])) ≤ (B (n 1)))@i
⊢ (E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (((3 s) 1) n))
∧ (E(f[n];(x.x x) rv-partial-sum(n;i.X[i])) ≤ (B n))

3
.....wf..... 
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. 0 ≤ s
10. : ℚ
11. k ≤ B
12. s ≤ B
13. : ℤ@i
14. 0 < n@i
⊢ (E(f[n 1];(x.(x x) x) rv-partial-sum(n 1;i.X[i])) ≤ (((3 s) 1) (n 1) (n 1)))
  ∧ (E(f[n 1];(x.x x) rv-partial-sum(n 1;i.X[i])) ≤ (B (n 1))) ∈ ℙ

4
.....wf..... 
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. 0 ≤ s
10. : ℚ
11. k ≤ B
12. s ≤ B
13. : ℕ@i
14. (E(f[0];(x.(x x) x) rv-partial-sum(0;i.X[i])) ≤ (((3 s) 1) 0))
∧ (E(f[0];(x.x x) rv-partial-sum(0;i.X[i])) ≤ (B 0))
15. ∀n:{n:ℤ0 < n} 
      (((E(f[n 1];(x.(x x) x) rv-partial-sum(n 1;i.X[i])) ≤ (((3 s) 1) (n 1) (n 1)))
      ∧ (E(f[n 1];(x.x x) rv-partial-sum(n 1;i.X[i])) ≤ (B (n 1))))
       ((E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (((3 s) 1) n))
         ∧ (E(f[n];(x.x x) rv-partial-sum(n;i.X[i])) ≤ (B n))))
⊢ λn.((E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (((3 s) 1) n))
     ∧ (E(f[n];(x.x x) rv-partial-sum(n;i.X[i])) ≤ (B n))) ∈ ℕ ─→ ℙ


Latex:


.....assertion..... 
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
\mvdash{}  \mforall{}n:\mBbbN{}
        ((E(f[n];(x.(x  *  x)  *  x  *  x)  o  rv-partial-sum(n;i.X[i]))  \mleq{}  (((3  *  s)  +  1)  *  B  *  n  *  n))
        \mwedge{}  (E(f[n];(x.x  *  x)  o  rv-partial-sum(n;i.X[i]))  \mleq{}  (B  *  n)))


By

InductionOnNat
\mcdot{}




Home Index