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.

Dirichlet's test for improper integrals

Statement

Let $f$ be locally Riemann integrable on $[a, \infty)$ and suppose its truncation primitive $F (x) = \int_{a}^{x} f$ is bounded. Each of the following conditions implies convergence of $\int_{a}^{\infty} f (x) g (x) d x$ :

$g$ is nonnegative, nonincreasing, and $g (x) \to 0$ .
$f$ is continuous, $g$ is differentiable with $g^{'}$ Riemann integrable on every compact subinterval, $g (x) \to 0$ , and $\int_{a}^{\infty} ∣ g^{'} (x) ∣ d x$ converges. Local integrability of $g^{'}$ is a hypothesis and not a consequence of the last one: convergence of $\int_{a}^{\infty} ∣ g^{'} ∣$ presupposes only that $∣ g^{'} ∣$ is integrable on each compact subinterval, and a bounded derivative need not be Riemann integrable.

The reflected statements hold at $- \infty$ and at finite singular endpoints, with monotonicity directed toward the singular end.

Facts & Assumptions

Given: A bounded truncation primitive $F$ and one of the two multiplier hypotheses.

[L1]

Bonnet's second mean value theorem represents $\int_{u}^{v} f g$ using endpoint values of a monotone $g$ and partial integrals of $f$ (Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$ ).

[L2]

The improper Cauchy criterion reduces convergence to small remote tail integrals (Cauchy criterion for improper integrals).

[L3]

Proper integration by parts gives $\int_{u}^{v} f g = [F g]_{u}^{v} - \int_{u}^{v} F g^{'}$ when $F^{'} = f$ (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ).

[L4]

A bounded factor times an absolutely integrable function is absolutely integrable by comparison (Comparison tests for improper integrals, Absolute convergence implies improper convergence).

[L5]

If $f$ is integrable on $[a, b]$ and continuous at $c$ , then its integral function $F$ satisfies $F^{'} (c) = f (c)$ ; in particular an $f$ continuous on the whole of $[a, b]$ has $F$ as a primitive there (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · cases

1.1

Choose $M$ with $∣ F ∣ \leq M$ . In clause 1, apply [L1] on $[u, v]$ . Every partial integral $\int_{u}^{x} f = F (x) - F (u)$ has absolute value at most $2 M$ , so [L1, L2, assume-case first] $∣ \int_{u}^{v} f g ∣ \leq 2 M (g (u) + g (v)) \leq 4 M g (u) .$ This tends to zero as $u \to \infty$ , and [L2] proves convergence.

1.2

In clause 2 $f$ is continuous, hence integrable on every $[u, v] \subseteq [a, \infty)$ , so [L5] gives $F^{'} = f$ there — the hypothesis [L3] requires and which boundedness of $F$ does not supply. With $g$ differentiable and $g^{'}$ integrable on $[u, v]$ , [L3] gives the integration-by-parts identity. The boundary term $F (R) g (R)$ tends to zero because $F$ is bounded and $g (R) \to 0$ . Also $∣ F g^{'} ∣ \leq M ∣ g^{'} ∣$ , so [L4] makes $\int F g^{'}$ converge. Passing $R \to \infty$ proves convergence of $\int f g$ .

L3L4L5assume-case second

2.1

The two clauses are exhausted by steps 1.1–1.2. Reversing orientation proves the $- \infty$ case. At a finite endpoint, use a primitive based at a fixed nonsingular point and take the corresponding one-sided limits; the same estimates are unchanged.

step 1.1step 1.2cases-exhaustive∎

Depends on

Used by

Abel's test for improper integrals Corollary
The sine integral converges conditionally but not absolutely Counterexample
The sine integral is improperly Riemann integrable and not Lebesgue integrable Counterexample
sin x/x has a Henstock–Kurzweil integral on [0,∞) Example
Uniform sine integral bound and dirichlet value Lemma
A Dirichlet-type transfer criterion for divergence Theorem

Dependency tree · two levels

75 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

William F. Trench, Introduction to Real Analysis, Theorem 3.4.10 (standard reference, not scraped)