# Pointwise tail certificates on a finite domain

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

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-pointwise-convergence-of-functions-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Prove pointwise convergence of f_n(p)=1+2/(n+1), f_n(q)=-2-3/(n+1) to f.

The common finite domain {p,q}, real values and n≥0; exact rational-tolerance tail certificates are extended to every positive real epsilon using the Archimedean property, with no infinite-domain extrapolation.





## Givens and symbols


- algebra
- epsilon
- definition_here


- G1 — D={p,q}, f(p)=1,f(q)=-2; the displayed full formulas define f_n for every n≥0.


- D — common finite domain
- N_p,N_q — point-dependent tail indices





## Rules and sources


- mko_definition · cited — This slice uses a complete finite domain and the symbolic tail f_n(x)=f(x)+c_x/(n+s). Supply an exact epsilon witness for each x. A maximum of the finitely many witnesses gives uniform convergence for this finite model, not for an arbitrary infinite domain. A finite prefix is insufficient. · mko-pointwise-convergence-of-functions
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- epsilon · prerequisite — Convergence requires for every positive epsilon an integer N controlling every n≥N by a strict error bound; use the Archimedean property of the reals.
- definition_here · prerequisite — Pointwise convergence: for each x and positive epsilon there exists N(x,epsilon) making the error at that x smaller than epsilon for every n≥N.





## Main derivation

S01 · impliesBefore

n\ge0

After

n+1>0,\quad f_n:D\to\mathbb R

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

The denominator is nonzero and all maps share the specified domain and codomain.



S02 · equivalentBefore

f_n(p)-f(p)=2/(n+1)

After

|f_n(p)-f(p)|=2/(n+1)

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

Fix p first; positivity of numerator and denominator removes the absolute value.



S03 · impliesBefore

\varepsilon>0,\quad N_p=\lfloor2/\varepsilon\rfloor+1

After

n\ge N_p\Longrightarrow n+1>2/\varepsilon

Conditions: \varepsilon\in\mathbb Q_{>0}

Rule: epsilon · Uses: S02

Leaf basis: epsilon

Choose an integer strictly greater than 2/epsilon; every later denominator is larger.



S04 · impliesBefore

n+1>2/\varepsilon

After

|f_n(p)-f(p)|<\varepsilon\quad(n\ge N_p)

Conditions: none

Rule: algebra · Uses: S02, S03

Leaf basis: algebra

Reciprocating positive numbers reverses the inequality and yields the strict epsilon bound.



S05 · equivalentBefore

f_n(q)-f(q)=-3/(n+1)

After

|f_n(q)-f(q)|=3/(n+1)

Conditions: none

Rule: algebra · Uses: G1, S01

Leaf basis: algebra

At q the negative sign disappears under absolute value.



S06 · impliesBefore

N_q=\lfloor3/\varepsilon\rfloor+1

After

n\ge N_q\Longrightarrow |f_n(q)-f(q)|<\varepsilon

Conditions: \varepsilon>0

Rule: epsilon · Uses: S05

Leaf basis: epsilon

The same denominator comparison supplies q's all-tail certificate.



S07 · definitionBefore

\forall x\in D\ \forall\varepsilon>0\ \exists N_x\ \forall n\ge N_x

After

f_n(x)\to f(x)\text{ pointwise on }D

Conditions: none

Rule: definition_here · Uses: G1, S04, S06

Leaf basis: definition_here

Given any real epsilon>0, the declared Archimedean property supplies a positive integer k>1/epsilon. Set delta=1/k, so delta is rational and 0<delta<epsilon. Instantiate the preceding tail certificates at tolerance delta to obtain N_p=2k+1 and N_q=3k+1, and take N=3k+1. For every n≥N, both pointwise errors are at most 3/(n+1)<1/k<epsilon. Thus the pointwise quantifiers hold for every positive real tolerance; this two-point model additionally has a common tail.



S08 · impliesBefore

N=\max(N_p,N_q)

After

n\ge N\Longrightarrow\forall x\in D\ |f_n(x)-f(x)|<\varepsilon

Conditions: none

Rule: epsilon · Uses: S03, S06

Leaf basis: epsilon

For any positive real epsilon, use the rational tolerance delta=1/k chosen in S07. Here N_p and N_q are the indices instantiated at delta; their finite maximum N=3k+1 controls both points for every n≥N with error smaller than epsilon. This is an additional finite-domain inference, not an extrapolation to infinite domains.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · S03, S06 — The common N is an additional finiteness inference, not part of pointwise convergence alone.
- S07 · premise_audit · G1, S04, S06 — The x and N quantifiers have not been interchanged in the definition.
- S06 · premise_audit · S05 — Pointwise convergence permits different N_q and N_p.
- S05 · inverse_equivalence · G1, S01 — Negative function values do not make the absolute error negative.
- S04 · premise_audit · S02, S03 — A non-strict epsilon bound is not silently substituted for the strict one.
- S03 · premise_audit · S02 — N_p depends only on p and epsilon, not the later index n.
- S02 · inverse_equivalence · G1, S01 — The sign check uses the full formula, not a finite table.
- S01 · premise_audit · G1 — The domain does not vary with n.





## Error controls and negative controls

Strict epsilonUse floor(C/epsilon)+1 to preserve strict inequality.

Complete domainThe two points exhaust this domain, not an infinite one.


- Checking n≤100 proves pointwise convergence. → reject — Every n≥N remains an obligation.
- The minus sign makes the q absolute error negative. → reject — The error is 3/(n+1)>0.
- Every infinite-domain pointwise limit permits a finite maximum N. → reject — Infinitely many pointwise indices may have no common bound.





## Result and limitations

Both points converge pointwise, and this finite instance additionally has common N=max(N_p,N_q).







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: f6cce455f215e1c616bf5c32ac57230c794304a90156dbf919ff58b5b4258783
- original source SHA-256: a911769c2c8e25b8fc40746c08867b7ff998c9f34caf51de52c5f65f95c6a20a
- 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-pointwise-convergence-of-functions-01.json)