---

Step * of Lemma expectation-rv-scale

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[q:ℚ].  (E(n;q*X) = (q * E(n;X)) ∈ ℚ)
BY
{ (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) }

---

Latex:


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


By

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

---

Home Index