`∀[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