---

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


1. p : FinProbSpace
2. q : {q:ℚ| 0 < q} 
3. ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} )
4. F : ℕ ⟶ {q:ℚ| 0 < q}  ⟶ p-open(p)
5. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q
6. n : ℕ
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. i : ℤ
10. 0 ≤ i
11. i < n
⊢ E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) ≤ (q * (1/2) ↑ i + 1)
BY
{ ((Assert E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) < q * (1/2) ↑ i + 1 BY
          OnMaybeHyp 5 (\h. (Unfold `p-measure-le` h
                             THEN InstHyp [⌜i⌝;⌜q * (1/2) ↑ i + 1⌝;⌜n⌝] h⋅
                             THEN Complete (Auto))))⋅
   THEN (RelRST  THEN Auto)⋅
   ) }

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  q  :  \{q:\mBbbQ{}|  0  <  q\} 
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)
5.  \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    measure(F  i  q)  \mleq{}  q
6.  n  :  \mBbbN{}
7.  \mneg{}(n  =  0)
8.  E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>);upto(n))))  \mleq{}  \mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  \000C*  (1/2)  \muparrow{}  i  +  1)  <n,  s>))
9.  i  :  \mBbbZ{}
10.  0  \mleq{}  i
11.  i  <  n
\mvdash{}  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  \mleq{}  (q  *  (1/2)  \muparrow{}  i  +  1)


By

---

Latex:
((Assert  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  <  q  *  (1/2)  \muparrow{}  i  +  1  BY
                OnMaybeHyp  5  (\mbackslash{}h.  (Unfold  `p-measure-le`  h
                                                      THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}q  *  (1/2)  \muparrow{}  i  +  1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}
                                                      THEN  Complete  (Auto))))\mcdot{}
  THEN  (RelRST    THEN  Auto)\mcdot{}
  )

---

Home Index