---

Step * 1 1 1 2 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. rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m - 1;i.X[i])
⊢ rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m - 1;i.X[i]) + X[m - 1]
BY
{ TACTIC:((MoveToConcl (-1))
          THEN (GenConcl ⌜rv-partial-sum(n;i.X[i]) = A ∈ RandomVariable(p;f[n])⌝⋅
                THENA (Auto THEN InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜n⌝]⋅ THEN Auto)
                )
          THEN (Thin (-1))
          THEN (GenConcl ⌜rv-partial-sum(m - 1;i.X[i]) = B ∈ RandomVariable(p;f[m - 1])⌝⋅
                THENA (Auto THEN InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜m - 1⌝]⋅ THEN Auto)
                )
          THEN (Thin (-1))
          THEN (Assert 0 ≤ X[m - 1] BY
                      Auto)
          THEN (MoveToConcl (-1))
          THEN (GenConcl ⌜X[m - 1] = C ∈ RandomVariable(p;f[m - 1])⌝⋅ THENA Auto)
          THEN (Thin (-1))) }

1
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])
⊢ 0 ≤ C ⇒ A ≤ B ⇒ A ≤ B + C

---

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.  rv-partial-sum(n;i.X[i])  \mleq{}  rv-partial-sum(m  -  1;i.X[i])
\mvdash{}  rv-partial-sum(n;i.X[i])  \mleq{}  rv-partial-sum(m  -  1;i.X[i])  +  X[m  -  1]


By

---

Latex:
TACTIC:((MoveToConcl  (-1))
                THEN  (GenConcl  \mkleeneopen{}rv-partial-sum(n;i.X[i])  =  A\mkleeneclose{}\mcdot{}
                            THENA  (Auto  THEN  InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            )
                THEN  (Thin  (-1))
                THEN  (GenConcl  \mkleeneopen{}rv-partial-sum(m  -  1;i.X[i])  =  B\mkleeneclose{}\mcdot{}
                            THENA  (Auto  THEN  InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}m  -  1\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            )
                THEN  (Thin  (-1))
                THEN  (Assert  0  \mleq{}  X[m  -  1]  BY
                                        Auto)
                THEN  (MoveToConcl  (-1))
                THEN  (GenConcl  \mkleeneopen{}X[m  -  1]  =  C\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (Thin  (-1)))

---

Home Index