# Chebyshev from squared deviations

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-chebyshev-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-chebyshev-inequality-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Derive Chebyshev from Markov and compute an exact instance.

A complete finite law; independence is not required.





## Givens and symbols


- work


- G1 — X takes -2,0,2 with masses 1/4,1/2,1/4; epsilon=1.


- μ — mean under this law
- Y — squared deviation
- ε — positive threshold





## Rules and sources


- mko_definition · cited — Require positive epsilon and finite mean/variance. The event |X−mean|≥epsilon equals (X−mean)^2≥epsilon^2, allowing Markov on the nonnegative squared deviation. The raw bound is not actual tail equality and needs no independence; zero-mass atoms and zero variance retain their almost-sure meaning. · mko-chebyshev-inequality
- work · prerequisite — Assumed prerequisite Markov: for nonnegative Y and a>0, P(Y≥a)≤E[Y]/a; variance is the centered second moment.





## Main derivation

S01 · impliesBefore

1/4+1/2+1/4=1

After

\mu=E[X]=-2/4+2/4=0

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

The complete normalized law gives mean zero.



S02 · impliesBefore

Y=(X-\mu)^2

After

Y\in\{4,0,4\},\quad Y\ge0

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Construct nonnegative Y rather than applying Markov directly to X.



S03 · impliesBefore

E[Y]=4/4+0/2+4/4

After

\operatorname{Var}(X)=E[Y]=2

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Compute the centered second moment across the support.



S04 · impliesBefore

\varepsilon>0

After

|X-\mu|\ge\varepsilon\iff Y\ge\varepsilon^2

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

Squaring nonnegative absolute deviations preserves threshold equivalence.



S05 · impliesBefore

P(Y\ge\varepsilon^2)\le E[Y]/\varepsilon^2

After

P(|X-\mu|\ge\varepsilon)\le\operatorname{Var}(X)/\varepsilon^2

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Apply Markov to Y, then substitute the event equivalence and variance.



S06 · impliesBefore

\varepsilon=1

After

\operatorname{Var}(X)/\varepsilon^2=2

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The raw bound is 2; a valid upper bound may exceed1 and be loose.



S07 · impliesBefore

\{|X|\ge1\}=\{-2,2\}

After

P(|X|\ge1)=1/2\le2

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The two endpoint masses give exact tail 1/2.



S08 · impliesBefore

\varepsilon=2

After

P(|X|\ge2)=1/2=2/2^2

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

At another threshold equality holds, showing the bound can be sharp or loose.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — This is equality for this law, not a universal equality claim.
- S07 · premise_audit · G1, S06, work — Zero is excluded; the event retains≥.
- S06 · premise_audit · G1, S05, work — One may clip to min(1,2), but cannot claim a tail of 2.
- S05 · premise_audit · G1, S04, work — Y nonnegative and finite expectation have already been established.
- S04 · premise_audit · G1, S03, work — Positive epsilon is necessary before division by its square.
- S03 · premise_audit · G1, S02, work — Center at mu=0, not an observation or another law's mean.
- S02 · premise_audit · G1, S01, work — Y retains the masses from the original X law.
- S01 · premise_audit · G1, work — Signed X is allowed; Markov will apply to its square.





## Error controls and negative controls

Squared eventEstablish the event equivalence before invoking Markov.

Same-law centerUse the same complete law for the mean, Y and variance.


- Chebyshev needs independent variables. → reject — The proof uses only one X and its second moment.
- The tail is 2 here. → reject — Two is a loose bound; the tail is 1/2.
- The formula applies at epsilon=0. → reject — Its denominator epsilon squared cannot be zero.





## Result and limitations

Chebyshev follows by Markov on squared deviations; at epsilon=1 the exact tail is 1/2.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 0bd2da48a49fb5d3544edcc75194ecfe281101c23dfc66699760f407b58858d2
- original source SHA-256: 740b165db0bc59f0b2d318f01da05196eceb990ec8921f46642cf8407f1c0144
- 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-chebyshev-inequality-01.json)