---

Step * of 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))
  ∈ ℚ)
BY
{ (Auto
   THEN (RWO "expectation-rv-scale<" 0 THENA Auto)
   THEN (RWW "expectation-rv-add<" 0 THENA Auto)
   THEN EqCD
   THEN Auto
   THEN (All (Unfold `random-variable`))
   THEN (All (Fold `p-outcome`))
   THEN RepUR ``rv-compose rv-scale rv-add rv-mul`` 0
   THEN Ext
   THEN Reduce 0
   THEN Auto
   THEN QNorm 0) }

---

Latex:


\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)))


By

(Auto
  THEN  (RWO  "expectation-rv-scale<"  0  THENA  Auto)
  THEN  (RWW  "expectation-rv-add<"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto
  THEN  (All  (Unfold  `random-variable`))
  THEN  (All  (Fold  `p-outcome`))
  THEN  RepUR  ``rv-compose  rv-scale  rv-add  rv-mul``  0
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto
  THEN  QNorm  0)

---

Home Index