Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The linear-approximation form of the derivative: f is differentiable at c with f′(c)=L if and only if the remainder r(x)=f(x)−f(c)−L(x−c) satisfies lim⁡x→cr(x)/(x−c)=0; at most one L does so, so x↦f(c)+L(x−c) is the unique affine map approximating f to first order at c

Statement

Let A⊆R, let f:A→R, let c∈A be a limit point of A (Limit point, isolated point, adherent point, derived set, and dense subset of R) and let L∈R. Write

αL:A→R,αL(x):=f(c)+L (x−c),

for the affine map through (c,f(c)) of slope L, and let rL:=f−αL, that is rL(x)=f(x)−f(c)−L(x−c).

  1. f is differentiable at c with f′(c)=L (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set) if and only if lim⁡x→crL(x)x−c  =  0, the quotient being taken as a function on A∖{c} (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A).
  2. At most one real L satisfies the condition of claim 1. Some real satisfies it exactly when f is differentiable at c, and then that real is f′(c).

So among all affine maps through (c,f(c)) there is at most one whose error rL is small compared with x−c near c; it exists exactly when f is differentiable at c, and its slope is the derivative. This is the sense in which the derivative is a first-order approximation and not merely a quotient.

What the statement does not say. It says nothing about how small rL is in absolute terms, and nothing about any x away from c. The assertion is only that the ratio rL(x)/(x−c) tends to 0; a second-order estimate on rL needs hypotheses this page does not have.

Facts & Assumptions

Given: A set A⊆R, a function f:A→R, a point c∈A that is a limit point of A, a real L, and the functions αL and rL=f−αL of the statement (Limit point, isolated point, adherent point, derived set, and dense subset of R, The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set).

[L1]

Differentiability at c (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set): the difference quotient q(x):=(f(x)−f(c))/(x−c) is a function on A∖{c}, the point c is a limit point of A∖{c}, and f is differentiable at c with f′(c)=L exactly when lim⁡x→cq(x)=L.

[L2]

The limit condition (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A): lim⁡x→ch(x)=P means that for every real ε>0 there is a real δ>0 such that every x in the domain of h with 0<∣x−c∣<δ satisfies ∣h(x)−P∣<ε.

[L3]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); in particular the value f′(c) is a single real.

[L4]

Absolute value: ∣u−0∣=∣u∣, since u−0=u (Basic properties of the absolute value).

Proof

technique · direct
1.1

For every x∈A with x≠c the number x−c is nonzero, so the quotient rL(x)/(x−c) is defined, and rL(x)/(x−c)=(f(x)−f(c))/(x−c)−L(x−c)/(x−c)=q(x)−L. So x↦rL(x)/(x−c) and x↦q(x)−L are the same function on A∖{c}.

L1algebra
2.1

Hence for every x∈A with x≠c one has ∣rL(x)/(x−c)−0∣=∣q(x)−L∣.

step 1.1L4
3.1

Fix a real ε>0 and a real δ>0. By step 2.1 the assertion "every x∈A∖{c} with 0<∣x−c∣<δ satisfies ∣rL(x)/(x−c)−0∣<ε" and the assertion "every x∈A∖{c} with 0<∣x−c∣<δ satisfies ∣q(x)−L∣<ε" are the same assertion. Quantifying over ε and δ, the two limit conditions of [L2] on the common domain A∖{c}, of which c is a limit point by [L1], coincide.

step 2.1L1L2
3.2

Therefore lim⁡x→crL(x)/(x−c)=0 holds if and only if lim⁡x→cq(x)=L holds, which by [L1] is exactly differentiability of f at c with f′(c)=L: claim 1.

step 2.1L1L2
4.1

Suppose reals L and L′ both satisfy the condition of claim 1. By step 3.2 the function f is differentiable at c with f′(c)=L and with f′(c)=L′; the derivative is a single real by [L1] and [L3], so L=L′. Conversely, if f is differentiable at c then L:=f′(c) satisfies the condition, again by step 3.2.

step 3.1step 3.2L1L3
5.1

Claims 1 and 2 are proved, the first by step 3.2 and the second by step 4.1; so the affine map αL with the stated approximation property is unique when it exists, and its slope is f′(c).

step 3.2step 4.1∎

Remarks

  • Why this is worth stating separately. The quotient form is what one computes with; the remainder form is what generalises, since it never divides by the increment and so survives verbatim in settings where the increment is not a number one may divide by. Nothing on this page needs that generality, but the equivalence is what licenses the phrase "best linear approximation" used informally elsewhere, and the phrase is otherwise unearned.

  • The two forms are the same ε-δ condition, not two conditions that happen to agree. Step 1.1 is an identity of functions on A∖{c}, and everything after it is bookkeeping. In particular the proof spends no limit theorem at all: no algebra of limits, no sequences and no choice principle.

  • Uniqueness is the whole of claim 2, and it is inherited. It comes from At a limit point of the domain a function has at most one limit, the same lemma that lets f′(c) be written at all (The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set). Without a limit point of the domain there is no uniqueness anywhere in sight, and the phrase "the best approximation" would name nothing.

Depends on

Used by

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources