### Nuprl Lemma : bounded-expectation

`∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀B:ℚ.`
`  (nullset(p;(X[n]─→∞ as n─→∞))) supposing `
`     ((∀n:ℕ. (0 ≤ X[n] ∧ E(f[n];X[n]) < B)) and `
`     0 < B and `
`     (∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]) and `
`     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))`

Proof

Definitions occuring in Statement :  rv-unbounded: `(X[n]─→∞ as n─→∞)` nullset: `nullset(p;S)` rv-le: `X ≤ Y` expectation: `E(n;F)` rv-const: `a` random-variable: `RandomVariable(p;n)` finite-prob-space: `FinProbSpace` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` so_apply: `x[s]` all: `∀x:A. B[x]` and: `P ∧ Q` function: `x:A ─→ B[x]` natural_number: `\$n` rationals: `ℚ`
Lemmas :  member-less_than int_seg_subtype-nat false_wf nat_wf int_seg_wf rv-le_witness subtype_rel-random-variable le_weakening2 Error :qless_witness,  int-subtype-rationals rv-const_wf expectation_wf all_wf rv-le_wf Error :qless_wf,  less_than_wf rationals_wf random-variable_wf finite-prob-space_wf Error :qless_transitivity_2_qorder,  Error :qle_weakening_eq_qorder,  Error :qless_irreflexivity,  equal-wf-T-base Error :qmul_preserves_qless,  qdiv_wf Error :qinv-positive,  qmul_wf squash_wf true_wf Error :qmul_comm_qrng,  qinv_wf assert-qeq assert_wf qeq_wf2 not_wf iff_weakening_equal Error :qmul_zero_qrng,  Error :qmul_assoc_qrng,  Error :qmul_one_qrng,  Markov-inequality rv-qle_wf equal_wf assert_functionality_wrt_uiff qmul_com Error :qdiv-qdiv,  Error :qmul-qdiv-cancel2,  qmul_ident Error :qless_transitivity_1_qorder,  exists_wf p-open_wf p-measure-le_wf p-outcome_wf Error :qle_wf,  subtype_rel_dep_function length_wf p-open-member_wf decidable__exists_int_seg subtype_rel-int_seg decidable__cand decidable__lt Error :decidable__qle,  decidable_wf lelt_wf equal-wf-base iff_wf le_wf subtype_rel_self decidable__equal_int less_than_transitivity2 less-iff-le add_functionality_wrt_le add-associates add-swap add-commutes le-add-cancel nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf decidable__le subtract_wf not-ge-2 condition-implies-le minus-one-mul zero-add minus-add minus-minus add-zero not-le-2 subtract-is-less subtype_rel_set Error :qle_reflexivity,  expectation-monotone-in-first expectation-monotone subtype_base_sq int_subtype_base q_le_wf bool_wf bnot_wf Error :qle-int,  uiff_transitivity2 eqtt_to_assert Error :assert-q_le-eq,  uiff_transitivity eqff_to_assert assert_of_bnot Error :qle_transitivity_qorder,  add-mul-special zero-mul sq_stable_from_decidable Error :decidable__qless,  rv-unbounded_wf set_wf le_weakening
\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).  \mforall{}B:\mBbbQ{}.
(nullset(p;(X[n]{}\mrightarrow{}\minfty{}  as  n{}\mrightarrow{}\minfty{})))  supposing
((\mforall{}n:\mBbbN{}.  (0  \mleq{}  X[n]  \mwedge{}  E(f[n];X[n])  <  B))  and
0  <  B  and
(\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    X[i]  \mleq{}  X[n])  and
(\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))

Date html generated: 2015_07_17-AM-08_01_56
Last ObjectModification: 2015_02_03-PM-09_47_36

Home Index