Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27
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.

Indented real-axis contours compute principal values with half-residue corrections

Statement

Let R=p/q, where p,q∈C[z] are nonzero, be a rational function with deg⁡q≥deg⁡p+2, and assume that its real poles a1<⋯<as are simple. For T large enough to contain all these poles and for pairwise disjoint symmetric deletion radii εj>0, put

I(T,ε):=∫[−T,T]∖⋃j=1s(aj−εj,aj+εj)R(x) dx,

where the integral is the sum over the remaining compact intervals. In this statement,

PV⁡ ⁣∫−∞∞R(x) dx:=lim⁡T→∞ε1,…,εs↓0I(T,ε).

When s=0, the deleted union is empty and only T→∞ remains. Indent every real pole above the real axis and close the contour in the upper half-plane. Then this principal value exists and

PV⁡ ⁣∫−∞∞R(x) dx=2πi∑ℑa>0Res⁡(R,a)+iπ∑jRes⁡(R,aj).

The correction term is the sum of the usual positive half-residues.

Facts & Assumptions

Given: A rational function R with a two-degree denominator gap and only simple real poles, all indented above the real axis.

[L1]

At a finite singularity, a principal value uses equal left and right deletions, while on the real line it uses the symmetric truncation [−T,T]; neither assertion implies separate improper convergence (Cauchy principal values at a finite singularity and on the real line, This page keeps Cauchy principal values distinct from genuine improper convergence).

[L2]

For an admissible cycle, the residue theorem gives its contour integral as 2πi times the index-weighted sum of the enclosed residues (The residue theorem for a null-homologous cycle).

[L3]

If the large upper semicircle meets no pole and sup⁡∣z∣=T, ℑz≥0∣zR(z)∣→0, then its integral tends to 0 (A rational large-semicircle integral vanishes under the zR(z) to 0 condition).

[L4]

An upper indentation contributes −iπRes⁡(R,a) in the limit (An indented arc around a simple singularity contributes the expected residue fraction).

Proof

technique · direct
1.1givenL2

For large T and small pairwise disjoint indentation radii εj, form the contour specified in the statement. It is an admissible positively oriented cycle, avoids every real pole, and encloses precisely the nonreal poles in the upper half-plane, so [L2] applies.

2.1givenstep 1.1L1L3L4algebra

The contour pieces have their asserted limits as T→∞ and every εj↓0.

Indeed, the straight pieces sum to I(T,ε) from the statement. The degree gap gives R(z)=O(∣z∣−2), so the large semicircle eventually meets no pole and satisfies the hypothesis of [L3]. Thus its integral tends to 0. Finally, [L4] makes the jth upper indentation tend to −iπRes⁡(R,aj). [given, step 1.1, L1, L3, L4, algebra]

3.1step 1.1step 2.1L2∎

The residue theorem and step 2.1 give PV⁡ ⁣∫−∞∞R(x) dx−iπ∑jRes⁡(R,aj)=2πi∑ℑa>0Res⁡(R,a). Hence the joint limit exists, and moving the indentation term to the right proves the formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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