TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Uniform oscillatory tail mass forces failure of absolute convergence

Statement

Let $g\ge0$ be monotone on $[a,\infty)$ and suppose $\int_a^\infty g$ diverges. Let $a\le x_0<x_1<\cdots$ tend to infinity and satisfy $x_{j+1}-x_j\le M$ for some $M>0$ , and suppose a locally integrable $f$ satisfies $\int_{x_j}^{x_{j+1}}|f(x)|\,dx\ge\delta>0$ for every $j$ . Then $\int_a^\infty|f(x)g(x)|\,dx$ diverges, so $\int_a^\infty fg$ cannot converge absolutely.

Facts & Assumptions

Given: The nonnegative monotone $g$ , bounded-gap sequence, and uniform block mass in the statement.

[L1]

Proper integration preserves order and is additive on adjacent intervals (If $f \le g$ on $[a,b]$ and both are integrable then $\int_a^b f \le \int_a^b g$ ; and $m(b-a) \le \int_a^b f \le M(b-a)$ , For $a<c<b$ : $f$ is integrable on $[a,b]$ if and only if it is integrable on $[a,c]$ and on $[c,b]$ , and then $\int_a^b f = \int_a^c f + \int_c^b f$ ; with the oriented form for arbitrary $a,b,c$ ).

[L2]

A nonnegative improper integral converges exactly when its truncations are bounded (A nonnegative improper integral converges iff its truncated integrals are bounded).

[L3]

Removing finitely many terms does not affect divergence of a nonnegative series (A series converges iff each of its tail series converges, and the sum splits as $s_N$ plus the $N$ -th tail).

Proof

technique · direct

1.1

Suppose first that $g$ is nonincreasing. On the $j$ th block, $g(x)\ge g(x_{j+1})$ , hence [L1, L2, L3] $\int_{x_j}^{x_{j+1}}|f|g\ge\delta g(x_{j+1}).$ Also $\int_{x_j}^{x_{j+1}}g\le M g(x_j)$ . Since $\int g$ diverges, additivity and [L2] force $\sum_jg(x_j)$ , and hence its shifted tail, to diverge. Thus the block lower bounds for $\int|f|g$ have unbounded partial sums.

L1L2L3

1.2

If $g$ is nondecreasing, divergence of its integral implies it is positive at some point; thereafter $g(x_j)$ is bounded below by a positive constant. Now $\int_{x_j}^{x_{j+1}}|f|g\ge\delta g(x_j)$ , whose partial sums diverge.

given

2.1

In either monotonicity case the nonnegative truncations of $|fg|$ are unbounded, so [L2] proves divergence and the definition rules out absolute convergence.

L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 96 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

William F. Trench, Introduction to Real Analysis, exercises following Section 3.4 (standard reference, not scraped)