---

Step * of Lemma rv-partial-sum-monotone

∀[p:FinProbSpace]. ∀[f:ℕ ⟶ ℕ]. ∀[X:n:ℕ ⟶ RandomVariable(p;f[n])].
  (∀[m:ℕ]. ∀[n:ℕm + 1].  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])) supposing 
     ((∀n:ℕ. 0 ≤ X[n]) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))
BY
{ TACTIC:(Auto
          THEN Try ((TACTIC:InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜m⌝]⋅ THEN Complete (Auto))⋅)
          THEN Try (((Assert f[n] ≤ f[m] BY
                            ((Decide m = n ∈ ℤ THEN Auto')
                             THEN Try ((HypSubst' (-1) 0 THEN Auto))
                             THEN InstHyp [⌜m⌝;⌜n⌝] 4⋅
                             THEN Auto))
                     THEN SubsumeC ⌜RandomVariable(p;f[n])⌝⋅
                     THEN TACTIC:InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜n⌝]⋅
                     THEN Auto)⋅)
          THEN Try ((D 1 THEN Complete (Auto)))) }

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. n : ℕm + 1
⊢ rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].
    (\mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].    rv-partial-sum(n;i.X[i])  \mleq{}  rv-partial-sum(m;i.X[i]))  supposing 
          ((\mforall{}n:\mBbbN{}.  0  \mleq{}  X[n])  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))


By

---

Latex:
TACTIC:(Auto
                THEN  Try  ((TACTIC:InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Complete  (Auto))\mcdot{})
                THEN  Try  (((Assert  f[n]  \mleq{}  f[m]  BY
                                                    ((Decide  m  =  n  THEN  Auto')
                                                      THEN  Try  ((HypSubst'  (-1)  0  THEN  Auto))
                                                      THEN  InstHyp  [\mkleeneopen{}m\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)\mcdot{})
                THEN  Try  ((D  1  THEN  Complete  (Auto))))

---

Home Index