### Nuprl Lemma : strong-law-of-large-numbers

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

This theorem is one of freek's list of 100 theorems

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` qsub: `r - s` qdiv: `(r/s)` qmul: `r * s` rationals: `ℚ`
Lemmas :  slln-lemma4 rv-add_wf rv-const_wf qmul_wf int-subtype-rationals rv-iid-add-const expectation-rv-add iff_weakening_equal qadd_wf squash_wf true_wf rationals_wf expectation-rv-const equal-wf-T-base equal_wf expectation_wf false_wf le_wf rv-iid_wf nat_wf random-variable_wf finite-prob-space_wf Error :qinverse_q,  nullset-monotone exists_wf Error :qless_wf,  all_wf less_than_wf Error :qle_wf,  Error :qabs_wf,  Error :qsum_wf,  qdiv_wf subtype_rel_set Error :int_nzero-rational,  less_than_transitivity1 le_weakening less_than_irreflexivity equal-wf-base int_subtype_base nequal_wf int_seg_subtype-nat subtype_rel_dep_function p-outcome_wf int_seg_wf length_wf qsub_wf sq_stable__le Error :sum_plus_q,  Error :prod_sum_l_q,  Error :qsum-const,  Error :qmul_over_plus_qrng,  Error :qmul_over_minus_qrng,  Error :qmul_comm_qrng,  Error :qmul_ac_1_qrng,  Error :qmul-qdiv-cancel4,  qmul_assoc
\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{}  (\mforall{}mean:\mBbbQ{}
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)  -  mean|)))))
supposing  E(f[0];X[0])  =  mean))

Date html generated: 2015_07_17-AM-08_04_23
Last ObjectModification: 2015_02_03-PM-09_46_18

Home Index