TheoremStatement: Literature-sourcedProof: 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.

The Cauchy criterion for a Henstock–Kurzweil integral at a missing endpoint

Statement

Let $f$ be HK integrable on every compact subinterval of $[a, b)$ , where $b$ may be finite or $+ \infty$ . Its noncompact integral exists if and only if for every $ε > 0$ there is a truncation point $c_{0}$ such that

$∣ \int_{c}^{d} f ∣ < ε$

whenever $c_{0} < c < d < b$ . Thus noncompact integrability is equivalent to uniformly small tail integrals. The reflected criterion holds at a missing left endpoint.

Noncompact integrability is equivalent to uniformly small tail integrals.

A missing finite-endpoint integral exists exactly when all sufficiently late tail integrals are small.

Facts & Assumptions

Given: The locally HK-integrable function and a finite or infinite missing endpoint.

[L1]

For points $u, v, w$ , $\int_{u}^{w} f = \int_{u}^{v} f + \int_{v}^{w} f$ whenever the compact pieces are integrable (Henstock–Kurzweil integrability on subintervals and additivity over adjacent intervals).

[L2]

Every Cauchy sequence of reals converges to a real (The Cauchy criterion from the least-upper-bound property: in a complete ordered field every Cauchy sequence converges).

[L3]

Finite-endpoint limits are defined by one-sided neighborhood control (The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ ).

[L4]

A limit at infinity is defined by eventual control beyond a real threshold (Limits at $+ \infty$ and $- \infty$ , and infinite limits at a point).

Proof

technique · direct

1.1

For the forward direction, the truncation primitive $A (c) = \int_{a}^{c} f$ has a finite limit, so late values $A (c), A (d)$ are close; [L1] identifies their difference with $\int_{c}^{d} f$ .

givenL1

2.1

For the reverse direction, take the explicit cofinal sequence $c_{n} = b - (b - a) / (n + 1)$ at a finite endpoint, or $c_{n} = a + n$ at $+ \infty$ . The tail condition makes $A (c_{n})$ Cauchy, so [L2] gives a finite limit $I$ . For an arbitrary sufficiently late $c$ , choose $n$ with $c_{n} > c$ ; then [L1] gives $∣ A (c) - I ∣ \leq ∣ \int_{c}^{c_{n}} f ∣ + ∣ A (c_{n}) - I ∣$ , and the two terms are small. This is exactly the limit in [L3] or [L4]; reflection handles a missing left endpoint.

givenL1L2L3L4algebra∎

Depends on

Used by

Dependency tree · two levels

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