---

Step * of Lemma rv-iid-add

∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X,Y:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
  ⇒ rv-iid(p;n.f[n];n.Y[n])
  ⇒ (∀n:ℕ. ∀i:ℕn + 1.  (rv-disjoint(p;f[n];Y[i];X[n]) ∧ rv-disjoint(p;f[n];X[i];Y[n])))
  ⇒ rv-iid(p;n.f[n];n.X[n] + Y[n]))
BY
{ (RepeatFor 6 ((D 0 THENA Complete (Auto)))
   THEN (Assert ∀n:ℕ. ∀i:ℕn + 1.  (RandomVariable(p;f[i]) ⊆r RandomVariable(p;f[n])) BY
               (Auto
                THEN Try ((Dvar 0 THEN Complete (Auto)))
                THEN Assert ⌈f[i] ≤ f[n]⌉⋅
                THEN Auto
                THEN Decide ⌈i = n ∈ ℤ⌉⋅
                THEN Auto
                THEN Assert ⌈f[i] < f[n]⌉⋅
                THEN Auto))⋅
   THEN Auto
   THEN Try ((DoSubsume THEN Auto))
   THEN (All (Unfold `rv-iid`))
   THEN ExRepD
   THEN D 0) }

1
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
⊢ rv-identically-distributed(p;n.f[n];n.X[n] + Y[n])

2
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]))

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X,Y:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).
    (rv-iid(p;n.f[n];n.X[n])
    {}\mRightarrow{}  rv-iid(p;n.f[n];n.Y[n])
    {}\mRightarrow{}  (\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])))
    {}\mRightarrow{}  rv-iid(p;n.f[n];n.X[n]  +  Y[n]))


By

(RepeatFor  6  ((D  0  THENA  Complete  (Auto)))
  THEN  (Assert  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n  +  1.    (RandomVariable(p;f[i])  \msubseteq{}r  RandomVariable(p;f[n]))  BY
                          (Auto
                            THEN  Try  ((Dvar  0  THEN  Complete  (Auto)))
                            THEN  Assert  \mkleeneopen{}f[i]  \mleq{}  f[n]\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  Decide  \mkleeneopen{}i  =  n\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  Assert  \mkleeneopen{}f[i]  <  f[n]\mkleeneclose{}\mcdot{}
                            THEN  Auto))\mcdot{}
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto))
  THEN  (All  (Unfold  `rv-iid`))
  THEN  ExRepD
  THEN  D  0)

---

Home Index