TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)

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.

If continuously differentiable functions converge at one point and their derivatives converge uniformly on a closed interval, then the functions converge uniformly to a differentiable function whose derivative is the derivative limit

Statement

Let $a < b$ be reals and let $f_{k} : [a, b] \to R$ be continuously differentiable: each $f_{k}$ is differentiable on $[a, b]$ and each derivative $f_{k}^{'}$ is continuous there (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point). Suppose there is $c \in [a, b]$ such that the real sequence $(f_{k} (c))$ converges to $A$ , and suppose $f_{k}^{'} \to g$ uniformly on $[a, b]$ . Then there is a differentiable function $f : [a, b] \to R$ such that

$f_{k} ⟶ f uniformly, f^{'} = g .$

Facts & Assumptions

Given: Reals $a < b$ , a point $c \in [a, b]$ , continuously differentiable functions $f_{k} : [a, b] \to R$ , convergence $f_{k} (c) \to A$ , and uniform convergence $f_{k}^{'} \to g$ .

[L1]

A uniform limit of continuous real-valued functions is continuous, and a continuous function on $[a, b]$ is Riemann integrable (The uniform limit of continuous real-valued functions on a metric space is continuous, A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L2]

Uniform convergence of integrable functions preserves integrability and the limit of the integrals (A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals).

[L3]

If $s < t$ , $G$ is differentiable on $[s, t]$ , and $G^{'}$ is integrable there, then $\int_{s}^{t} G^{'} = G (t) - G (s)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ). Restriction to a closed subinterval preserves differentiability and the derivative at its limit points, and integrability on $[a, b]$ passes to every nondegenerate closed subinterval (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ , Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, A function integrable on $[a, b]$ is integrable on every closed subinterval). Finally $\int_{t}^{s} h = - \int_{s}^{t} h$ and $\int_{s}^{s} h = 0$ whenever the displayed integrals are defined (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L4]

If $g$ is continuous, its integral function $H (x) = \int_{a}^{x} g$ is differentiable with $H^{'} = g$ ; oriented additivity gives $\int_{c}^{x} g = H (x) - H (c)$ (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L5]

Sums and scalar multiples of differentiable functions are differentiable, with the corresponding derivative rules (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L6]

A uniform bound $∣ p - q ∣ \leq η$ on an interval gives $∣ \int_{u}^{v} p - \int_{u}^{v} q ∣ \leq η ∣ v - u ∣$ (Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error).

[L7]

On a subset of $R$ with its usual subspace metric, real-native continuity is equivalent to metric-space continuity (Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace).

Proof

technique · constructive

1.1

By [L7], each real-continuous derivative $f_{k}^{'}$ is metric-continuous. The uniform-limit clause of [L1] makes $g$ metric-continuous, and [L7] makes $g$ real-continuous. The integrability clause of [L1] therefore makes every $f_{k}^{'}$ and $g$ Riemann integrable; [L2] also gives the integrability of the uniform limit.

L1L2L7

1.2

Let $ε > 0$ . Choose $N_{0}$ such that $∣ f_{k} (c) - A ∣ < ε / 2$ for $k \geq N_{0}$ , and choose $N_{1}$ such that $∣ f_{k}^{'} (x) - g (x) ∣ < ε / (2 (b - a + 1))$ for $k \geq N_{1}$ and all $x \in [a, b]$ .

givenchoose

2.1

Fix $k$ and $x \in [a, b]$ . If $c < x$ , restrict $f_{k}$ to $[c, x]$ ; its derivative is $f_{k}^{'}$ there and that derivative is integrable there by steps 1.1 and [L3], so the first clause of [L3] gives $f_{k} (x) = f_{k} (c) + \int_{c}^{x} f_{k}^{'}$ . If $x < c$ , apply that clause on $[x, c]$ and then use orientation; if $x = c$ , use $\int_{c}^{c} f_{k}^{'} = 0$ . Thus in every case $f_{k} (x) = f_{k} (c) + \int_{c}^{x} f_{k}^{'}$ .

step 1.1L3

2.2

Define $H (x) : = \int_{a}^{x} g$ and construct $f : [a, b] \to R$ by $f (x) : = A + H (x) - H (c) = A + \int_{c}^{x} g$ .

step 1.1L4construct

3.1

By [L4] and [L5], $H$ is differentiable with $H^{'} = g$ , and therefore the constructed function $f = A + H - H (c)$ is differentiable with $f^{'} = g$ .

step 2.2L4L5

3.2

Choose $N$ at least as large as $N_{0}, N_{1}$ . For $k \geq N$ and $x \in [a, b]$ , steps 2.2 and 2.1 with [L6] give $∣ f_{k} (x) - f (x) ∣ \leq ∣ f_{k} (c) - A ∣ + ∣ \int_{c}^{x} f_{k}^{'} - \int_{c}^{x} g ∣ < ε / 2 + ε ∣ x - c ∣ / (2 (b - a + 1)) < ε$ .

step 2.2step 2.1step 1.2L6choosealgebra

4.1

The index $N$ in step 3.2 serves every $x \in [a, b]$ , so $f_{k} \to f$ uniformly; step 3.1 gives $f^{'} = g$ . Thus the constructed $f$ has both asserted properties.

step 3.2step 3.1discharge-construct∎

Depends on

Used by

Dependency tree · two levels

81 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

MIT OpenCourseWare 18.100B, Real Analysis, Lectures 20–21 (standard reference, not scraped)
W. Trench, Introduction to Real Analysis (standard reference, not scraped)