### Nuprl 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]`

Proof

Definitions occuring in Statement :  rv-partial-sum: `rv-partial-sum(n;i.X[i])` random-variable: `RandomVariable(p;n)` finite-prob-space: `FinProbSpace` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` function: `x:A ─→ B[x]` natural_number: `\$n`
Lemmas :  Error :qsum_wf,  int_seg_subtype-nat false_wf subtype_rel_dep_function int_seg_wf p-outcome_wf subtype_rel-int_seg le_weakening2 subtype_rel_self all_wf nat_wf less_than_wf random-variable_wf finite-prob-space_wf
\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]

Date html generated: 2015_07_17-AM-08_02_22
Last ObjectModification: 2015_01_27-AM-11_21_57

Home Index