TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

The Takagi series converges uniformly to a continuous nowhere differentiable function

Statement

The Takagi series $T(x)=\sum_{n\ge0}2^{-n}\phi(2^nx)$ converges uniformly on $[0,1]$ . Its sum is continuous and has no finite derivative at any point of $[0,1]$ , with one-sided derivatives at the endpoints understood.

Facts & Assumptions

Given: The tent function and series are as in The tent function $\phi(t)=\operatorname{dist}(t,\mathbb Z)$ and the Takagi series $T(x)=\sum_{n\ge0}2^{-n}\phi(2^n x)$ .

[L1]

The Weierstrass M-test gives uniform convergence from a summable uniform majorant (The Weierstrass M-test gives absolute pointwise convergence and uniform convergence of a function series).

[L2]

A uniform limit of continuous real functions is continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).

[L3]

Differentiability requires convergence of the relevant difference quotients (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).

Proof

technique · direct

1.1

Since $0\le\phi\le1/2$ , the $n$ th summand is bounded by $2^{-n-1}$ ; its majorant series converges. Thus $T$ converges uniformly by [L1].

givenL1algebra

1.2

For $x\in[0,1)$ and each $N$ , let $u_N\le x<v_N$ be the adjacent dyadic rationals of order $N$ ; at $x=1$ use the left adjacent interval. Every summand of index at least $N$ vanishes at both endpoints, while each earlier summand is affine on that interval with slope $\varepsilon_k\in\{-1,1\}$ .

givenalgebra

2.1

Every summand is continuous, so $T$ is continuous by [L2].

step 1.1L2algebra

2.2

Hence $\bigl(T(v_N)-T(u_N)\bigr)/(v_N-u_N)=\sum_{k<N}\varepsilon_k$ . These secant slopes cannot converge to a finite real number, because consecutive partial sums differ by $\varepsilon_N$ of absolute value one.

step 1.2algebra

3.1

If a finite derivative existed at an interior point, both endpoint difference quotients and therefore their secant combination would tend to it; at a dyadic point or endpoint the same argument uses the nested one-sided dyadic intervals. This contradicts step 2.2 and [L3].

step 2.2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 14 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

The Takagi function: a survey (standard reference, not scraped)