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

p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
        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


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: supposing a so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q apply: a lambda: λx.A[x] function: x:A ─→ B[x] natural_number: $n equal: t ∈ T qsub: s qdiv: (r/s) qmul: 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]).
    {}\mRightarrow{}  (\mforall{}mean:\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