---

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

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:


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


By

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

---

Home Index