TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11

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.

Absolute convergence implies improper convergence

Statement

Every absolutely convergent improper integral converges. Moreover, on a one-ended interval, $∣ \int f ∣ \leq \int ∣ f ∣ .$ For a mixed interval the same conclusion applies separately to each singular-end piece.

Facts & Assumptions

Given: Convergence of the improper integral of $∣ f ∣$ .

[L1]

On every compact interval, $∣ \int_{u}^{v} f ∣ \leq \int_{u}^{v} ∣ f ∣$ (If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[L2]

The improper Cauchy criterion characterizes convergence (Cauchy criterion for improper integrals).

[L3]

Inequalities persist under limits of real sequences; integer and reciprocal truncation sequences approach the infinite and finite singular ends (Limits preserve non-strict inequalities, Sequences of reals: bounded, eventually, frequently, tails, subsequences, Every complete ordered field is Archimedean, For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · direct

1.1L2L1

By the Cauchy criterion [L2], remote tail integrals of $∣ f ∣$ are arbitrarily small. The proper inequality [L1] makes the corresponding tail integrals of $f$ no larger in absolute value. A second application of [L2] proves convergence of $\int f$ .

1.2L1L3

Apply [L1] on compact truncations. Along integer truncations at infinity, or reciprocal truncations at a finite endpoint, both sides converge to the corresponding improper values; [L3] passes the inequality to those sequence limits and gives the displayed bound.

2.1given∎

For a mixed integral, absolute convergence is required on every piece. Steps 1.1–1.2 apply piecewise, and finite addition completes the claim.

Depends on

Dependency tree · 2 levels

Sources

William F. Trench, Introduction to Real Analysis, Theorem 3.4.9