---

Step * 1 1 2 1 1 1 1 of Lemma not-nullset

.....equality..... 
1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. ∀n:ℕ. E(n;λs.(C <n, s>)) < (1/2)
6. ∀tree:(n:ℕ × (ℕn ─→ Outcome)) ─→ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ─→ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ─→ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ─→ Outcome. ∀n:ℕ. (↑(tree <n, s>))))@i
7. b : ℕ@i
8. ∀x:ℕb ─→ Outcome. C <b, x> ≠ 0@i
9. E(b;λs.(C <b, s>)) < (1/2)
⊢ E(b;λs.(C <b, s>)) = 1 ∈ ℚ
BY
{ (BLemma `expectation-constant` THEN Auto) }

1
1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. ∀n:ℕ. E(n;λs.(C <n, s>)) < (1/2)
6. ∀tree:(n:ℕ × (ℕn ─→ Outcome)) ─→ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ─→ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ─→ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ─→ Outcome. ∀n:ℕ. (↑(tree <n, s>))))@i
7. b : ℕ@i
8. ∀x:ℕb ─→ Outcome. C <b, x> ≠ 0@i
9. E(b;λs.(C <b, s>)) < (1/2)
10. s : ℕb ─→ Outcome@i
11. ℤ ∈ Type
⊢ ((λs.(C <b, s>)) s) = 1 ∈ ℤ

---

Latex:


.....equality..... 
1.  p  :  FinProbSpace
2.  nullset(p;\mlambda{}s.True)@i
3.  C  :  p-open(p)
4.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C
5.  \mforall{}n:\mBbbN{}.  E(n;\mlambda{}s.(C  <n,  s>))  <  (1/2)
6.  \mforall{}tree:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbB{}
          ((\mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}j  {}\mrightarrow{}  Outcome.  ((\muparrow{}(tree  <j,  x>))  {}\mRightarrow{}  (\muparrow{}(tree  <i,  x>))))))
          {}\mRightarrow{}  (\mneg{}(\mexists{}b:\mBbbN{}.  \mforall{}x:\mBbbN{}b  {}\mrightarrow{}  Outcome.  (\mneg{}\muparrow{}(tree  <b,  x>))))
          {}\mRightarrow{}  (\mexists{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}.  (\muparrow{}(tree  <n,  s>))))@i
7.  b  :  \mBbbN{}@i
8.  \mforall{}x:\mBbbN{}b  {}\mrightarrow{}  Outcome.  C  <b,  x>  \mneq{}  0@i
9.  E(b;\mlambda{}s.(C  <b,  s>))  <  (1/2)
\mvdash{}  E(b;\mlambda{}s.(C  <b,  s>))  =  1


By

(BLemma  `expectation-constant`  THEN  Auto)

---

Home Index