Solution (source code)

= Solution

For a <function> with <continuous> <derivatives> through order $m+1$ on the interval between $0$ and $x$, the <Taylor formula with integral remainder> is
$$
f(x)=\sum_{j=0}^{m}\frac{f^{(j)}(0)}{j!}x^j+R_m(x),\qquad
R_m(x)=\frac1{m!}\int_0^x(x-t)^m f^{(m+1)}(t)\,dt.
$$
This is <Taylor's theorem> about zero; <translation> gives the formula about any other point. To prove it, the case $m=0$ is the <fundamental theorem of calculus>. For $m\ge1$, <integration by parts> gives
$$
R_m(x)=-\frac{f^{(m)}(0)x^m}{m!}
+\frac1{(m-1)!}\int_0^x(x-t)^{m-1}f^{(m)}(t)\,dt
=R_{m-1}(x)-\frac{f^{(m)}(0)x^m}{m!}.
$$
Substitution into the formula at order $m-1$ proves the formula at order $m$ by induction. The <integral> estimate, valid also for negative $x$, is
$$
|R_m(x)|\le\frac{|x|^{m+1}}{(m+1)!}
\sup_{t\text{ between }0\text{ and }x}|f^{(m+1)}(t)|.
$$
For the <smooth function> satisfying $f^{(3)}=f$, each fixed <derivative> is <continuous> on $[-R,R]$ and hence is bounded there by the <extreme value theorem>. Thus a bound $M_j$ exists for every $j$. Differentiating the <differential equation> repeatedly gives $f^{(j+3)}=f^{(j)}$. Only the three <functions> $f,f',f''$ are needed: take $M$ to be the maximum of their absolute-value bounds on $[-R,R]$. Then $|f^{(j)}(x)|\le M$ simultaneously for every $j\ge0$ and $|x|\le R$.

At zero the <derivatives> consequently repeat the values $1,0,0$. <Taylor's theorem> therefore gives
$$
f(x)=\sum_{n=0}^{\lfloor m/3\rfloor}\frac{x^{3n}}{(3n)!}+R_m(x),\qquad
\sup_{|x|\le R}|R_m(x)|\le\frac{MR^{m+1}}{(m+1)!}\longrightarrow0.
$$
The last <limit of a sequence> follows because the ratio of consecutive majorants is $R/(m+2)$, eventually less than $1/2$. Since $R$ is arbitrary, <Taylor expansion from a periodic derivative equation> proves
$$
\boxed{f(x)=\sum_{n=0}^{\infty}\frac{x^{3n}}{(3n)!}\quad\text{for every }x\in\mathbb R.}
$$
This proves convergence to the <function> using a remainder bound; it does not assume beforehand that a <smooth function> equals its <Taylor series>.