---

Step * of 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))
  ∈ ℚ)
BY
{ (Auto
   THEN (RWO "expectation-rv-scale<" 0 THENA Auto)
   THEN (RWW "expectation-rv-add<" 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

1
.....subterm..... T:t
3:n
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. Y : RandomVariable(p;n)
⊢ (x.(x * x) * x) o X + Y = (x.(x * x) * x) o X + 3*X * X * Y + 3*X * Y * Y + (x.(x * x) * x) o Y ∈ RandomVariable(p;n)

---

Latex:


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


By

(Auto
  THEN  (RWO  "expectation-rv-scale<"  0  THENA  Auto)
  THEN  (RWW  "expectation-rv-add<"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index