A series about iterated cosine

I was swiping through my Twitter timeline and saw this tweet:

If you take any real number and repeatedly applying the cosine to it, the result always converges to the same constant (0.73908...). This problem shows that the convergence is fast enough that the differences add up to some differentiable function. #calculus #Math pic.twitter.com/8scsuWldTV

— Sam Walters ☕️ (@SamuelGWalters) January 18, 2020

It is well known that repeatedly applying $\cos$ to any real number converges to the only real solution $\alpha$ to cosα=α. This can be proven using the intermediate value theorem and the mean value theorem. Yet at first sight, it might come as a surprise that the series $$F(x)=\sum _{k=1}^{\infty }(\alpha -{\cos }^{(k)}x)$$ mentioned in the tweet uniformly converges to a differentiable function, because the remainder could be pathological without looking into the actual function being iterated. However, once you start using a scratch paper, it becomes ‘of course it’s like this’.

We want to bound $\alpha -{\cos }^{(k)}x$ uniformly. First, by some (not so numerical) computation, 0≤α≤1, so $-2\le \alpha -\cos x\le 1$ for all x. Next, by Lagrange’s mean value theorem, we have $$\begin{array}{rl}\alpha -{\cos }^{(k+1)}x& =\cos \alpha -\cos {\cos }^{(k)}x\\ & =(\alpha -{\cos }^{(k)}x)(-\sin y)\end{array}$$ for some $y$ between $0\le \alpha \le 1$ and −1≤cos(k)x≤1. Therefore, we know −1≤y≤1, which implies $|\alpha -{\cos }^{(k+1)}x|\le |\alpha -{\cos }^{(k)}x|\sin 1$ for all x.

Now that ∣α−cos(k)x∣≤2sink−11, by Weierstrass criterion, the series $F(x)$ converges uniformly.

Next we want to show that the sum is differentiable. To this end, consider the term-by-term derivative $$G(x)=\sum _{k=1}^{\infty }(\alpha -{\cos }^{(k)}x{)}^{\prime }=\sum _{k=1}^{\infty }{g}_k(x),$$ where gk​(x)=(−1)k+1∏j=0k−1​sincos(j)x. Since ∣gk​(x)∣≤sink−11, again by Weierstrass criterion, $G(x)$ converges uniformly. Together with that each $g_k(x)$ is continuous thus integrable, we know that $G(x)$ is also continuous and that the integration of $G(x)$ equals the sum of the term-by-term integration of gk​(x). By how we did the term-by-term derivative in the first place, $$\alpha -{\cos }^{(k)}x={\int }_{\alpha }^x{g}_k(t)\mathrm{d}t,$$ which readily gives $$F(x)=\sum _{k=1}^{\infty }{\int }_{\alpha }^x{g}_k(t)\mathrm{d}t={\int }_{\alpha }^{x}G(t)\mathrm{d}t,$$ whence $F^{\prime }(x)=G(x)$ by the fundamental theorem of calculus.