Step
*
1
2
2
2
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 )
⊢ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|)))))
BY
{ (InstLemma `bounded-expectation` [⌈p⌉;⌈f⌉;⌈λ2k.rv-partial-sum(k;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 + 1⌉]⋅
THENA Auto
) }
1
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. n : ℕ@i
⊢ 0 ≤ 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 )
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. n : ℕ@i
16. 0 ≤ 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 )
⊢ 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 + 1
3
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. nullset(p;(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 )─→∞ as n─→∞))
⊢ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|)))))
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 )
\mvdash{} nullset(p;\mlambda{}s.\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] s)|)))))
By
(InstLemma `bounded-expectation` [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}k.rv-partial-sum(k;k.if (k =\msubz{} 0)
then 0
else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])
fi )\mkleeneclose{};\mkleeneopen{}B + 1\mkleeneclose{}]\mcdot{}
THENA Auto
)
Home
Index