---

Step * of Lemma Markov-inequality

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  ∀[e:ℚ]. E(n;e ≤ X) ≤ (E(n;X)/e) supposing 0 < e supposing 0 ≤ X
BY
{ (Auto THEN Auto) }

1
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. 0 ≤ X
5. e : ℚ
6. 0 < e
⊢ E(n;e ≤ X) ≤ (E(n;X)/e)

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:RandomVariable(p;n)].
    \mforall{}[e:\mBbbQ{}].  E(n;e  \mleq{}  X)  \mleq{}  (E(n;X)/e)  supposing  0  <  e  supposing  0  \mleq{}  X


By

(Auto  THEN  Auto)

---

Home Index