---

Step * 1 2 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
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) = a ∈ ℚ
BY
{ (BLemma `ws-constant` THEN Auto THEN Reduce 0 THEN BackThruSomeHyp THEN Auto) }

1
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 ∈ ℚ

---

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
\mvdash{}  weighted-sum(p;\mlambda{}x.E(n  -  1;rv-shift(x;X)))  =  a


By

(BLemma  `ws-constant`  THEN  Auto  THEN  Reduce  0  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index