Uniform convergence of derivatives allows term-by-term differentiation

Statement

Let $a < b$, and let $f_n \colon [a, b] \to \mathbb{R}$ be differentiable for each $n$. Assume that $(f_n(x_0))$ converges for some $x_0 \in [a, b]$, and that $(f_n')$ converges uniformly on $[a, b]$ to a function $g$. Then $(f_n)$ converges uniformly on $[a, b]$ to a differentiable function $f$, and $f' = g$.

Remarks

The mean value theorem applied to $f_n - f_m$ shows that $(f_n)$ is uniformly Cauchy. Uniform convergence of $f_n$ alone is not enough. The functions $\frac{\sin(n^2 x)}{n}$ tend to $0$ uniformly, but their derivatives $n \cos(n^2 x)$ do not converge. Mathlib states a version as hasDerivAt_of_tendstoUniformly.

Explanations

L1 human

Derivatives are sensitive to small wiggles, so uniform convergence of functions does not control them. We need uniform convergence of the derivatives themselves.