---

Step * 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. n : ℕm + 1
⊢ rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])
BY
{ (CompNatInd (-2) THEN Auto THEN Try ((UsingVars [`p';`f'] MemCD THEN 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 : ℕ@i
7. ∀m1:ℕm. ∀n:ℕm1 + 1.  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m1;i.X[i])@i
8. n : ℕm + 1@i
⊢ rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])

2
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 : ℕ@i
7. m1 : ℕm@i
8. n : ℕm1 + 1@i
⊢ rv-partial-sum(n;i.X[i]) ∈ RandomVariable(p;f[m1])

3
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:ℕ
     ((∀m1:ℕi. ∀n:ℕm1 + 1.  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m1;i.X[i]))
     ⇒ (∀n:ℕi + 1. rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(i;i.X[i])))
8. m1 : ℕ@i
9. n : ℕm1 + 1@i
⊢ rv-partial-sum(n;i.X[i]) ∈ RandomVariable(p;f[m1])

---

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


By

(CompNatInd  (-2)  THEN  Auto  THEN  Try  ((UsingVars  [`p';`f']  MemCD  THEN  Auto)))

---

Home Index