TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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\mathbb{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 \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ 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\mathbb{R}$ such that

$f_k\longrightarrow f\ \text{ uniformly},\qquad f'=g.$

Facts & Assumptions

Given: Reals $a<b$ , a point $c\in[a,b]$ , continuously differentiable functions $f_k:[a,b]\to\mathbb{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^tG'=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 \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, The $\varepsilon$ - $\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$ , Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$ , Intervals of $\mathbb{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^xg$ is differentiable with $H'=g$ ; oriented additivity gives $\int_c^xg=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)$ , $(\alpha f)'(c) = \alpha f'(c)$ , $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$ , and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$ , The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L6]

[L7]

On a subset of $\mathbb R$ with its usual subspace metric, real-native continuity is equivalent to metric-space continuity (Dictionary: for $A \subseteq \mathbb{R}$ with the metric $d(x,y) = |x-y|$ , continuity and uniform continuity of $f : A \to \mathbb{R}$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $\mathbb{R}$ is compact in the open-cover sense of $\mathbb{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 $\varepsilon>0$ . Choose $N_0$ such that $|f_k(c)-A|<\varepsilon/2$ for $k\ge N_0$ , and choose $N_1$ such that $|f_k'(x)-g(x)|<\varepsilon/\bigl(2(b-a+1)\bigr)$ for $k\ge 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^xg$ and construct $f:[a,b]\to\mathbb{R}$ by $f(x):=A+H(x)-H(c)=A+\int_c^xg$ .

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

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

Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 148 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)