Step
*
2
2
1
2
of Lemma
slln-lemma1
.....upcase.....
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. [%9] : 0 < n
15. (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1)))
∧ (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (B * (n - 1)))
⊢ (E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n;i.X[i])) ≤ (((3 * s) + 1) * B * n * n))
∧ (E(f[n];(x.x * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n))
BY
{ (((Assert ⌜f[n - 1] < f[n]⌝⋅ THENA Auto) THEN PromoteHyp (-1) 14)
THEN (InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜n - 1⌝]⋅ THENA Auto)
THEN Subst' rv-partial-sum(n;i.X[i]) = rv-partial-sum(n - 1;i.X[i]) + X[n - 1] ∈ RandomVariable(p;f[n]) 0⋅) }
1
.....equality.....
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. 0 < n
16. (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1)))
∧ (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (B * (n - 1)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
⊢ rv-partial-sum(n;i.X[i]) = rv-partial-sum(n - 1;i.X[i]) + X[n - 1] ∈ RandomVariable(p;f[n])
2
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. [%9] : 0 < n
16. (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1)))
∧ (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (B * (n - 1)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
⊢ (E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i]) + X[n - 1]) ≤ (((3 * s) + 1) * B * n * n))
∧ (E(f[n];(x.x * x) o rv-partial-sum(n - 1;i.X[i]) + X[n - 1]) ≤ (B * n))
3
.....wf.....
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. 0 ≤ s
10. B : ℚ
11. k ≤ B
12. s ≤ B
13. n : ℤ
14. f[n - 1] < f[n]
15. 0 < n
16. (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (((3 * s) + 1) * B * (n - 1) * (n - 1)))
∧ (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) ≤ (B * (n - 1)))
17. rv-partial-sum(n - 1;i.X[i]) ∈ RandomVariable(p;f[n - 1])
18. z : RandomVariable(p;f[n])
⊢ (E(f[n];(x.(x * x) * x * x) o z) ≤ (((3 * s) + 1) * B * n * n)) ∧ (E(f[n];(x.x * x) o z) ≤ (B * n)) ∈ ℙ
Latex:
Latex:
.....upcase.....
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. 0 \mleq{} s
10. B : \mBbbQ{}
11. k \mleq{} B
12. s \mleq{} B
13. n : \mBbbZ{}
14. [\%9] : 0 < n
15. (E(f[n - 1];(x.(x * x) * x * x) o rv-partial-sum(n - 1;i.X[i])) \mleq{} (((3 * s) + 1)
* B
* (n - 1)
* (n - 1)))
\mwedge{} (E(f[n - 1];(x.x * x) o rv-partial-sum(n - 1;i.X[i])) \mleq{} (B * (n - 1)))
\mvdash{} (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
Latex:
(((Assert \mkleeneopen{}f[n - 1] < f[n]\mkleeneclose{}\mcdot{} THENA Auto) THEN PromoteHyp (-1) 14)
THEN (InstLemma `rv-partial-sum\_wf` [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}n - 1\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Subst' rv-partial-sum(n;i.X[i]) = rv-partial-sum(n - 1;i.X[i]) + X[n - 1] 0\mcdot{})
Home
Index