---

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
{ xxx(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)xxx }

---

Latex:

---

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

---

Latex:
xxx(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)xxx

---

Home Index