CounterexampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Henstock–Kurzweil integrability does not imply integrability of the absolute value

Statement refuted

Henstock–Kurzweil integrability implies Henstock–Kurzweil integrability of the absolute value. The derivative $f$ of $F (x) = x^{2} \sin (1 / x^{2})$ on $[0, 1]$ refutes this implication.

Facts & Assumptions

Given: The derivative $f$ from the stated example.

[L1]

The derivative $f$ of $x^{2} \sin (1 / x^{2})$ is Henstock–Kurzweil integrable on $[0, 1]$ ( $F (x) = x^{2} \sin (1 / x^{2})$ has an unbounded derivative whose Henstock–Kurzweil integral is $\sin 1$ ).

[L2]

A finite-endpoint noncompact integral extends to a proper HK integral if and only if the truncation limit exists (Hake's theorem: a finite-endpoint generalized integral is a proper Henstock–Kurzweil integral after assigning the endpoint value).

[L3]

The harmonic series $\sum_{k \geq 1} 1 / k$ diverges (For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ ).

[L4]

Substitution for derivatives evaluates the integral of a composed derivative by its endpoint values (Henstock–Kurzweil substitution for a derivative composed with a differentiable map).

[L5]

If $p$ and $q$ are HK integrable on a compact interval and $p \leq q$ there, then $\int p \leq \int q$ (Monotonicity of the Henstock–Kurzweil integral).

[L6]

Every continuous function on a compact interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L7]

Every Riemann integrable function is Henstock–Kurzweil integrable with the same integral (Every Riemann integrable function is Henstock–Kurzweil integrable with the same integral).

Counterexample

technique · contradiction

1.1

By [L1], $f$ is HK integrable on $[0, 1]$ .

givenL1

2.1

Put $u_{k} = π / 2 + k π$ and $x_{k} = u_{k}^{- 1 / 2}$ . On each compact interval $[x_{k + 1}, x_{k}]$ , both $f$ and $∣ f ∣$ are continuous, so [L6] and [L7] make $∣ f ∣$ locally HK integrable. Since $F (x_{k}) = (- 1)^{k} / u_{k}$ , [L4] and [L5] give $\int_{x_{k + 1}}^{x_{k}} ∣ f ∣ \geq ∣ F (x_{k}) - F (x_{k + 1}) ∣ = 1 / u_{k} + 1 / u_{k + 1}$ , whose partial sums diverge by comparison with [L3].

step 1.1L3L4L5L6L7algebra

3.1

Suppose $∣ f ∣$ were properly HK integrable on $[0, 1]$ ; [L2] would make its truncation integrals converge as the left endpoint tends to zero, contradicting the unbounded sums of step 2.1.

step 2.1L2assume-contradischarge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

59 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

Alessandro Fonda, The Kurzweil-Henstock Integral for Undergraduates, Ch. 1 (standard reference, not scraped)
Andrew Bruckner, Judith Bruckner and Brian Thomson, Real Analysis, Section 1.21 (standard reference, not scraped)