---

Step * of Lemma rv-shift-linear

∀[k:FinProbSpace]. ∀[x:Outcome]. ∀[n:ℕ+]. ∀[X,Y:RandomVariable(k;n)]. ∀[a,b:ℚ].
  (rv-shift(x;a*X + b*Y) = a*rv-shift(x;X) + b*rv-shift(x;Y) ∈ RandomVariable(k;n - 1))
BY
{ (RepUR ``random-variable finite-prob-space p-outcome rv-shift rv-scale rv-add`` 0 THEN Auto) }

---

Latex:


\mforall{}[k:FinProbSpace].  \mforall{}[x:Outcome].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[X,Y:RandomVariable(k;n)].  \mforall{}[a,b:\mBbbQ{}].
    (rv-shift(x;a*X  +  b*Y)  =  a*rv-shift(x;X)  +  b*rv-shift(x;Y))


By

(RepUR  ``random-variable  finite-prob-space  p-outcome  rv-shift  rv-scale  rv-add``  0  THEN  Auto)

---

Home Index