ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

$\sum_{n = 1}^{\infty} \sin (n x) / n$ converges pointwise but not uniformly

Example

The function series

$\sum_{n = 1}^{\infty} \frac{\sin (n x)}{n}$

converges at every real $x$ , but it does not converge uniformly on $[0, 2]$ and therefore does not converge uniformly on $R$ .

Facts & Assumptions

Given: The zero-based function series $\sum_{k = 0}^{\infty} f_{k} (x)$ with $f_{k} (x) : = \sin ((k + 1) x) / (k + 1)$ .

[L1]

If $x \notin 2 π Z$ , then for every positive integer $N$ , $∣ \sum_{n = 1}^{N} \sin (n x) ∣ \leq 1 / ∣ \sin (x / 2) ∣$ (Finite sums of the sine harmonics).

[L2]

If the partial sums of $(a_{k})$ are bounded and $(b_{k})$ is nonincreasing with limit zero, then $\sum a_{k} b_{k}$ converges (Dirichlet's test: if the partial sums of $\sum a_{k}$ are bounded and $(b_{k})$ is nonincreasing with $b_{k} \to 0$ , then $\sum a_{k} b_{k}$ converges).

[L3]

Sine vanishes at every integer multiple of $π$ and has period $2 π$ (The zero sets of sine and cosine and the least positive common period 2 pi).

[L4]

Uniform convergence of a function series is equivalent to the uniform Cauchy condition on every sufficiently late finite tail (A series of real-valued functions converges uniformly if and only if its tails are uniformly small).

[L5]

For $0 < t \leq 2$ , $\sin t \geq t / 3 > 0$ (Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3).

[L6]

For every real $ε > 0$ , there is a positive integer $N$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Verification

technique · direct

1.1L3

If $x \in 2 π Z$ , every term $f_{k} (x)$ is zero by [L3], so the series converges there.

1.2L1L2L6algebra

If $x \notin 2 π Z$ , [L1] bounds the partial sums of $a_{k} : = \sin ((k + 1) x)$ independently of the partial-sum index. The weights $b_{k} : = 1 / (k + 1)$ are positive, nonincreasing, and tend to zero by [L6], so [L2] proves convergence at this $x$ .

1.3L5constructalgebra

Let $K$ be a positive integer and put $x : = 1 / K$ . For the indices $k = K$ through $2 K - 1$ , the angles $(k + 1) x$ lie in $(1, 2]$ , so [L5] gives $\sin ((k + 1) x) \geq 1 / 3$ , while $1 / (k + 1) \geq 1 / (2 K)$ . These $K$ terms have sum at least $1 / 6$ .

2.1step 1.1step 1.2

Steps 1.1 and 1.2 cover all real $x$ , so the series converges pointwise on $R$ .

2.2step 1.3L4algebra

Given any proposed uniform-Cauchy threshold $N$ , choose a positive $K > N + 1$ . The tail from $k = K$ to $k = 2 K - 1$ lies beyond $N$ but has value at least $1 / 6$ at $x = 1 / K$ by step 1.3. Therefore [L4] fails for $ε = 1 / 7$ , and the series is not uniform on $[0, 2]$ .

3.1step 2.1step 2.2∎

Pointwise convergence is step 2.1. Nonuniformity on $[0, 2]$ is step 2.2, and uniform convergence on $R$ would restrict to uniform convergence on that interval, so the series is not uniform on $R$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

43 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

NCSU MA 401 course text, Chapter 5, Example 5.18 (standard reference, not scraped)

∑n=1∞sin⁡(nx)/n∑n=1∞​sin(nx)/n converges pointwise but not uniformly