---

Step * 1 1 2 1 1 1 1 of Lemma rv-partial-sum-monotone


1. p : FinProbSpace
2. f : ℕ ─→ ℕ
3. X : n:ℕ ─→ (ℕf[n] ─→ Outcome) ─→ ℚ
4. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
5. ∀n:ℕ. ∀s:ℕf[n] ─→ Outcome.  (0 ≤ (X[n] s))
6. m : ℕ@i
7. ∀m1:ℕm. ∀n:ℕm1 + 1. ∀s:ℕf[m1] ─→ Outcome.  ((rv-partial-sum(n;i.X[i]) s) ≤ (rv-partial-sum(m1;i.X[i]) s))@i
8. n : ℕm + 1@i
9. ¬(n = m ∈ ℤ)
10. A : (ℕf[n] ─→ Outcome) ─→ ℚ@i
11. B : (ℕf[m - 1] ─→ Outcome) ─→ ℚ@i
12. C : (ℕf[m - 1] ─→ Outcome) ─→ ℚ@i
13. f[n] ≤ f[m - 1]
14. ∀s:ℕf[m - 1] ─→ Outcome. (0 ≤ (C s))@i
15. ∀s:ℕf[m - 1] ─→ Outcome. ((A s) ≤ (B s))@i
16. s : ℕf[m] ─→ Outcome@i
17. f[m - 1] < f[m]
18. 0 ≤ (C s)
19. (A s) ≤ (B s)
⊢ (B s) ≤ ((B s) + (C s))
BY
{ (QSubtract ⌈B s⌉ 0⋅ THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}f[n]  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbQ{}
4.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]
5.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}f[n]  {}\mrightarrow{}  Outcome.    (0  \mleq{}  (X[n]  s))
6.  m  :  \mBbbN{}@i
7.  \mforall{}m1:\mBbbN{}m.  \mforall{}n:\mBbbN{}m1  +  1.  \mforall{}s:\mBbbN{}f[m1]  {}\mrightarrow{}  Outcome.
          ((rv-partial-sum(n;i.X[i])  s)  \mleq{}  (rv-partial-sum(m1;i.X[i])  s))@i
8.  n  :  \mBbbN{}m  +  1@i
9.  \mneg{}(n  =  m)
10.  A  :  (\mBbbN{}f[n]  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbQ{}@i
11.  B  :  (\mBbbN{}f[m  -  1]  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbQ{}@i
12.  C  :  (\mBbbN{}f[m  -  1]  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbQ{}@i
13.  f[n]  \mleq{}  f[m  -  1]
14.  \mforall{}s:\mBbbN{}f[m  -  1]  {}\mrightarrow{}  Outcome.  (0  \mleq{}  (C  s))@i
15.  \mforall{}s:\mBbbN{}f[m  -  1]  {}\mrightarrow{}  Outcome.  ((A  s)  \mleq{}  (B  s))@i
16.  s  :  \mBbbN{}f[m]  {}\mrightarrow{}  Outcome@i
17.  f[m  -  1]  <  f[m]
18.  0  \mleq{}  (C  s)
19.  (A  s)  \mleq{}  (B  s)
\mvdash{}  (B  s)  \mleq{}  ((B  s)  +  (C  s))


By

(QSubtract  \mkleeneopen{}B  s\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index