---

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 ((GenConclTerms Auto [⌜X x⌝;⌜Y x⌝]⋅ THEN All Thin THEN QNorm 0) ORELSE Auto)) }

1
1. v : ℚ
2. v1 : ℚ
⊢ ((2 * v * v * v1) + (2 * v * v1 * v1) + (v * v * v) + (v * v * v1) + (v * v1 * v1) + (v1 * v1 * v1))
= ((3 * v * v * v1) + (3 * v * v1 * v1) + (v * v * v) + (v1 * v1 * v1))
∈ ℚ

---

Latex:

---

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

---

Latex:
(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  ((GenConclTerms  Auto  [\mkleeneopen{}X  x\mkleeneclose{};\mkleeneopen{}Y  x\mkleeneclose{}]\mcdot{}  THEN  All  Thin  THEN  QNorm  0)  ORELSE  Auto))

---

Home Index