---

Step * of Lemma rv-iid-add-const

∀p:FinProbSpace. ∀a:ℚ. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n]) ⇒ rv-iid(p;n.f[n];n.X[n] + a))
BY
{ (Auto
   THEN BLemma `rv-iid-add`
   THEN Auto
   THEN Try ((BLemma `rv-disjoint-const` THEN Auto))
   THEN Try (((BLemma `rv-disjoint-symmetry` THENM BLemma `rv-disjoint-const`) THEN Auto))) }

1
1. p : FinProbSpace@i
2. a : ℚ@i
3. f : ℕ ─→ ℕ@i
4. X : n:ℕ ─→ RandomVariable(p;f[n])@i
5. rv-iid(p;n.f[n];n.X[n])@i
⊢ rv-iid(p;n.f[n];n.a)

2
.....wf..... 
1. p : FinProbSpace@i
2. a : ℚ@i
3. f : ℕ ─→ ℕ@i
4. X : n:ℕ ─→ RandomVariable(p;f[n])@i
5. rv-iid(p;n.f[n];n.X[n])@i
6. n : ℕ@i
7. i : ℕn + 1@i
8. rv-disjoint(p;f[n];a;X[n])
⊢ X[i] ∈ RandomVariable(p;f[n])

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}a:\mBbbQ{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).
    (rv-iid(p;n.f[n];n.X[n])  {}\mRightarrow{}  rv-iid(p;n.f[n];n.X[n]  +  a))


By

(Auto
  THEN  BLemma  `rv-iid-add`
  THEN  Auto
  THEN  Try  ((BLemma  `rv-disjoint-const`  THEN  Auto))
  THEN  Try  (((BLemma  `rv-disjoint-symmetry`  THENM  BLemma  `rv-disjoint-const`)  THEN  Auto)))

---

Home Index