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]))`
`     `` (∃B:ℚ`
`          ∀n:ℕ`
`            (E(f[n];rv-partial-sum(n;k.if (k =z 0)`
`            then 0`
`            else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])`
`            fi )) ≤ B))) supposing `
`     ((∀n:ℕ`
`         ((E(f[n];X[n]) = 0 ∈ ℚ)`
`         ∧ (E(f[n];(x.x * x) o X[n]) = s ∈ ℚ)`
`         ∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = k ∈ ℚ))) and `
`     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))`

Proof

Definitions occuring in Statement :  rv-partial-sum: `rv-partial-sum(n;i.X[i])` rv-compose: `(x.F[x]) o 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 b then t else f fi ` eq_int: `(i =z j)` 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` function: `x:A ─→ B[x]` natural_number: `\$n` equal: `s = t ∈ T` qdiv: `(r/s)` qmul: `r * 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{}
\mforall{}n:\mBbbN{}
(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
((\mforall{}n:\mBbbN{}
((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