Alphabeta Math
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.

Dirichlet's test for improper integrals

Statement

Let ff be locally Riemann integrable on [a,∞)[a,\infty) and suppose its truncation primitive F(x)=∫axfF(x)=\int_a^x f is bounded. Each of the following conditions implies convergence of ∫a∞f(x)g(x) dx\int_a^\infty f(x)g(x)\,dx:

  1. gg is nonnegative, nonincreasing, and g(x)→0g(x)\to0.
  2. ff is continuous, gg is differentiable with g′g' Riemann integrable on every compact subinterval, g(x)→0g(x)\to0, and ∫a∞∣g′(x)∣ dx\int_a^\infty|g'(x)|\,dx converges. Local integrability of g′g' is a hypothesis and not a consequence of the last one: convergence of ∫a∞∣g′∣\int_a^\infty|g'| presupposes only that ∣g′∣|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 FF and one of the two multiplier hypotheses.

[L1]

Bonnet's second mean value theorem represents ∫uvfg\int_u^vfg using endpoint values of a monotone gg and partial integrals of ff (Bonnet's second mean value theorem: for ff monotone and gg integrable on [a,b][a,b] there is ξ∈[a,b]\xi\in[a,b] with ∫abfg=f(a)∫aξg+f(b)∫ξbg\int_a^b fg = f(a)\int_a^\xi g + f(b)\int_\xi^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 ∫uvfg=[Fg]uv−∫uvFg′\int_u^vfg=[Fg]_u^v-\int_u^vFg' when F′=fF'=f (If u,vu,v are differentiable on [a,b][a,b] with u′,v′u',v' integrable, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v\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 ff is integrable on [a,b][a,b] and continuous at cc, then its integral function FF satisfies F′(c)=f(c)F'(c)=f(c); in particular an ff continuous on the whole of [a,b][a,b] has FF as a primitive there (The first fundamental theorem: if ff is integrable on [a,b][a,b] and continuous at cc, then F′(c)=f(c)F'(c) = f(c); in particular a continuous ff has FF as a primitive).

Proof

technique · cases
1.1

Choose MM with ∣F∣≤M|F|\le M. In clause 1, apply [L1] on [u,v][u,v]. Every partial integral ∫uxf=F(x)−F(u)\int_u^xf=F(x)-F(u) has absolute value at most 2M2M, so [L1, L2, assume-case first] ∣∫uvfg∣≤2M(g(u)+g(v))≤4Mg(u).\left|\int_u^vfg\right|\le2M(g(u)+g(v))\le4Mg(u). This tends to zero as u→∞u\to\infty, and [L2] proves convergence.

1.2

In clause 2 ff is continuous, hence integrable on every [u,v]⊆[a,∞)[u,v]\subseteq[a,\infty), so [L5] gives F′=fF'=f there — the hypothesis [L3] requires and which boundedness of FF does not supply. With gg differentiable and g′g' integrable on [u,v][u,v], [L3] gives the integration-by-parts identity. The boundary term F(R)g(R)F(R)g(R) tends to zero because FF is bounded and g(R)→0g(R)\to0. Also ∣Fg′∣≤M∣g′∣|Fg'|\le M|g'|, so [L4] makes ∫Fg′\int Fg' converge. Passing R→∞R\to\infty proves convergence of ∫fg\int fg.

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

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 136 results over 20 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