Nuprl Lemma : slln-lemma2

p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀s,k:ℚ.
  ((∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n]))
            (E(f[n];rv-partial-sum(n;k.if (k =z 0)
            then 0
            else (x.(x x) x) (1/k)*rv-partial-sum(k;i.X[i])
            fi )) ≤ B))) supposing 
         ((E(f[n];X[n]) 0 ∈ ℚ)
         ∧ (E(f[n];(x.x x) X[n]) s ∈ ℚ)
         ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))


Definitions occuring in Statement :  rv-partial-sum: rv-partial-sum(n;i.X[i]) rv-compose: (x.F[x]) X rv-disjoint: rv-disjoint(p;n;X;Y) expectation: E(n;F) rv-const: a rv-scale: q*X random-variable: RandomVariable(p;n) finite-prob-space: FinProbSpace int_seg: {i..j-} nat: ifthenelse: if then else fi  eq_int: (i =z j) 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 function: x:A ─→ B[x] natural_number: $n equal: t ∈ T qdiv: (r/s) qmul: s rationals:
Lemmas :  member-less_than int_seg_subtype-nat false_wf nat_wf int_seg_wf slln-lemma1 qmul_wf int-subtype-rationals all_wf Error :qle_wf,  expectation_wf rv-partial-sum_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int rv-const_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base iff_transitivity assert_wf bnot_wf not_wf equal-wf-T-base iff_weakening_uiff assert_of_bnot int_upper_subtype_nat le_wf nat_properties nequal-le-implies zero-add rv-compose_wf rv-scale_wf qdiv_wf subtype_rel_set Error :int_nzero-rational,  subtype_rel_sets nequal_wf not-equal-2 decidable__le not-le-2 condition-implies-le minus-add minus-one-mul add-swap add-associates add-commutes add_functionality_wrt_le le-add-cancel2 or_wf equal-wf-base int_subtype_base rv-disjoint_wf subtype_rel-random-variable le_weakening2 rationals_wf less_than_wf random-variable_wf finite-prob-space_wf expectation-qsum assert-bnot neg_assert_of_eq_int lelt_wf int-equal-in-rationals int_entire_a qmul-mul Error :qsum-qle,  uiff_transitivity Error :qle_reflexivity,  Error :non-neg-qmul,  iff_weakening_equal expectation-rv-const true_wf squash_wf expectation-monotone-in-first p-outcome_wf mul_nzero Error :qmul-qdiv,  Error :qmul_comm_qrng,  Error :qmul_ac_1_qrng,  Error :qmul_assoc_qrng,  le_antisymmetry_iff decidable__equal_int zero_ann_a mul-associates minus-zero le-add-cancel add-zero expectation-rv-scale Error :qle_weakening_eq_qorder,  Error :qmul_functionality_wrt_qle,  Error :qle_functionality_wrt_implies,  Error :qless_wf,  decidable__lt Error :qless-int,  Error :qmul-positive,  Error :qinv-nonneg,  expectation-non-neg Error :q-square-non-neg,  Error :qmul_preserves_qle,  qmul_assoc qmul_com Error :qmul-qdiv-cancel,  Error :qsum_wf,  Error :prod_sum_l_q,  sq_stable__le Error :sum_unroll_base_q,  less_than_irreflexivity less_than_transitivity1 subtype_rel-equal Error :qle_witness,  Error :qmul_preserves_qle2,  Error :qmul_zero_qrng,  Error :sum_unroll_lo_q,  Error :qsum-reciprocal-squares-bound,  Error :decidable__equal_rationals,  Error :mon_ident_q,  Error :qmul_over_plus_qrng,  qadd_wf Error :qmul_one_qrng,  Error :qmul-qdiv-cancel2,  Error :qle_weakening_lt_qorder,  Error :qinv-positive,  Error :q-square-positive,  Error :qmul_preserves_qless,  Error :qle-iff
\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).  \mforall{}s,k:\mBbbQ{}.
    ((\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    rv-disjoint(p;f[n];X[i];X[n]))
          {}\mRightarrow{}  (\mexists{}B:\mBbbQ{}
                        (E(f[n];rv-partial-sum(n;k.if  (k  =\msubz{}  0)
                        then  0
                        else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
                        fi  ))  \mleq{}  B)))  supposing 
                  ((E(f[n];X[n])  =  0)
                  \mwedge{}  (E(f[n];(x.x  *  x)  o  X[n])  =  s)
                  \mwedge{}  (E(f[n];(x.(x  *  x)  *  x  *  x)  o  X[n])  =  k)))  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))

Date html generated: 2015_07_17-AM-08_03_40
Last ObjectModification: 2015_07_17-AM-07_31_03

Home Index