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.

Separate improper convergence implies convergence of the principal value

Statement

If the two one-sided improper integrals at an interior singularity converge separately, then the Cauchy principal value exists and equals their sum. If both tails of a whole-line improper integral converge separately, its principal value exists and equals the whole-line improper integral.

The converses need not hold.

Facts & Assumptions

Given: Separate convergence at the two singular ends in either setting.

[L1]

A mixed improper value is the sum of the two independent limits (Improper integrals with several singular ends).

[L2]

Moving finite split points preserves both convergence and value (Improper convergence is independent of finite truncations and split points).

[L3]

Principal values use coupled symmetric truncations (Cauchy principal values at a finite singularity and on the real line).

[L4]

For every rational pp, 01xpdx\int_0^1x^{-p}\,dx converges exactly when p<1p<1, and 1xpdx\int_1^\infty x^{-p}\,dx converges exactly when p>1p>1 (The improper pp-test for rational exponents).

[L5]

The whole-line Cauchy principal value is limRRRf\lim_{R\to\infty}\int_{-R}^{R}f for a function locally Riemann integrable on the real line, and it does not assert that the two tails converge separately (Cauchy principal values at a finite singularity and on the real line).

Proof

technique · direct
1.1

At an interior point cc, the two truncated terms in [L3] tend separately to the two finite one-sided values. Given ε>0\varepsilon>0, take the common smaller truncation scale on which each term is within ε/2\varepsilon/2 of its limit; the triangle inequality then puts their sum within ε\varepsilon of the sum in [L1].

L3L1
1.2

On the real line, split at zero. As RR\to\infty, R0f\int_{-R}^0f and 0Rf\int_0^Rf tend separately to their two tail values. The same ε/2\varepsilon/2 estimate shows that their sum tends to the mixed value. Split-point invariance [L2] removes any dependence on zero.

L2
2.1

The converses fail, and a witness is available on this page rather than assumed. Take f(x)=1/xf(x)=1/x on [1,1][-1,1] with the interior singularity at 00. For every δ(0,1)\delta\in(0,1) the substitution xxx\mapsto-x gives 1δx1dx=δ1x1dx\int_{-1}^{-\delta}x^{-1}\,dx=-\int_{\delta}^{1}x^{-1}\,dx, so the symmetric truncations cancel exactly and the principal value exists and is 00. But 01xpdx\int_0^1x^{-p}\,dx converges exactly when p<1p<1 by [L4], so at p=1p=1 the right-hand one-sided integral diverges, and by the same reflection so does the left-hand one. Hence the principal value can exist while neither one-sided improper integral converges, and the converse of the first claim fails. For the whole line a separate witness is needed, because [L5] admits only a function locally Riemann integrable on all of R\mathbb R and 1/x1/x is not one: take f(x)=xf(x)=x, which is continuous and therefore locally integrable. For every RR the substitution xxx\mapsto-x gives R0xdx=0Rxdx\int_{-R}^0x\,dx=-\int_0^Rx\,dx, so RRxdx=0\int_{-R}^Rx\,dx=0 and the whole-line principal value is 00; but 0Rxdx=R2/2\int_0^Rx\,dx=R^2/2 is unbounded in RR, so the tail 0xdx\int_0^\infty x\,dx does not converge.

L4L5given

Depends on

Used by

Dependency tree · next 3 levels

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