---

Step * 1 of Lemma Markov-inequality


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)
BY
{ (Subst' (E(n;X)/e) = E(n;(1/e)*X) ∈ ℚ 0
   THEN Auto
   THEN Try ((BLemma `expectation-monotone` THEN Auto))
   THEN Try ((RWO "expectation-rv-scale" 0
              THEN Auto
              THEN Unfold `qdiv` 0
              THEN QNorm 0
              THEN Auto
              THEN RWO "assert-qeq" 0
              THEN Auto)⋅))⋅ }

1
1. p : FinProbSpace
2. n : ℕ
3. X : RandomVariable(p;n)
4. 0 ≤ X
5. e : ℚ
6. 0 < 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(n;e  \mleq{}  X)  \mleq{}  (E(n;X)/e)


By

(Subst'  (E(n;X)/e)  =  E(n;(1/e)*X)  0
  THEN  Auto
  THEN  Try  ((BLemma  `expectation-monotone`  THEN  Auto))
  THEN  Try  ((RWO  "expectation-rv-scale"  0
                        THEN  Auto
                        THEN  Unfold  `qdiv`  0
                        THEN  QNorm  0
                        THEN  Auto
                        THEN  RWO  "assert-qeq"  0
                        THEN  Auto)\mcdot{}))\mcdot{}

---

Home Index