ExampleConstruction: Literature-sourcedVerification: 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.

$\sin x / x$ has a Henstock–Kurzweil integral on $[0, \infty)$

Example

Define $s (0) = 1$ and $s (x) = \sin x / x$ for $x > 0$ . Then $s$ has a noncompact Henstock–Kurzweil integral on $[0, \infty)$ . No value for that integral is asserted here.

Facts & Assumptions

Given: The removable extension $s$ in the Example; differentiability of sine at $0$ gives $\lim_{x \to 0} \sin x / x = 1$ .

[L1]

Dirichlet's improper-integral test applies when the first factor is locally Riemann integrable with a bounded truncation primitive and the second is nonnegative, nonincreasing, and tends to zero (Dirichlet's test for improper integrals).

[L2]

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

[L3]

Sine is differentiable at zero with derivative $1$ , and $- \cos$ is a primitive of sine (The derivatives of sine and cosine are cosine and minus sine).

[L4]

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

[L5]

A noncompact HK integral is the finite limit of its compact truncation integrals (Henstock–Kurzweil integrals on half-open and unbounded intervals by compact truncation limits).

[L6]

For every real $x$ , $∣ \cos x ∣ \leq 1$ (Parity and the Pythagorean identity for sine and cosine).

[L7]

Henstock–Kurzweil integrals restrict to compact subintervals and add over adjacent intervals (Henstock–Kurzweil integrability on subintervals and additivity over adjacent intervals).

Verification

technique · direct

1.1

On $[1, \infty)$ the first factor $\sin x$ is continuous and hence locally Riemann integrable by [L4], while its primitive $- \cos x$ is bounded by [L3] and [L6]. Apply [L1] with second factor $1 / x$ , which is nonnegative, decreasing, and tends to zero; the compact truncation integrals therefore have a finite limit.

givenL1L3L4L6

2.1

The derivative clause in [L3] gives the removable limit at zero, so [L4] makes the extension Riemann integrable on each compact truncation and [L2] makes it HK integrable there. By [L7], for every $c > 1$ its integral on $[0, c]$ is the fixed integral on $[0, 1]$ plus the integral on $[1, c]$ ; the limit from step 1.1 and [L5] therefore give the noncompact HK integral.

step 1.1L2L3L4L5L7∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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)

sin⁡x/xsinx/x has a Henstock–Kurzweil integral on [0,∞)[0,∞)