---

Step * 1 of Lemma expectation-constant


1. p : FinProbSpace
2. a : ℚ
3. n : ℕ
4. X : RandomVariable(p;n)
5. ∀s:ℕn ⟶ Outcome. ((X s) = a ∈ ℚ)
⊢ E(n;X) = a ∈ ℚ
BY
{ (NatInd (-3) THEN RecUnfold `expectation` 0 THEN Reduce 0) }

1
1. p : FinProbSpace
2. a : ℚ
3. n : ℤ
⊢ ∀X:RandomVariable(p;0). ((∀s:ℕ0 ⟶ Outcome. ((X s) = a ∈ ℚ)) ⇒ ((X null) = a ∈ ℚ))

2
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 ∈ ℚ))

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  a  :  \mBbbQ{}
3.  n  :  \mBbbN{}
4.  X  :  RandomVariable(p;n)
5.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  =  a)
\mvdash{}  E(n;X)  =  a


By

---

Latex:
(NatInd  (-3)  THEN  RecUnfold  `expectation`  0  THEN  Reduce  0)

---

Home Index