---

Step * of Lemma rv-disjoint-rv-partial-sum

∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀N:ℕ. ∀Z:RandomVariable(p;N). ∀n:ℕ.
  (∀i:ℕn - 1. rv-disjoint(p;N;X[i];Z)) ⇒ (∀k:ℕn. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) supposing ∀i:ℕn. f[i] < N
BY
{ (RepeatFor 5 ((D 0 THENA Auto)) THEN InductionOnNat THEN Auto THEN (Assert ||p|| ∈ ℕ BY (DVar `p' THEN Auto))) }

1
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. N : ℕ@i
5. Z : RandomVariable(p;N)@i
6. n : ℤ@i
7. \\%1 : 0 < n@i
8. (∀i:ℕn - 1 - 1. rv-disjoint(p;N;X[i];Z)) ⇒ (∀k:ℕn - 1. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) 
   supposing ∀i:ℕn - 1. f[i] < N@i
9. ∀i:ℕn. f[i] < N
10. ∀i:ℕn - 1. rv-disjoint(p;N;X[i];Z)@i
11. k : ℕn@i
12. ||p|| ∈ ℕ
⊢ rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)

2
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. N : ℕ@i
5. Z : RandomVariable(p;N)@i
6. n : ℤ@i
7. 0 < n@i
8. ∀i:ℕn - 1. f[i] < N@i
9. ∀i:ℕn - 1 - 1. rv-disjoint(p;N;X[i];Z)
10. k : ℕn - 1@i
11. ||p|| ∈ ℕ
⊢ rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;N)

3
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. N : ℕ@i
5. Z : RandomVariable(p;N)@i
6. n : ℕ@i
7. (∀i:ℕ0 - 1. rv-disjoint(p;N;X[i];Z)) ⇒ (∀k:ℕ0. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) 
   supposing ∀i:ℕ0. f[i] < N
8. ∀n:{n:ℤ| 0 < n} 
     ((∀i:ℕn - 1 - 1. rv-disjoint(p;N;X[i];Z)) ⇒ (∀k:ℕn - 1. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) 
      supposing ∀i:ℕn - 1. f[i] < N
     ⇒ (∀i:ℕn - 1. rv-disjoint(p;N;X[i];Z)) ⇒ (∀k:ℕn. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) 
        supposing ∀i:ℕn. f[i] < N)
9. n1 : ℕ@i
10. ∀i:ℕn1. f[i] < N@i
11. ∀i:ℕn1 - 1. rv-disjoint(p;N;X[i];Z)
12. k : ℕn1@i
13. ||p|| ∈ ℕ
⊢ rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;N)

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).  \mforall{}N:\mBbbN{}.  \mforall{}Z:RandomVariable(p;N).  \mforall{}n:\mBbbN{}.
    (\mforall{}i:\mBbbN{}n  -  1.  rv-disjoint(p;N;X[i];Z))  {}\mRightarrow{}  (\mforall{}k:\mBbbN{}n.  rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) 
    supposing  \mforall{}i:\mBbbN{}n.  f[i]  <  N


By

(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  InductionOnNat
  THEN  Auto
  THEN  (Assert  ||p||  \mmember{}  \mBbbN{}  BY
                          (DVar  `p'  THEN  Auto)))

---

Home Index