Nuprl Lemma : rv-iid-add
∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X,Y:n:ℕ ─→ RandomVariable(p;f[n]).
(rv-iid(p;n.f[n];n.X[n])
⇒ rv-iid(p;n.f[n];n.Y[n])
⇒ (∀n:ℕ. ∀i:ℕn + 1. (rv-disjoint(p;f[n];Y[i];X[n]) ∧ rv-disjoint(p;f[n];X[i];Y[n])))
⇒ rv-iid(p;n.f[n];n.X[n] + Y[n]))
Proof
Definitions occuring in Statement :
rv-iid: rv-iid(p;n.f[n];i.X[i]),
rv-disjoint: rv-disjoint(p;n;X;Y),
rv-add: X + Y,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
int_seg: {i..j-},
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ─→ B[x],
add: n + m,
natural_number: $n
Lemmas :
decidable__equal_int,
le_weakening,
int_seg_subtype-nat,
false_wf,
sq_stable__le,
le_wf,
and_wf,
equal_wf,
nat_wf,
le_weakening2,
subtype_rel-random-variable,
int_seg_wf,
all_wf,
rv-disjoint_wf,
rv-iid_wf,
random-variable_wf,
finite-prob-space_wf,
decidable__lt,
not-equal-2,
add_functionality_wrt_le,
add-swap,
add-commutes,
le-add-cancel,
less-iff-le,
condition-implies-le,
add-associates,
minus-add,
minus-one-mul,
zero-add,
le-add-cancel2,
lelt_wf,
rationals_wf,
qadd_wf,
iff_weakening_equal,
qmul_wf,
int-subtype-rationals,
expectation_wf,
rv-add_wf,
expectation-rv-add,
squash_wf,
true_wf,
add-mul-special,
zero-mul,
add-zero,
rv-mul_wf,
rv-disjoint-rv-mul2,
rv-disjoint-rv-mul,
expectation-rv-disjoint,
expectation-rv-add-fourth,
expectation-rv-add-cubed,
expectation-rv-add-squared,
rv-disjoint-rv-add2,
rv-disjoint-rv-add
\mforall{}p:FinProbSpace. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}X,Y:n:\mBbbN{} {}\mrightarrow{} RandomVariable(p;f[n]).
(rv-iid(p;n.f[n];n.X[n])
{}\mRightarrow{} rv-iid(p;n.f[n];n.Y[n])
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. \mforall{}i:\mBbbN{}n + 1. (rv-disjoint(p;f[n];Y[i];X[n]) \mwedge{} rv-disjoint(p;f[n];X[i];Y[n])))
{}\mRightarrow{} rv-iid(p;n.f[n];n.X[n] + Y[n]))
Date html generated:
2015_07_17-AM-08_02_17
Last ObjectModification:
2015_02_03-PM-09_46_35
Home
Index