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

Cauchy criterion for improper integrals

Statement

The integral ∫a∞f converges if and only if, for every ε>0, there is A>a such that A≤u<v⟹∣∫uvf∣<ε. At a finite right singular endpoint b, replace the condition by b−δ<u<v<b; at a finite left endpoint use a<u<v<a+δ; at −∞ use u<v≤−A. In each case all displayed proper integrals must exist.

Facts & Assumptions

Given: A locally Riemann-integrable f on the relevant one-ended interval.

[L3]

The Archimedean property supplies integer truncations beyond every real bound and reciprocal truncations inside every positive neighborhood (Every complete ordered field is Archimedean, For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

Proof

technique · direct
1.1

Put F(R)=∫aRf. If F(R) has a finite limit as R→∞, then ∣F(v)−F(u)∣<ε for all sufficiently large u,v. By [L1], this difference is ∫uvf, proving necessity.

L1
1.2

Conversely, the tail condition and [L3] make the sequence F(n) Cauchy, hence convergent to some L by [L2]. Given ε>0, choose a large integer n for which ∣F(n)−L∣<ε/2 and the tail condition is below ε/2. For every real R≥n, [L1] gives F(R)−L=(F(R)−F(n))+(F(n)−L), so F(R)→L.

L1L2L3
2.1

For a finite endpoint use the reciprocal sequence a+1/n or b−1/n furnished by [L3]; the identical Cauchy argument applies. Reversing the real line gives the −∞ form.

L3∎

Depends on

Used by

Dependency tree · two levels

45 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