---

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

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:

---

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

---

Latex:
xxx(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)xxx

---

Home Index