---

Step * 2 of Lemma expectation-monotone-in-first


1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀[m:ℕ]. ∀[X:RandomVariable(p;n - 1)]. (E(n - 1;X) = E(m;X) ∈ ℚ) supposing (n - 1) ≤ m
5. m : ℕ
6. n ≤ m
7. X : RandomVariable(p;n)
⊢ E(n;X) = E(m;X) ∈ ℚ
BY
{ ((RecUnfold `expectation` 0 THEN RepeatFor 2 ((SplitOnConclITE THEN Auto')))⋅
   THEN EqCD
   THEN Auto
   THEN Ext
   THEN Reduce 0
   THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[m:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n  -  1)].  (E(n  -  1;X)  =  E(m;X))  supposing  (n  -  1)  \mleq{}  m
5.  m  :  \mBbbN{}
6.  n  \mleq{}  m
7.  X  :  RandomVariable(p;n)
\mvdash{}  E(n;X)  =  E(m;X)


By

((RecUnfold  `expectation`  0  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto')))\mcdot{}
  THEN  EqCD
  THEN  Auto
  THEN  Ext
  THEN  Reduce  0
  THEN  Auto)

---

Home Index