# A Bernoulli parameter-tail CDF certificate

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

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-convergence-in-distribution-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Prove distributional convergence at continuity points of the limiting CDF.

No common coupling is required; no stronger mode is inferred.





## Givens and symbols


- work


- G1 — For n≥1, X_n has Bernoulli(p_n) law with p_n=1/3+1/(n+2); X has Bernoulli(1/3) law. Only laws, not a coupling, are declared.


- p_n — Bernoulli parameter
- F_n,F — respective CDFs





## Rules and sources


- mko_definition · cited — A common probability space or chosen coupling is not required. A finite prefix does not prove convergence, and the definition imposes no convergence requirement at discontinuities of the limiting CDF. Convergence in distribution does not generally imply convergence in probability, almost surely or in Lp. · mko-convergence-in-distribution
- work · prerequisite — The Bernoulli CDF formula; distributional convergence tests each continuity point of the limit; floor(u)+1>u.





## Main derivation

S01 · impliesBefore

n\ge1

After

1/3<p_n\le2/3<1

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

Parameters lie in the probability range throughout the family.



S02 · impliesBefore

t<0

After

F_n(t)=F(t)=0

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

All negative-threshold cumulative events are empty.



S03 · impliesBefore

0\le t<1

After

F_n(t)=1-p_n=2/3-1/(n+2),\quad F(t)=2/3

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

In the middle interval the CDF includes only the mass at zero.



S04 · impliesBefore

t\ge1

After

F_n(t)=F(t)=1

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

At thresholds at least1 the whole law is included.



S05 · impliesBefore

F\text{ is Bernoulli}(1/3)\text{ CDF}

After

\operatorname{Cont}(F)=\mathbb R\setminus\{0,1\}

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

The limiting CDF jumps only at 0 and 1; all other points lie in constant open regions.



S06 · impliesBefore

0<t<1

After

|F_n(t)-F(t)|=1/(n+2)

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

On the only nontrivial continuity region, the error has an explicit rational tail.



S07 · impliesBefore

\eta>0,\quad N=\lfloor1/\eta\rfloor+1

After

n\ge N\implies1/(n+2)<\eta

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

N exceeds 1/eta, making all later denominators sufficiently large.



S08 · impliesBefore

F_n(t)\to F(t)\quad(t\in\operatorname{Cont}(F))

After

X_n\Rightarrow X

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Combining the three regions establishes the continuity-point CDF definition.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — No common space was specified, so this is not stated as convergence in probability.
- S07 · premise_audit · G1, S06, work — Eta is arbitrary positive and N is selected before the tail conclusion.
- S06 · premise_audit · G1, S05, work — The bound covers every t in the interval, not a few fixed points.
- S05 · premise_audit · G1, S04, work — The definition imposes no convergence requirement at those jumps.
- S04 · premise_audit · G1, S03, work — The point 1 belongs to the right branch, although it is a jump point of the limiting CDF.
- S03 · premise_audit · G1, S02, work — Do not use p_n as the CDF on this interval.
- S02 · premise_audit · G1, S01, work — This covers every t<0.
- S01 · premise_audit · G1, work — The maximum occurs at n=1, rather than being estimated from samples.





## Error controls and negative controls

Legal parametersProve p_n≤2/3 for every n≥1.

Mode boundaryLaw convergence does not supply same-space differences.


- All variables share one coin here. → reject — Only laws, not a coupling, were specified.
- Jump points must be checked for the definition. → reject — Only continuity points of the limiting CDF are required.
- A finite set of close CDFs proves convergence. → reject — The proof uses a universal tail for arbitrary eta.





## Result and limitations

Bernoulli(1/3+1/(n+2)) converges in distribution to Bernoulli(1/3).







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 57b8fd580f0c495a9a33f194a0df094ac8136b1ac350e6e98cc85f9a09eff859
- original source SHA-256: 3f7025055c3497aa6b82b00d019258a96a7e7d544c185df0da1bf15436bbdbd0
- 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-convergence-in-distribution-01.json)