---

Step * of Lemma expectation-rv-add-cubed

No Annotations
∀[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 EqCDA) }

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:

---

Latex:
No  Annotations
\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

---

Latex:
(Auto
  THEN  (RWO  "expectation-rv-scale<"  0  THENA  Auto)
  THEN  (RWW  "expectation-rv-add<"  0  THENA  Auto)
  THEN  EqCDA)

---

Home Index