---

Step * of Lemma rv-partial-sum_wf

∀[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])]. ∀[n:ℕ].
  rv-partial-sum(n;i.X[i]) ∈ RandomVariable(p;f[n]) supposing ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
BY
{ (Auto THEN Unfold `rv-partial-sum` 0 THEN All (Unfold `random-variable`) THEN All (Fold `p-outcome`) THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].  \mforall{}[n:\mBbbN{}].
    rv-partial-sum(n;i.X[i])  \mmember{}  RandomVariable(p;f[n])  supposing  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]


By

(Auto
  THEN  Unfold  `rv-partial-sum`  0
  THEN  All  (Unfold  `random-variable`)
  THEN  All  (Fold  `p-outcome`)
  THEN  Auto)

---

Home Index