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.

The sine harmonics are pointwise bounded but have no uniformly convergent subsequence

Example

For $k \in N$ , define

$f_{k} : [0, π] \to R, f_{k} (x) : = \sin ((k + 1) x) .$

The sequence $(f_{k})$ is uniformly bounded, is not equicontinuous, and has no uniformly convergent subsequence. It does not converge pointwise on all of $[0, π]$ . Nevertheless, for every fixed continuous $g : [0, π] \to R$ ,

$\lim_{k \to \infty} \int_{0}^{π} g (x) f_{k} (x) d x = 0.$

Facts & Assumptions

Given: The functions $f_{k}$ in the Example, on the compact interval $[0, π]$ with its usual metric.

[L1]

Sine is differentiable and hence continuous, and $∣ \sin x ∣ \leq 1$ for every real $x$ (The derivatives of sine and cosine are cosine and minus sine, A function differentiable at $c$ is continuous at $c$ , Parity and the Pythagorean identity for sine and cosine).

[L2]

The quarter-turn values and shift formulas determine $\sin (n π / 2)$ and give $\sin (π / 2) = 1$ (Quarter-turn values and shifts by pi/2 and pi).

[L3]

A family $F$ is equicontinuous at $a$ when, for every $ε > 0$ , one $δ > 0$ makes $d (x, a) < δ$ imply $∣ f (x) - f (a) ∣ < ε$ for every $f \in F$ (Equicontinuity, pointwise boundedness, and uniform boundedness for families in $C (K, R)$ ).

[L4]

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

[L5]

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 < ε$ ).

[L6]

For every continuous $g : [0, π] \to R$ , $\lim_{n \to \infty} \int_{0}^{π} g (x) \sin (n x) d x = 0$ (Riemann–Lebesgue lemma for continuous functions on a compact interval).

[L7]

The number $π = 2 γ$ is positive because the smallest positive zero of cosine satisfies $γ \in (0, 2)$ . Thus $[0, π]$ is compact by Heine--Borel; real and metric compactness agree for its absolute-value subspace metric (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two, Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace, claim 5).

[L8]

Affine real functions are continuous, and composites of continuous real functions are continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 5, A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).

Verification

technique · contradiction

1.1L1L8

Sine is continuous by [L1], while [L8] makes each affine argument $x \mapsto (k + 1) x$ and its composite $f_{k}$ continuous. Also $∣ f_{k} (x) ∣ \leq 1$ for every $k$ and every $x \in [0, π]$ , so the sequence is uniformly bounded.

1.2L2algebra

At $x = π / 2$ , the values $f_{k} (π / 2)$ cycle through $1, 0, - 1, 0$ , so the sequence does not converge pointwise on the whole interval.

1.3L5L7constructalgebra

At zero, $f_{k} (0) = 0$ , and the points $x_{k} : = π / (2 (k + 1))$ lie in $[0, π]$ and tend to zero by [L5] and [L7].

1.4L6

Applying [L6] at the positive integer frequency $k + 1$ gives the asserted convergence of every fixed continuous test-function integral.

1.5assume-contra

Suppose, for contradiction, that a subsequence $(f_{k_{j}})$ converges uniformly to a function $g$ .

2.1step 1.3L2L3L7

On the compact metric interval from [L7], the points from step 1.3 satisfy $f_{k} (x_{k}) = 1$ by [L2]. Hence [L3] fails at zero for $ε = 1 / 2$ , and the family is not equicontinuous.

2.2step 1.5L4

By [L4], the uniform limit $g$ is continuous; because every $f_{k_{j}} (0) = 0$ , uniform convergence also gives $g (0) = 0$ .

3.1step 2.2

Continuity at zero gives a $δ > 0$ with $∣ g (x) ∣ < 1 / 4$ for $0 \leq x < δ$ , and uniform convergence gives an index after which $∣ f_{k_{j}} (x) - g (x) ∣ < 1 / 4$ for every $x \in [0, π]$ .

4.1step 1.5step 3.1L2L5discharge-contradiction∎

A subsequence has strictly increasing indices, so $k_{j} \geq j$ by induction and [L5] gives $x_{j} : = π / (2 (k_{j} + 1)) < δ$ for all sufficiently large $j$ . Then [L2] gives $f_{k_{j}} (x_{j}) = 1$ , while step 3.1 gives both $∣ g (x_{j}) ∣ < 1 / 4$ and $∣ f_{k_{j}} (x_{j}) - g (x_{j}) ∣ < 1 / 4$ , an impossibility. Thus no uniformly convergent subsequence exists, completing all the claims.

Depends on

Used by

FALSE: every pointwise bounded sequence of continuous functions has a uniformly convergent subsequence False statement

Dependency tree · two levels

88 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

John Hutchinson, Introduction to Analysis, §15.7, Remark 15.7.2 (standard reference, not scraped)
Jiří Lebl, Basic Analysis I, Exercise 5.2.18 (standard reference, not scraped)