Nuprl Lemma : expectation-rv-add
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)]. (E(n;X + Y) = (E(n;X) + E(n;Y)) ∈ ℚ)
Proof
Definitions occuring in Statement :
expectation: E(n;F),
rv-add: X + Y,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
nat: ℕ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
qadd: r + s,
rationals: ℚ
Lemmas :
rationals_wf,
qadd_wf,
squash_wf,
true_wf,
qmul_wf,
int-subtype-rationals,
qmul_ident,
iff_weakening_equal,
int_seg_wf,
length_wf
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X,Y:RandomVariable(p;n)]. (E(n;X + Y) = (E(n;X) + E(n;Y)))
Date html generated:
2015_07_17-AM-07_58_56
Last ObjectModification:
2015_02_03-PM-09_44_17
Home
Index