Step
*
1
2
2
2
3
2
1
of Lemma
slln-lemma3
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. B : ℚ
10. ∀n:ℕ
(E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
11. ∀n:ℕ
(rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
rv-partial-sum(i;k.if (k =z 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi ) ≤ rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
15. ∀s:ℕ ─→ Outcome. ∀n:ℕ+. (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ]. ((∀s:ℕ ─→ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ─→ Outcome@i
18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i
19. B1 : ℚ@i
⊢ ∃n:ℕ
∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ0 ≤ k < m. if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s fi s1))
BY
{ Assert ⌈∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))⌉⋅ }
1
.....assertion.....
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. B : ℚ
10. ∀n:ℕ
(E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
11. ∀n:ℕ
(rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
rv-partial-sum(i;k.if (k =z 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi ) ≤ rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
15. ∀s:ℕ ─→ Outcome. ∀n:ℕ+. (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ]. ((∀s:ℕ ─→ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ─→ Outcome@i
18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i
19. B1 : ℚ@i
⊢ ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))
2
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. B : ℚ
10. ∀n:ℕ
(E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
11. ∀n:ℕ
(rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
rv-partial-sum(i;k.if (k =z 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi ) ≤ rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )
15. ∀s:ℕ ─→ Outcome. ∀n:ℕ+. (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ]. ((∀s:ℕ ─→ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ─→ Outcome@i
18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i
19. B1 : ℚ@i
20. ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))
⊢ ∃n:ℕ
∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ0 ≤ k < m. if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s fi s1))
Latex:
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. \mforall{}n:\mBbbN{}
(E(f[n];rv-partial-sum(n;k.if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi )) \mleq{} B)
11. \mforall{}n:\mBbbN{}
(rv-partial-sum(n;k.if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi ) \mmember{} RandomVariable(p;f[n]))
12. 0 \mleq{} B
13. B < B + 1
14. \mforall{}n:\mBbbN{}. \mforall{}i:\mBbbN{}n.
rv-partial-sum(i;k.if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi ) \mleq{} rv-partial-sum(n;k.if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi )
15. \mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. \mforall{}n:\mBbbN{}\msupplus{}. (\mSigma{}0 \mleq{} i < n. (1/n) * (X i s) \mmember{} \mBbbQ{})
16. \mforall{}p:FinProbSpace
\mforall{}[P,Q:(\mBbbN{} {}\mrightarrow{} Outcome) {}\mrightarrow{} \mBbbP{}].
((\mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. (Q[s] {}\mRightarrow{} P[s])) {}\mRightarrow{} \{nullset(p;P) {}\mRightarrow{} nullset(p;Q)\})
17. s1 : \mBbbN{} {}\mrightarrow{} Outcome@i
18. \mexists{}q:\mBbbQ{}. (0 < q \mwedge{} (\mforall{}n:\mBbbN{}. \mexists{}m:\mBbbN{}. (n < m \mwedge{} (q \mleq{} |\mSigma{}0 \mleq{} i < m. (1/m) * (X i s1)|))))@i
19. B1 : \mBbbQ{}@i
\mvdash{} \mexists{}n:\mBbbN{}
\mforall{}m:\mBbbN{}
((n \mleq{} m)
{}\mRightarrow{} (B1 \mleq{} \mSigma{}0 \mleq{} k < m. if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s
fi
s1))
By
Assert \mkleeneopen{}\mexists{}n:\mBbbN{}
\mforall{}m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} (B1 \mleq{} \mSigma{}1 \mleq{} k < m. (x.(x * x) * x * x) o (1/k)*\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s s1))\mkleeneclose{}\mcdot{}
Home
Index