---

Step * of Lemma expectation-constant

∀[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  E(n;X) = a ∈ ℚ supposing ∀s:ℕn ─→ Outcome. ((X s) = a ∈ ℚ)
BY
{ (Auto THEN Try ((Fold `p-outcome` 0 THEN Auto))) }

1
1. p : FinProbSpace
2. a : ℚ
3. n : ℕ
4. X : RandomVariable(p;n)
5. ∀s:ℕn ─→ Outcome. ((X s) = a ∈ ℚ)
⊢ E(n;X) = a ∈ ℚ

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[a:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n)].
    E(n;X)  =  a  supposing  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  Outcome.  ((X  s)  =  a)


By

(Auto  THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))

---

Home Index