---

Step * of Lemma expectation-rv-add

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (E(n;X + Y) = (E(n;X) + E(n;Y)) ∈ ℚ)
BY
{ xxx(InstLemma `expectation-linear` []
      THEN RepeatFor 4 (ParallelLast)
      THEN RepeatFor 2 (((InstHyp [⌜1⌝] (-1))⋅ THENA Auto))
      THEN (NthHypEq (-1))
      THEN RepeatFor 2 ((EqCD THEN Auto))
      THEN QNorm 0
      THEN All Thin)xxx }

1
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. Y : RandomVariable(p;n)
⊢ X + Y = 1*X + 1*Y ∈ RandomVariable(p;n)

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X,Y:RandomVariable(p;n)].    (E(n;X  +  Y)  =  (E(n;X)  +  E(n;Y)))


By

---

Latex:
xxx(InstLemma  `expectation-linear`  []
        THEN  RepeatFor  4  (ParallelLast)
        THEN  RepeatFor  2  (((InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto))
        THEN  (NthHypEq  (-1))
        THEN  RepeatFor  2  ((EqCD  THEN  Auto))
        THEN  QNorm  0
        THEN  All  Thin)xxx

---

Home Index