---

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
{ (Auto
   THEN Try ((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 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:


\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

(Auto
  THEN  Try  ((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  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