TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

The Cauchy principal-value subtraction identity

Statement

For $a < c < b$ and $f \in C^{1} ([a, b])$ , the principal value of Symmetric Cauchy principal value by subtraction exists and, with $g (c) = f^{'} (c)$ and $g (x) = (f (x) - f (c)) / (x - c)$ otherwise, satisfies $PV ⁣ \int_{a}^{b} \frac{f (x)}{x - c} d x = \int_{a}^{b} g (x) d x + f (c) \log \frac{b - c}{c - a} .$ The first integral is an ordinary integral of a continuous function.

Facts & Assumptions

Given: Reals $a < c < b$ and $f \in C^{1} ([a, b])$ .

[F1]

Symmetric Cauchy principal value by subtraction: the principal value is the symmetric limit of the two truncated integrals.

[F2]

The first divided difference of a C1 function extends continuously: the subtraction quotient $g$ extended by $g (c) = f^{'} (c)$ is continuous on $[a, b]$ .

[F3]

The natural logarithm as the inverse of the exponential function and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: on $(0, \infty)$ , $\log$ is a primitive of $1 / x$ and is continuous; $\log u - \log v = \log (u / v)$ for $u, v > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F4]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : integrating a continuous derivative on a compact interval gives the endpoint difference.

[F5]

The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive: the integral function of a continuous integrand is a continuous primitive, so its increments over intervals whose endpoints tend to $c$ tend to zero.

Proof

1.1F1F2F3F4algebra

For $x \neq c$ , $f (x) / (x - c) = g (x) + f (c) / (x - c)$ . If $0 < ε < \min (c - a, b - c)$ , apply [F3]–[F4] separately on $[a, c - ε]$ and $[c + ε, b]$ . The two singular terms sum to $f (c) (\log ε - \log (c - a) + \log (b - c) - \log ε) = f (c) \log \frac{b - c}{c - a} .$ Thus the truncated principal value equals $\int_{a}^{c - ε} g + \int_{c + ε}^{b} g + f (c) \log ((b - c) / (c - a))$ .

2.1F2F5step 1.1algebra

Let $G (x) = \int_{a}^{x} g$ . By [F2] and [F5], $G$ is continuous and its interval increments equal the corresponding integrals. Additivity gives $\int_{a}^{c - ε} g + \int_{c + ε}^{b} g = \int_{a}^{b} g - [G (c + ε) - G (c - ε)]$ . The bracket tends to zero by continuity of $G$ .

3.1F1F2step 1.1step 2.1∎

Taking $ε ↓ 0$ in step 1.1 and using step 2.1 proves existence of the symmetric limit and the asserted identity. Since $g$ is continuous, its ordinary integral exists.

Depends on

Used by

An interior Cauchy principal value reduces to a regular integral Example

Cited to discharge well-definedness by Symmetric Cauchy principal value by subtraction.

Dependency tree · two levels

43 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

Lloyd N. Trefethen and J. A. C. Weideman, The Exponentially Convergent Trapezoidal Rule, SIAM Review 56(3), 2014 (standard reference, not scraped)