Nuprl Lemma : rv-partial-sum-monotone

[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].
  (∀[m:ℕ]. ∀[n:ℕ1].  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])) supposing 
     ((∀n:ℕ0 ≤ X[n]) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))


Proof




Definitions occuring in Statement :  rv-partial-sum: rv-partial-sum(n;i.X[i]) rv-le: X ≤ Y rv-const: a random-variable: RandomVariable(p;n) finite-prob-space: FinProbSpace int_seg: {i..j-} nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] function: x:A ─→ B[x] add: m natural_number: $n
Lemmas :  decidable__equal_int le_wf and_wf equal_wf nat_wf int_seg_subtype-nat false_wf le_weakening2 rv-partial-sum_wf subtype_rel-random-variable lelt_wf rv-le_witness int_seg_wf all_wf rv-le_wf rv-const_wf int-subtype-rationals less_than_wf random-variable_wf finite-prob-space_wf complete_nat_ind subtype_rel-int_seg rationals_wf length_wf p-outcome_wf subtype_rel_dep_function Error :qsum_wf,  Error :qle_reflexivity,  int_subtype_base subtype_base_sq le-add-cancel2 add-commutes minus-one-mul minus-add condition-implies-le less-iff-le le-add-cancel zero-add add-swap add-zero add-associates add_functionality_wrt_le not-equal-2 decidable__lt rv-partial-sum-unroll subtract_wf minus-minus sq_stable__le not-le-2 decidable__le le_weakening le-add-cancel-alt Error :qle_weakening_eq_qorder,  Error :qle_functionality_wrt_implies,  qadd_wf subtract-is-less Error :qle_wf,  subtype_rel_self iff_weakening_equal Error :qadd_inv_assoc_q,  Error :qinverse_q,  Error :qadd_ac_1_q,  Error :qadd_comm_q,  true_wf squash_wf qmul_wf Error :qadd_preserves_qle
\mforall{}[p:FinProbSpace].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])].
    (\mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].    rv-partial-sum(n;i.X[i])  \mleq{}  rv-partial-sum(m;i.X[i]))  supposing 
          ((\mforall{}n:\mBbbN{}.  0  \mleq{}  X[n])  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))



Date html generated: 2015_07_17-AM-08_02_34
Last ObjectModification: 2015_07_16-AM-11_19_35

Home Index