Nuprl Lemma : rv-iid-add-const
∀p:FinProbSpace. ∀a:ℚ. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
(rv-iid(p;n.f[n];n.X[n]) ⇒ rv-iid(p;n.f[n];n.X[n] + a))
Proof
Definitions occuring in Statement :
rv-iid: rv-iid(p;n.f[n];i.X[i]),
rv-const: a,
rv-add: X + Y,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ─→ B[x],
rationals: ℚ
Lemmas :
rv-iid-add,
rv-const_wf,
rv-disjoint-const,
int_seg_wf,
rv-iid_wf,
nat_wf,
random-variable_wf,
rationals_wf,
finite-prob-space_wf,
rv-disjoint-symmetry,
expectation-rv-const,
expectation_wf,
iff_weakening_equal,
qmul_wf,
int_seg_subtype-nat,
false_wf,
subtype_rel-random-variable,
decidable__equal_int,
le_weakening,
sq_stable__le,
le_wf,
and_wf,
equal_wf,
le_weakening2,
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
\mforall{}p:FinProbSpace. \mforall{}a:\mBbbQ{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbN{}. \mforall{}X:n:\mBbbN{} {}\mrightarrow{} RandomVariable(p;f[n]).
(rv-iid(p;n.f[n];n.X[n]) {}\mRightarrow{} rv-iid(p;n.f[n];n.X[n] + a))
Date html generated:
2015_07_17-AM-08_02_20
Last ObjectModification:
2015_02_03-PM-09_45_41
Home
Index