---

Step * 1 2 1 1 2 2 2 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:ℚ. (0 < q ⇒ (∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q))
10. q : ℚ
11. 0 < q
12. b : ℚ
13. ∀n:ℕ. E(f[n];b ≤ X[n]) < q
14. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  Dec(∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
15. g : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
16. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  ((g <n, s>) = 1 ∈ ℤ ⇐⇒ ∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
17. n : ℕ
⊢ E(n;λs.(g <n, s>)) < q
BY
{ Assert ⌜E(n;λs.(g <n, s>)) ≤ E(f[n];b ≤ X[n])⌝⋅ }

1
.....assertion..... 
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:ℚ. (0 < q ⇒ (∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q))
10. q : ℚ
11. 0 < q
12. b : ℚ
13. ∀n:ℕ. E(f[n];b ≤ X[n]) < q
14. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  Dec(∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
15. g : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
16. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  ((g <n, s>) = 1 ∈ ℤ ⇐⇒ ∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
17. n : ℕ
⊢ E(n;λs.(g <n, s>)) ≤ E(f[n];b ≤ X[n])

2
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:ℚ. (0 < q ⇒ (∃b:ℚ. ∀n:ℕ. E(f[n];b ≤ X[n]) < q))
10. q : ℚ
11. 0 < q
12. b : ℚ
13. ∀n:ℕ. E(f[n];b ≤ X[n]) < q
14. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  Dec(∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
15. g : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
16. ∀n:ℕ. ∀s:ℕn ⟶ Outcome.  ((g <n, s>) = 1 ∈ ℤ ⇐⇒ ∃i:ℕn. (f[i] < n c∧ (b ≤ (X[i] s))))
17. n : ℕ
18. E(n;λs.(g <n, s>)) ≤ E(f[n];b ≤ X[n])
⊢ E(n;λs.(g <n, s>)) < q

---

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.  \mforall{}q:\mBbbQ{}.  (0  <  q  {}\mRightarrow{}  (\mexists{}b:\mBbbQ{}.  \mforall{}n:\mBbbN{}.  E(f[n];b  \mleq{}  X[n])  <  q))
10.  q  :  \mBbbQ{}
11.  0  <  q
12.  b  :  \mBbbQ{}
13.  \mforall{}n:\mBbbN{}.  E(f[n];b  \mleq{}  X[n])  <  q
14.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.    Dec(\mexists{}i:\mBbbN{}n.  (f[i]  <  n  c\mwedge{}  (b  \mleq{}  (X[i]  s))))
15.  g  :  (n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2
16.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.    ((g  <n,  s>)  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (f[i]  <  n  c\mwedge{}  (b  \mleq{}  (X[i]  s))))
17.  n  :  \mBbbN{}
\mvdash{}  E(n;\mlambda{}s.(g  <n,  s>))  <  q


By

---

Latex:
Assert  \mkleeneopen{}E(n;\mlambda{}s.(g  <n,  s>))  \mleq{}  E(f[n];b  \mleq{}  X[n])\mkleeneclose{}\mcdot{}

---

Home Index