### Nuprl Lemma : slln-lemma4

`∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).`
`  (rv-iid(p;n.f[n];n.X[n])`
`  `` nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|))))) `
`     supposing E(f[0];X[0]) = 0 ∈ ℚ)`

Proof

Definitions occuring in Statement :  rv-iid: `rv-iid(p;n.f[n];i.X[i])` nullset: `nullset(p;S)` expectation: `E(n;F)` random-variable: `RandomVariable(p;n)` finite-prob-space: `FinProbSpace` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` lambda: `λx.A[x]` function: `x:A ─→ B[x]` natural_number: `\$n` equal: `s = t ∈ T` qdiv: `(r/s)` qmul: `r * s` rationals: `ℚ`
Lemmas :  slln-lemma3 expectation_wf false_wf le_wf rv-compose_wf qmul_wf rationals_wf int_seg_wf equal-wf-T-base rv-iid_wf nat_wf random-variable_wf finite-prob-space_wf and_wf equal_wf
\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).
(rv-iid(p;n.f[n];n.X[n])
{}\mRightarrow{}  nullset(p;\mlambda{}s.\mexists{}q:\mBbbQ{}.  (0  <  q  \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X[i]  s)|)))))
supposing  E(f[0];X[0])  =  0)

Date html generated: 2015_07_17-AM-08_04_18
Last ObjectModification: 2015_01_27-AM-11_22_50

Home Index