---

Step * 1 of Lemma expectation-rv-add-cubed

.....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)
BY
{ (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) }

1
1. p : FinProbSpace
2. n : ℕ
3. X : (ℕn ─→ Outcome) ─→ ℚ
4. Y : (ℕn ─→ Outcome) ─→ ℚ
5. x : ℕn ─→ Outcome
⊢ ((((X x) + (Y x)) * ((X x) + (Y x))) * ((X x) + (Y x)))
= (((((X x) * (X x)) * (X x)) + (3 * ((X x) * (X x)) * (Y x)) + (3 * (X x) * (Y x) * (Y x)))
  + (((Y x) * (Y x)) * (Y x)))
∈ ℚ

---

Latex:


.....subterm.....  T:t
3:n
1.  p  :  FinProbSpace
2.  n  :  \mBbbN{}
3.  X  :  RandomVariable(p;n)
4.  Y  :  RandomVariable(p;n)
\mvdash{}  (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


By

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

---

Home Index