---

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

.....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>)) ≤ Σ0 ≤ i < n. q * (1/2) ↑ i + 1
BY
{ (BLemma `qsum-qle` THEN Auto)⋅ }

1
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. i : ℤ@i
10. 0 ≤ i@i
11. i < n@i
⊢ E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) ≤ (q * (1/2) ↑ i + 1)

---

Latex:


.....assertion..... 
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)
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>))
\mvdash{}  \mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  \mleq{}  \mSigma{}0  \mleq{}  i  <  n.  q  *  (1/2)  \muparrow{}  i  +  1


By

(BLemma  `qsum-qle`  THEN  Auto)\mcdot{}

---

Home Index