---

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)
8. ∀s:ℕn ⟶ Outcome. ((X s) = a ∈ ℚ)
9. x : Outcome
10. s : ℕn - 1 ⟶ Outcome
⊢ (rv-shift(x;X) s) = a ∈ ℚ
BY
{ xxx(RepUR ``rv-shift`` 0 THEN BackThruSomeHyp)xxx }

---

Latex:

---

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)
8.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  =  a)
9.  x  :  Outcome
10.  s  :  \mBbbN{}n  -  1  {}\mrightarrow{}  Outcome
\mvdash{}  (rv-shift(x;X)  s)  =  a


By

---

Latex:
xxx(RepUR  ``rv-shift``  0  THEN  BackThruSomeHyp)xxx

---

Home Index