Nuprl Lemma : expectation-rv-add-fourth
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x * x) o X + Y)
= ((E(n;(x.(x * x) * x * x) o X) + ((4 * E(n;X * X * X * Y)) + (6 * E(n;X * X * Y * Y))) + (4 * E(n;X * Y * Y * Y)))
+ E(n;(x.(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 :
random-variable_wf,
nat_wf,
finite-prob-space_wf,
rationals_wf,
expectation_wf,
rv-compose_wf,
rv-add_wf,
qmul_wf,
rv-mul_wf,
int-subtype-rationals,
rv-scale_wf,
squash_wf,
true_wf,
int_seg_wf,
p-outcome_wf,
qadd_wf,
expectation-rv-scale,
iff_weakening_equal,
expectation-rv-add,
Error :qmul_over_plus_qrng,
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
\mforall{}[p:FinProbSpace]. \mforall{}[n:\mBbbN{}]. \mforall{}[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x * x) o X + Y)
= ((E(n;(x.(x * x) * x * x) o X)
+ ((4 * E(n;X * X * X * Y)) + (6 * E(n;X * X * Y * Y)))
+ (4 * E(n;X * Y * Y * Y)))
+ E(n;(x.(x * x) * x * x) o Y)))
Date html generated:
2015_07_17-AM-07_59_41
Last ObjectModification:
2015_02_03-PM-09_44_53
Home
Index