---

Step * of Lemma expectation-rv-sample

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[X:Outcome ─→ ℚ].  (E(n;X@i) = weighted-sum(p;X) ∈ ℚ)
BY
{ (InductionOnNat THEN RecUnfold `expectation` 0 THEN Reduce 0 THEN Auto THEN SplitOnConclITE THEN Auto') }

1
.....falsecase..... 
1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀[i:ℕn - 1]. ∀[X:Outcome ─→ ℚ].  (E(n - 1;X@i) = weighted-sum(p;X) ∈ ℚ)
5. i : ℕn
6. X : Outcome ─→ ℚ
7. ¬(n = 0 ∈ ℤ)
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X@i))) = weighted-sum(p;X) ∈ ℚ

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[i:\mBbbN{}n].  \mforall{}[X:Outcome  {}\mrightarrow{}  \mBbbQ{}].    (E(n;X@i)  =  weighted-sum(p;X))


By

(InductionOnNat
  THEN  RecUnfold  `expectation`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  SplitOnConclITE
  THEN  Auto')

---

Home Index