Nuprl Lemma : expectation-rv-scale
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[q:ℚ]. (E(n;q*X) = (q * E(n;X)) ∈ ℚ)
Proof
Definitions occuring in Statement :
expectation: E(n;F),
rv-scale: q*X,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
nat: ℕ,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
qmul: r * s,
rationals: ℚ
Lemmas :
expectation-linear,
rv-const_wf,
int-subtype-rationals,
equal_wf,
squash_wf,
true_wf,
expectation_wf,
Error :mon_ident_q,
qmul_wf,
int_seg_wf,
length_wf,
rationals_wf,
random-variable_wf,
nat_wf,
finite-prob-space_wf,
qadd_wf,
Error :qmul_zero_qrng,
Error :qmul_comm_qrng,
Error :qadd_comm_q,
iff_weakening_equal
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X:RandomVariable(p;n)]. \mforall{}[q:\mBbbQ{}]. (E(n;q*X) = (q * E(n;X)))
Date html generated:
2015_07_17-AM-07_58_58
Last ObjectModification:
2015_02_03-PM-09_44_25
Home
Index