---

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


1. p : FinProbSpace@i
2. q : {q:ℚ| 0 < q} @i
3. ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} )
4. F : ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)@i
5. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q@i
6. n : ℕ@i
7. ¬(n = 0 ∈ ℤ)
⊢ E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) < q
BY
{ ((InstLemma `expectation-imax-list` [⌈p⌉;⌈n⌉;⌈n⌉;⌈λ2i.λs.(F i (q * (1/2) ↑ i + 1) <n, s>)⌉]⋅ THENA Auto)
   THEN (Reduce (-1))
   THEN Assert ⌈Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) < q⌉⋅)⋅ }

1
.....assertion..... 
1. p : FinProbSpace@i
2. q : {q:ℚ| 0 < q} @i
3. ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} )
4. F : ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)@i
5. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q@i
6. n : ℕ@i
7. ¬(n = 0 ∈ ℤ)
8. E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) ≤ Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n,\000C s>))
⊢ Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) < q

2
1. p : FinProbSpace@i
2. q : {q:ℚ| 0 < q} @i
3. ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} )
4. F : ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)@i
5. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q@i
6. n : ℕ@i
7. ¬(n = 0 ∈ ℤ)
8. E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) ≤ Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n,\000C s>))
9. Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) < q
⊢ E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) < q

---

Latex:



1.  p  :  FinProbSpace@i
2.  q  :  \{q:\mBbbQ{}|  0  <  q\}  @i
3.  \mforall{}k:\mBbbN{}.  (q  *  (1/2)  \muparrow{}  k  \mmember{}  \{q:\mBbbQ{}|  0  <  q\}  )
4.  F  :  \mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p)@i
5.  \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    measure(F  i  q)  \mleq{}  q@i
6.  n  :  \mBbbN{}@i
7.  \mneg{}(n  =  0)
\mvdash{}  E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>);upto(n))))  <  q


By

((InstLemma  `expectation-imax-list`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>)\mkleeneclose{}]\mcdot{}  THENA  A\000Cuto)
  THEN  (Reduce  (-1))
  THEN  Assert  \mkleeneopen{}\mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  <  q\mkleeneclose{}\mcdot{})\mcdot{}

---

Home Index