# Deriving a Markov bound pointwise

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-markov-inequality/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-markov-inequality-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Prove the finite-law bound and compare its exact tail.

A nonnegative random variable with a fully specified finite probability law; not a sampled proof of the general measure-theoretic theorem.





## Givens and symbols


- work


- G1 — X takes 0,2,6 with masses 1/2,1/3,1/6; threshold a=3.


- a — positive threshold
- 1_A — event indicator





## Rules and sources


- mko_definition · cited — Require X≥0 almost surely, a>0 and finite E[X]; then P(X≥a)≤E[X]/a. Complete finite rational laws allow exact tail and bound calculations. The bound is not the tail probability, signed variables cannot directly use the nonnegative theorem, and threshold0 is excluded. · mko-markov-inequality
- work · prerequisite — Indicator expectations equal event probabilities; nonnegative weighted sums and division by positive numbers preserve order.





## Main derivation

S01 · impliesBefore

1/2+1/3+1/6=1

After

X\ge0,\quad a=3>0,\quad E[X]<\infty

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

The law is normalized, X nonnegative, and the threshold positive; finite values ensure integrability.



S02 · impliesBefore

x<3,\ x\in\{0,2,6\}

After

3\mathbf1_{\{x\ge3\}}=0\le x

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Below threshold the indicator is zero and x is nonnegative.



S03 · impliesBefore

x\ge3

After

3\mathbf1_{\{x\ge3\}}=3\le x

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Above threshold the inequality follows directly from x≥3.



S04 · impliesBefore

3\mathbf1_{\{X\ge3\}}\le X

After

3P(X\ge3)\le E[X]

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Multiply by nonnegative masses and sum, preserving the inequality.



S05 · impliesBefore

E[X]=0/2+2/3+6/6

After

E[X]=5/3

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Compute the expectation from the complete law.



S06 · impliesBefore

3P(X\ge3)\le5/3

After

P(X\ge3)\le5/9

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Divide by positive 3 to obtain the Markov upper bound.



S07 · impliesBefore

\{X\ge3\}=\{X=6\}

After

P(X\ge3)=1/6<5/9

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

Only the mass at 6 is in the tail, so the bound is not equality.



S08 · impliesBefore

a\mathbf1_{\{X\ge a\}}\le X,\quad a>0

After

P(X\ge a)\le E[X]/a

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

The same pointwise case proof works for any qualifying finite nonnegative law.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — This generalization rests on the pointwise proof, not on observed numbers.
- S07 · premise_audit · G1, S06, work — Do not substitute5/9 for the actual event probability.
- S06 · premise_audit · G1, S05, work — The positive threshold makes division valid without reversing order.
- S05 · premise_audit · G1, S04, work — The mass at 6 is 1/6; the three points are not uniform.
- S04 · premise_audit · G1, S03, work — Every support value is used, not a random sample.
- S03 · premise_audit · G1, S02, work — Together the branches exhaust the support.
- S02 · premise_audit · G1, S01, work — A signed x could fail in this branch, locating the nonnegativity requirement.
- S01 · premise_audit · G1, work — A positive mean alone does not replace these qualifications.





## Error controls and negative controls

NonnegativityCheck every positive-mass value, not merely the mean.

Bound versus actual valueCompute tail 1/6 separately from{6}, then compare with 5/9.


- The tail always equals E[X]/a. → reject — Here1/6 is not 5/9.
- Division is valid at a=0. → reject — A positive threshold is a denominator requirement.
- A signed X with positive mean qualifies directly. → reject — The below-threshold branch0≤X can fail.





## Result and limitations

The exact tail is 1/6 and the Markov bound5/9; the finite-law version follows pointwise.







## Verification and source binding

3 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: c8a078764616e58290cc4d16694339f57787010b9ba42b16d383b7a1a892a42c
- original source SHA-256: 1ef70a0328ec764a48d0df0ab90defc38d6cbe51d3d15f7ef7e50556ddc7cdc8
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-markov-inequality-01.json)