ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

$G (x) = x^{2} \sin (1 / x)$ has a bounded derivative discontinuous at $0$ that is nevertheless Riemann integrable, and Newton–Leibniz evaluates its integral

Example

Define $G : [0, 1] \to R$ by

$G (0) = 0, G (x) = x^{2} \sin (1 / x) (0 < x \leq 1) .$

Then $G$ is differentiable on $[0, 1]$ , with

$G^{'} (0) = 0, G^{'} (x) = 2 x \sin (1 / x) - \cos (1 / x) (0 < x \leq 1) .$

The derivative is bounded and is continuous except at $0$ , but it is not continuous at $0$ . Consequently $G^{'}$ is Riemann integrable and

$\int_{0}^{1} G^{'} (x) d x = G (1) - G (0) = \sin 1.$

Moreover, arbitrarily near $0$ the derivative takes the values $- 1$ and $1$ up to terms tending to $0$ : at $x_{k} = 1 / (2 π k)$ and $y_{k} = 1 / ((2 k + 1) π)$ , $G^{'} (x_{k}) = - 1$ and $G^{'} (y_{k}) = 1$ for every integer $k \geq 1$ .

Facts & Assumptions

Given: The function $G$ above.

[L1]

Sine and cosine are differentiable with derivatives cosine and negative sine; the chain and product rules apply (The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

$∣ \sin t ∣ \leq 1$ and $∣ \cos t ∣ \leq 1$ for every real $t$ (Parity and the Pythagorean identity for sine and cosine).

[L3]

The number $π$ is positive, and shifts by $π$ alternate the signs of sine and cosine (Pi as twice the smallest positive zero of cosine, Quarter-turn values and shifts by pi/2 and pi).

[L4]

Reciprocals of positive natural numbers tend to zero (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L5]

A bounded function with an at-most-countable discontinuity set is Riemann integrable (A bounded function on $[a, b]$ whose set of discontinuities is at most countable is Riemann integrable).

[L6]

Newton--Leibniz holds for a continuous function with an interior derivative having an integrable extension (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

Verification

technique · direct

1.1

Since $∣ G (x) ∣ \leq x^{2}$ , the quotient $(G (x) - G (0)) / x$ has absolute value at most $x$ and tends to $0$ ; hence $G^{'} (0) = 0$ .

givenL2

1.2

For $x > 0$ , [L1] gives $G^{'} (x) = 2 x \sin (1 / x) - \cos (1 / x)$ .

givenL1

2.1

By [L2], $∣ G^{'} (x) ∣ \leq 2 x + 1 \leq 3$ on $(0, 1]$ , so $G^{'}$ is bounded. The displayed formula is continuous away from $0$ .

step 1.2L2

2.2

By [L3], sine vanishes and cosine equals $1$ at $2 π k$ , while sine vanishes and cosine equals $- 1$ at $(2 k + 1) π$ ; substituting gives $G^{'} (x_{k}) = - 1$ and $G^{'} (y_{k}) = 1$ . Both sequences tend to $0$ by [L4], so $G^{'}$ is discontinuous there.

step 1.2L3L4

3.1

Thus the discontinuity set is exactly ${0}$ , and [L5] makes $G^{'}$ Riemann integrable.

step 2.1step 2.2L5

4.1

Applying [L6] to $G$ and $G^{'}$ yields $\int_{0}^{1} G^{'} = G (1) - G (0) = \sin 1$ .

step 1.1step 1.2step 3.1L6∎

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: 113 results over 24 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

J. K. Hunter, An Introduction to Real Analysis, Example 12.2 (standard reference, not scraped)

G(x)=x2sin⁡(1/x)G(x)=x2sin(1/x) has a bounded derivative discontinuous at 00 that is nevertheless Riemann integrable, and Newton–Leibniz evaluates its integral