Function limits: a removable-factor quotient, affine δ bounds and unequal one-sided limits

Goal and scope

On punctured real domains: (1) prove by ε-δ that f(x)=(x²−9)/(x−3) has lim_(x→3) f(x)=6 while f(3) stays undefined; (2) for the affine g(x)=4x−1 at a=2 with ε=1/2, prove that δ=1/8 is valid (the equality |m|δ=ε is allowed) and δ=1/7 is not; (3) for the branch function h(x)=x+1 (x<1), h(x)=2x+3 (x>1), find the one-sided limits 2 and 5 and prove that the two-sided limit does not exist.

Treats only the MKO's three kinds of exercise: affine expressions, removable-factor quotients and left/right affine branches, on the domain ℝ∖{a}. It does not prove general limit laws (sums, products, composition) and does not treat isolated points or other approach domains. It does not change the canonical MKO or its English edition.

Givens and symbols

• abs_rules
• order_basics
• frac_rules
• distributive
• func_limit_def
• numeric_evaluation

• G1 — Functions are defined on the punctured domain ℝ∖{a}; f(a) need not exist.
• G2 — f(x)=(x²−9)/(x−3) on ℝ∖{3}.
• G3 — g(x)=4x−1 (m=4, b=−1), a=2; ε=1/2 (p=1, q=2); candidate δ=1/8 (u=1, v=8) and δ=1/7.
• G4 — h(x)=x+1 for x<1 and h(x)=2x+3 for x>1, on ℝ∖{1}.

• \lim_{x\to a}f(x)=L — the punctured two-sided limit
• \varepsilon,\ \delta — the output tolerance and the input distance bound, both positive
• 0<|x-a|<\delta — the punctured neighbourhood: x≠a and distance strictly below δ
• \varepsilon=\tfrac{p}{q},\ \delta=\tfrac{u}{v} — rational tolerance and rational distance bound
• L^-,\ L^+ — the left and right limits

Rules and sources

• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_func_limit · cited — For a real f defined at all x≠a near a, lim_(x→a) f(x)=L means each ε>0 admits δ>0 with |f(x)−L|<ε whenever 0<|x−a|<δ; a finite two-sided limit requires equal one-sided limits. The affine limit of mx+b is ma+b; for ε=p/q and δ=u/v the uniform affine bound permits |m|uq≤pv, equality included. · mko-function-limit
• one_sided_def · prerequisite — Left limit L⁻: each ε>0 admits δ>0 with |f(x)−L⁻|<ε whenever a−δ<x<a; right limit L⁺: the same with a<x<a+δ.
• L_affine_bound · lemma — For g(x)=mx+b, a real a, ε>0 and δ>0: if |m|δ≤ε, then 0<|x−a|<δ implies |g(x)−(ma+b)|<ε.

Main derivation

\lim_{x\to a}f(x)=L

\forall\varepsilon>0\ \exists\delta>0\ \forall x:\ 0<|x-a|<\delta\Rightarrow|f(x)-L|<\varepsilon

\mathrm{dom}(f)=\mathbb{R}\setminus\{3\}

\forall\delta>0:\ \{x:0<|x-3|<\delta\}\subseteq\mathrm{dom}(f),\ 3+\tfrac{\delta}{2}\ \text{in it}

x^2-9

(x-3)(x+3)

f(x)=\frac{(x-3)(x+3)}{x-3}\ (x\neq 3)

f(x)=x+3\ (x\neq 3)

|f(x)-6|\ (x\neq 3)

|(x+3)-6|=|x-3|

\varepsilon>0\ \text{arbitrary},\ \delta=\varepsilon

0<|x-3|<\delta\Rightarrow|f(x)-6|=|x-3|<\varepsilon;\ \lim_{x\to 3}f(x)=6

|g(x)-7|,\ g(x)=4x-1,\ 7=4\cdot 2-1

|4x-8|=|4(x-2)|=4|x-2|

|m|\cdot\frac{u}{v}\le\frac{p}{q}

|m|\,u\,q\le p\,v

4\cdot 1\cdot 2=8\le 8=1\cdot 8

0<|x-2|<\tfrac18\Rightarrow|g(x)-7|<\tfrac12

\delta=\tfrac17:\ 4\cdot 1\cdot 2=8>7=1\cdot 7

x=2+\tfrac18:\ 0<|x-2|<\tfrac17,\ |g(x)-7|=\tfrac12\not<\tfrac12

x<1:\ |h(x)-2|

|(x+1)-2|=|x-1|;\ \delta=\varepsilon\ \text{gives}\ L^-=2

x>1:\ |h(x)-5|

|(2x+3)-5|=2|x-1|;\ \delta=\tfrac{\varepsilon}{2}\ \text{gives}\ L^+=5

\lim_{x\to 1}h(x)=L\ \text{(assumed)},\ \varepsilon=\tfrac32

\delta>0,\ t=\tfrac{\delta}{2}:\ |h(1+t)-L|<\tfrac32,\ |h(1-t)-L|<\tfrac32

|h(1+t)-h(1-t)|\le|h(1+t)-L|+|L-h(1-t)|<3

h(1+t)-h(1-t)=3+3t>3:\ \text{contradiction};\ \lim_{x\to 1}h(x)\ \text{does not exist}

\text{S06, S09, S10, S11, S12, S14}

\lim_{x\to3}f=6;\ \delta=\tfrac18\ \text{valid},\ \tfrac17\ \text{not};\ L^-=2\neq 5=L^+,\ \text{no two-sided limit}

Substeps and lemmas

|(mx+b)-(ma+b)|

|m(x-a)|=|m|\,|x-a|

m=0

|g(x)-(ma+b)|=0<\varepsilon\ \text{for every}\ x

m\neq 0,\ 0<|x-a|<\delta,\ |m|\delta\le\varepsilon

|m||x-a|<|m|\delta\le\varepsilon

Reverse audits

• S15 · sufficient_goal_reduction · S06, S09, S10, S11, S12, S14 — Goal G: the three conclusions of this guide. Each part is proved forwards by the listed steps; this step only conjoins them, without assuming G.
• S14 · premise_audit · S13, abs_rules, contradiction — The contradiction refutes only the assumption that a two-sided limit exists; the one-sided limits of S11 and S12 are unaffected.
• S13 · premise_audit · S01, exists_elim, forall_elim — δ is a fresh name taken from the assumption; the final conclusion does not mention δ.
• S12 · premise_audit · G4, one_sided_def, forall_intro — Only the right branch formula on x>1 is used; each one-sided limit exists on its own.
• S11 · premise_audit · G4, one_sided_def, forall_intro — Only the left branch formula on x<1 is used; ε is arbitrary.
• S10 · premise_audit · S07, quantifier_negation, numeric_evaluation — The failed criterion only means the lemma does not apply; invalidity comes from the explicit counterexample (N6, N7, N8).
• S09.3 · premise_audit · S09.1, order_basics — |m|>0 is needed to keep the strict inequality; m=0 is handled separately in S09.2.
• S09.2 · premise_audit · S09.1, mul_zero — Only ε>0 is needed; this is the first case of the lemma.
• S09.1 · inverse_equivalence · distributive, abs_rules — An identity, valid both ways.
• S09 · premise_audit · S08, L_affine_bound, numeric_evaluation — The lemma's hypothesis |m|δ≤ε is checked by N4 and N5; the lemma gives only a sufficient condition.
• S08 · inverse_equivalence · order_basics, frac_rules — Backward, divide by the positive qv.
• S07 · inverse_equivalence · abs_rules, distributive — Identities, valid both ways.
• S06 · sufficient_goal_reduction · S01, S05, forall_intro — Goal G: the limit is 6. Sufficient condition H: for arbitrary ε, δ=ε works; H⇒G by the definition. H is proved forwards from S05, without assuming G and without using f(3).
• S05 · inverse_equivalence · S04, eq_replace — Replacement of equals, valid both ways; used only at x≠3.
• S04 · inverse_equivalence · frac_rules, mul_inverse_nonzero — Backward, multiply numerator and denominator by x−3, which needs x−3≠0; the condition holds throughout the domain.
• S03 · inverse_equivalence · distributive — An identity, valid both ways.
• S02 · premise_audit · G2, S01, order_basics — It only confirms that the limit question is meaningful (3 is a limit point of the domain); it does not claim the limit exists.
• S01 · premise_audit · G1, mko_func_limit, func_limit_def — This step only unfolds the definition and derives no new fact.

Error controls and negative controls

Distinguish the limit from f(a); do not patch a value in after division by zero

One misconception the MKO lists is taking the limit to be f(a). f(3) is 0/0 and undefined; the limit 6 comes from the simplification f(x)=x+3 at x≠3 (S04), and 0<|x−3| keeps the centre out (S01). The simplification does not define f at 3; if one separately set f(3)=100, the limit would still be 6.

Equality at the δ boundary is allowed

Another misconception is rejecting |m|δ=ε. Because the input distance is strictly below δ, 4|x−2|<4δ=ε stays strict (S09.3), so δ=1/8 is valid. This differs from sequence cutoffs, where the error itself is compared and an error equal to ε fails. That δ=1/7 fails must be shown by an explicit counterexample (S10).

Unequal one-sided limits deny only the two-sided limit

The one-sided limits 2 and 5 of h both exist but differ, so there is no two-sided limit (S14). This does not mean the right limit fails to exist, and finitely many test points (for example x=0.9 and 1.1) cannot replace the ε-δ argument.

• f(3)=0/0 is undefined, so lim_(x→3) f(x) does not exist → reject — The punctured limit ignores f(3); S06 proves the limit is 6.
• f(x)=x+3, so f(3)=6 → reject — The simplification holds only at x≠3; the domain of f is ℝ∖{3}, and cancelling at 3 would divide by 0.
• For ε=1/2, δ=1/8 is invalid because |m|δ equals ε exactly → reject — 0<|x−2|<1/8 gives 4|x−2|<1/2, a strict inequality.
• h has no two-sided limit at 1, so its right limit does not exist either → reject — The right limit is 5 (S12); it merely differs from the left limit 2.
• f(3.1)=6.1 and f(2.9)=5.9, so the limit 6 is proved → reject — Finitely many test points are only consistent with the conclusion, not a proof; the proof is the argument of S06 for arbitrary ε.

Result and limitations

f(x)=(x²−9)/(x−3) on ℝ∖{3} has lim_(x→3) f(x)=6 (with δ=ε), while f(3) stays undefined. For g(x)=4x−1 at a=2 with ε=1/2: δ=1/8 is valid (4·1·2=8≤8, equality allowed) and δ=1/7 is not (at x=2+1/8 the error is exactly 1/2). h has left limit 2 and right limit 5, and no two-sided limit.

• This guide does not prove general limit laws and does not treat domains with isolated points.
• N2 is a numerical check at two test points, consistent with the simplification of S04; it plays no part in the proof.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
• original source SHA-256: f75050de6a74ead986b8699e576b6dd6e5e0acae0be6646bdbb41b727c4ac99e
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)