---

Step * 1 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
⊢ rv-identically-distributed(p;n.f[n];n.X[n] + Y[n])
BY
{ ((All (Unfold `rv-identically-distributed`))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN AllHyps h.(((InstHyp [⌈n⌉; ⌈m⌉] h)⋅ THENA Complete (Auto)) THEN Thin h) 
   THEN ExRepD
   THEN (RWO "expectation-rv-add" 0 THENA Auto)⋅
   THEN Try ((RWO "expectation-rv-add" 0 THEN Auto)⋅)
   THEN (RWO "expectation-rv-add-squared" 0 THENA Auto)⋅
   THEN Try ((RWO "expectation-rv-add-squared" 0 THEN Auto)⋅)
   THEN (RWO "expectation-rv-add-cubed" 0 THENA Auto)⋅
   THEN Try ((RWO "expectation-rv-add-cubed" 0 THEN Auto))
   THEN (RWO "expectation-rv-add-fourth" 0 THENA Auto)⋅
   THEN (Try ((RWO "expectation-rv-add-fourth" 0 THEN Auto))
         THEN Auto
         THEN (RepeatFor 3 ((EqCD THEN Auto))
               THEN (RWO "expectation-rv-disjoint" 0 THENA Auto)
               THEN Repeat ((BLemma `rv-disjoint-rv-mul2` THEN Auto))
               THEN Repeat ((BLemma `rv-disjoint-rv-mul` THEN Auto))
               THEN RepeatFor 2 ((EqCD THEN Auto))
               THEN Try (OnMaybeHyp 13 (\h. (NthHypSq h
                                             THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
                                             THEN RepUR ``rv-compose rv-mul`` 0
                                             THEN Trivial)))
               THEN EqCD
               THEN Auto
               THEN Try (OnMaybeHyp 13 (\h. (NthHypSq h
                                             THEN RepeatFor 2 ((EqCD THEN Try (Trivial)))
                                             THEN RepUR ``rv-compose rv-mul`` 0
                                             THEN Trivial))))⋅)⋅)⋅ }

---

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


By

((All  (Unfold  `rv-identically-distributed`))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  AllHyps  h.(((InstHyp  [\mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{}]  h)\mcdot{}  THENA  Complete  (Auto))  THEN  Thin  h) 
  THEN  ExRepD
  THEN  (RWO  "expectation-rv-add"  0  THENA  Auto)\mcdot{}
  THEN  Try  ((RWO  "expectation-rv-add"  0  THEN  Auto)\mcdot{})
  THEN  (RWO  "expectation-rv-add-squared"  0  THENA  Auto)\mcdot{}
  THEN  Try  ((RWO  "expectation-rv-add-squared"  0  THEN  Auto)\mcdot{})
  THEN  (RWO  "expectation-rv-add-cubed"  0  THENA  Auto)\mcdot{}
  THEN  Try  ((RWO  "expectation-rv-add-cubed"  0  THEN  Auto))
  THEN  (RWO  "expectation-rv-add-fourth"  0  THENA  Auto)\mcdot{}
  THEN  (Try  ((RWO  "expectation-rv-add-fourth"  0  THEN  Auto))
              THEN  Auto
              THEN  (RepeatFor  3  ((EqCD  THEN  Auto))
                          THEN  (RWO  "expectation-rv-disjoint"  0  THENA  Auto)
                          THEN  Repeat  ((BLemma  `rv-disjoint-rv-mul2`  THEN  Auto))
                          THEN  Repeat  ((BLemma  `rv-disjoint-rv-mul`  THEN  Auto))
                          THEN  RepeatFor  2  ((EqCD  THEN  Auto))
                          THEN  Try  (OnMaybeHyp  13  (\mbackslash{}h.  (NthHypSq  h
                                                                                      THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
                                                                                      THEN  RepUR  ``rv-compose  rv-mul``  0
                                                                                      THEN  Trivial)))
                          THEN  EqCD
                          THEN  Auto
                          THEN  Try  (OnMaybeHyp  13  (\mbackslash{}h.  (NthHypSq  h
                                                                                      THEN  RepeatFor  2  ((EqCD  THEN  Try  (Trivial)))
                                                                                      THEN  RepUR  ``rv-compose  rv-mul``  0
                                                                                      THEN  Trivial))))\mcdot{})\mcdot{})\mcdot{}

---

Home Index