DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)audited 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 tent function $\phi(t)=\operatorname{dist}(t,\mathbb Z)$ and the Takagi series $T(x)=\sum_{n\ge0}2^{-n}\phi(2^n x)$

Definition

For $t\in\mathbb R$ , put $r(t):=t-\lfloor t\rfloor$ and

$\phi(t):=\min\{r(t),\,1-r(t)\}.$

By the integer-part convention of Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ , $0\le r(t)<1$ ; thus this is equivalently the distance from $t$ to the integers. In particular $0\le\phi(t)\le1/2$ and $\phi$ is $1$ -periodic.

For $x\in[0,1]$ , the Takagi series is the series of real functions in the sense of A series of real-valued functions and its pointwise and uniform convergence through its partial sums

$T(x):=\sum_{n\ge0}2^{-n}\phi(2^n x).$

Depends on

Used by

The Takagi series converges uniformly to a continuous nowhere differentiable function Theorem

Dependency tree · next 3 levels

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

The tent function ϕ(t)=dist⁡(t,Z)\phi(t)=\operatorname{dist}(t,\mathbb Z)ϕ(t)=dist(t,Z) and the Takagi series T(x)=∑n≥02−nϕ(2nx)T(x)=\sum_{n\ge0}2^{-n}\phi(2^n x)T(x)=∑n≥0​2−nϕ(2nx)