---

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


1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
5. ∀n:ℕ. 0 ≤ X[n]
6. m : ℕ
7. ∀m1:ℕm. ∀n:ℕm1 + 1.  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m1;i.X[i])
8. n : ℕm + 1
9. ¬(n = m ∈ ℤ)
10. A : RandomVariable(p;f[n])
11. B : RandomVariable(p;f[m - 1])
12. C : RandomVariable(p;f[m - 1])
13. f[n] ≤ f[m - 1]
⊢ 0 ≤ C ⇒ A ≤ B ⇒ A ≤ B + C
BY
{ TACTIC:((All (RepUR ``random-variable rv-le rv-const rv-add``))
          THEN (All (Fold `p-outcome`))
          THEN Auto
          THEN (Assert f[m - 1] < f[m] BY
                      Auto)
          THEN RepeatFor 2 (((InstHyp [⌜s⌝] (-4))⋅ THENA Auto))
          THEN (RW (SweepDnC (HypC (-1))) 0)
          THEN Auto) }

1
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 : ℕ
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))
8. n : ℕm + 1
9. ¬(n = m ∈ ℤ)
10. A : (ℕf[n] ⟶ Outcome) ⟶ ℚ
11. B : (ℕf[m - 1] ⟶ Outcome) ⟶ ℚ
12. C : (ℕf[m - 1] ⟶ Outcome) ⟶ ℚ
13. f[n] ≤ f[m - 1]
14. ∀s:ℕf[m - 1] ⟶ Outcome. (0 ≤ (C s))
15. ∀s:ℕf[m - 1] ⟶ Outcome. ((A s) ≤ (B s))
16. s : ℕf[m] ⟶ Outcome
17. f[m - 1] < f[m]
18. 0 ≤ (C s)
19. (A s) ≤ (B s)
⊢ (B s) ≤ ((B s) + (C s))

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((All  (RepUR  ``random-variable  rv-le  rv-const  rv-add``))
                THEN  (All  (Fold  `p-outcome`))
                THEN  Auto
                THEN  (Assert  f[m  -  1]  <  f[m]  BY
                                        Auto)
                THEN  RepeatFor  2  (((InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  (-4))\mcdot{}  THENA  Auto))
                THEN  (RW  (SweepDnC  (HypC  (-1)))  0)
                THEN  Auto)

---

Home Index