---

Step * 1 1 1 of Lemma Markov-inequality


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
BY
{ (RepUR ``rv-le rv-qle rv-const rv-scale`` 0
   THEN Auto
   THEN RepUR ``rv-const rv-le`` 4
   THEN ((InstHyp [⌈s⌉] 4)⋅ THENA Auto)
   THEN ((SplitOnConclITE
          THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Fold `p-outcome` 0 THEN Auto)
          )
         THENL [Id; (Thin (-1))]
   )
   THEN QMul ⌈e⌉ 0⋅
   THEN Auto
   THEN Fold `p-outcome` 0
   THEN Auto) }

---

Latex:



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


By

(RepUR  ``rv-le  rv-qle  rv-const  rv-scale``  0
  THEN  Auto
  THEN  RepUR  ``rv-const  rv-le``  4
  THEN  ((InstHyp  [\mkleeneopen{}s\mkleeneclose{}]  4)\mcdot{}  THENA  Auto)
  THEN  ((SplitOnConclITE
                THENA  (Auto
                              THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                              THEN  Fold  `p-outcome`  0
                              THEN  Auto)
                )
              THENL  [Id;  (Thin  (-1))]
  )
  THEN  QMul  \mkleeneopen{}e\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  Fold  `p-outcome`  0
  THEN  Auto)

---

Home Index