---

Step * 1 1 of Lemma Markov-inequality


1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. 0 ≤ X
5. e : ℚ
6. 0 < e
⊢ e ≤ X ≤ (1/e)*X
BY
{ ((Assert ¬(e = 0 ∈ ℚ) BY Auto) THEN (Assert 0 < (1/e) BY (BLemma `qinv-positive`  THEN Auto))) }

1
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. 0 ≤ X
5. e : ℚ
6. 0 < e
7. ¬(e = 0 ∈ ℚ)
8. 0 < (1/e)
⊢ e ≤ X ≤ (1/e)*X

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbN{}
3.  X  :  RandomVariable(p;n)
4.  0  \mleq{}  X
5.  e  :  \mBbbQ{}
6.  0  <  e
\mvdash{}  e  \mleq{}  X  \mleq{}  (1/e)*X


By

((Assert  \mneg{}(e  =  0)  BY  Auto)  THEN  (Assert  0  <  (1/e)  BY  (BLemma  `qinv-positive`    THEN  Auto)))

---

Home Index