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.
A uniform limit of smooth functions need not be differentiable anywhere
Statement
There is a sequence of smooth functions that converges uniformly on to a continuous function which is differentiable at no real point. Consequently, uniform convergence does not preserve even first differentiability, despite every approximating function being .
Facts & Assumptions
Given: The Weierstrass partial sums .
A function is smooth, or , when it is for every (Higher derivatives and the classes and ).
The partial sums of the classical Weierstrass series converge uniformly to on (The classical Weierstrass series converges uniformly to a continuous function).
If , is an odd integer, and , then is continuous everywhere and differentiable nowhere (Under , the classical Weierstrass function is continuous everywhere and differentiable nowhere).
Sine and cosine are differentiable on , and their derivatives are cosine and negative sine (The derivatives of sine and cosine are cosine and minus sine).
The chain rule and the sum and scalar-multiple rules compute derivatives of finite sums and affine composites (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , Sums, scalar multiples, products and quotients: , , , and when ).
Differentiable real functions are continuous (A function differentiable at is continuous at ).
There is a unique with , and (Cosine has a smallest positive zero, lying strictly between zero and two, Pi as twice the smallest positive zero of cosine).
Proof
Choose and . The integer is odd, and [L7] gives , so ; all hypotheses of [L3] hold.
Repeated application of [L4] and [L5] shows that every derivative of every finite partial sum is a finite linear combination of sine and cosine functions. Those derivatives are continuous by [L6], so each is smooth in the sense of [L1].
By [L2], the smooth functions from step 1.2 converge uniformly on to .
The parameter check in step 1.1 lets [L3] identify this uniform limit as continuous everywhere and differentiable nowhere.
Thus the sequence in step 2.1 consists of smooth functions and converges uniformly to the nowhere-differentiable function in step 2.2.
Depends on
- The classical Weierstrass function
- The classical Weierstrass series converges uniformly to a continuous function
- Under $ab>1+3\pi/2$, the classical Weierstrass function is continuous everywhere and differentiable nowhere
- Higher derivatives and the classes $C^k$ and $C^\infty$
- The derivatives of sine and cosine are cosine and minus sine
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- 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$
- A function differentiable at $c$ is continuous at $c$
- Pi as twice the smallest positive zero of cosine
- Cosine has a smallest positive zero, lying strictly between zero and two
Used by
Dependency tree · two levels
41 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
- Jeff Calder, Weierstrass's Non-Differentiable Function, Theorem 1 (standard reference, not scraped)
- John K. Hunter, An Introduction to Real Analysis, Example 9.24 (standard reference, not scraped)