---

Step * of Lemma expectation-monotone-in-first

∀[p:FinProbSpace]. ∀[n,m:ℕ].  ∀[X:RandomVariable(p;n)]. (E(n;X) = E(m;X) ∈ ℚ) supposing n ≤ m
BY
{ (InductionOnNat⋅ THEN Auto)⋅ }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. X : RandomVariable(p;0)
⊢ E(0;X) = E(m;X) ∈ ℚ

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

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n,m:\mBbbN{}].    \mforall{}[X:RandomVariable(p;n)].  (E(n;X)  =  E(m;X))  supposing  n  \mleq{}  m


By

(InductionOnNat\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index