---

Step * of Lemma expectation-rv-scale

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[q:ℚ].  (E(n;q*X) = (q * E(n;X)) ∈ ℚ)
BY
{ xxx(InstLemma `expectation-linear` []
      THEN RepeatFor 3 (ParallelLast)
      THEN Auto
      THEN ((InstHyp [⌜0⌝;⌜q⌝;⌜0⌝] (-2))⋅ THENA Auto)
      THEN (NthHypEq (-1))
      THEN EqCD
      THEN Auto
      THEN QNorm 0
      THEN EqCD
      THEN Auto
      THEN (All (Unfolds ``random-variable rv-const rv-scale rv-add finite-prob-space``))
      THEN Ext
      THEN Reduce 0
      THEN Auto
      THEN QNorm 0)xxx }

---

Latex:

---

Latex:
\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n)].  \mforall{}[q:\mBbbQ{}].    (E(n;q*X)  =  (q  *  E(n;X)))


By

---

Latex:
xxx(InstLemma  `expectation-linear`  []
        THEN  RepeatFor  3  (ParallelLast)
        THEN  Auto
        THEN  ((InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
        THEN  (NthHypEq  (-1))
        THEN  EqCD
        THEN  Auto
        THEN  QNorm  0
        THEN  EqCD
        THEN  Auto
        THEN  (All  (Unfolds  ``random-variable  rv-const  rv-scale  rv-add  finite-prob-space``))
        THEN  Ext
        THEN  Reduce  0
        THEN  Auto
        THEN  QNorm  0)xxx

---

Home Index