---

Step * 1 1 1 1 1 1 1 1 1 of Lemma bounded-expectation


1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. B : ℚ
5. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
6. ∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]
7. 0 < B
8. ∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)
9. q : ℚ
10. 0 < q
11. ¬(q = 0 ∈ ℚ)
12. 0 < (B/q)
13. ¬((B/q) = 0 ∈ ℚ)
14. n : ℕ
15. E(f[n];(B/q) ≤ X[n]) ≤ (E(f[n];X[n])/(B/q))
16. 0 ≤ X[n]
17. E(f[n];X[n]) * (1/(B/q)) < (1/(B/q)) * B
⊢ (E(f[n];X[n])/(B/q)) < q
BY
{ (NthHypEq (-1) THEN EqCD THEN Auto) }

1
.....subterm..... T:t
1:n
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. B : ℚ
5. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
6. ∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]
7. 0 < B
8. ∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)
9. q : ℚ
10. 0 < q
11. ¬(q = 0 ∈ ℚ)
12. 0 < (B/q)
13. ¬((B/q) = 0 ∈ ℚ)
14. n : ℕ
15. E(f[n];(B/q) ≤ X[n]) ≤ (E(f[n];X[n])/(B/q))
16. 0 ≤ X[n]
17. E(f[n];X[n]) * (1/(B/q)) < (1/(B/q)) * B
⊢ (E(f[n];X[n])/(B/q)) = (E(f[n];X[n]) * (1/(B/q))) ∈ ℚ

2
.....subterm..... T:t
2:n
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. B : ℚ
5. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
6. ∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]
7. 0 < B
8. ∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)
9. q : ℚ
10. 0 < q
11. ¬(q = 0 ∈ ℚ)
12. 0 < (B/q)
13. ¬((B/q) = 0 ∈ ℚ)
14. n : ℕ
15. E(f[n];(B/q) ≤ X[n]) ≤ (E(f[n];X[n])/(B/q))
16. 0 ≤ X[n]
17. E(f[n];X[n]) * (1/(B/q)) < (1/(B/q)) * B
⊢ q = ((1/(B/q)) * B) ∈ ℚ

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])
4.  B  :  \mBbbQ{}
5.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]
6.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    X[i]  \mleq{}  X[n]
7.  0  <  B
8.  \mforall{}n:\mBbbN{}.  (0  \mleq{}  X[n]  \mwedge{}  E(f[n];X[n])  <  B)
9.  q  :  \mBbbQ{}
10.  0  <  q
11.  \mneg{}(q  =  0)
12.  0  <  (B/q)
13.  \mneg{}((B/q)  =  0)
14.  n  :  \mBbbN{}
15.  E(f[n];(B/q)  \mleq{}  X[n])  \mleq{}  (E(f[n];X[n])/(B/q))
16.  0  \mleq{}  X[n]
17.  E(f[n];X[n])  *  (1/(B/q))  <  (1/(B/q))  *  B
\mvdash{}  (E(f[n];X[n])/(B/q))  <  q


By

---

Latex:
(NthHypEq  (-1)  THEN  EqCD  THEN  Auto)

---

Home Index