---

Step * 1 2 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 ∈ ℚ))
⊢ ∀X:RandomVariable(p;n)
    ((∀s:ℕn ─→ Outcome. ((X s) = a ∈ ℚ))
    ⇒ (if (n =z 0) then X null else weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) fi  = a ∈ ℚ))
BY
{ (SplitOnConclITE
   THEN Auto'
   THEN Try ((Fold `random-variable` 0 THEN Auto))
   THEN Try ((DVar `p' THEN Unfold `p-outcome` 0 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
⊢ weighted-sum(p;λx.E(n - 1;rv-shift(x;X))) = 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))
\mvdash{}  \mforall{}X:RandomVariable(p;n)
        ((\mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  =  a))
        {}\mRightarrow{}  (if  (n  =\msubz{}  0)  then  X  null  else  weighted-sum(p;\mlambda{}x.E(n  -  1;rv-shift(x;X)))  fi    =  a))


By

(SplitOnConclITE
  THEN  Auto'
  THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
  THEN  Try  ((DVar  `p'  THEN  Unfold  `p-outcome`  0  THEN  Auto)))

---

Home Index