---

Step * of Lemma expectation-rv-add-squared

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  (E(n;(x.x * x) o X + Y) = ((E(n;(x.x * x) o X) + (2 * E(n;X * Y))) + E(n;(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) o X + Y = (x.x * x) o X + 2*X * Y + (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)  o  X  +  Y)  =  ((E(n;(x.x  *  x)  o  X)  +  (2  *  E(n;X  *  Y)))  +  E(n;(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