---

Step * 1 2 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. i : ℕ
8. m1 : ℕi
9. n : ℕm1 + 1
⊢ rv-partial-sum(n;i.X[i]) ∈ RandomVariable(p;f[m1])
BY
{ ((Assert f[n] ≤ f[m1] BY
          ((Decide m1 = n ∈ ℤ THEN Auto') THEN Try ((HypSubst' (-1) 0 THEN Auto)) THEN InstHyp [⌜m1⌝;⌜n⌝] 4⋅ THEN Auto))
   THEN SubsumeC ⌜RandomVariable(p;f[n])⌝⋅
   THEN TACTIC:InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜n⌝]⋅
   THEN Auto) }

---

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.  i  :  \mBbbN{}
8.  m1  :  \mBbbN{}i
9.  n  :  \mBbbN{}m1  +  1
\mvdash{}  rv-partial-sum(n;i.X[i])  \mmember{}  RandomVariable(p;f[m1])


By

---

Latex:
((Assert  f[n]  \mleq{}  f[m1]  BY
                ((Decide  m1  =  n  THEN  Auto')
                  THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto))
                  THEN  InstHyp  [\mkleeneopen{}m1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  4\mcdot{}
                  THEN  Auto))
  THEN  SubsumeC  \mkleeneopen{}RandomVariable(p;f[n])\mkleeneclose{}\mcdot{}
  THEN  TACTIC:InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index