Nuprl Lemma : expectation-rv-add-cubed
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x) o X + Y)
= ((E(n;(x.(x * x) * x) o X) + (3 * E(n;X * X * Y)) + (3 * E(n;X * Y * Y))) + E(n;(x.(x * x) * x) o Y))
∈ ℚ)
Proof
Definitions occuring in Statement :
rv-compose: (x.F[x]) o X,
expectation: E(n;F),
rv-mul: X * Y,
rv-add: X + Y,
random-variable: RandomVariable(p;n),
finite-prob-space: FinProbSpace,
nat: ℕ,
uall: ∀[x:A]. B[x],
natural_number: $n,
equal: s = t ∈ T,
qmul: r * s,
qadd: r + s,
rationals: ℚ
Lemmas :
int_seg_wf,
p-outcome_wf,
rationals_wf,
qmul_wf,
qadd_wf,
int-subtype-rationals,
Error :qmul_over_plus_qrng,
squash_wf,
true_wf,
Error :qmul_assoc_qrng,
Error :qmul_comm_qrng,
Error :mon_assoc_q,
Error :qmul_ac_1_qrng,
Error :qadd_ac_1_q,
Error :q_distrib,
qmul_ident,
iff_weakening_equal
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x) o X + Y)
= ((E(n;(x.(x * x) * x) o X) + (3 * E(n;X * X * Y)) + (3 * E(n;X * Y * Y)))
+ E(n;(x.(x * x) * x) o Y)))
Date html generated:
2015_07_17-AM-07_59_39
Last ObjectModification:
2015_02_03-PM-09_44_39
Home
Index