---

Step * 1 of Lemma expectation-linear


1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀[X,Y:RandomVariable(p;n - 1)]. ∀[a,b:ℚ].  (E(n - 1;a*X + b*Y) = ((a * E(n - 1;X)) + (b * E(n - 1;Y))) ∈ ℚ)
5. ¬(n = 0 ∈ ℤ)
6. X : RandomVariable(p;n)
7. Y : RandomVariable(p;n)
8. a : ℚ
9. b : ℚ
⊢ weighted-sum(p;λx.E(n - 1;a*rv-shift(x;X) + b*rv-shift(x;Y)))
= weighted-sum(p;λx.((a * ((λx.E(n - 1;rv-shift(x;X))) x)) + (b * ((λx.E(n - 1;rv-shift(x;Y))) x))))
∈ ℚ
BY
{ (EqCD THEN Auto)⋅ }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[X,Y:RandomVariable(p;n  -  1)].  \mforall{}[a,b:\mBbbQ{}].
          (E(n  -  1;a*X  +  b*Y)  =  ((a  *  E(n  -  1;X))  +  (b  *  E(n  -  1;Y))))
5.  \mneg{}(n  =  0)
6.  X  :  RandomVariable(p;n)
7.  Y  :  RandomVariable(p;n)
8.  a  :  \mBbbQ{}
9.  b  :  \mBbbQ{}
\mvdash{}  weighted-sum(p;\mlambda{}x.E(n  -  1;a*rv-shift(x;X)  +  b*rv-shift(x;Y)))
=  weighted-sum(p;\mlambda{}x.((a  *  ((\mlambda{}x.E(n  -  1;rv-shift(x;X)))  x))  +  (b  *  ((\mlambda{}x.E(n  -  1;rv-shift(x;Y)))  x))))


By

(EqCD  THEN  Auto)\mcdot{}

---

Home Index