Nuprl Lemma : rv-partial-sum-monotone
∀[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].
  (∀[m:ℕ]. ∀[n:ℕm + 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: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s]
, 
all: ∀x:A. B[x]
, 
function: x:A ─→ B[x]
, 
add: n + 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