---

Step * 1 2 1 1 of Lemma expectation-constant


1. p : FinProbSpace
2. a : ℚ
3. n : ℤ
4. 0 < n
5. ∀X:RandomVariable(p;n - 1). ((∀s:ℕn - 1 ─→ Outcome. ((X s) = a ∈ ℚ)) ⇒ (E(n - 1;X) = a ∈ ℚ))
6. ¬(n = 0 ∈ ℤ)
7. X : RandomVariable(p;n)@i
8. ∀s:ℕn ─→ Outcome. ((X s) = a ∈ ℚ)@i
9. x : Outcome@i
10. s : ℕn - 1 ─→ Outcome@i
⊢ (rv-shift(x;X) s) = a ∈ ℚ
BY
{ (RepUR ``rv-shift`` 0 THEN BackThruSomeHyp) }

---

Latex:



1.  p  :  FinProbSpace
2.  a  :  \mBbbQ{}
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}X:RandomVariable(p;n  -  1).  ((\mforall{}s:\mBbbN{}n  -  1  {}\mrightarrow{}  Outcome.  ((X  s)  =  a))  {}\mRightarrow{}  (E(n  -  1;X)  =  a))
6.  \mneg{}(n  =  0)
7.  X  :  RandomVariable(p;n)@i
8.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  =  a)@i
9.  x  :  Outcome@i
10.  s  :  \mBbbN{}n  -  1  {}\mrightarrow{}  Outcome@i
\mvdash{}  (rv-shift(x;X)  s)  =  a


By

(RepUR  ``rv-shift``  0  THEN  BackThruSomeHyp)

---

Home Index