DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 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 $ϕ (t) = dist (t, Z)$ and the Takagi series $T (x) = \sum_{n \geq 0} 2^{- n} ϕ (2^{n} x)$

Definition

For $t \in R$ , put $r (t) : = t - ⌊ t ⌋$ and

$ϕ (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 \leq x < m + 1$ , $0 \leq r (t) < 1$ ; thus this is equivalently the distance from $t$ to the integers. In particular $0 \leq ϕ (t) \leq 1 / 2$ and $ϕ$ 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 \geq 0} 2^{- n} ϕ (2^{n} x) .$

Depends on

Used by

Dependency tree · two levels

21 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

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

The tent function ϕ(t)=dist⁡(t,Z)ϕ(t)=dist(t,Z) and the Takagi series T(x)=∑n≥02−nϕ(2nx)T(x)=∑n≥0​2−nϕ(2nx)