---

Step * 1 1 of Lemma rv-iid-add-const


1. p : FinProbSpace@i
2. a : ℚ@i
3. f : ℕ ─→ ℕ@i
4. X : n:ℕ ─→ RandomVariable(p;f[n])@i
5. ∀n:ℕ. ∀n@0:ℕn.  (f[n@0] < f[n] ∧ rv-disjoint(p;f[n];X[n@0];X[n]))@i
6. rv-identically-distributed(p;n.f[n];n.X[n])@i
⊢ rv-identically-distributed(p;n.f[n];n.a)
BY
{ ((D 0 THEN Auto)
   THEN RepUR ``rv-const rv-compose`` 0
   THEN (Fold `rv-const` 0⋅ THEN RWO "expectation-rv-const" 0)
   THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace@i
2.  a  :  \mBbbQ{}@i
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
4.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
5.  \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
6.  rv-identically-distributed(p;n.f[n];n.X[n])@i
\mvdash{}  rv-identically-distributed(p;n.f[n];n.a)


By

((D  0  THEN  Auto)
  THEN  RepUR  ``rv-const  rv-compose``  0
  THEN  (Fold  `rv-const`  0\mcdot{}  THEN  RWO  "expectation-rv-const"  0)
  THEN  Auto)

---

Home Index