---

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

.....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)
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) * (X x)) + (2 * (X 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)  o  X  +  Y  =  (x.x  *  x)  o  X  +  2*X  *  Y  +  (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