---

Step * 2 of Lemma rv-iid-add


1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. Y : n:ℕ ─→ RandomVariable(p;f[n])@i
5. rv-identically-distributed(p;n.f[n];n.X[n])@i
6. ∀n:ℕ. ∀n@0:ℕn.  (f[n@0] < f[n] ∧ rv-disjoint(p;f[n];X[n@0];X[n]))@i
7. rv-identically-distributed(p;n.f[n];n.Y[n])@i
8. ∀n:ℕ. ∀n@0:ℕn.  (f[n@0] < f[n] ∧ rv-disjoint(p;f[n];Y[n@0];Y[n]))@i
9. ∀n:ℕ. ∀i:ℕn + 1.  (RandomVariable(p;f[i]) ⊆r RandomVariable(p;f[n]))
10. ∀n:ℕ. ∀i:ℕn + 1.  (rv-disjoint(p;f[n];Y[i];X[n]) ∧ rv-disjoint(p;f[n];X[i];Y[n]))@i
⊢ ∀n:ℕ. ∀n@0:ℕn.  (f[n@0] < f[n] ∧ rv-disjoint(p;f[n];X[n@0] + Y[n@0];X[n] + Y[n]))
BY
{ (Auto⋅
   THEN (BLemma `rv-disjoint-rv-add2`  THENM Try (BLemma `rv-disjoint-rv-add` ⋅))⋅
   THEN Try ((DoSubsume THEN Complete (Auto)))
   THEN Try (Complete (Auto)))⋅ }

---

Latex:



1.  p  :  FinProbSpace@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
4.  Y  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
5.  rv-identically-distributed(p;n.f[n];n.X[n])@i
6.  \mforall{}n:\mBbbN{}.  \mforall{}n@0:\mBbbN{}n.    (f[n@0]  <  f[n]  \mwedge{}  rv-disjoint(p;f[n];X[n@0];X[n]))@i
7.  rv-identically-distributed(p;n.f[n];n.Y[n])@i
8.  \mforall{}n:\mBbbN{}.  \mforall{}n@0:\mBbbN{}n.    (f[n@0]  <  f[n]  \mwedge{}  rv-disjoint(p;f[n];Y[n@0];Y[n]))@i
9.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n  +  1.    (RandomVariable(p;f[i])  \msubseteq{}r  RandomVariable(p;f[n]))
10.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n  +  1.    (rv-disjoint(p;f[n];Y[i];X[n])  \mwedge{}  rv-disjoint(p;f[n];X[i];Y[n]))@i
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}n@0:\mBbbN{}n.    (f[n@0]  <  f[n]  \mwedge{}  rv-disjoint(p;f[n];X[n@0]  +  Y[n@0];X[n]  +  Y[n]))


By

(Auto\mcdot{}
  THEN  (BLemma  `rv-disjoint-rv-add2`    THENM  Try  (BLemma  `rv-disjoint-rv-add`  \mcdot{}))\mcdot{}
  THEN  Try  ((DoSubsume  THEN  Complete  (Auto)))
  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index