# An epsilon/3 transfer through one fixed approximant [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-uniform-limit-continuity-theorem/) 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-uniform-limit-continuity-theorem-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Prove uniform convergence of affine perturbations on [0,1] and transfer continuity step by step. A common domain and full supremum error; fix one f_N rather than require a common delta for all terms. ## Givens and symbols - algebra - polynomial - epsilon - continuity_def - G1 — f_n(x)=2*x+1+(3*x-1)/(n+1), n≥0, x in [0,1]; f(x)=2*x+1. - N — common approximation index - \delta — continuity radius for fixed f_N - L_N — affine slope ## Rules and sources Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged. - mko_definition · cited — Every approximating f_n is continuous on the same declared domain and sup_x|f_n(x)−f(x)| tends to 0. Exact families use affine perturbations on[0,1], exact supremum errors and epsilon–N certificates. An epsilon/3 transfer fixes one continuous approximant f_N and passes its continuity to f. Pointwise-only powers, uniform sequences whose terms are discontinuous and finite-grid agreement do not supply both theorem hypotheses. · mko-uniform-limit-continuity-theorem - algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities. - polynomial · prerequisite — Real polynomials are continuous and differentiate termwise: the derivative of x^k is k*x^(k-1), and constants differentiate to zero. - 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. - continuity_def · prerequisite — On the common domain, continuity at x_0 means every positive epsilon has a positive delta controlling every domain point with |x-x_0|0,\quad N=\lfloor6/\varepsilon\rfloor+1 After \sup_{x\in[0,1]}|f_n(x)-f(x)|<\varepsilon/3\quad(n\ge N) Conditions: none Rule: epsilon · Uses: S02 Leaf basis: epsilon One N depending only on epsilon controls all points and all later terms. S04 · impliesBefore x_0\in[0,1],\quad L_N=2+3/(N+1)>0 After \delta=\varepsilon/(3L_N)>0 Conditions: none Rule: algebra · Uses: G1, S03 Leaf basis: algebra Choose an arbitrary point x_0 in the domain at which continuity is to be proved, and fix the single approximant f_N selected above. S05 · impliesBefore x\in[0,1],\quad|x-x_0|<\delta After |f_N(x)-f_N(x_0)|=L_N|x-x_0|<\varepsilon/3 Conditions: none Rule: algebra · Uses: S01, S04 Leaf basis: algebra The affine difference supplies the exact continuity bound for the fixed approximant. S06 · impliesBefore |f(x)-f(x_0)|\le|f(x)-f_N(x)|+|f_N(x)-f_N(x_0)|+|f_N(x_0)-f(x_0)| After |f(x)-f(x_0)|<\varepsilon/3+\varepsilon/3+\varepsilon/3=\varepsilon Conditions: none Rule: algebra · Uses: S03, S05 Leaf basis: algebra Two uniform errors and one fixed-function continuity error combine by the triangle inequality. S07 · definitionBefore x_0\in[0,1]\text{ arbitrary},\quad\forall\varepsilon>0\ \exists\delta>0 After f\text{ continuous on }[0,1] Conditions: none Rule: continuity_def · Uses: S04, S06, continuity_def Leaf basis: continuity_def Arbitrariness of x_0 establishes continuity everywhere; the same transfer in general only needs approximant continuity and uniform error. S08 · impliesBefore u_n(x)=x^n\ (n\ge1),\quad u(x)=0\ (x<1),\ u(1)=1 After u_n\to u\text{ pointwise but }|u_n(2^{-1/n})-u(2^{-1/n})|=1/2 Conditions: none Rule: algebra · Uses: G1 Leaf basis: algebra Continuous powers have a pointwise limit discontinuous at one; every n has a domain point with error 1/2, so convergence is not uniform. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S08 · premise_audit · G1 — The point may depend on n when refuting supremum control, unlike a fixed-point test. - S07 · premise_audit · S04, S06, continuity_def — No common delta for all f_n is required. - S06 · premise_audit · S03, S05 — Both approximation errors require the same N valid for every x. - S05 · premise_audit · S01, S04 — At endpoints, x remains in the relative domain [0,1]. - S04 · premise_audit · G1, S03 — N is fixed before choosing delta, which may depend on N and epsilon. - S03 · premise_audit · S02 — N is not chosen after fixing x. - S02 · premise_audit · G1 — No finite-grid maximum is substituted for the whole-interval supremum. - S01 · premise_audit · G1 — Uniform convergence alone cannot replace this premise. ## Error controls and negative controls Quantifier orderChoose N independently of x, then fix f_N and choose delta. Three error piecesBoth uniform approximation errors and the middle continuity error are required. - Pointwise limits are always continuous. → reject — The limit of x^n is discontinuous at one. - Uniform convergence preserves continuity without continuous terms. → reject — A sequence constantly equal to one discontinuous function has zero uniform error and the same discontinuous limit. - All f_n need the same delta for the theorem. → reject — S04-S06 only fix one f_N, which suffices. ## Result and limitations The exact supremum 2/(n+1) proves uniform convergence; epsilon/3 transfer proves continuity of the limit without a shared-delta requirement. ## Verification and source binding 1 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 5b91758154756c5c6299fe5034cdb6883620b334d25e460b7f132e304c588e23 - original source SHA-256: 1da07516f1abb614567738a8bf1eec3d0b56736b28e9c367c0e769a458db9746 - 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-uniform-limit-continuity-theorem-01.json)